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

src/abstract-solver/asolver.ml

@@ -48,7 +48,7 @@ class type t =
     (** Returns the result of the last call to {!solve}, if the logic statee
         has not changed (mostly by asserting new clauses). *)
 
-    method proof_tracer : #Proof.Tracer.t
+    method proof_tracer : Proof.Tracer.t
     (** TODO: remove, use Tracer instead *)
   end
 

src/abstract-solver/check_res.ml

@@ -8,7 +8,7 @@ type t =
   | Unsat of {
       unsat_core: unit -> Lit.t Iter.t;
           (** Unsat core (subset of assumptions), or empty *)
-      unsat_step_id: unit -> Sidekick_proof.Step.id option;
+      unsat_proof: unit -> Sidekick_proof.Step.id option;
           (** Proof step for the empty clause *)
     }  (** Unsatisfiable *)
   | Unknown of Unknown.t

src/smt/solver.ml

@@ -2,8 +2,6 @@ open Sigs
 
 open struct
   module SI = Solver_internal
-  module P = Proof_trace
-  module Rule_ = Proof_core
 end
 
 module Check_res = Sidekick_abstract_solver.Check_res
@@ -18,7 +16,7 @@ type res = Check_res.t =
   | Unsat of {
       unsat_core: unit -> lit Iter.t;
           (** Unsat core (subset of assumptions), or empty *)
-      unsat_step_id: unit -> step_id option;
+      unsat_proof: unit -> step_id option;
           (** Proof step for the empty clause *)
     }  (** Unsatisfiable *)
   | Unknown of Unknown.t
@@ -30,7 +28,6 @@ type t = {
   solver: Sat_solver.t;
   mutable last_res: res option;
   stat: Stat.t;
-  proof: P.t;
   tracer: Tracer.t; [@ocaml.warn "-69"]
   theory_id_gen: Theory_id.state;
   n_clause_input: int Stat.counter;
@@ -63,18 +60,15 @@ let add_theory (self : t) (th : theory) : unit =
 let add_theory_l self = List.iter (add_theory self)
 
 (* create a new solver *)
-let create arg ?(stat = Stat.global) ?size ?(tracer = Tracer.dummy) ~proof
+let create arg ?(stat = Stat.global) ?size ~tracer ~theories tst () : t =
-    ~theories tst () : t =
   Log.debug 5 "smt-solver.create";
-  let si = Solver_internal.create arg ~tracer ~stat ~proof tst () in
+  let si = Solver_internal.create arg ~stat ~tracer tst () in
   let self =
     {
       si;
-      proof;
       tracer;
       last_res = None;
-      solver =
+      solver = Sat_solver.create ?size ~tracer ~stat (SI.to_sat_plugin si);
-        Sat_solver.create ~proof ?size ~tracer ~stat (SI.to_sat_plugin si);
       stat;
       theory_id_gen = Theory_id.create ();
       n_clause_input = Stat.mk_int stat "smt.solver.add-clause.input";
@@ -88,7 +82,7 @@ let create arg ?(stat = Stat.global) ?size ?(tracer = Tracer.dummy) ~proof
    let t_true = Term.true_ tst in
    Sat_solver.add_clause self.solver
      [ Lit.atom tst t_true ]
-     (P.add_step self.proof @@ fun () -> Rule_.lemma_true t_true));
+     (fun () -> Proof.Core_rules.lemma_true t_true));
   self
 
 let default_arg =
@@ -96,13 +90,13 @@ let default_arg =
     let view_as_cc = Default_cc_view.view_as_cc
   end : ARG)
 
-let create_default ?stat ?size ?tracer ~proof ~theories tst () : t =
+let create_default ?stat ?size ~tracer ~theories tst () : t =
-  create default_arg ?stat ?size ?tracer ~proof ~theories tst ()
+  create default_arg ?stat ?size ~tracer ~theories tst ()
 
 let[@inline] solver self = self.solver
 let[@inline] stats self = self.stat
 let[@inline] tst self = Solver_internal.tst self.si
-let[@inline] proof self = self.proof
+let[@inline] tracer self = self.tracer
 let[@inline] last_res self = self.last_res
 let[@inline] registry self = Solver_internal.registry self.si
 let reset_last_res_ self = self.last_res <- None
@@ -132,7 +126,9 @@ let add_clause_nopreproc_ ~internal (self : t) (c : lit array) (proof : step_id)
   Log.debugf 50 (fun k ->
       k "(@[solver.add-clause@ %a@])" (Util.pp_array Lit.pp) c);
   let pb = Profile.begin_ "add-clause" in
-  Sat_solver.add_clause_a self.solver (c :> lit array) proof;
+  Sat_solver.add_clause_a self.solver
+    (c :> lit array)
+    (fun () -> Proof.Pterm.ref proof);
   Profile.exit pb
 
 let add_clause_nopreproc_l_ ~internal self c p =
@@ -148,9 +144,10 @@ module Perform_delayed_ = Solver_internal.Perform_delayed (struct
     Sat_solver.add_lit solver.solver ?default_pol lit
 end)
 
-let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
+let add_clause (self : t) (c : lit array) (proof : Proof.Pterm.delayed) : unit =
+  let proof = Proof.Tracer.add_step self.tracer proof in
   let c, proof = preprocess_clause_ self c proof in
-  Tracer.assert_clause' self.tracer ~id:0 (Iter.of_array c);
+  Tracer.assert_clause' self.tracer ~id:0 (Iter.of_array c) proof;
   add_clause_nopreproc_ ~internal:false self c proof;
   Perform_delayed_.top self.si self;
   (* finish preproc *)
