proof stubs and sat proof

src/base-solver/sidekick_base_solver.ml

@@ -60,9 +60,14 @@ module Th_data = Sidekick_th_data.Make(struct
     let ty_is_finite = Ty.finite
     let ty_set_is_finite = Ty.set_finite
 
-    let lemma_isa_disj p lits = Proof.lemma_isa_disj p lits
+    let lemma_isa_cstor = Proof.lemma_isa_cstor
-    let lemma_isa_split p lits = Proof.lemma_isa_split p lits
+    let lemma_select_cstor = Proof.lemma_select_cstor
-    let lemma_cstor_inj p lits = Proof.lemma_cstor_inj p lits
+    let lemma_isa_split = Proof.lemma_isa_split
+    let lemma_isa_sel = Proof.lemma_isa_sel
+    let lemma_isa_disj = Proof.lemma_isa_disj
+    let lemma_cstor_inj = Proof.lemma_cstor_inj
+    let lemma_cstor_distinct = Proof.lemma_cstor_distinct
+    let lemma_acyclicity = Proof.lemma_acyclicity
   end)
 
 (** Reducing boolean formulas to clauses *)

src/base/Proof_stub.ml

@@ -5,26 +5,43 @@ type lit = Lit.t
 type term = Term.t
 
 type t = unit
-type dproof = t -> unit
+type proof_step = unit
+type proof_rule = t -> proof_step
+
+module Step_vec = Vec_unit
 
 let create () : t = ()
 let with_proof _ _ = ()
 
+let enabled (_pr:t) = false
 let begin_subproof _ = ()
 let end_subproof _ = ()
-let del_clause _ _ = ()
+let del_clause _ _ (_pr:t) = ()
-let emit_redundant_clause _ _ = ()
+let emit_redundant_clause _ ~hyps:_ _ = ()
 let emit_input_clause _ _ = ()
 let define_term _ _ _ = ()
-let lemma_preprocess _ _ _ = ()
+let emit_unsat _ _ = ()
+let proof_p1 _ _ (_pr:t) = ()
+let emit_unsat_core _ (_pr:t) = ()
+let lemma_preprocess _ _ ~using:_ (_pr:t) = ()
 let lemma_true _ _ = ()
 let lemma_cc _ _ = ()
+let lemma_rw_clause _ ~using:_ (_pr:t) = ()
+let with_defs _ _ (_pr:t) = ()
+
 let lemma_lra _ _ = ()
-let lemma_cstor_inj _ _ = ()
+
-let lemma_isa_disj _ _ = ()
-let lemma_isa_split _ _ = ()
 let lemma_bool_tauto _ _ = ()
 let lemma_bool_c _ _ _ = ()
 let lemma_bool_equiv _ _ _ = ()
-let lemma_ite_true ~a:_ ~ite:_ _ = ()
+let lemma_ite_true ~ite:_ _ = ()
-let lemma_ite_false ~a:_ ~ite:_ _ = ()
+let lemma_ite_false ~ite:_ _ = ()
+
+let lemma_isa_cstor ~cstor_t:_ _ (_pr:t) = ()
+let lemma_select_cstor ~cstor_t:_ _ (_pr:t) = ()
+let lemma_isa_split _ _ (_pr:t) = ()
+let lemma_isa_sel _ (_pr:t) = ()
+let lemma_isa_disj _ _ (_pr:t) = ()
+let lemma_cstor_inj _ _ _ (_pr:t) = ()
+let lemma_cstor_distinct _ _ (_pr:t) = ()
+let lemma_acyclicity _ (_pr:t) = ()

src/base/Proof_stub.mli

@@ -3,20 +3,27 @@
 
 open Base_types
 
+
 include Sidekick_core.PROOF
-  with type lit = Lit.t
+  with type t = private unit
+   and type proof_step = private unit
+   and type lit = Lit.t
    and type term = Term.t
 
+type proof_rule = t -> proof_step
+
 val create : unit -> t
 
