From 87fc9aef26cf049568936d43c8d35d706097eb8c Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Dec 2017 19:00:32 +0100 Subject: [PATCH] reinstate better way of picking watch literals --- src/core/Internal.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 6bf75876..570e06d1 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -560,14 +560,8 @@ module Make 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 *) - let[@inline] put_high_level_atoms_first (arr:atom array) : unit = + let put_high_level_atoms_first (arr:atom array) : unit = Array.iteri (fun i a -> if i>0 && Atom.level a > Atom.level arr.(0) then ( @@ -584,7 +578,6 @@ module Make swap_arr arr 1 i; )) arr - *) (* evaluate an atom for MCsat, if it's not assigned by boolean propagation/decision *)