From 16eb12fac21fe166a7aeb245ce9f42244d801968 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 31 Aug 2022 00:12:44 -0400 Subject: [PATCH] wip: preprocess in its own file --- src/smt/preprocess.ml | 88 +++++++++++++++++++++++++++++++++++ src/smt/preprocess.mli | 58 +++++++++++++++++++++++ src/th-lra/sidekick_th_lra.ml | 9 ++-- 3 files changed, 152 insertions(+), 3 deletions(-) create mode 100644 src/smt/preprocess.ml create mode 100644 src/smt/preprocess.mli diff --git a/src/smt/preprocess.ml b/src/smt/preprocess.ml new file mode 100644 index 00000000..a6aa13fb --- /dev/null +++ b/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 diff --git a/src/smt/preprocess.mli b/src/smt/preprocess.mli new file mode 100644 index 00000000..ac29b0fd --- /dev/null +++ b/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 diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml index 9f36e2a8..294fadb5 100644 --- a/src/th-lra/sidekick_th_lra.ml +++ b/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