-val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
+val lemma_lra : Lit.t Iter.t -> proof_rule
-val lemma_bool_c : string -> term list -> t -> unit
-val lemma_bool_equiv : term -> term -> t -> unit
-val lemma_ite_true : a:term -> ite:term -> t -> unit
-val lemma_ite_false : a:term -> ite:term -> t -> unit
 
-val lemma_lra : Lit.t Iter.t -> t -> unit
+include Sidekick_th_data.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
 
-val lemma_isa_split : Lit.t Iter.t -> t -> unit
+include Sidekick_th_bool_static.PROOF
-val lemma_isa_disj : Lit.t Iter.t -> t -> unit
+  with type proof := t
-val lemma_cstor_inj : Lit.t Iter.t -> t -> unit
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t

src/base/dune

@@ -3,7 +3,7 @@
  (public_name sidekick-base)
  (synopsis "Base term definitions for the standalone SMT solver and library")
  (libraries containers sidekick.core sidekick.util sidekick.lit
-            sidekick.arith-lra sidekick.th-bool-static
+            sidekick.arith-lra sidekick.th-bool-static sidekick.th-data
             sidekick.zarith
             bare_encoding zarith)
  (flags :standard -w -32 -open Sidekick_util))

src/core/Sidekick_core.ml

@@ -190,7 +190,7 @@ module type SAT_PROOF = sig
   val emit_unsat : proof_step -> t -> unit
   (** Signal "unsat" result at the given proof *)
 
-  val del_clause : proof_step -> t -> unit
+  val del_clause : proof_step -> lit Iter.t -> t -> unit
   (** Forget a clause. Only useful for performance considerations. *)
 end
 
@@ -1083,6 +1083,7 @@ module type SOLVER = sig
   val stats : t -> Stat.t
   val tst : t -> T.Term.store
   val ty_st : t -> T.Ty.store
+  val proof : t -> proof
 
   val create :
     ?stat:Stat.t ->

src/main/pure_sat_solver.ml

@@ -48,12 +48,13 @@ end = struct
         oc: out_channel;
         close: (unit -> unit);
       }
+  type proof_step = unit
+  type proof_rule = t -> proof_step
+  module Step_vec = Vec_unit
 
-  type dproof = t -> unit
+  let[@inline] enabled pr = match pr with
-
+    | Dummy -> false
-  let[@inline] with_proof pr f = match pr with
+    | Inner _ | Out _ -> true
-    | Dummy -> ()
-    | Inner _ | Out _ -> f pr
 
   let[@inline] emit_lits_buf_ buf lits =
     lits (fun i -> bpf buf "%d " i)
@@ -68,14 +69,14 @@ end = struct
     | Out {oc;_} ->
       fpf oc "i "; emit_lits_out_ oc lits; fpf oc "0\n"
 
-  let emit_redundant_clause lits self =
+  let emit_redundant_clause lits ~hyps:_ self =
     match self with
     | Dummy -> ()
     | Inner buf ->
       bpf buf "r "; emit_lits_buf_ buf lits; bpf buf "0\n"
     | Out {oc;_} -> fpf oc "r "; emit_lits_out_ oc lits; fpf oc "0\n"
 
-  let del_clause lits self =
+  let del_clause () lits self =
     match self with
     | Dummy -> ()
     | Inner buf ->
@@ -83,6 +84,9 @@ end = struct
     | Out {oc; _}->
       fpf oc "d "; emit_lits_out_ oc lits; fpf oc "0\n"
 
+  let emit_unsat _ _ = ()
+  let emit_unsat_core _ _ = ()
+
   (* lifetime *)
 
   let dummy : t = Dummy
@@ -130,6 +134,7 @@ module Arg = struct
   type lit = Lit.t
   module Proof = Proof
   type proof = Proof.t
+  type proof_step = Proof.proof_step
 end
 
 module SAT = Sidekick_sat.Make_pure_sat(Arg)

src/sat/Solver.ml

