wip: refactor(smt): use sidekick.proof for proof tracing

src/smt/dune

@@ -3,6 +3,6 @@
  (public_name sidekick.smt-solver)
  (synopsis "main SMT solver")
  (libraries containers iter sidekick.core sidekick.util sidekick.cc
-   sidekick.sat sidekick.abstract-solver sidekick.simplify
-   sidekick.model sidekick.trace)
+   sidekick.sat sidekick.abstract-solver sidekick.simplify sidekick.model
+   sidekick.proof sidekick.trace)
  (flags :standard -w +32 -open Sidekick_util))

src/smt/preprocess.ml

@@ -1,7 +1,7 @@
 open Sigs
 
 module type PREPROCESS_ACTS = sig
-  val proof : proof_trace
+  val proof_tracer : Proof.Tracer.t
   val mk_lit : ?sign:bool -> term -> lit
   val add_clause : lit list -> step_id -> unit
   val add_lit : ?default_pol:bool -> lit -> unit
@@ -13,7 +13,7 @@ type t = {
   tst: Term.store;  (** state for managing terms *)
   cc: CC.t;
   simplify: Simplify.t;
-  proof: proof_trace;
+  proof: Proof.Tracer.t;
   mutable preprocess: preprocess_hook list;
   preprocessed: Term.t Term.Tbl.t;
   n_preprocess_clause: int Stat.counter;
@@ -28,6 +28,7 @@ and preprocess_hook =
   term option
 
 let create ?(stat = Stat.global) ~proof ~cc ~simplify tst : t =
+  let proof = (proof : #Proof.Tracer.t :> Proof.Tracer.t) in
   {
     tst;
     proof;
@@ -130,8 +131,8 @@ module Preprocess_clause (A : ARR) = struct
         pr_c
       else (
         Stat.incr self.n_preprocess_clause;
-        Proof_trace.add_step self.proof @@ fun () ->
-        Proof_core.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps
+        Proof.Tracer.add_step self.proof @@ fun () ->
+        Proof.Core_rules.lemma_rw_clause pr_c ~res:(A.to_list c') ~using:!steps
       )
     in
     c', pr_c'

src/smt/preprocess.mli

@@ -14,7 +14,7 @@ type t
 
 val create :
   ?stat:Stat.t ->
-  proof:proof_trace ->
+  proof:#Proof.Tracer.t ->
   cc:CC.t ->
   simplify:Simplify.t ->
   Term.store ->
@@ -22,7 +22,7 @@ val create :
 
 (** Actions given to preprocessor hooks *)
 module type PREPROCESS_ACTS = sig
-  val proof : proof_trace
+  val proof_tracer : Proof.Tracer.t
 
   val mk_lit : ?sign:bool -> term -> lit
   (** [mk_lit t] creates a new literal for a boolean term [t]. *)

src/smt/sigs.ml

@@ -18,14 +18,14 @@ module Simplify = Sidekick_simplify
 module CC = Sidekick_cc.CC
 module E_node = Sidekick_cc.E_node
 module CC_expl = Sidekick_cc.Expl
+module Proof = Sidekick_proof
 
 type term = Term.t
 type ty = term
 type value = Term.t
 type lit = Lit.t
 type term_store = Term.store
-type proof_trace = Proof_trace.t
-type step_id = Proof_step.id
+type step_id = Sidekick_proof.Step.id
 
 (* actions from the sat solver *)
 type sat_acts = Sidekick_sat.acts

src/smt/solver.ml

@@ -11,8 +11,6 @@ module Check_res = Sidekick_abstract_solver.Check_res
 module Sat_solver = Sidekick_sat
 (** the parametrized SAT Solver *)
 
-(** {2 Result} *)
-
 module Unknown = Sidekick_abstract_solver.Unknown [@@ocaml.warning "-37"]
 
 type res = Check_res.t =

src/smt/solver.mli

@@ -31,15 +31,14 @@ val mk_theory :
 
 val stats : t -> Stat.t
 val tst : t -> Term.store
-val proof : t -> proof_trace
+val tracer : t -> #Tracer.t
 
 val create :
   (module ARG) ->
   ?stat:Stat.t ->
   ?size:[ `Big | `Tiny | `Small ] ->
   (* TODO? ?config:Config.t -> *)
-  ?tracer:Tracer.t ->
-  proof:proof_trace ->
+  tracer:Tracer.t ->
   theories:Theory.t list ->
   Term.store ->
   unit ->
@@ -61,8 +60,7 @@ val create_default :
   ?stat:Stat.t ->
   ?size:[ `Big | `Tiny | `Small ] ->
   (* TODO? ?config:Config.t -> *)
-  ?tracer:Tracer.t ->
-  proof:proof_trace ->
+  tracer:Tracer.t ->
   theories:Theory.t list ->
   Term.store ->
   unit ->

src/smt/solver_internal.ml

@@ -39,7 +39,7 @@ type preprocess_hook =
 type t = {
   tst: Term.store;  (** state for managing terms *)
   cc: CC.t;  (** congruence closure *)
-  proof: proof_trace;  (** proof logger *)
+  tracer: Tracer.t;
   registry: Registry.t;
   seen_types: Term.Weak_set.t;  (** types we've seen so far *)
   on_progress: (unit, unit) Event.Emitter.t;
@@ -58,7 +58,6 @@ type t = {
   mutable level: int;
   mutable complete: bool;
   stat: Stat.t;
-  tracer: Tracer.t; [@ocaml.warning "-69"]
   count_axiom: int Stat.counter;
   count_conflict: int Stat.counter;
   count_propagate: int Stat.counter;
@@ -73,7 +72,7 @@ type solver = t
 
 let[@inline] cc (self : t) = self.cc
 let[@inline] tst self = self.tst
-let[@inline] proof self = self.proof
+let[@inline] tracer self = self.tracer
 let stats self = self.stat
 let registry self = self.registry
 let simplifier self = self.simp
@@ -111,7 +110,7 @@ let add_sat_clause_ self (acts : theory_actions) ~keep lits (proof : step_id) :
     unit =
   let (module A) = acts in
   Stat.incr self.count_axiom;
-  A.add_clause ~keep lits proof
+  A.add_clause ~keep lits (fun () -> Proof.Pterm.ref proof)
 
 let add_sat_lit_ _self ?default_pol (acts : theory_actions) (lit : Lit.t) : unit
     =
@@ -129,7 +128,7 @@ let delayed_add_clause (self : t) ~keep (c : Lit.t list) (pr : step_id) : unit =
 
 let preprocess_acts (self : t) : Preprocess.preprocess_actions =
   (module struct
-    let proof = self.proof
+    let proof_tracer = (self.tracer :> Proof.Tracer.t)
     let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t
     let add_clause c pr = delayed_add_clause self ~keep:true c pr
     let add_lit ?default_pol lit = delayed_add_lit self ?default_pol lit
@@ -307,7 +306,7 @@ let cc_are_equal self t1 t2 =
 
 let cc_resolve_expl self e : lit list * _ =
   let r = CC.explain_expl (cc self) e in
-  r.lits, r.pr self.proof
+  r.lits, r.pr
 
 (** {2 Interface with the SAT solver} *)
 
@@ -411,7 +410,7 @@ let check_cc_with_acts_ (self : t) (acts : theory_actions) =
       acts
   | Error (CC.Result_action.Conflict (lits, pr)) ->
     Stat.incr self.count_conflict;
-    A.raise_conflict lits pr
+    A.raise_conflict lits (fun () -> Proof.Pterm.ref pr)
 
 (* handle a literal assumed by the SAT solver *)
 let assert_lits_ ~final (self : t) (acts : theory_actions) (lits : Lit.t Iter.t)
@@ -521,16 +520,18 @@ let add_theory_state ~st ~push_level ~pop_levels (self : t) =
   self.th_states <-
     Ths_cons { st; push_level; pop_levels; next = self.th_states }
 
-let create (module A : ARG) ~stat ~tracer ~proof (tst : Term.store) () : t =
-  let simp = Simplify.create tst ~proof in
-  let cc = CC.create (module A : CC.ARG) ~size:`Big tst proof in
-  let preprocess = Preprocess.create ~stat ~proof ~cc ~simplify:simp tst in
+let create (module A : ARG) ~stat ~tracer (tst : Term.store) () : t =
+  let tracer = (tracer : #Tracer.t :> Tracer.t) in
+  let simp = Simplify.create tst ~proof:tracer in
+  let cc = CC.create (module A : CC.ARG) ~size:`Big tst tracer in
+  let preprocess =
+    Preprocess.create ~stat ~proof:tracer ~cc ~simplify:simp tst
+  in
   let find_foreign = Find_foreign.create () in
   let self =
     {
       tst;
       cc;
-      proof;
       tracer;
       th_states = Ths_nil;
       stat;

src/smt/solver_internal.mli

@@ -13,8 +13,8 @@ type solver = t
 val tst : t -> term_store
 val stats : t -> Stat.t
 
-val proof : t -> proof_trace
-(** Access the proof object *)
+val tracer : t -> Tracer.t
+(** Access the tracer object *)
 
 val registry : t -> Registry.t
 (** A solver contains a registry so that theories can share data *)
@@ -121,11 +121,13 @@ val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit
 (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-val add_clause_temp : t -> theory_actions -> lit list -> step_id -> unit
+val add_clause_temp :
+  t -> theory_actions -> lit list -> Proof.Pterm.delayed -> unit
 (** Add local clause to the SAT solver. This clause will be
       removed when the solver backtracks. *)
 
-val add_clause_permanent : t -> theory_actions -> lit list -> step_id -> unit
+val add_clause_permanent :
+  t -> theory_actions -> lit list -> Proof.Pterm.delayed -> unit
 (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
@@ -150,7 +152,7 @@ val cc_find : t -> E_node.t -> E_node.t
 val cc_are_equal : t -> term -> term -> bool
 (** Are these two terms equal in the congruence closure? *)
 
-val cc_resolve_expl : t -> CC_expl.t -> lit list * step_id
+val cc_resolve_expl : t -> CC_expl.t -> lit list * Proof.Pterm.delayed
 
 (*
   val cc_raise_conflict_expl : t -> theory_actions -> CC_expl.t -> 'a
@@ -284,10 +286,4 @@ val add_theory_state :
   unit
 
 val create :
-  (module ARG) ->
-  stat:Stat.t ->
-  tracer:Tracer.t ->
-  proof:Proof_trace.t ->
-  Term.store ->
-  unit ->
-  t
+  (module ARG) -> stat:Stat.t -> tracer:#Tracer.t -> Term.store -> unit -> t

src/smt/tracer.ml

@@ -1,18 +1,20 @@
 open Sidekick_core
 module Tr = Sidekick_trace
+module Proof = Sidekick_proof
 module V = Ser_value
 
 class type t =
   object
     inherit Term.Tracer.t
-    method emit_assert_term : Term.t -> Tr.Entry_id.t
-    inherit Clause_tracer.t
+    inherit Sidekick_proof.Tracer.t
+    inherit Sidekick_sat.Tracer.t
     method emit_assert_term : Term.t -> Tr.Entry_id.t
   end
 
 class concrete (sink : Tr.Sink.t) : t =
   object (self)
     inherit Term.Tracer.concrete ~sink as emit_t
+    inherit Sidekick_proof.Tracer.concrete ~sink
 
     method emit_assert_term t =
       let id_t = emit_t#emit_term t in
@@ -20,23 +22,23 @@ class concrete (sink : Tr.Sink.t) : t =
       let id = Tr.Sink.emit sink ~tag:"AssT" v in
       id
 
-    method encode_lit (lit : Lit.t) : V.t =
+    method sat_encode_lit (lit : Lit.t) : V.t =
       let sign = Lit.sign lit in
       let id_t = emit_t#emit_term @@ Lit.term lit in
       V.(list [ bool sign; int id_t ])
 
-    method assert_clause ~id (c : Lit.t Iter.t) =
+    method sat_assert_clause ~id (c : Lit.t Iter.t) (pr : Proof.Step.id) =
       (* get a list of pairs *)
-      let l = Iter.map self#encode_lit c |> Iter.to_rev_list |> V.list in
-      let v = V.(dict_of_list [ "id", int id; "c", l ]) in
+      let l = Iter.map self#sat_encode_lit c |> Iter.to_rev_list |> V.list in
+      let v = V.(dict_of_list [ "id", int id; "c", l; "p", int pr ]) in
       let id = Tr.Sink.emit sink ~tag:"AssC" v in
       id
 
-    method unsat_clause ~id =
+    method sat_unsat_clause ~id =
       let v = Ser_value.(dict_of_list [ "id", int id ]) in
       Tr.Sink.emit sink ~tag:"UnsatC" v
 
-    method delete_clause ~id _lits : unit =
+    method sat_delete_clause ~id _lits : unit =
       let v = Ser_value.(dict_of_list [ "id", int id ]) in
       ignore (Tr.Sink.emit sink ~tag:"DelCSat" v : Tr.Entry_id.t)
   end
@@ -44,23 +46,25 @@ class concrete (sink : Tr.Sink.t) : t =
 class dummy : t =
   object
     inherit Term.Tracer.dummy
-    inherit Clause_tracer.dummy
+    inherit Sidekick_sat.Tracer.dummy
     method emit_assert_term _ = Tr.Entry_id.dummy
   end
 
 let dummy : #t = new dummy
 let make ~sink () = new concrete sink
-let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
 
-let assert_clause' (self : #t) ~id c : unit =
-  ignore (self#assert_clause ~id c : Tr.Entry_id.t)
+let assert_clause (self : #t) ~id c pr : Tr.Entry_id.t =
+  self#sat_assert_clause ~id c pr
 
-let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id
+let assert_clause' (self : #t) ~id c pr : unit =
+  ignore (self#sat_assert_clause ~id c pr : Tr.Entry_id.t)
+
+let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#sat_unsat_clause ~id
 
 let unsat_clause' (self : #t) ~id : unit =
-  ignore (self#unsat_clause ~id : Tr.Entry_id.t)
+  ignore (self#sat_unsat_clause ~id : Tr.Entry_id.t)
 
-let delete_clause (self : #t) ~id c = self#delete_clause ~id c
-let encode_lit (self : #t) lit = self#encode_lit lit
+let delete_clause (self : #t) ~id c = self#sat_delete_clause ~id c
+let encode_lit (self : #t) lit = self#sat_encode_lit lit
 let assert_term (self : #t) t = self#emit_assert_term t
 let assert_term' (self : #t) t = ignore (assert_term self t : Tr.Entry_id.t)

src/smt/tracer.mli

@@ -1,10 +1,17 @@
+(** Tracer for SMT solvers.
+
+  The tracer is used to track clauses and terms used or deduced during proof
+  search. *)
+
 open Sidekick_core
 module Tr = Sidekick_trace
+module Proof = Sidekick_proof
 
 class type t =
   object
     inherit Term.Tracer.t
-    inherit Clause_tracer.t
+    inherit Sidekick_sat.Tracer.t
+    inherit Sidekick_proof.Tracer.t
 
     method emit_assert_term : Term.t -> Tr.Entry_id.t
     (** Emit an assertion *)
@@ -20,8 +27,11 @@ val dummy : t
 val make : sink:Tr.Sink.t -> unit -> t
 val assert_term : #t -> Term.t -> Tr.Entry_id.t
 val assert_term' : #t -> Term.t -> unit
-val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
-val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit
+
+val assert_clause :
+  #t -> id:int -> Lit.t Iter.t -> Proof.Step.id -> Tr.Entry_id.t
+
+val assert_clause' : #t -> id:int -> Lit.t Iter.t -> Proof.Step.id -> unit
 val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit
 val unsat_clause : #t -> id:int -> Tr.Entry_id.t
 val unsat_clause' : #t -> id:int -> unit