refator(preproc): remove explicit recursion, but rewrite top-down

give a chance to simplifiers to rewrite before we rewrite subterms.

src/arith/lra/sidekick_arith_lra.ml

@@ -223,10 +223,13 @@ module Make(A : ARG) : S with module A = A = struct
         proxy
 
   (* preprocess linear expressions away *)
-  let preproc_lra (self:state) si ~recurse ~mk_lit ~add_clause (t:T.t) : T.t option =
+  let preproc_lra (self:state) si ~mk_lit ~add_clause (t:T.t) : T.t option =
     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
+
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
       Log.debugf 50 (fun k->k "(@[simplex2.declare-term-to-cc@ %a@])" T.pp t);
@@ -245,8 +248,8 @@ module Make(A : ARG) : S with module A = A = struct
 
         (* encode [t <=> (u1 /\ u2)] *)
         let lit_t = mk_lit t in
-        let lit_u1 = mk_lit (recurse u1) in
-        let lit_u2 = mk_lit (recurse u2) in
+        let lit_u1 = mk_lit u1 in
+        let lit_u2 = mk_lit u2 in
         add_clause [SI.Lit.neg lit_t; lit_u1];
         add_clause [SI.Lit.neg lit_t; lit_u2];
         add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t];
@@ -254,8 +257,8 @@ module Make(A : ARG) : S with module A = A = struct
       None
 
     | LRA_pred (pred, t1, t2) ->
-      let l1 = as_linexp ~f:recurse t1 in
-      let l2 = as_linexp ~f:recurse t2 in
+      let l1 = as_linexp ~f:simp_t t1 in
+      let l2 = as_linexp ~f:simp_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
@@ -303,7 +306,7 @@ module Make(A : ARG) : S with module A = A = struct
       end
 
     | LRA_op _ | LRA_mult _ ->
-      let le = as_linexp ~f:recurse t in
+      let le = as_linexp ~f:simp_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

@@ -518,13 +518,11 @@ module type SOLVER_INTERNAL = sig
 
   type preprocess_hook =
     t ->
-    recurse:(term -> term) ->
     mk_lit:(term -> lit) ->
     add_clause:(lit list -> unit) ->
     term -> term option
   (** Given a term, try to preprocess it. Return [None] if it didn't change.
       Can also add clauses to define new terms.
-      @param recurse call preprocessor on subterms.
       @param mk_lit creates a new literal for a boolean term.
       @param add_clause pushes a new clause into the SAT solver.
   *)

src/msat-solver/Sidekick_msat_solver.ml

@@ -179,7 +179,6 @@ module Make(A : ARG)
 
     and preprocess_hook =
       t ->
-      recurse:(term -> term) ->
       mk_lit:(term -> lit) ->
       add_clause:(lit list -> unit) ->
       term -> term option
@@ -234,27 +233,24 @@ module Make(A : ARG)
         match Term.Tbl.find self.preprocess_cache t with
         | u -> u
         | exception Not_found ->
-          (* try rewrite here *)
-          let u =
-            match aux_rec t self.preprocess with
-            | None ->
-              Term.map_shallow self.tst aux t (* just map subterms *)
-            | Some u -> u
-          in
+          (* try rewrite at root *)
+          let t1 = aux_rec t self.preprocess in
+          (* then map subterms *)
+          let t2 = Term.map_shallow self.tst aux t1 in (* map subterms *)
+          let u = if t != t2 then aux t2 (* fixpoint *) else t2 in
           Term.Tbl.add self.preprocess_cache t u;
           u
       (* try each function in [hooks] successively *)
       and aux_rec t hooks = match hooks with
-        | [] -> None
+        | [] -> t
         | h :: hooks_tl ->
-          match h self ~recurse:aux ~mk_lit ~add_clause t with
+          match h self ~mk_lit ~add_clause t with
           | None -> aux_rec t hooks_tl
           | Some u ->
             Log.debugf 30
               (fun k->k "(@[msat-solver.preprocess.step@ :from %a@ :to %a@])"
                   Term.pp t Term.pp u);
-            let u' = aux u in
-            Some u'
+            aux u
       in
       let t = Lit.term lit |> simp_t self |> aux in
       let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
@@ -262,7 +258,7 @@ module Make(A : ARG)
         (fun k->k "(@[msat-solver.preprocess@ :lit %a@ :into %a@])" Lit.pp lit Lit.pp lit');
       lit'
 
-    let mk_lit self acts ?sign t =
+    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

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -135,18 +135,16 @@ module Make(A : ARG) : S with module A = A = struct
     mk_lit t
 
   (* preprocess "ite" away *)
-  let preproc_ite self _si ~recurse ~mk_lit ~add_clause (t:T.t) : T.t option =
+  let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : T.t option =
     match A.view_as_bool t with
     | B_ite (a,b,c) ->
-      let a = recurse a in
+      let a = SI.simp_t si a in
       begin match A.view_as_bool a with
-        | B_bool true -> Some (recurse b)
-        | B_bool false -> Some (recurse c)
+        | B_bool true -> Some b
+        | B_bool false -> Some c
         | _ ->
           let t_a = fresh_term self ~pre:"ite" (T.ty b) in
           let lit_a = mk_lit a in
-          let b = recurse b in
-          let c = recurse c in
           add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_a b)];
           add_clause [lit_a; mk_lit (eq self.tst t_a c)];
           Some t_a
@@ -154,7 +152,7 @@ module Make(A : ARG) : S with module A = A = struct
     | _ -> None
 
   (* TODO: polarity? *)
-  let cnf (self:state) (_si:SI.t) ~recurse:_ ~mk_lit ~add_clause (t:T.t) : T.t option =
+  let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : T.t option =
     let rec get_lit (t:T.t) : Lit.t =
       let t_abs, t_sign = T.abs self.tst t in
       let lit =
@@ -229,7 +227,6 @@ module Make(A : ARG) : S with module A = A = struct
     in
     let cnf_of t =
       cnf self si t
-        ~recurse:(fun t -> t)
         ~mk_lit:(SI.mk_lit si acts) ~add_clause:(SI.add_clause_permanent si acts)
     in
     begin