@@ -1890,7 +1890,8 @@ module Make(Plugin : PLUGIN)
       (match self.on_gc with
        | Some f -> let lits = Clause.lits_a store c in f self lits
        | None -> ());
-      Proof.del_clause (Clause.proof_step store c) self.proof;
+      Proof.del_clause
+        (Clause.proof_step store c) (Clause.lits_iter store c) self.proof;
     in
 
     let gc_arg =

src/smt-solver/Sidekick_smt_solver.ml

@@ -688,6 +688,7 @@ module Make(A : ARG)
   let[@inline] stats self = self.stat
   let[@inline] tst self = Solver_internal.tst self.si
   let[@inline] ty_st self = Solver_internal.ty_st self.si
+  let[@inline] proof self = self.si.proof
 
   let preprocess_acts_of_solver_
       (self:t) : (module Solver_internal.PREPROCESS_ACTS) =

src/smtlib/Process.ml

@@ -252,7 +252,7 @@ let process_stmt
       );
       let lit = Solver.mk_lit_t solver t in
       Solver.add_clause solver (IArray.singleton lit)
-        (Solver.P.emit_input_clause (Iter.singleton lit));
+        (Solver.P.emit_input_clause (Iter.singleton lit) (Solver.proof solver));
       E.return()
 
     | Statement.Stmt_assert_clause c_ts ->
@@ -263,14 +263,14 @@ let process_stmt
       let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in
 
       (* proof of assert-input + preprocessing *)
-      let emit_proof p =
+      let pr =
         let module P = Solver.P in
+        let proof = Solver.proof solver in
         let tst = Solver.tst solver in
-        P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) p;
+        P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) proof
-        P.emit_redundant_clause (Iter.of_list c) p;
       in
 
-      Solver.add_clause solver (IArray.of_list c) emit_proof;
+      Solver.add_clause solver (IArray.of_list c) pr;
       E.return()
 
     | Statement.Stmt_data _ ->

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -18,6 +18,29 @@ type ('a, 'args) bool_view =
   | B_opaque_bool of 'a (* do not enter *)
   | B_atom of 'a
 
+module type PROOF = sig
+  type proof
+  type proof_step
+  type term
+  type lit
+
+  val lemma_bool_tauto : lit Iter.t -> proof -> proof_step
+  (** Boolean tautology lemma (clause) *)
+
+  val lemma_bool_c : string -> term list -> proof -> proof_step
+  (** Basic boolean logic lemma for a clause [|- c].
+      [proof_bool_c b name cs] is the rule designated by [name]. *)
+
+  val lemma_bool_equiv : term -> term -> proof -> proof_step
+  (** Boolean tautology lemma (equivalence) *)
+
+  val lemma_ite_true : ite:term -> proof -> proof_step
+  (** lemma [a ==> ite a b c = b] *)
+
+  val lemma_ite_false : ite:term -> proof -> proof_step
+  (** lemma [¬a ==> ite a b c = c] *)
+end
+
 (** Argument to the theory *)
 module type ARG = sig
   module S : Sidekick_core.SOLVER
@@ -36,21 +59,11 @@ module type ARG = sig
       Only enable if some theories are susceptible to
       create boolean formulas during the proof search. *)
 
-  val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.proof_rule
+  include PROOF
-  (** Boolean tautology lemma (clause) *)
+    with type proof := S.P.t
-
+     and type proof_step := S.P.proof_step
-  val lemma_bool_c : string -> term list -> S.P.proof_rule
+     and type lit := S.Lit.t
-  (** Basic boolean logic lemma for a clause [|- c].
+     and type term := S.T.Term.t
-      [proof_bool_c b name cs] is the rule designated by [name]. *)
-
-  val lemma_bool_equiv : term -> term -> S.P.proof_rule
-  (** Boolean tautology lemma (equivalence) *)
-
-  val lemma_ite_true : ite:term -> S.P.proof_rule
-  (** lemma [a ==> ite a b c = b] *)
-
-  val lemma_ite_false : ite:term -> S.P.proof_rule
-  (** lemma [¬a ==> ite a b c = c] *)
 
   (** Fresh symbol generator.
 

src/th-data/th_intf.ml

@@ -21,6 +21,45 @@ type ('c, 'ty) data_ty_view =
     }
   | Ty_other
 
