From 92edae353d64c06d450b020c121546c1227d9268 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 13 Aug 2022 13:30:08 -0400 Subject: [PATCH] feat(sat): add `mk_plugin_cdcl_t` --- src/sat/solver.ml | 10 ++++++++++ src/sat/solver.mli | 19 +++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/src/sat/solver.ml b/src/sat/solver.ml index c4399c2e..5137508e 100644 --- a/src/sat/solver.ml +++ b/src/sat/solver.ml @@ -2022,6 +2022,16 @@ let plugin_cdcl_t (module P : THEORY_CDCL_T) : (module PLUGIN) = let has_theory = true end) +let mk_plugin_cdcl_t ~push_level ~pop_levels ?(partial_check = ignore) + ~final_check () : (module PLUGIN) = + (module struct + let push_level = push_level + let pop_levels = pop_levels + let partial_check = partial_check + let final_check = final_check + let has_theory = true + end) + let plugin_pure_sat : plugin = (module struct let push_level () = () diff --git a/src/sat/solver.mli b/src/sat/solver.mli index 808dde58..689bb6ba 100644 --- a/src/sat/solver.mli +++ b/src/sat/solver.mli @@ -154,6 +154,25 @@ val check_sat_propagations_only : val plugin_cdcl_t : (module THEORY_CDCL_T) -> (module PLUGIN) +val mk_plugin_cdcl_t : + push_level:(unit -> unit) -> + pop_levels:(int -> unit) -> + ?partial_check:(acts -> unit) -> + final_check:(acts -> unit) -> + unit -> + (module PLUGIN) +(** Create a plugin + @param push_level create a new backtrack level + @param pop_levels Pop [n] levels of the plugin + @param partial_check Assume the lits in the slice, possibly using the [slice] + to push new lits to be propagated or to raising a conflict or to add + new lemmas. + @param final_check 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 lemmas are added, search is resumed; + if a conflict clause is added, search backtracks and then resumes. + *) + val create : ?stat:Stat.t -> ?size:[ `Tiny | `Small | `Big ] ->