mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 14:23:40 +00:00
Code Activity

fix #3185 - move handling of to_real within def conversion

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-09 10:04:31 +01:00 • committed by Lev Nachmanson
parent f636a481d3
commit 0f779c9c0d
1 changed files with 18 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/theory_lra.cpp
View file

@ -584,18 +584,27 @@ class theory_lra::imp {
coeffs[index].neg(); coeffs[index].neg();
terms[index] = n1; terms[index] = n1;
} }
else if (a.is_to_real(n, n1)) {
terms[index] = n1;
if (!ctx().e_internalized(n)) {
app* t = to_app(n);
internalize_args(t);
mk_enode(t);
theory_var v = mk_var(n);
theory_var w = mk_var(n1);
lpvar vj = register_theory_var_in_lar_solver(v);
lpvar wj = register_theory_var_in_lar_solver(w);
auto lu_constraints = lp().add_equality(vj, wj);
add_def_constraint(lu_constraints.first);
add_def_constraint(lu_constraints.second);
}
}
else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) { else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
bool is_first = !ctx().e_internalized(n); bool is_first = !ctx().e_internalized(n);
app* t = to_app(n); app* t = to_app(n);
internalize_args(t); internalize_args(t);
mk_enode(t); mk_enode(t);
theory_var v; theory_var v = mk_var(n);
if (a.is_to_real(n, n1)) {
v = mk_var(n1);
}
else {
v = mk_var(n);
}
coeffs[vars.size()] = coeffs[index]; coeffs[vars.size()] = coeffs[index];
vars.push_back(v); vars.push_back(v);
++index; ++index;
@ -606,9 +615,6 @@ class theory_lra::imp {
if (!ctx().relevancy()) if (!ctx().relevancy())
mk_to_int_axiom(t); mk_to_int_axiom(t);
} }
else if (a.is_to_real(n, n1)) {
// already handled
}
else if (a.is_idiv(n, n1, n2)) { else if (a.is_idiv(n, n1, n2)) {
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
m_idiv_terms.push_back(n); m_idiv_terms.push_back(n);
@ -760,7 +766,7 @@ class theory_lra::imp {
return th.is_attached_to_var(e); return th.is_attached_to_var(e);
} }
theory_var mk_var(expr* n, bool internalize = true) { theory_var mk_var(expr* n) {
if (!ctx().e_internalized(n)) { if (!ctx().e_internalized(n)) {
ctx().internalize(n, false); ctx().internalize(n, false);
} }
@ -922,7 +928,7 @@ class theory_lra::imp {
TRACE("arith", tout << expr_ref(term, m) << "\n";); TRACE("arith", tout << expr_ref(term, m) << "\n";);
if (ctx().e_internalized(term)) { if (ctx().e_internalized(term)) {
IF_VERBOSE(0, verbose_stream() << "repeated term\n";); IF_VERBOSE(0, verbose_stream() << "repeated term\n";);
return mk_var(term, false); return mk_var(term);
} }
linearize_term(term, st); linearize_term(term, st);
if (is_unit_var(st)) { if (is_unit_var(st)) {