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

details

Browse source
This commit is contained in:
Simon Cruanes 2019-01-25 17:53:14 -06:00 • committed by Guillaume Bury
parent 9024b0f0a9
commit cf6147c500
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/core/Internal.ml
View file

@ -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;

4
src/core/Solver_intf.ml
View file

@ -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} *)
}