wip: preprocess in its own file

src/smt/preprocess.ml

@@ -0,0 +1,88 @@
+open Sigs
+
+module type PREPROCESS_ACTS = sig
+  val proof : proof_trace
+  val mk_lit : ?sign:bool -> term -> lit
+  val add_clause : lit list -> step_id -> unit
+  val add_lit : ?default_pol:bool -> lit -> unit
+end
+
+type preprocess_actions = (module PREPROCESS_ACTS)
+
+(* action taken later *)
+type delayed_action =
+  | DA_add_clause of lit list * step_id
+  | DA_add_lit of { default_pol: bool option; lit: lit }
+
+type t = {
+  tst: Term.store;  (** state for managing terms *)
+  proof: proof_trace;
+  mutable preprocess: preprocess_hook list;
+  preprocessed: Term.t Term.Tbl.t;
+  delayed_actions: delayed_action Vec.t;
+  n_preprocess_clause: int Stat.counter;
+}
+
+and preprocess_hook = t -> preprocess_actions -> term -> term option
+
+let create ?(stat = Stat.global) ~proof tst : t =
+  {
+    tst;
+    proof;
+    preprocess = [];
+    preprocessed = Term.Tbl.create 8;
+    delayed_actions = Vec.create ();
+    n_preprocess_clause = Stat.mk_int stat "smt.preprocess.n-clauses";
+  }
+
+let on_preprocess self f = self.preprocess <- f :: self.preprocess
+
+let preprocess_term_ (self : t) (t0 : term) : unit =
+  let module A = struct
+    let proof = self.proof
+    let mk_lit ?sign t : Lit.t = Lit.atom ?sign self.tst t
+
+    let add_lit ?default_pol lit : unit =
+      Vec.push self.delayed_actions (DA_add_lit { default_pol; lit })
+
+    let add_clause c pr : unit =
+      Vec.push self.delayed_actions (DA_add_clause (c, pr))
+  end in
+  let acts = (module A : PREPROCESS_ACTS) in
+
+  (* how to preprocess a term and its subterms *)
+  let rec preproc_rec_ t : Term.t =
+    match Term.Tbl.find_opt self.preprocessed t with
+    | Some u -> u
+    | None ->
+
+      (* process sub-terms first *)
+      let u = Term.map_shallow self.tst t
+        ~f:(fun _inb u -> preproc_rec_ u);
+
+      Log.debugf 50 (fun k -> k "(@[smt.preprocess@ %a@])" Term.pp_debug t);
+
+      (* signal boolean subterms, so as to decide them
+         in the SAT solver *)
+      if Ty.is_bool (Term.ty t) then (
+        Log.debugf 5 (fun k ->
+            k "(@[solver.map-bool-subterm-to-lit@ :subterm %a@])" Term.pp_debug
+              t);
+
+        (* make a literal *)
+        let lit = Lit.atom self.tst t in
+        (* ensure that SAT solver has a boolean atom for [u] *)
+        delayed_add_lit self lit;
+
+        (* also map [sub] to this atom in the congruence closure, for propagation *)
+        let cc = cc self in
+        CC.set_as_lit cc (CC.add_term cc t) lit;
+
+
+        Term.Tbl.add self.preprocessed t u;
+      )
+
+      List.iter (fun f -> f self acts t) self.preprocess
+    )
+  in
+  preproc_rec_ t0

src/smt/preprocess.mli

