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

reinstate better way of picking watch literals

Browse source
This commit is contained in:
Simon Cruanes 2017-12-29 19:00:32 +01:00 • committed by Guillaume Bury
parent 5279456419
commit 87fc9aef26
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Internal.ml
View file

@ -560,14 +560,8 @@ module Make
a.(j) <- tmp; a.(j) <- tmp;
) )
let[@inline] put_high_level_atoms_first (arr:atom array) : unit =
Array.sort
(fun a b -> compare b.var.v_level a.var.v_level)
arr
(* FIXME
(* move atoms assigned at high levels first *) (* move atoms assigned at high levels first *)
let[@inline] put_high_level_atoms_first (arr:atom array) : unit = let put_high_level_atoms_first (arr:atom array) : unit =
Array.iteri Array.iteri
(fun i a -> (fun i a ->
if i>0 && Atom.level a > Atom.level arr.(0) then ( if i>0 && Atom.level a > Atom.level arr.(0) then (
@ -584,7 +578,6 @@ module Make
swap_arr arr 1 i; swap_arr arr 1 i;
)) ))
arr arr
*)
(* evaluate an atom for MCsat, if it's not assigned (* evaluate an atom for MCsat, if it's not assigned
by boolean propagation/decision *) by boolean propagation/decision *)