count lazy bindings

Z3Prover · Sep 28, 2021 · 2e176a0 · 2e176a0
1 parent 3abecc3
commit 2e176a0
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
@@ -240,6 +240,7 @@ namespace q {
             b->m_nodes[i] = _binding[i];        
         binding::push_to_front(c.m_bindings, 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) {
@@ -612,6 +613,7 @@ namespace q {
         st.update("q redundant", m_stats.m_num_redundant);
         st.update("q units",     m_stats.m_num_propagations);
         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 {

diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
@@ -41,6 +41,7 @@ namespace q {
             unsigned m_num_propagations;
             unsigned m_num_conflicts;
             unsigned m_num_redundant;
+            unsigned m_num_delayed_bindings;
 
             stats() { reset(); }