feat(core): expose a preprocess function

src/arith/lra/sidekick_arith_lra.ml

@@ -227,8 +227,8 @@ module Make(A : ARG) : S with module A = A = struct
     Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t);
     let tst = SI.tst si in
 
-    (* simplify subterm *)
-    let simp_t = SI.simp_t si in
+    (* preprocess subterm *)
+    let preproc_t = SI.preprocess_term ~add_clause si in
 
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
@@ -257,8 +257,8 @@ module Make(A : ARG) : S with module A = A = struct
       None
 
     | LRA_pred (pred, t1, t2) ->
-      let l1 = as_linexp ~f:simp_t t1 in
-      let l2 = as_linexp ~f:simp_t t2 in
+      let l1 = as_linexp ~f:preproc_t t1 in
+      let l2 = as_linexp ~f:preproc_t t2 in
       let le = LE.(l1 - l2) in
       let le_comb, le_const = LE.comb le, LE.const le in
       let le_const = Q.neg le_const in
@@ -306,7 +306,7 @@ module Make(A : ARG) : S with module A = A = struct
       end
 
     | LRA_op _ | LRA_mult _ ->
-      let le = as_linexp ~f:simp_t t in
+      let le = as_linexp ~f:preproc_t t in
       let le_comb, le_const = LE.comb le, LE.const le in
 
       if Q.(le_const = zero) then (

src/core/Sidekick_core.ml

@@ -437,7 +437,11 @@ module type SOLVER_INTERNAL = sig
       not be backtracked. *)
 
   val mk_lit : t -> actions -> ?sign:bool -> term -> lit
-  (** Create a literal *)
+  (** Create a literal. This automatically preprocesses the term. *)
+
+  val preprocess_term :
+    t -> add_clause:(Lit.t list -> unit) -> term -> term
+  (** Preprocess a term. *)
 
   val add_lit : t -> actions -> lit -> unit
   (** Add the given literal to the SAT solver, so it gets assigned

src/msat-solver/Sidekick_msat_solver.ml

@@ -226,8 +226,9 @@ module Make(A : ARG)
       Stat.incr self.count_axiom;
       acts.Msat.acts_add_clause ~keep lits P.default
 
-    let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit =
-      let mk_lit t = Lit.atom self.tst t in
+    let preprocess_term_ (self:t) ~add_clause (t:term) : term =
+      let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
+
       (* compute and cache normal form of [t] *)
       let rec aux t =
         match Term.Tbl.find self.preprocess_cache t with
@@ -255,19 +256,27 @@ module Make(A : ARG)
           | None -> aux_rec t hooks_tl
           | Some u -> aux u
       in
-      let t = Lit.term lit |> simp_t self |> aux in
+      t |> simp_t self |> aux
+
+    let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit =
+      let t = Lit.term lit |> preprocess_term_ self ~add_clause in
       let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
       Log.debugf 10
         (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
       lit'
 
-    let mk_lit self acts ?sign t : Lit.t =
-      let add_clause lits =
-        Stat.incr self.count_preprocess_clause;
-        add_sat_clause_ self acts ~keep:true lits
-      in
+    (* add a clause using [acts] *)
+    let add_clause_ self acts lits : unit =
+      Stat.incr self.count_preprocess_clause;
+      add_sat_clause_ self acts ~keep:true lits
+
+    let mk_lit self acts ?sign t =
+      let add_clause = add_clause_ self acts in
       preprocess_lit_ self ~add_clause @@ Lit.atom self.tst ?sign t
 
+    let[@inline] preprocess_term self ~add_clause (t:term) : term =
+      preprocess_term_ self ~add_clause t
+
     let[@inline] add_clause_temp self acts lits : unit =
       add_sat_clause_ self acts ~keep:false lits