From a7afce3af42f063b8c8272c932646e53cd4413c2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 16 Feb 2021 18:35:21 -0500 Subject: [PATCH] fix(lra): only do theory combination on terms known to the CC --- src/arith/lra/sidekick_arith_lra.ml | 9 ++++++--- src/arith/lra/simplex2.ml | 4 +++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index 989c8d6e..c8772cf5 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/src/arith/lra/sidekick_arith_lra.ml @@ -405,9 +405,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); - (* FIXME: we need these equalities to be considered - by the congruence closure *) - if not (SI.cc_are_equal si t1 t2) then ( + (* 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 ( 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 diff --git a/src/arith/lra/simplex2.ml b/src/arith/lra/simplex2.ml index 1c7ae836..1ddf1f37 100644 --- a/src/arith/lra/simplex2.ml +++ b/src/arith/lra/simplex2.ml @@ -378,9 +378,11 @@ module Make(Var: VAR) } let push_level self : unit = + Log.debug 10 "(simplex2.push-level)"; Backtrack_stack.push_level self.bound_stack let pop_levels self n : unit = + Log.debugf 10 (fun k->k "(simplex2.pop-levels %d)" n); Backtrack_stack.pop_levels self.bound_stack n ~f:(fun (var, kind, bnd) -> match kind with @@ -981,7 +983,7 @@ module Make(Var: VAR) V_map.add x.var v subst) V_map.empty in - Log.debugf 5 + Log.debugf 10 (fun k->k "(@[simplex2.model@ %a@])" Subst.pp subst); subst