From 27796da5a8afe1dd80c44a35e7377dfc20bf0cc6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 22 Aug 2021 01:29:01 -0400 Subject: [PATCH] fix preprocessing in th-bool --- src/lra/sidekick_arith_lra.ml | 1 - src/sat/Solver.ml | 1 - src/smt-solver/Sidekick_smt_solver.ml | 68 ++++++++-------- src/th-bool-static/Sidekick_th_bool_static.ml | 79 +++++++++++-------- 4 files changed, 80 insertions(+), 69 deletions(-) diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index abadae5f..9dc60761 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -381,7 +381,6 @@ module Make(A : ARG) : S with module A = A = struct | LRA_other t when A.has_ty_real t -> None | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ -> - Log.debug 0 "LRA NONE"; None let simplify (self:state) (_recurse:_) (t:T.t) : T.t option = diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 2b31da92..4bbfecb8 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1842,7 +1842,6 @@ module Make(Plugin : PLUGIN) let[@inline] proof st = st.proof let[@inline] add_lit self ?default_pol lit = - Log.debugf 0 (fun k->k"add lit %a" Lit.pp lit); (* XXX *) ignore (make_atom_ self lit ?default_pol : atom) let[@inline] set_default_pol (self:t) (lit:lit) (pol:bool) : unit = let a = make_atom_ self lit ~default_pol:pol in diff --git a/src/smt-solver/Sidekick_smt_solver.ml b/src/smt-solver/Sidekick_smt_solver.ml index 4a5156bd..f301bfe0 100644 --- a/src/smt-solver/Sidekick_smt_solver.ml +++ b/src/smt-solver/Sidekick_smt_solver.ml @@ -251,7 +251,7 @@ module Make(A : ARG) (* actual preprocessing logic, acting on terms. this calls all the preprocessing hooks on subterms, ensuring a fixpoint. *) - let preprocess_term_ (self:t) (module A:PREPROCESS_ACTS) (t:term) : term = + let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term = let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *) (* compute and cache normal form [u] of [t]. @@ -261,19 +261,19 @@ module Make(A : ARG) next time we preprocess [t], we will have to re-emit the same proofs, even though we will not do any actual preprocessing work. *) - let rec aux t : term = + let rec preproc_rec t : term = match Term.Tbl.find self.preprocess_cache t with | u -> u | exception Not_found -> (* try rewrite at root *) - let t1 = aux_rec t self.preprocess in + let t1 = preproc_with_hooks t self.preprocess in (* map subterms *) - let t2 = Term.map_shallow self.tst aux t1 in + let t2 = Term.map_shallow self.tst preproc_rec t1 in let u = if not (Term.equal t t2) then ( - aux t2 (* fixpoint *) + preproc_rec t2 (* fixpoint *) ) else ( t2 ) @@ -288,7 +288,7 @@ module Make(A : ARG) (* make a literal (already preprocessed) *) let lit = mk_lit_nopreproc u in (* ensure that SAT solver has a boolean atom for [u] *) - A.add_lit lit; + A0.add_lit lit; (* also map [sub] to this atom in the congruence closure, for propagation *) let cc = cc self in @@ -305,39 +305,21 @@ module Make(A : ARG) u (* try each function in [hooks] successively *) - and aux_rec t hooks : term = + and preproc_with_hooks t hooks : term = match hooks with | [] -> t | h :: hooks_tl -> - match h self (module A) t with - | None -> aux_rec t hooks_tl - | Some u -> aux u - in - - P.begin_subproof self.proof; - - (* simplify the term *) - let t1 = simp_t self t in - - (* preprocess *) - let u = aux t1 in - (* emit [|- t=u] *) - if not (Term.equal t u) then ( - P.with_proof self.proof (P.lemma_preprocess t u); - ); - - P.end_subproof self.proof; - u - - (* return preprocessed lit + proof they are equal *) - let preprocess_lit_ (self:t) (module A0:PREPROCESS_ACTS) (lit:lit) : lit = + (* call hook, using [pacts] which will ensure all new + literals and clauses are also preprocessed *) + match h self (Lazy.force pacts) t with + | None -> preproc_with_hooks t hooks_tl + | Some u -> preproc_rec u (* create literal and preprocess it with [pacts], which uses [A0] for the base operations, and preprocesses new literals and clauses recursively. *) - let rec mk_lit ?sign t = - Log.debug 0 "A.MK_LIT"; - let u = preprocess_term_ self (Lazy.force pacts) t in + and mk_lit ?sign t = + let u = preproc_rec t in if not (Term.equal t u) then ( Log.debugf 10 (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])" @@ -364,7 +346,27 @@ module Make(A : ARG) end : PREPROCESS_ACTS) ) in - preprocess_lit lit + P.begin_subproof self.proof; + + (* simplify the term *) + let t1 = simp_t self t in + + (* preprocess *) + let u = preproc_rec t1 in + (* emit [|- t=u] *) + if not (Term.equal t u) then ( + P.with_proof self.proof (P.lemma_preprocess t u); + ); + + P.end_subproof self.proof; + u + + (* return preprocessed lit *) + let preprocess_lit_ (self:t) (pacts:preprocess_actions) (lit:lit) : lit = + let t = Lit.term lit in + let sign = Lit.sign lit in + let u = preprocess_term_ self pacts t in + Lit.atom self.tst ~sign u (* add a clause using [acts] *) let add_clause_ self acts lits (proof:dproof) : unit = diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 5edf0ae8..2c702cc8 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -216,29 +216,37 @@ module Make(A : ARG) : S with module A = A = struct (* TODO: polarity? *) let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option = - let rec get_lit (t:T.t) : Lit.t = + Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t); + + let mk_lit = PA.mk_lit in + + let rec get_lit_opt (t:T.t) : Lit.t option = let t_abs, t_sign = T.abs self.tst t in let lit_abs = match T.Tbl.find self.cnf t_abs with - | lit -> lit (* cached *) + | lit -> Some lit (* cached *) | exception Not_found -> - (* compute and cache *) + (* compute and cache, if present *) let lit = get_lit_uncached si t_abs in - if not (T.equal (Lit.term lit) t_abs) then ( - T.Tbl.add self.cnf t_abs lit; - Log.debugf 20 - (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])" - Lit.pp lit T.pp t_abs); - ); + begin match lit with + | None -> () + | Some lit -> + if not (T.equal (Lit.term lit) t_abs) then ( + T.Tbl.add self.cnf t_abs lit; + Log.debugf 20 + (fun k->k "(@[sidekick.bool.add-lit@ :lit %a@ :for-t %a@])" + Lit.pp lit T.pp t_abs); + ); + end; lit in - let lit = if t_sign then lit_abs else Lit.neg lit_abs in + let lit = if t_sign then lit_abs else CCOpt.map Lit.neg lit_abs in lit - and equiv_ si ~get_lit ~is_xor ~for_t t_a t_b : Lit.t = - let a = get_lit t_a in - let b = get_lit t_b in + and equiv_ si ~is_xor ~for_t t_a t_b : Lit.t = + let a = mk_lit t_a in + let b = mk_lit t_b in let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *) let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in @@ -266,17 +274,17 @@ module Make(A : ARG) : S with module A = A = struct proxy (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *) - and get_lit_uncached si t : Lit.t = + and get_lit_uncached si t : Lit.t option = match A.view_as_bool t with - | B_bool b -> PA.mk_lit (T.bool self.tst b) - | B_opaque_bool t -> PA.mk_lit t + | B_opaque_bool _ -> None + | B_bool b -> Some (PA.mk_lit (T.bool self.tst b)) | B_not u -> - let lit = get_lit u in - Lit.neg lit + let lit = get_lit_opt u in + CCOpt.map Lit.neg lit | B_and l -> let t_subs = Iter.to_list l in - let subs = List.map get_lit t_subs in + let subs = List.map mk_lit t_subs in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in SI.define_const si ~const:t_proxy ~rhs:t; SI.with_proof si (SI.P.define_term t_proxy t); @@ -289,11 +297,11 @@ module Make(A : ARG) : S with module A = A = struct t_subs subs; PA.add_clause (proxy :: List.map Lit.neg subs) (A.lemma_bool_c "and-i" [t_proxy]); - proxy + Some proxy | B_or l -> let t_subs = Iter.to_list l in - let subs = List.map get_lit t_subs in + let subs = List.map mk_lit t_subs in let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in SI.define_const si ~const:t_proxy ~rhs:t; SI.with_proof si (SI.P.define_term t_proxy t); @@ -305,13 +313,13 @@ module Make(A : ARG) : S with module A = A = struct t_subs subs; PA.add_clause (Lit.neg proxy :: subs) (A.lemma_bool_c "or-e" [t_proxy]); - proxy + Some proxy | B_imply (t_args, t_u) -> (* transform into [¬args \/ u] on the fly *) let t_args = Iter.to_list t_args in - let args = List.map (fun t -> Lit.neg (get_lit t)) t_args in - let u = get_lit t_u in + let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in + let u = mk_lit t_u in let subs = u :: args in (* now the or-encoding *) @@ -327,19 +335,22 @@ module Make(A : ARG) : S with module A = A = struct (t_u::t_args) subs; PA.add_clause (Lit.neg proxy :: subs) (A.lemma_bool_c "imp-e" [t_proxy]); - proxy + Some proxy - | B_ite _ | B_eq _ | B_neq _ -> PA.mk_lit t - | B_equiv (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:false a b - | B_xor (a,b) -> equiv_ si ~get_lit ~for_t:t ~is_xor:true a b - | B_atom u -> PA.mk_lit u + | B_ite _ | B_eq _ | B_neq _ -> None + | B_equiv (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:false a b) + | B_xor (a,b) -> Some (equiv_ si ~for_t:t ~is_xor:true a b) + | B_atom _ -> None in - let lit = get_lit t in - let u = Lit.term lit in - (* put sign back as a "not" *) - let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in - if T.equal u t then None else Some u + begin match get_lit_opt t with + | None -> None + | Some lit -> + let u = Lit.term lit in + (* put sign back as a "not" *) + let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in + if T.equal u t then None else Some u + end (* check if new terms were added to the congruence closure, that can be turned into clauses *)