feat(sat): add mk_plugin_cdcl_t

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 () = ()

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 ] ->