From 5135d9920afac864b7fa066cc43372b9e799af6f Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 12 Oct 2022 12:21:20 -0400
Subject: [PATCH] refactor(asolver): use new proof tracer from sidekick.proof

---
 src/abstract-solver/asolver.ml   |  9 +++++----
 src/abstract-solver/check_res.ml |  2 +-
 src/abstract-solver/dune         | 10 ++++------
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/abstract-solver/asolver.ml b/src/abstract-solver/asolver.ml
index eb5f6aa9..376b43c3 100644
--- a/src/abstract-solver/asolver.ml
+++ b/src/abstract-solver/asolver.ml
@@ -3,6 +3,7 @@
 open Sidekick_core
 module Unknown = Unknown
 module Check_res = Check_res
+module Proof = Sidekick_proof
 
 class type t =
   object
@@ -12,11 +13,11 @@ class type t =
 
         This uses {!Proof_sat.sat_input_clause} to justify the assertion. *)
 
-    method assert_clause : Lit.t array -> Proof_step.id -> unit
+    method assert_clause : Lit.t 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. *)
 
-    method assert_clause_l : Lit.t list -> Proof_step.id -> unit
+    method assert_clause_l : Lit.t list -> Proof.Pterm.delayed -> unit
     (** Add a clause to the solver, given as a list. *)
 
     method add_ty : ty:Term.t -> unit
@@ -47,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 : Proof_trace.t
+    method proof_tracer : #Proof.Tracer.t
     (** TODO: remove, use Tracer instead *)
   end
 
@@ -62,4 +63,4 @@ let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () :
   self#solve ?on_exit ?on_progress ?should_stop ~assumptions ()
 
 let last_res (self : #t) = self#last_res
-let proof (self : #t) : Proof_trace.t = self#proof
+let proof (self : #t) : #Proof.Tracer.t = self#proof
diff --git a/src/abstract-solver/check_res.ml b/src/abstract-solver/check_res.ml
index 17dbbc91..14f4fb6e 100644
--- a/src/abstract-solver/check_res.ml
+++ b/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 -> Proof_trace.step_id option;
+      unsat_step_id: unit -> Sidekick_proof.Step.id option;
           (** Proof step for the empty clause *)
     }  (** Unsatisfiable *)
   | Unknown of Unknown.t
diff --git a/src/abstract-solver/dune b/src/abstract-solver/dune
index 440f122f..2e32b504 100644
--- a/src/abstract-solver/dune
+++ b/src/abstract-solver/dune
@@ -1,7 +1,5 @@
-
 (library
-  (name sidekick_abstract_solver)
-  (public_name sidekick.abstract-solver)
-  (flags :standard -open Sidekick_util -open Sidekick_core)
-  (libraries containers iter
-             sidekick.core sidekick.model))
+ (name sidekick_abstract_solver)
+ (public_name sidekick.abstract-solver)
+ (flags :standard -open Sidekick_util -open Sidekick_core)
+ (libraries containers iter sidekick.core sidekick.model sidekick.proof))