From 0393fae090323fd901aebf68a8e1c24ede8a8c4a Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 9 May 2023 20:42:24 -0400
Subject: [PATCH] cdsat

---
 src/cdsat/plugin_bool.ml          | 8 ++++----
 src/cdsat/plugin_uninterpreted.ml | 2 +-
 src/cdsat/reason.mli              | 1 +
 src/cdsat/term_to_var.ml          | 4 ++--
 src/cdsat/term_to_var.mli         | 2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/cdsat/plugin_bool.ml b/src/cdsat/plugin_bool.ml
index 8707e9d1..69885276 100644
--- a/src/cdsat/plugin_bool.ml
+++ b/src/cdsat/plugin_bool.ml
@@ -16,8 +16,8 @@ type TVar.theory_view +=
 (* our internal state *)
 type t = { arg: (module ARG); tst: Term.store; vst: TVar.store }
 
-let push_level (self : t) = ()
-let pop_levels (self : t) n = ()
+let push_level (_self : t) = ()
+let pop_levels (_self : t) _n = ()
 
 let decide (self : t) (v : TVar.t) : Value.t option =
   match TVar.theory_view self.vst v with
@@ -60,7 +60,7 @@ let propagate (self : t) (act : Core.Plugin_action.t) (v : TVar.t)
       k "(@[bool-plugin.propagate %a@])" (TVar.pp self.vst) v);
   ()
 
-let term_to_var_hooks (self : t) : _ list =
+let term_to_var_hooks (self : t) : Term_to_var.hook list =
   let (module A) = self.arg in
 
   let rec to_tlit t2v (t : Term.t) : TLit.t =
@@ -85,7 +85,7 @@ let term_to_var_hooks (self : t) : _ list =
       Some (T_or lits)
     | _ -> None
   in
-  [ h ]
+  [ { Term_to_var.conv = h } ]
 
 let iter_theory_view _ (v : TVar.theory_view) k =
   match v with
diff --git a/src/cdsat/plugin_uninterpreted.ml b/src/cdsat/plugin_uninterpreted.ml
index 2f39f056..cf84cdcb 100644
--- a/src/cdsat/plugin_uninterpreted.ml
+++ b/src/cdsat/plugin_uninterpreted.ml
@@ -60,7 +60,7 @@ let term_to_var_hooks (self : t) : _ list =
     ) else
       None
   in
-  [ h ]
+  [ { Term_to_var.conv = h } ]
 
 let iter_theory_view _ (v : TVar.theory_view) k : unit =
   match v with
diff --git a/src/cdsat/reason.mli b/src/cdsat/reason.mli
index 2e0761ae..37e8c795 100644
--- a/src/cdsat/reason.mli
+++ b/src/cdsat/reason.mli
@@ -8,6 +8,7 @@ type t = TVar.reason =
       hyps: TVar.Vec_of.t;
       proof: Sidekick_proof.step_id;
     }
+(* TODO: merge is also a reason *)
 
 include Sidekick_sigs.PRINT with type t := t
 
diff --git a/src/cdsat/term_to_var.ml b/src/cdsat/term_to_var.ml
index f49f18ab..bc99a786 100644
--- a/src/cdsat/term_to_var.ml
+++ b/src/cdsat/term_to_var.ml
@@ -1,5 +1,5 @@
 type t = { vst: TVar.store; mutable hooks: hook list }
-and hook = t -> Term.t -> TVar.theory_view option
+and hook = { conv: t -> Term.t -> TVar.theory_view option } [@@unboxed]
 
 let create vst : t = { vst; hooks = [] }
 let add_hook self h = self.hooks <- h :: self.hooks
@@ -12,7 +12,7 @@ let rec convert (self : t) (t : Term.t) : TVar.t =
         (Term.pp_limit ~max_depth:5 ~max_nodes:30)
         t
     | h :: tl_h ->
-      (match h self t with
+      (match h.conv self t with
       | Some theory_view ->
         let v = TVar.Internal.create self.vst t ~theory_view in
         v
diff --git a/src/cdsat/term_to_var.mli b/src/cdsat/term_to_var.mli
index db29b8d1..d83e32b1 100644
--- a/src/cdsat/term_to_var.mli
+++ b/src/cdsat/term_to_var.mli
@@ -22,7 +22,7 @@ val convert : t -> Term.t -> TVar.t
     Hooks are responsible for converting {b some} terms (the terms their theory
     knows) into variables. *)
 
-type hook = t -> Term.t -> TVar.theory_view option
+type hook = { conv: t -> Term.t -> TVar.theory_view option } [@@unboxed]
 (** A hook, responsible to keep some internal state and assigning a theory
     view if it "accepts" the term. A term that is recognized by no hook
     cannot be turned into a variable. *)