simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 19:25:36 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lra): only do theory combination on terms known to the CC

Browse source
This commit is contained in:
Simon Cruanes 2021-02-16 18:35:21 -05:00
parent 0e5e40f145
commit a7afce3af4
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/arith/lra/sidekick_arith_lra.ml
View file

@ -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

4
src/arith/lra/simplex2.ml
View file

@ -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