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

#5778

Browse source 
reprogram flush, mark clauses during reinit as non-redundant.
This commit is contained in:
Nikolaj Bjorner 2022-04-25 11:22:00 +01:00
parent 0b453a4af5
commit 489459a1f7
3 changed files with 40 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -614,7 +614,7 @@ namespace euf {
if (si.is_bool_op(e))
lit = literal(replay.m[e], false);
else
lit = si.internalize(e, true);
lit = si.internalize(e, false);
VERIFY(lit.var() == v);
if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
ptr_buffer<euf::enode> args;

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

@ -610,42 +610,51 @@ namespace q {
return ctx.get_config().m_ematching && propagate(false);
}
void ematch::propagate(clause& c, bool flush, bool& propagated) {
ptr_buffer<binding> to_remove;
binding* b = c.m_bindings;
if (!b)
return;
do {
if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated))
to_remove.push_back(b);
else if (flush) {
instantiate(*b);
to_remove.push_back(b);
propagated = true;
}
b = b->next();
}
while (b != c.m_bindings);
for (auto* b : to_remove) {
SASSERT(binding::contains(c.m_bindings, b));
binding::remove_from(c.m_bindings, b);
binding::detach(b);
ctx.push(insert_binding(ctx, c, b));
}
}
bool ematch::propagate(bool flush) {
m_mam->propagate();
bool propagated = flush_prop_queue();
if (!flush && m_qhead >= m_clause_queue.size())
return m_inst_queue.propagate() || propagated;
ctx.push(value_trail<unsigned>(m_qhead));
ptr_buffer<binding> to_remove;
unsigned qhead = flush ? 0 : m_qhead;
for (; qhead < m_clause_queue.size() && m.inc(); ++qhead) {
unsigned idx = m_clause_queue[qhead];
clause& c = *m_clauses[idx];
binding* b = c.m_bindings;
if (!b)
continue;
do {
if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated))
to_remove.push_back(b);
else if (flush) {
instantiate(*b);
to_remove.push_back(b);
propagated = true;
}
b = b->next();
}
while (b != c.m_bindings);
for (auto* b : to_remove) {
SASSERT(binding::contains(c.m_bindings, b));
binding::remove_from(c.m_bindings, b);
binding::detach(b);
ctx.push(insert_binding(ctx, c, b));
}
to_remove.reset();
if (flush) {
for (auto* c : m_clauses)
propagate(*c, flush, propagated);
}
else {
ctx.push(value_trail<unsigned>(m_qhead));
for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) {
unsigned idx = m_clause_queue[m_qhead];
clause& c = *m_clauses[idx];
propagate(c, flush, propagated);
}
}
m_qhead = std::max(m_qhead, qhead);
m_clause_in_queue.reset();
m_node_in_queue.reset();
m_in_queue_set = true;

1
src/sat/smt/q_ematch.h
View file

@ -121,6 +121,7 @@ namespace q {
void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
bool propagate(bool flush);
void propagate(clause& c, bool flush, bool& propagated);
expr_ref_vector m_new_defs;
proof_ref_vector m_new_proofs;