mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix #3214, suppress assertion as it triggers in benign cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-09 08:07:41 +01:00
parent da27edfd9e
commit ee1f7edfa0
1 changed files with 31 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

44
src/nlsat/nlsat_solver.cpp
View file

@ -335,12 +335,13 @@ namespace nlsat {
}
void inc_ref(bool_var b) {
TRACE("ref", tout << "inc: " << b << "\n";);
if (b == null_bool_var)
return;
if (m_atoms[b] == nullptr)
atom * a = m_atoms[b];
if (a == nullptr)
return;
m_atoms[b]->inc_ref();
TRACE("ref", display(tout << "inc: " << b << " " << a->ref_count() << " ", *a) << "\n";);
a->inc_ref();
}
void inc_ref(literal l) {
@ -348,7 +349,6 @@ namespace nlsat {
}
void dec_ref(bool_var b) {
TRACE("ref", tout << "dec: " << b << "\n";);
if (b == null_bool_var)
return;
atom * a = m_atoms[b];
@ -356,6 +356,7 @@ namespace nlsat {
return;
SASSERT(a->ref_count() > 0);
a->dec_ref();
TRACE("ref", display(tout << "dec: " << b << " " << a->ref_count() << " ", *a) << "\n";);
if (a->ref_count() == 0)
del(a);
}
@ -546,7 +547,9 @@ namespace nlsat {
}
void del(ineq_atom * a) {
SASSERT(a->ref_count() == 0);
CTRACE("nlsat_solver", a->ref_count() > 0, display(tout, *a) << "\n";);
// this triggers in too many benign cases:
// SASSERT(a->ref_count() == 0);
m_ineq_atoms.erase(a);
del(a->bvar());
unsigned sz = a->size();
@ -566,7 +569,7 @@ namespace nlsat {
void del(atom * a) {
if (a == nullptr)
return;
TRACE("nlsat_verbose", display(tout << "del: b" << a->m_bool_var << " ", *a) << "\n";);
TRACE("nlsat_verbose", display(tout << "del: b" << a->m_bool_var << " " << a->ref_count() << " ", *a) << "\n";);
if (a->is_ineq_atom())
del(to_ineq_atom(a));
else
@ -790,6 +793,26 @@ namespace nlsat {
}
};
class scoped_bool_vars {
imp& s;
svector<bool_var> vec;
public:
scoped_bool_vars(imp& s):s(s) {}
~scoped_bool_vars() {
std::cout << "scoped del: " << vec << "\n";
for (bool_var v : vec) {
s.dec_ref(v);
}
}
void push_back(bool_var v) {
s.inc_ref(v);
vec.push_back(v);
}
bool_var const* begin() const { return vec.begin(); }
bool_var const* end() const { return vec.end(); }
bool_var operator[](bool_var v) const { return vec[v]; }
};
void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) {
TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n";
display(tout););
@ -803,13 +826,12 @@ namespace nlsat {
checker.m_inline_vars = false;
// need to translate Boolean variables and literals
svector<bool_var> tr;
scoped_bool_vars tr(checker);
for (var x = 0; x < m_is_int.size(); ++x) {
checker.register_var(x, m_is_int[x]);
}
bool_var bv = 0;
tr.push_back(bv);
checker.inc_ref(bv);
for (bool_var b = 1; b < m_atoms.size(); ++b) {
atom* a = m_atoms[b];
if (a == nullptr) {
@ -837,7 +859,6 @@ namespace nlsat {
else {
UNREACHABLE();
}
checker.inc_ref(bv);
tr.push_back(bv);
}
if (!is_valid) {
@ -889,9 +910,6 @@ namespace nlsat {
}
UNREACHABLE();
}
for (bool_var b : tr) {
checker.dec_ref(b);
}
}
void log_lemma(std::ostream& out, clause const& cls) {
@ -1965,7 +1983,7 @@ namespace nlsat {
resolve_clause(null_bool_var, *conflict_clause);
unsigned top = m_trail.size();
unsigned top = m_trail.size();
bool found_decision;
while (true) {
found_decision = false;