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

fix(sat): bugfix about adding clauses with true lits

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 17:47:04 -05:00
parent 46ff8c3ba6
commit 72750b9e1a
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/Internal.ml
View file

@ -999,12 +999,14 @@ module Make (Th : Theory_intf.S) = struct
a.(j) <- tmp; a.(j) <- tmp;
) )
(* move atoms that are not assigned first, (* move true atoms first,
else move atoms that are not assigned first,
else put atoms assigned at high levels first *) else put atoms assigned at high levels first *)
let put_high_level_atoms_first (arr:atom array) : unit = let put_high_level_atoms_first (arr:atom array) : unit =
(* move [a] in front of [b]? *) (* move [a] in front of [b]? *)
let[@inline] put_before a b = let[@inline] put_before a b =
if Atom.level a < 0 then Atom.level b >= 0 if Atom.is_true a then not (Atom.is_true b) || Atom.level a>Atom.level b
else if Atom.level a < 0 then Atom.level b >= 0
else (Atom.level b >= 0 && Atom.level a > Atom.level b) else (Atom.level b >= 0 && Atom.level a > Atom.level b)
in in
Array.iteri Array.iteri