feat(sat): provide a proof_dumm module

src/sat/Proof_dummy.ml

@@ -0,0 +1,22 @@
+
+module Make(Lit : sig type t end)
+  : Solver_intf.PROOF
+    with type lit = Lit.t
+     and type t = unit
+     and type proof_step = unit
+= struct
+  type lit = Lit.t
+  type t = unit
+  type proof_step = unit
+  type proof_rule = t -> proof_step
+
+  module Step_vec = Vec_unit
+
+  let enabled (_pr:t) = false
+  let del_clause _ _ (_pr:t) = ()
+
+  let emit_redundant_clause _ ~hyps:_ _ = ()
+  let emit_input_clause _ _ = ()
+  let emit_unsat _ _ = ()
+  let emit_unsat_core _ (_pr:t) = ()
+end

src/sat/Proof_dummy.mli

@@ -0,0 +1,9 @@
+
+(** Dummy proof module that does nothing. *)
+
+module Make(Lit : sig type t end) : sig
+  include Solver_intf.PROOF
+    with type lit = Lit.t
+     and type t = unit
+     and type proof_step = unit
+end

src/sat/Sidekick_sat.ml

@@ -32,3 +32,6 @@ exception No_proof = Solver_intf.No_proof
 module Solver = Solver
 module Make_cdcl_t = Solver.Make_cdcl_t
 module Make_pure_sat = Solver.Make_pure_sat
+
+(** Module for dummy proofs based on unit *)
+module Proof_dummy = Proof_dummy