cdsat

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

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

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
 

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

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. *)