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

count lazy bindings

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-28 08:27:46 -07:00
parent 3abecc3428
commit 2e176a0e02
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -240,6 +240,7 @@ namespace q {
b->m_nodes[i] = _binding[i]; b->m_nodes[i] = _binding[i];
binding::push_to_front(c.m_bindings, b); binding::push_to_front(c.m_bindings, b);
ctx.push(remove_binding(ctx, c, b)); ctx.push(remove_binding(ctx, c, b));
++m_stats.m_num_delayed_bindings;
} }
void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) { void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@ -612,6 +613,7 @@ namespace q {
st.update("q redundant", m_stats.m_num_redundant); st.update("q redundant", m_stats.m_num_redundant);
st.update("q units", m_stats.m_num_propagations); st.update("q units", m_stats.m_num_propagations);
st.update("q conflicts", m_stats.m_num_conflicts); st.update("q conflicts", m_stats.m_num_conflicts);
st.update("q delayed bindings", m_stats.m_num_delayed_bindings);
} }
std::ostream& ematch::display(std::ostream& out) const { std::ostream& ematch::display(std::ostream& out) const {

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

@ -41,6 +41,7 @@ namespace q {
unsigned m_num_propagations; unsigned m_num_propagations;
unsigned m_num_conflicts; unsigned m_num_conflicts;
unsigned m_num_redundant; unsigned m_num_redundant;
unsigned m_num_delayed_bindings;
stats() { reset(); } stats() { reset(); }