From cfede762c9af9e8474c2a637f096eda4439f7df1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 7 Dec 2021 14:08:16 -0500 Subject: [PATCH] feat(sat): provide a proof_dumm module --- src/sat/Proof_dummy.ml | 22 ++++++++++++++++++++++ src/sat/Proof_dummy.mli | 9 +++++++++ src/sat/Sidekick_sat.ml | 3 +++ 3 files changed, 34 insertions(+) create mode 100644 src/sat/Proof_dummy.ml create mode 100644 src/sat/Proof_dummy.mli diff --git a/src/sat/Proof_dummy.ml b/src/sat/Proof_dummy.ml new file mode 100644 index 00000000..5cfb08b9 --- /dev/null +++ b/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 diff --git a/src/sat/Proof_dummy.mli b/src/sat/Proof_dummy.mli new file mode 100644 index 00000000..488ebab6 --- /dev/null +++ b/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 diff --git a/src/sat/Sidekick_sat.ml b/src/sat/Sidekick_sat.ml index ccbeda03..fc956231 100644 --- a/src/sat/Sidekick_sat.ml +++ b/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