@@ -160,7 +157,7 @@ let add_clause_l self c p = add_clause self (CCArray.of_list c) p
 
 let assert_terms self c =
   let c = CCList.map (Lit.atom (tst self)) c in
-  let pr_c = P.add_step self.proof @@ fun () -> Proof_sat.sat_input_clause c in
+  let pr_c () = Proof.Sat_rules.sat_input_clause c in
   add_clause_l self c pr_c
 
 let assert_term self t = assert_terms self [ t ]
@@ -213,9 +210,9 @@ let solve ?(on_exit = []) ?(on_progress = fun _ -> ())
       Sat m
     | Sat_solver.Unsat (module UNSAT) ->
       let unsat_core () = UNSAT.unsat_assumptions () in
-      let unsat_step_id () = Some (UNSAT.unsat_proof ()) in
+      let unsat_proof () = Some (UNSAT.unsat_proof ()) in
       do_on_exit ();
-      Unsat { unsat_core; unsat_step_id }
+      Unsat { unsat_core; unsat_proof }
     | exception Resource_exhausted -> Unknown Unknown.U_asked_to_stop
   in
   self.last_res <- Some res;
@@ -227,7 +224,7 @@ let as_asolver (self : t) : Sidekick_abstract_solver.Asolver.t =
     method assert_clause c p : unit = add_clause self c p
     method assert_clause_l c p : unit = add_clause_l self c p
     method lit_of_term ?sign t : Lit.t = mk_lit_t self ?sign t
-    method proof = self.proof
+    method proof_tracer = (self.tracer :> Proof.Tracer.t)
     method last_res = last_res self
     method add_ty ~ty = add_ty self ty
 

src/smt/solver.mli

@@ -31,7 +31,7 @@ val mk_theory :
 
 val stats : t -> Stat.t
 val tst : t -> Term.store
-val tracer : t -> #Tracer.t
+val tracer : t -> Tracer.t
 
 val create :
   (module ARG) ->
@@ -85,11 +85,11 @@ val mk_lit_t : t -> ?sign:bool -> term -> lit
 
       The proof of [|- lit = lit'] is directly added to the solver's proof. *)
 
-val add_clause : t -> lit array -> step_id -> unit
+val add_clause : t -> lit array -> Proof.Pterm.delayed -> unit
 (** [add_clause solver cs] adds a boolean clause to the solver.
     Subsequent calls to {!solve} will need to satisfy this clause. *)
 
-val add_clause_l : t -> lit list -> step_id -> unit
+val add_clause_l : t -> lit list -> Proof.Pterm.delayed -> unit
 (** Add a clause to the solver, given as a list. *)
 
 val assert_terms : t -> term list -> unit
@@ -108,7 +108,7 @@ type res = Check_res.t =
   | Unsat of {
       unsat_core: unit -> lit Iter.t;
           (** Unsat core (subset of assumptions), or empty *)
-      unsat_step_id: unit -> step_id option;
+      unsat_proof: unit -> step_id option;
           (** Proof step for the empty clause *)
     }  (** Unsatisfiable *)
   | Unknown of Unknown.t

src/smt/solver_internal.ml

@@ -246,14 +246,16 @@ let simplify_and_preproc_lit self lit =
   find_foreign_vars_in_lit self lit;
   lit, pr
 
-let add_clause_temp self _acts c (proof : step_id) : unit =
+let add_clause_temp self _acts c (proof : Proof.Pterm.delayed) : unit =
+  let proof = Proof.Tracer.add_step self.tracer proof in
   let c, proof =
     Preprocess.preprocess_clause self.preprocess (preprocess_acts self) c proof
   in
   find_foreign_vars_in_lits self c;
   delayed_add_clause self ~keep:false c proof
 
-let add_clause_permanent self _acts c (proof : step_id) : unit =
+let add_clause_permanent self _acts c (proof : Proof.Pterm.delayed) : unit =
+  let proof = Proof.Tracer.add_step self.tracer proof in
   let c, proof =
     Preprocess.preprocess_clause self.preprocess (preprocess_acts self) c proof
   in

src/smt/solver_internal.mli

@@ -103,7 +103,8 @@ val on_find_foreign : t -> Find_foreign.hook -> unit
 
 (** {3 hooks for the theory} *)
 
-val raise_conflict : t -> theory_actions -> lit list -> step_id -> 'a
+val raise_conflict :
+  t -> theory_actions -> lit list -> Proof.Pterm.delayed -> 'a
 (** Give a conflict clause to the solver *)
 
 val push_decision : t -> theory_actions -> lit -> unit
@@ -113,11 +114,16 @@ val push_decision : t -> theory_actions -> lit -> unit
       and forgotten. *)
 
 val propagate :
-  t -> theory_actions -> lit -> reason:(unit -> lit list * step_id) -> unit
+  t ->
+  theory_actions ->
+  lit ->
+  reason:(unit -> lit list * Proof.Pterm.delayed) ->
+  unit
 (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-val propagate_l : t -> theory_actions -> lit -> lit list -> step_id -> unit
+val propagate_l :
+  t -> theory_actions -> lit -> lit list -> Proof.Pterm.delayed -> unit
 (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
@@ -204,7 +210,8 @@ val on_cc_conflict : t -> (CC.ev_on_conflict -> unit) -> unit
 
 val on_cc_propagate :
   t ->
-  (CC.t * lit * (unit -> lit list * step_id) -> CC.Handler_action.t list) ->
+  (CC.t * lit * (unit -> lit list * Proof.Pterm.delayed) ->
+  CC.Handler_action.t list) ->
   unit
 (** Callback called on every CC propagation *)