From cf6147c500698221f3d7b56ebd2892d7342eb39d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 25 Jan 2019 17:53:14 -0600 Subject: [PATCH] details --- src/core/Internal.ml | 3 +++ src/core/Solver_intf.ml | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 673e47a3..314d2707 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -1376,6 +1376,9 @@ module Make(Plugin : PLUGIN) | _ -> assert false done; List.iter (fun q -> Var.clear q.var) !seen; + (* put high-level literals first, so that: + - they make adequate watch lits + - the first literal is the UIP, if any *) let l = List.fast_sort (fun p q -> compare q.var.v_level p.var.v_level) !learnt in let level, is_uip = backtrack_lvl st l in { cr_backtrack_lvl = level; diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 5f209785..a51fee18 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -87,7 +87,7 @@ type ('term, 'formula, 'proof) slice = { iter_assumptions: (('term,'formula) assumption -> unit) -> unit; (** Traverse the new assumptions on the boolean trail. *) - push : ?keep:bool -> 'formula list -> 'proof -> unit; + push: ?keep:bool -> 'formula list -> 'proof -> unit; (** Add a clause to the solver. @param keep if true, the clause will be kept by the solver. Otherwise the solver is allowed to GC the clause and propose this @@ -99,7 +99,7 @@ type ('term, 'formula, 'proof) slice = { The list of atoms must be a valid theory lemma that is false in the current trail. *) - propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit; + propagate: 'formula -> ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can evaluate the formula to be true (see the definition of {!type:eval_res} *) }