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

fix #3126

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-08 17:58:59 +01:00
parent 611c14844d
commit 170a534681
2 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/nlsat/nlsat_solver.cpp
View file

@ -580,6 +580,7 @@ namespace nlsat {
} }
} }
ineq_atom* mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool& is_new) { ineq_atom* mk_ineq_atom(atom::kind k, unsigned sz, poly * const * ps, bool const * is_even, bool& is_new) {
SASSERT(sz >= 1); SASSERT(sz >= 1);
SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ); SASSERT(k == atom::LT || k == atom::GT || k == atom::EQ);
@ -602,10 +603,10 @@ namespace nlsat {
if (sign < 0) if (sign < 0)
k = atom::flip(k); k = atom::flip(k);
ineq_atom * tmp_atom = new (mem) ineq_atom(k, sz, uniq_ps.c_ptr(), is_even, max); ineq_atom * tmp_atom = new (mem) ineq_atom(k, sz, uniq_ps.c_ptr(), is_even, max);
TRACE("nlsat_table_bug", ineq_atom::hash_proc h;
tout << "mk_ineq_atom hash: " << h(tmp_atom) << "\n"; display(tout, *tmp_atom, m_display_var); tout << "\n";);
ineq_atom * atom = m_ineq_atoms.insert_if_not_there(tmp_atom); ineq_atom * atom = m_ineq_atoms.insert_if_not_there(tmp_atom);
CTRACE("nlsat_table_bug", atom->max_var() != max, display(tout, *atom, m_display_var); tout << "\n";); CTRACE("nlsat_table_bug", tmp_atom != atom, ineq_atom::hash_proc h;
tout << "mk_ineq_atom hash: " << h(tmp_atom) << "\n"; display(tout, *tmp_atom, m_display_var) << "\n";);
CTRACE("nlsat_table_bug", atom->max_var() != max, display(tout << "nonmax: ", *atom, m_display_var) << "\n";);
SASSERT(atom->max_var() == max); SASSERT(atom->max_var() == max);
is_new = (atom == tmp_atom); is_new = (atom == tmp_atom);
if (is_new) { if (is_new) {
@ -2675,12 +2676,13 @@ namespace nlsat {
bool is_sat = true; bool is_sat = true;
polynomial_ref pr(m_pm); polynomial_ref pr(m_pm);
polynomial_ref_vector ps(m_pm); polynomial_ref_vector ps(m_pm);
u_map<literal> b2l; u_map<literal> b2l;
scoped_literal_vector lits(m_solver);
svector<bool> even; svector<bool> even;
unsigned num_atoms = m_atoms.size(); unsigned num_atoms = m_atoms.size();
for (unsigned j = 0; j < num_atoms; ++j) { for (unsigned j = 0; j < num_atoms; ++j) {
atom* a = m_atoms[j]; atom* a = m_atoms[j];
if (a && a->is_ineq_atom()) { if (a && a->is_ineq_atom()) {
ineq_atom const& a1 = *to_ineq_atom(a); ineq_atom const& a1 = *to_ineq_atom(a);
unsigned sz = a1.size(); unsigned sz = a1.size();
@ -2708,16 +2710,13 @@ namespace nlsat {
} }
if (!change) continue; if (!change) continue;
literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr()); literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr());
lits.push_back(l);
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);
} }
} }
} }
is_sat = update_clauses(b2l); is_sat = update_clauses(b2l);
for (auto const& kv : b2l) {
dec_ref(kv.m_value);
}
return is_sat; return is_sat;
} }

5
src/qe/nlqsat.cpp
View file

@ -89,6 +89,10 @@ namespace qe {
m_t2x(m) m_t2x(m)
{} {}
~solver_state() {
reset();
}
void g2s(goal const& g) { void g2s(goal const& g) {
goal2nlsat gs; goal2nlsat gs;
gs(g, m_params, m_solver, m_a2b, m_t2x); gs(g, m_params, m_solver, m_a2b, m_t2x);
@ -231,6 +235,7 @@ namespace qe {
m_bound_bvars.reset(); m_bound_bvars.reset();
m_preds.reset(); m_preds.reset();
for (auto const& kv : m_bvar2level) { for (auto const& kv : m_bvar2level) {
m_solver.dec_ref(kv.m_key); m_solver.dec_ref(kv.m_key);
} }
m_rvar2level.reset(); m_rvar2level.reset();