+module type PROOF = sig
+  type term
+  type lit
+  type proof_step
+  type proof
+
+  val lemma_isa_cstor : cstor_t:term -> term -> proof -> proof_step
+  (** [lemma_isa_cstor (d …) (is-c t)] returns the clause
+      [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *)
+
+  val lemma_select_cstor : cstor_t:term -> term -> proof -> proof_step
+  (** [lemma_select_cstor (c t1…tn) (sel-c-i t)]
+      returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *)
+
+  val lemma_isa_split : term -> lit Iter.t -> proof -> proof_step
+  (** [lemma_isa_split t lits] is the proof of
+      [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *)
+
+  val lemma_isa_sel : term -> proof -> proof_step
+  (** [lemma_isa_sel (is-c t)] is the proof of
+      [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *)
+
+  val lemma_isa_disj : lit -> lit -> proof -> proof_step
+  (** [lemma_isa_disj (is-c t) (is-d t)] is the proof
+      of [¬ (is-c t) \/ ¬ (is-c t)] *)
+
+  val lemma_cstor_inj : term -> term -> int -> proof -> proof_step
+  (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of
+      [c t1…tn = c u1…un |- ti = ui] *)
+
+  val lemma_cstor_distinct : term -> term -> proof -> proof_step
+  (** [lemma_isa_distinct (c …) (d …)] is the proof
+      of the unit clause [|- (c …) ≠ (d …)] *)
+
+  val lemma_acyclicity : (term * term) Iter.t -> proof -> proof_step
+  (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
+      by acyclicity. *)
+end
+
 module type ARG = sig
   module S : Sidekick_core.SOLVER
 
@@ -66,35 +105,9 @@ module type ARG = sig
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
   (** Modify the "finite" field (see {!ty_is_finite}) *)
 
-  val lemma_isa_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.proof_rule
+  include PROOF
-  (** [lemma_isa_cstor (d …) (is-c t)] returns the clause
+    with type proof := S.P.t
-      [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *)
+     and type proof_step := S.P.proof_step
-
+     and type term := S.T.Term.t
-  val lemma_select_cstor : cstor_t:S.T.Term.t -> S.T.Term.t -> S.P.proof_rule
+     and type lit := S.Lit.t
-  (** [lemma_select_cstor (c t1…tn) (sel-c-i t)]
-      returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *)
-
-  val lemma_isa_split : S.T.Term.t -> S.Lit.t Iter.t -> S.P.proof_rule
-  (** [lemma_isa_split t lits] is the proof of
-      [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *)
-
-  val lemma_isa_sel : S.T.Term.t -> S.P.proof_rule
-  (** [lemma_isa_sel (is-c t)] is the proof of
-      [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *)
-
-  val lemma_isa_disj : S.Lit.t -> S.Lit.t -> S.P.proof_rule
-  (** [lemma_isa_disj (is-c t) (is-d t)] is the proof
-      of [¬ (is-c t) \/ ¬ (is-c t)] *)
-
-  val lemma_cstor_inj : S.T.Term.t -> S.T.Term.t -> int -> S.P.proof_rule
-  (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of
-      [c t1…tn = c u1…un |- ti = ui] *)
-
-  val lemma_cstor_distinct : S.T.Term.t -> S.T.Term.t -> S.P.proof_rule
-  (** [lemma_isa_distinct (c …) (d …)] is the proof
-      of the unit clause [|- (c …) ≠ (d …)] *)
-
-  val lemma_acyclicity : (S.T.Term.t * S.T.Term.t) Iter.t -> S.P.proof_rule
-  (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
-      by acyclicity. *)
 end