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

refactor: change API to {final,partial}_check

Browse source
This commit is contained in:
Simon Cruanes 2019-01-26 11:23:45 -06:00 • committed by Guillaume Bury
parent a0ba576b0f
commit 8f1c24c1a6
3 changed files with 20 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/core/Internal.ml
View file

@ -1690,7 +1690,7 @@ module Make(Plugin : PLUGIN)
) else ( ) else (
let slice = current_slice st in let slice = current_slice st in
st.th_head <- st.elt_head; (* catch up *) st.th_head <- st.elt_head; (* catch up *)
match Plugin.assume st.th slice with match Plugin.partial_check st.th slice with
| () -> | () ->
flush_clauses st; flush_clauses st;
propagate st propagate st
@ -1914,7 +1914,7 @@ module Make(Plugin : PLUGIN)
n_of_learnts := !n_of_learnts *. learntsize_inc n_of_learnts := !n_of_learnts *. learntsize_inc
| E_sat -> | E_sat ->
assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = Vec.size st.trail);
begin match Plugin.if_sat st.th (full_slice st) with begin match Plugin.final_check st.th (full_slice st) with
| () -> | () ->
if st.elt_head = Vec.size st.trail && if st.elt_head = Vec.size st.trail &&
Vec.is_empty st.clauses_to_add then ( Vec.is_empty st.clauses_to_add then (
@ -2113,8 +2113,8 @@ module Make_pure_sat(F: Solver_intf.FORMULA) =
type proof = Solver_intf.void type proof = Solver_intf.void
let push_level () = () let push_level () = ()
let pop_levels _ _ = () let pop_levels _ _ = ()
let assume () _ = () let partial_check () _ = ()
let if_sat () _ = () let final_check () _ = ()
let eval () _ = Solver_intf.Unknown let eval () _ = Solver_intf.Unknown
let assign () t = t let assign () t = t
let mcsat = false let mcsat = false

22
src/core/Solver_intf.ml
View file

@ -174,13 +174,14 @@ module type PLUGIN_CDCL_T = sig
val pop_levels : t -> int -> unit val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *) (** Pop [n] levels of the theory *)
val assume : t -> (void, Formula.t, proof) slice -> unit val partial_check : t -> (void, Formula.t, proof) slice -> unit
(** Assume the formulas in the slice, possibly pushing new formulas to be (** Assume the formulas in the slice, possibly using the [slice]
propagated or raising a conflict. *) to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val if_sat : t -> (void, Formula.t, proof) slice -> unit val final_check : t -> (void, Formula.t, proof) slice -> unit
(** Called at the end of the search in case a model has been found. (** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and 'sat' is returned; If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed; if lemmas are added, search is resumed;
if a conflict clause is added, search backtracks and then resumes. *) if a conflict clause is added, search backtracks and then resumes. *)
end end
@ -199,13 +200,14 @@ module type PLUGIN_MCSAT = sig
val pop_levels : t -> int -> unit val pop_levels : t -> int -> unit
(** Pop [n] levels of the theory *) (** Pop [n] levels of the theory *)
val assume : t -> (Term.t, Formula.t, proof) slice -> unit val partial_check : t -> (Term.t, Formula.t, proof) slice -> unit
(** Assume the formulas in the slice, possibly pushing new formulas to be (** Assume the formulas in the slice, possibly using the [slice]
propagated or raising a conflict. *) to push new formulas to be propagated or to raising a conflict or to add
new lemmas. *)
val if_sat : t -> (Term.t, Formula.t, proof) slice -> unit val final_check : t -> (Term.t, Formula.t, proof) slice -> unit
(** Called at the end of the search in case a model has been found. (** Called at the end of the search in case a model has been found.
If no new clause is pushed, then proof search ends and 'sat' is returned; If no new clause is pushed, then proof search ends and "sat" is returned;
if lemmas are added, search is resumed; if lemmas are added, search is resumed;
if a conflict clause is added, search backtracks and then resumes. *) if a conflict clause is added, search backtracks and then resumes. *)

8
src/sudoku/sudoku_solve.ml
View file

@ -261,14 +261,14 @@ end = struct
) )
) )
let assume (self:t) acts : unit = let partial_check (self:t) acts : unit =
Log.debugf 4 Log.debugf 4
(fun k->k "(@[sudoku.assume@ :trail [@[%a@]]@])" (Fmt.seq F.pp) (trail_ acts)); (fun k->k "(@[sudoku.partial-check@ :trail [@[%a@]]@])" (Fmt.seq F.pp) (trail_ acts));
add_slice self acts; add_slice self acts;
check_ self acts check_ self acts
let if_sat (self:t) acts : unit = let final_check (self:t) acts : unit =
Log.debugf 4 (fun k->k "(@[sudoku.if-sat@])"); Log.debugf 4 (fun k->k "(@[sudoku.final-check@])");
check_full_ self acts; check_full_ self acts;
check_ self acts check_ self acts