simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 13:14:09 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Still working...

Browse source
This commit is contained in:
Guillaume Bury 2015-03-15 22:12:21 +01:00
parent 5a61a6c852
commit 25dae83c6e
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcsolver.ml
View file

@ -572,6 +572,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
done; done;
(* no watch lit found *) (* no watch lit found *)
if first.neg.is_true || (th_eval first = Some false) then begin if first.neg.is_true || (th_eval first = Some false) then begin
L.debug 100 "clause is false";
(* clause is false *) (* clause is false *)
env.qhead <- Vec.size env.trail; env.qhead <- Vec.size env.trail;
for k = i to Vec.size watched - 1 do for k = i to Vec.size watched - 1 do
@ -580,8 +581,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
done; done;
L.debug 3 "Conflict found : %a" St.pp_clause c; L.debug 3 "Conflict found : %a" St.pp_clause c;
raise (Conflict c) raise (Conflict c)
end end else begin
else begin L.debug 100 "clause is unit";
(* clause is unit *) (* clause is unit *)
Vec.set watched !new_sz c; Vec.set watched !new_sz c;
incr new_sz; incr new_sz;