unit propagate with fingerprints

src/ast/euf/euf_egraph.cpp

@@ -681,6 +681,7 @@ namespace euf {
     void egraph::begin_explain() {
         SASSERT(m_todo.empty());
         m_uses_congruence = false;
+        DEBUG_CODE(for (enode* n : m_nodes) SASSERT(!n->is_marked1()););
     }
 
     void egraph::end_explain() {

src/sat/smt/array_axioms.cpp

@@ -621,8 +621,7 @@ namespace array {
                 continue;            
             // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529            
             if (ctx.is_shared(r) || is_shared_arg(r)) 
-                roots.push_back(r->get_th_var(get_id()));
+                roots.push_back(r->get_th_var(get_id()));           
-            
             r->mark1();
             to_unmark.push_back(r);            
         }

src/sat/smt/q_ematch.cpp

@@ -218,11 +218,17 @@ namespace q {
         }
     };
 
-    binding* ematch::alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top) {
+
-        unsigned sz = sizeof(binding) + sizeof(euf::enode* const*)*n;
+    binding* ematch::alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
+        unsigned n = c.num_decls();
+        unsigned sz = sizeof(binding) + sizeof(euf::enode* const*) * n;
         void* mem = ctx.get_region().allocate(sz);
-        return new (mem) binding(pat, max_generation, min_top, max_top);
+        binding* b = new (mem) binding(pat, max_generation, min_top, max_top);
-    }  
+        b->init(b);
+        for (unsigned i = 0; i < n; ++i)
+            b->m_nodes[i] = _binding[i];
+        return b;
+    }
 
     euf::enode* const* ematch::alloc_binding(clause& c, euf::enode* const* _binding) {
         unsigned sz = sizeof(euf::enode* const*) * c.num_decls();
@@ -232,24 +238,22 @@ namespace q {
         return binding;
     }
 
-    void ematch::add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
-        unsigned n = c.num_decls();
-        binding* b = alloc_binding(n, pat, max_generation, min_top, max_top);
-        b->init(b);
-        for (unsigned i = 0; i < n; ++i)
-            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) {
         TRACE("q", tout << "on-binding " << mk_pp(q, m) << "\n";);
         unsigned idx = m_q2clauses[q];
         clause& c = *m_clauses[idx];
         bool new_propagation = false;
-        if (!propagate(false, _binding, max_generation, c, new_propagation)) 
+        binding* b = alloc_binding(c, pat, _binding, max_generation, min_gen, max_gen);
-            add_binding(c, pat, _binding, max_generation, min_gen, max_gen);
+        fingerprint* f = add_fingerprint(c, *b, max_generation);
+        if (!f)
+            return;
+
+        if (propagate(false, _binding, max_generation, c, new_propagation))
+            return;
+
+        binding::push_to_front(c.m_bindings, b);
+        ctx.push(remove_binding(ctx, c, b));
+        ++m_stats.m_num_delayed_bindings;
     }
 
     bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
@@ -547,6 +551,10 @@ namespace q {
     }
 
 
+    bool ematch::unit_propagate() {
+        return ctx.get_config().m_ematching && propagate(false);
+    }
+
     bool ematch::propagate(bool flush) {
         m_mam->propagate();
         bool propagated = flush_prop_queue();

src/sat/smt/q_ematch.h

@@ -90,10 +90,10 @@ namespace q {
         unsigned_vector               m_clause_queue;
         euf::enode_pair_vector        m_evidence;
 
-        binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top);
         euf::enode* const* alloc_binding(clause& c, euf::enode* const* _binding);
+        binding* alloc_binding(clause& c, app* pat, euf::enode* const* _bidning, unsigned max_generation, unsigned min_top, unsigned max_top);
         void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
-
+        
         sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b);
 
         void ensure_ground_enodes(expr* e);
@@ -121,13 +121,15 @@ namespace q {
         bool flush_prop_queue();
         void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
 
+        bool propagate(bool flush);
+
     public:
         
         ematch(euf::solver& ctx, solver& s);
             
         bool operator()();
 
-        bool propagate(bool flush);
+        bool unit_propagate();        
 
         // void init_search();
 

src/sat/smt/q_mam.cpp

@@ -1987,33 +1987,36 @@ namespace q {
                 m_backtrack_stack.resize(t->get_num_choices());
         }
 
+        struct scoped_unmark {
+            code_tree* t;
+            scoped_unmark(code_tree* t) : t(t) {}
+            ~scoped_unmark() {
+                for (enode* app : t->get_candidates()) 
+                    if (app->is_marked1())
+                        app->unmark1();                
+            }
+        };
+
         void execute(code_tree * t) {
             TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
             init(t);
-            if (t->filter_candidates()) {
+            if (t->filter_candidates()) {                
-                for (unsigned i = 0; i < t->get_candidates().size(); ++i) {
+                scoped_unmark _unmark(t);
+                for (unsigned i = 0; i < t->get_candidates().size() && !ctx.resource_limits_exceeded(); ++i) {
                     enode* app = t->get_candidates()[i];
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
                     if (!app->is_marked1() && app->is_cgr()) {
-                        if (ctx.resource_limits_exceeded() || !execute_core(t, app))
+                        execute_core(t, app);                       
-                            return;
                         app->mark1();
                     }
                 }
-                for (enode* app : t->get_candidates()) {
-                    if (app->is_marked1())
-                        app->unmark1();
-                }
             }
             else {
-                for (unsigned i = 0; i < t->get_candidates().size(); ++i) {
+                for (unsigned i = 0; i < t->get_candidates().size() && !ctx.resource_limits_exceeded(); ++i) {
                     enode* app = t->get_candidates()[i];
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_expr(), m) << "\n";);
-                    if (app->is_cgr()) {
+                    if (app->is_cgr()) 
-                        TRACE("trigger_bug", tout << "is_cgr\n";);
+                        execute_core(t, app);                                              
-                        if (ctx.resource_limits_exceeded() || !execute_core(t, app))
-                            return;
-                    }
                 }
             }
         }

src/sat/smt/q_solver.cpp

@@ -100,7 +100,7 @@ namespace q {
     }
 
     bool solver::unit_propagate() {
-        return ctx.get_config().m_ematching && m_ematch.propagate(false);
+        return m_ematch.unit_propagate();
     }
 
     euf::theory_var solver::mk_var(euf::enode* n) {