From 45893e92f14f8ae21242225f76b47c32d2d1c910 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 22 Feb 2021 14:01:55 -0500 Subject: [PATCH] fix: missing preprocessing in LRA; better theory combination --- src/arith/lra/sidekick_arith_lra.ml | 50 ++++++++++++++++++++++------- src/cc/Sidekick_cc.ml | 5 ++- src/th-data/Sidekick_th_data.ml | 6 +++- 3 files changed, 48 insertions(+), 13 deletions(-) diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index 51bbdd1e..341bd03d 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/src/arith/lra/sidekick_arith_lra.ml @@ -89,14 +89,17 @@ module Make(A : ARG) : S with module A = A = struct module Tag = struct type t = + | By_def | Lit of Lit.t | CC_eq of N.t * N.t let pp out = function + | By_def -> Fmt.string out "by-def" | Lit l -> Fmt.fprintf out "(@[lit %a@])" Lit.pp l | CC_eq (n1,n2) -> Fmt.fprintf out "(@[cc-eq@ %a@ %a@])" N.pp n1 N.pp n2 let to_lits si = function + | By_def -> [] | Lit l -> [l] | CC_eq (n1,n2) -> SI.CC.explain_eq (SI.cc si) n1 n2 @@ -196,10 +199,19 @@ module Make(A : ARG) : S with module A = A = struct let proxy = fresh_term self ~pre (A.ty_lra self.tst) in self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le; Log.debugf 50 - (fun k->k "(@[lra.encode-le@ %a@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); + (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy); - LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; - SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); + (* it's actually 0 *) + if LE_.Comb.is_empty le_comb then ( + Log.debug 50 "(lra.encode-le.is-trivially-0)"; + SimpSolver.add_constraint self.simplex + (SimpSolver.Constraint.leq proxy Q.zero) Tag.By_def; + SimpSolver.add_constraint self.simplex + (SimpSolver.Constraint.geq proxy Q.zero) Tag.By_def; + ) else ( + LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb; + SimpSolver.define self.simplex proxy (LE_.Comb.to_list le_comb); + ); proxy (* preprocess linear expressions away *) @@ -207,6 +219,12 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 50 (fun k->k "lra.preprocess %a" T.pp t); let tst = SI.tst 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); + ignore (SI.CC.add_term (SI.cc si) t : SI.CC.N.t); + in + match A.view_as_lra t with | LRA_pred ((Eq | Neq), t1, t2) -> (* the equality side. *) @@ -219,8 +237,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 u1 in - let lit_u2 = mk_lit u2 in + let lit_u1 = mk_lit (recurse u1) in + let lit_u2 = mk_lit (recurse 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]; @@ -239,6 +257,8 @@ module Make(A : ARG) : S with module A = A = struct | None, _ -> (* non trivial linexp, give it a fresh name in the simplex *) let proxy = var_encoding_comb self ~pre:"_le" le_comb in + declare_term_to_cc proxy; + let new_t = match pred with | Eq | Neq -> assert false (* unreachable *) @@ -254,6 +274,7 @@ module Make(A : ARG) : S with module A = A = struct | Some (coeff, v), pred -> (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *) let q = Q.div le_const coeff in + declare_term_to_cc v; let op = match pred with | Leq -> S_op.Leq @@ -266,6 +287,7 @@ module Make(A : ARG) : S with module A = A = struct let op = if Q.(coeff < zero) then S_op.neg_sign op else op in let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in + Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t); Some new_t end @@ -278,6 +300,8 @@ module Make(A : ARG) : S with module A = A = struct (* if there is no constant, define [proxy] as [proxy := le_comb] and return [proxy] *) let proxy = var_encoding_comb self ~pre:"_le" le_comb in + declare_term_to_cc proxy; + Some proxy ) else ( (* a bit more complicated: we cannot just define [proxy := le_comb] @@ -298,6 +322,9 @@ module Make(A : ARG) : S with module A = A = struct (fun k->k "(@[lra.encode-le.with-offset@ %a@ :var %a@ :diff-var %a@])" LE_.Comb.pp le_comb T.pp proxy T.pp proxy2); + declare_term_to_cc proxy; + declare_term_to_cc proxy2; + add_clause [ mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, Q.neg le_const))) ]; @@ -367,10 +394,10 @@ module Make(A : ARG) : S with module A = A = struct if n_th_comb > 0 then ( Log.debugf 5 (fun k->k "(@[LRA.needs-th-combination@ :n-lits %d@])" n_th_comb); + Log.debugf 50 + (fun k->k "(@[LRA.needs-th-combination@ :terms [@[%a@]]@])" + (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination)); ); - Log.debugf 50 - (fun k->k "(@[LRA.needs-th-combination@ :lits %a@])" - (Util.pp_iter @@ Fmt.within "`" "`" T.pp) (T.Tbl.keys self.needs_th_combination)); (* theory combination: for [t1,t2] terms in [self.needs_th_combination] that have same value, but are not provably equal, push @@ -397,12 +424,12 @@ module Make(A : ARG) : S with module A = A = struct Log.debugf 50 (fun k->k "(@[LRA.th-comb.check-pair[val=%a]@ %a@ %a@])" Q.pp_print _q T.pp t1 T.pp t2); + assert(SI.cc_mem_term si t1); + assert(SI.cc_mem_term si t2); (* if both [t1] and [t2] are relevant to the congruence closure, and are not equal in it yet, add [t1=t2] as the next decision to do *) - if SI.cc_mem_term si t1 && - SI.cc_mem_term si t2 && - not (SI.cc_are_equal si t1 t2) then ( + if not (SI.cc_are_equal si t1 t2) then ( Log.debug 50 "LRA.th-comb.must-decide-equal"; let t = A.mk_eq (SI.tst si) t1 t2 in let lit = SI.mk_lit si acts t in @@ -472,6 +499,7 @@ module Make(A : ARG) : S with module A = A = struct (* look for subterms of type Real, for they will need theory combination *) let on_subterm (self:state) _ (t:T.t) : unit = + Log.debugf 50 (fun k->k "lra: cc-on-subterm %a" T.pp t); if A.has_ty_real t && not (T.Tbl.mem self.needs_th_combination t) then ( Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t); diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml index 94683b2a..e806ce83 100644 --- a/src/cc/Sidekick_cc.ml +++ b/src/cc/Sidekick_cc.ml @@ -534,10 +534,13 @@ module Make (A: CC_ARG) begin let sub_r = find_ sub in let old_parents = sub_r.n_parents in + if Bag.is_empty old_parents then ( + (* first time it has parents: call watchers that this is a subterm *) + List.iter (fun f -> f sub u) self.on_is_subterm; + ); on_backtrack self (fun () -> sub_r.n_parents <- old_parents); sub_r.n_parents <- Bag.cons n sub_r.n_parents; end; - List.iter (fun f -> f sub u) self.on_is_subterm; sub in let[@inline] return x = Some x in diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 4fa87ed4..ddb21773 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -390,7 +390,11 @@ module Make(A : ARG) : S with module A = A = struct let pp_entry out (n,node) = Fmt.fprintf out "@[<1>@[graph_node[%a]@]@ := %a@]" N.pp n pp_node node in - Fmt.fprintf out "(@[graph@ %a@])" (Fmt.iter pp_entry) (N_tbl.to_iter g) + if N_tbl.length g = 0 then ( + Fmt.string out "(graph ΓΈ)" + ) else ( + Fmt.fprintf out "(@[graph@ %a@])" (Fmt.iter pp_entry) (N_tbl.to_iter g) + ) let mk_graph (self:t) cc : graph = let g: graph = N_tbl.create ~size:32 () in