From 07ca5546f5c05c12320d1475cf5b220f4b75c860 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 18 Mar 2021 12:19:30 -0400 Subject: [PATCH] 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 | 15 ++++++++----- src/core/Sidekick_core.ml | 2 -- src/msat-solver/Sidekick_msat_solver.ml | 22 ++++++++----------- src/th-bool-static/Sidekick_th_bool_static.ml | 13 +++++------ 4 files changed, 23 insertions(+), 29 deletions(-) diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index 14625334..76043634 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/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 ( diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 5c61f624..56883d0c 100644 --- a/src/core/Sidekick_core.ml +++ b/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. *) diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 63f650ac..0531ac9e 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/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 diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index e89a7c26..5e50e33d 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/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