mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix missing propagation on final

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-24 16:29:25 +01:00
parent 33ffd464cf
commit 24baf56e27
2 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_model.cpp
View file

@ -335,8 +335,8 @@ namespace euf {
continue; continue;
if (!tt && !mdl.is_true(e)) if (!tt && !mdl.is_true(e))
continue; continue;
IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
CTRACE("euf", first, display_validation_failure(tout, mdl, n);); CTRACE("euf", first, display_validation_failure(tout, mdl, n););
IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
(void)first; (void)first;
first = false; first = false;
exit(1); exit(1);

13
src/sat/smt/q_ematch.cpp
View file

@ -341,7 +341,6 @@ namespace q {
return false; return false;
if (ctx.s().inconsistent()) if (ctx.s().inconsistent())
return true; return true;
TRACE("q", c.display(ctx, tout) << "\n";);
unsigned idx = UINT_MAX; unsigned idx = UINT_MAX;
m_evidence.reset(); m_evidence.reset();
lbool ev = m_eval(binding, c, idx, m_evidence); lbool ev = m_eval(binding, c, idx, m_evidence);
@ -614,12 +613,13 @@ namespace q {
bool ematch::propagate(bool flush) { bool ematch::propagate(bool flush) {
m_mam->propagate(); m_mam->propagate();
bool propagated = flush_prop_queue(); bool propagated = flush_prop_queue();
if (m_qhead >= m_clause_queue.size()) if (!flush && m_qhead >= m_clause_queue.size())
return m_inst_queue.propagate() || propagated; return m_inst_queue.propagate() || propagated;
ctx.push(value_trail<unsigned>(m_qhead)); ctx.push(value_trail<unsigned>(m_qhead));
ptr_buffer<binding> to_remove; ptr_buffer<binding> to_remove;
for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) { unsigned qhead = flush ? 0 : m_qhead;
unsigned idx = m_clause_queue[m_qhead]; for (; qhead < m_clause_queue.size() && m.inc(); ++qhead) {
unsigned idx = m_clause_queue[qhead];
clause& c = *m_clauses[idx]; clause& c = *m_clauses[idx];
binding* b = c.m_bindings; binding* b = c.m_bindings;
if (!b) if (!b)
@ -645,6 +645,7 @@ namespace q {
} }
to_remove.reset(); to_remove.reset();
} }
m_qhead = std::max(m_qhead, qhead);
m_clause_in_queue.reset(); m_clause_in_queue.reset();
m_node_in_queue.reset(); m_node_in_queue.reset();
m_in_queue_set = true; m_in_queue_set = true;
@ -662,7 +663,7 @@ namespace q {
if (propagate(false)) if (propagate(false))
return true; return true;
for (unsigned i = 0; i < m_clauses.size(); ++i) for (unsigned i = 0; i < m_clauses.size(); ++i)
if (m_clauses[i]->m_bindings) if (m_clauses[i]->m_bindings)
insert_clause_in_queue(i); insert_clause_in_queue(i);
if (propagate(true)) if (propagate(true))
return true; return true;
@ -671,7 +672,7 @@ namespace q {
for (unsigned i = 0; i < m_clauses.size(); ++i) for (unsigned i = 0; i < m_clauses.size(); ++i)
if (m_clauses[i]->m_bindings) { if (m_clauses[i]->m_bindings) {
IF_VERBOSE(0, verbose_stream() << "missed propagation " << i << "\n"); IF_VERBOSE(0, verbose_stream() << "missed propagation " << i << "\n");
TRACE("q", display(tout)); TRACE("q", display(tout << "missed propagation\n"));
break; break;
} }