refactor: rename some hooks; prepare for model generation in th-data

src/arith/lra/sidekick_arith_lra.ml

@@ -583,7 +583,7 @@ module Make(A : ARG) : S with module A = A = struct
     let stat = SI.stats si in
     let st = create ~stat (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
-    SI.add_preprocess si (preproc_lra st);
+    SI.on_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);
     SI.on_partial_check si (partial_check_ st);
     SI.on_cc_is_subterm si (on_subterm st);

src/core/Sidekick_core.ml

@@ -531,7 +531,7 @@ module type SOLVER_INTERNAL = sig
       @param add_clause pushes a new clause into the SAT solver.
   *)
 
-  val add_preprocess : t -> preprocess_hook -> unit
+  val on_preprocess : t -> preprocess_hook -> unit
 
   (** {3 Model production} *)
 
@@ -541,7 +541,7 @@ module type SOLVER_INTERNAL = sig
   (** A model-production hook. It takes the solver, a class, and returns
       a term for this class. *)
 
-  val add_model_hook : t -> model_hook -> unit
+  val on_model_gen : t -> model_hook -> unit
 end
 
 (** Public view of the solver *)

src/msat-solver/Sidekick_msat_solver.ml

@@ -210,8 +210,8 @@ module Make(A : ARG)
     let simp_t self (t:Term.t) : Term.t = Simplify.normalize self.simp t
     let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
 
-    let add_preprocess self f = self.preprocess <- f :: self.preprocess
-    let add_model_hook self f = self.mk_model <- f :: self.mk_model
+    let on_preprocess self f = self.preprocess <- f :: self.preprocess
+    let on_model_gen self f = self.mk_model <- f :: self.mk_model
 
     let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
       let sign = Lit.sign lit in

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -268,8 +268,8 @@ module Make(A : ARG) : S with module A = A = struct
     Log.debug 2 "(th-bool.setup)";
     let st = create (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
-    SI.add_preprocess si (preproc_ite st);
-    SI.add_preprocess si (cnf st);
+    SI.on_preprocess si (preproc_ite st);
+    SI.on_preprocess si (cnf st);
     if A.check_congruence_classes then (
       Log.debug 5 "(th-bool.add-final-check)";
       SI.on_final_check si (check_new_terms st);

src/th-data/Sidekick_th_data.ml

@@ -532,6 +532,16 @@ module Make(A : ARG) : S with module A = A = struct
     end;
     ()
 
+  let on_model_gen (self:t) ~recurse (si:SI.t) (n:N.t) : T.t option =
+    (* TODO: option to complete model or not (by picking sth at leaves)? *)
+    let cc = SI.cc si in
+    let repr = SI.CC.find cc n in
+    match ST_cstors.get self.cstors repr with
+    | None -> None
+    | Some c ->
+      Log.debugf 1 (fun k->k "FIND CSTOR %a" Monoid_cstor.pp c);
+      None
+
   let create_and_setup (solver:SI.t) : t =
     let self = {
       tst=SI.tst solver;
@@ -545,6 +555,7 @@ module Make(A : ARG) : S with module A = A = struct
     SI.on_cc_new_term solver (on_new_term self);
     SI.on_cc_pre_merge solver (on_pre_merge self);
     SI.on_final_check solver (on_final_check self);
+    SI.on_model_gen solver (on_model_gen self);
     self
 
   let theory =