simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 20:34:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

small changes

Browse source
This commit is contained in:
Simon Cruanes 2016-07-29 20:04:54 +02:00
parent 672b5945ce
commit 85c290c0ce
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/core/internal.ml
View file

@ -296,7 +296,7 @@ module Make
let a = atoms.(i) in let a = atoms.(i) in
if a.is_true then if a.is_true then
let l = a.var.v_level in let l = a.var.v_level in
if 0 <= l && l <= root then if l = 0 then
raise Trivial (* A var true at level 0 gives a trivially true clause *) raise Trivial (* A var true at level 0 gives a trivially true clause *)
else else
(a :: trues) @ unassigned @ falses @ (a :: trues) @ unassigned @ falses @
@ -530,6 +530,7 @@ module Make
b.var.v_level b.var.v_level
) else ( ) else (
assert (a.var.v_level = b.var.v_level); assert (a.var.v_level = b.var.v_level);
assert (a.var.v_level >= env.base_level);
max (a.var.v_level - 1) env.base_level max (a.var.v_level - 1) env.base_level
) )
@ -756,7 +757,7 @@ module Make
(fun a b -> compare b.var.v_level a.var.v_level) (fun a b -> compare b.var.v_level a.var.v_level)
clause.atoms; clause.atoms;
attach_clause clause; attach_clause clause;
add_boolean_conflict init add_boolean_conflict clause
end else begin end else begin
attach_clause clause; attach_clause clause;
if b.neg.is_true && not a.is_true && not a.neg.is_true then begin if b.neg.is_true && not a.is_true && not a.neg.is_true then begin