@@ -0,0 +1,58 @@
+(** Preprocessor
+
+    The preprocessor turn mixed, raw literals (possibly simplified) into
+    literals suitable for reasoning.
+    Every literal undergoes preprocessing.
+    Typically some clauses are also added to the solver on the side.
+*)
+
+open Sigs
+
+type t
+(** Preprocessor *)
+
+val create : ?stat:Stat.t -> proof:proof_trace -> Term.store -> t
+
+(** Actions given to preprocessor hooks *)
+module type PREPROCESS_ACTS = sig
+  val proof : proof_trace
+
+  val mk_lit : ?sign:bool -> term -> lit
+  (** [mk_lit t] creates a new literal for a boolean term [t]. *)
+
+  val add_clause : lit list -> step_id -> unit
+  (** pushes a new clause into the SAT solver. *)
+
+  val add_lit : ?default_pol:bool -> lit -> unit
+  (** Ensure the literal will be decided/handled by the SAT solver. *)
+end
+
+type preprocess_actions = (module PREPROCESS_ACTS)
+(** Actions available to the preprocessor *)
+
+type preprocess_hook = t -> preprocess_actions -> term -> term option
+(** Given a term, preprocess it.
+
+    The idea is to add literals and clauses to help define the meaning of
+    the term, if needed. For example for boolean formulas, clauses
+    for their Tseitin encoding can be added, with the formula acting
+    as its own proxy symbol; or a new symbol might be added.
+
+    @param preprocess_actions actions available during preprocessing.
+*)
+
+val on_preprocess : t -> preprocess_hook -> unit
+(** Add a hook that will be called when terms are preprocessed *)
+
+val preprocess_clause : t -> lit list -> step_id -> lit list * step_id
+val preprocess_clause_array : t -> lit array -> step_id -> lit array * step_id
+
+(** {2 Delayed actions} *)
+
+(** Action that preprocess hooks took, but were not effected yet.
+    The SMT solver itself should obtain these actions and perform them. *)
+type delayed_action =
+  | DA_add_clause of lit list * step_id
+  | DA_add_lit of { default_pol: bool option; lit: lit }
+
+val pop_delayed_actions : t -> delayed_action Iter.t

src/th-lra/sidekick_th_lra.ml

@@ -131,6 +131,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     in_model: unit Term.Tbl.t; (* terms to add to model *)
     encoded_eqs: unit Term.Tbl.t;
     (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
+    encoded_lits: Lit.t Term.Tbl.t;  (** [t => lit for t], using gensym *)
     simp_preds: (Term.t * S_op.t * A.Q.t) Term.Tbl.t;
     (* term -> its simplex meaning *)
     simp_defined: LE.t Term.Tbl.t;
@@ -157,6 +158,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
       simp_preds = Term.Tbl.create 32;
       simp_defined = Term.Tbl.create 16;
       encoded_eqs = Term.Tbl.create 8;
+      encoded_lits = Term.Tbl.create 8;
       encoded_le = Comb_map.empty;
       simplex = SimpSolver.create ~stat ();
       last_res = None;
@@ -274,7 +276,6 @@ module Make (A : ARG) = (* : S with module A = A *) struct
     | Geq -> S_op.Geq
     | Gt -> S_op.Gt
 
-  (* TODO: refactor that and {!var_encoding_comb} *)
   (* turn a linear expression into a single constant and a coeff.
      This might define a side variable in the simplex. *)
   let le_comb_to_singleton_ (self : state) (le_comb : LE_.Comb.t) :
@@ -341,6 +342,8 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         add_clause_lra_ (module PA) [ Lit.neg lit_t; lit_u2 ];
         add_clause_lra_ (module PA) [ Lit.neg lit_u1; Lit.neg lit_u2; lit_t ]
       )
+    | LRA_pred _ when Term.Tbl.mem self.encoded_lits t ->
+      (* already encoded *) ()
     | LRA_pred (pred, t1, t2) ->
       let l1 = as_linexp t1 in
       let l2 = as_linexp t2 in
@@ -369,10 +372,10 @@ module Make (A : ARG) = (* : S with module A = A *) struct
           op
       in
 
-      let lit = PA.mk_lit t in
+      let lit = fresh_lit self ~mk_lit:PA.mk_lit ~pre:"$lra" in
       let constr = SimpSolver.Constraint.mk v op q in
       SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
-      Term.Tbl.add self.simp_preds t (v, op, q);
+      Term.Tbl.add self.simp_preds (Lit.term lit) (v, op, q);
 
       Log.debugf 50 (fun k ->
           k "(@[lra.preproc@ :t %a@ :to-constr %a@])" Term.pp_debug t