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

#5417 - delay propagation from callbacks from mam

Browse source 
mam assumes the egraph isn't updated during callbacks.
This commit is contained in:
Nikolaj Bjorner 2021-07-19 11:10:48 -07:00
parent 776f270b64
commit 3156ca5e77
2 changed files with 34 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -275,16 +275,34 @@ namespace q {
auto j_idx = mk_justification(idx, c, binding); auto j_idx = mk_justification(idx, c, binding);
if (ev == l_false) { if (is_owned)
propagate(ev == l_false, idx, j_idx);
else
m_prop_queue.push_back(prop(ev == l_false, idx, j_idx));
propagated = true;
return true;
}
void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) {
if (is_conflict) {
++m_stats.m_num_conflicts; ++m_stats.m_num_conflicts;
ctx.set_conflict(j_idx); ctx.set_conflict(j_idx);
} }
else { else {
++m_stats.m_num_propagations; ++m_stats.m_num_propagations;
auto lit = instantiate(c, binding, c[idx]); auto& j = justification::from_index(j_idx);
auto lit = instantiate(j.m_clause, j.m_binding, j.m_clause[idx]);
ctx.propagate(lit, j_idx); ctx.propagate(lit, j_idx);
} }
propagated = true; }
bool ematch::flush_prop_queue() {
if (m_prop_queue.empty())
return false;
for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
auto [is_conflict, idx, j_idx] = m_prop_queue[i];
propagate(is_conflict, idx, j_idx);
}
return true; return true;
} }
@ -508,7 +526,7 @@ namespace q {
bool ematch::propagate(bool flush) { bool ematch::propagate(bool flush) {
m_mam->propagate(); m_mam->propagate();
bool propagated = false; bool propagated = flush_prop_queue();
if (m_qhead >= m_clause_queue.size()) if (m_qhead >= m_clause_queue.size())
return m_inst_queue.propagate(); return m_inst_queue.propagate();
ctx.push(value_trail<unsigned>(m_qhead)); ctx.push(value_trail<unsigned>(m_qhead));

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

@ -49,6 +49,13 @@ namespace q {
} }
}; };
struct prop {
bool is_conflict;
unsigned idx;
sat::ext_justification_idx j;
prop(bool is_conflict, unsigned idx, sat::ext_justification_idx j) : is_conflict(is_conflict), idx(idx), j(j) {}
};
struct remove_binding; struct remove_binding;
struct insert_binding; struct insert_binding;
struct pop_clause; struct pop_clause;
@ -65,6 +72,7 @@ namespace q {
scoped_ptr<binding> m_tmp_binding; scoped_ptr<binding> m_tmp_binding;
unsigned m_tmp_binding_capacity = 0; unsigned m_tmp_binding_capacity = 0;
queue m_inst_queue; queue m_inst_queue;
svector<prop> m_prop_queue;
pattern_inference_rw m_infer_patterns; pattern_inference_rw m_infer_patterns;
scoped_ptr<q::mam> m_mam, m_lazy_mam; scoped_ptr<q::mam> m_mam, m_lazy_mam;
ptr_vector<clause> m_clauses; ptr_vector<clause> m_clauses;
@ -108,6 +116,9 @@ namespace q {
fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation); fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
void set_tmp_binding(fingerprint& fp); void set_tmp_binding(fingerprint& fp);
bool flush_prop_queue();
void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
public: public:
ematch(euf::solver& ctx, solver& s); ematch(euf::solver& ctx, solver& s);