mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3208

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-08 13:07:19 +01:00
parent 7452e55698
commit f0451b68f3
2 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/nlsat_evaluator.cpp
View file

@ -490,7 +490,7 @@ namespace nlsat {
interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) {
sign_table & table = m_sign_table_tmp; sign_table & table = m_sign_table_tmp;
table.reset(); table.reset();
TRACE("nsat_evaluator", m_solver.display(tout, a) << "\n";); TRACE("nsat_evaluator", m_solver.display(tout, *a) << "\n";);
unsigned num_ps = a->size(); unsigned num_ps = a->size();
var x = a->max_var(); var x = a->max_var();
for (unsigned i = 0; i < num_ps; i++) { for (unsigned i = 0; i < num_ps; i++) {

17
src/nlsat/nlsat_solver.cpp
View file

@ -2644,6 +2644,7 @@ namespace nlsat {
del_clause(c, m_clauses); del_clause(c, m_clauses);
if (!substitute_var(v, p, q)) if (!substitute_var(v, p, q))
return false; return false;
TRACE("nlsat", display(tout << "simplified\n"););
change = true; change = true;
break; break;
} }
@ -2686,21 +2687,29 @@ namespace nlsat {
ps.reset(); ps.reset();
even.reset(); even.reset();
bool change = false; bool change = false;
auto k = a1.get_kind();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
poly * po = a1.p(i); poly * po = a1.p(i);
m_pm.substitute(po, x, q, p, pr); m_pm.substitute(po, x, q, p, pr);
ps.push_back(pr);
even.push_back(a1.is_even(i));
change |= pr != po;
if (m_pm.is_zero(pr)) { if (m_pm.is_zero(pr)) {
ps.reset(); ps.reset();
even.reset(); even.reset();
change = true; change = true;
break; break;
} }
if (m_pm.is_const(pr)) {
if (!a1.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) {
k = atom::flip(k);
}
change = true;
continue;
}
ps.push_back(pr);
even.push_back(a1.is_even(i));
change |= pr != po;
} }
if (!change) continue; if (!change) continue;
literal l = mk_ineq_literal(a1.get_kind(), ps.size(), ps.c_ptr(), even.c_ptr()); literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr());
if (a1.m_bool_var != l.var()) { if (a1.m_bool_var != l.var()) {
b2l.insert(a1.m_bool_var, l); b2l.insert(a1.m_bool_var, l);
inc_ref(l); inc_ref(l);