#5336

src/sat/smt/q_clause.cpp

@@ -32,6 +32,12 @@ namespace q {
                 << mk_bounded_pp(rhs, m, 2);
     }
 
+    std::ostream& binding::display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const {
+        for (unsigned i = 0; i < num_nodes; ++i) 
+            out << ctx.bpp((*this)[i]) << " ";
+        return out;
+    }
+
     std::ostream& clause::display(euf::solver& ctx, std::ostream& out) const {
         out << "clause:\n";
         for (auto const& lit : m_lits)
@@ -39,9 +45,7 @@ namespace q {
         binding* b = m_bindings;
         if (b) {
             do {
-                for (unsigned i = 0; i < num_decls(); ++i)
-                    out << ctx.bpp((*b)[i]) << " ";
-                out << "\n";            
+                b->display(ctx, num_decls(), out) << " - " << b << "\n";
                 b = b->next();
             }
             while (b != m_bindings);

src/sat/smt/q_clause.h

@@ -49,6 +49,8 @@ namespace q {
         euf::enode* const* nodes() { return m_nodes; }
 
         euf::enode* operator[](unsigned i) const { return m_nodes[i]; }
+
+        std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const;
     };
 
     struct clause {

src/sat/smt/q_ematch.cpp

@@ -192,20 +192,26 @@ namespace q {
     }
 
     struct ematch::remove_binding : public trail {
+        euf::solver& ctx;
         clause& c;
         binding* b;
-        remove_binding(clause& c, binding* b): c(c), b(b) {}
-        void undo() override {
+        remove_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {}
+        void undo() override {            
+            SASSERT(binding::contains(c.m_bindings, b));
             binding::remove_from(c.m_bindings, b);
+            binding::detach(b);
         }        
     };
 
     struct ematch::insert_binding : public trail {
+        euf::solver& ctx;
         clause& c;
         binding* b;
-        insert_binding(clause& c, binding* b): c(c), b(b) {}
-        void undo() override {
+        insert_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {}
+        void undo() override {            
+            SASSERT(!c.m_bindings || c.m_bindings->invariant());
             binding::push_to_front(c.m_bindings, b);
+            SASSERT(!c.m_bindings || c.m_bindings->invariant());
         }
     };
 
@@ -230,7 +236,7 @@ namespace q {
         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(c, b));
+        ctx.push(remove_binding(ctx, c, b));
     }
 
     void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@@ -503,8 +509,10 @@ namespace q {
             while (b != c.m_bindings);
 
             for (auto* b : to_remove) {
+                SASSERT(binding::contains(c.m_bindings, b));
                 binding::remove_from(c.m_bindings, b);
-                ctx.push(insert_binding(c, b));
+                binding::detach(b);
+                ctx.push(insert_binding(ctx, c, b));
             }
             to_remove.reset();
         }

src/util/dlist.h

@@ -74,6 +74,10 @@ public:
         }
     }
 
+    static void detach(T* elem) {
+        elem->init(elem);
+    }
+
     bool invariant() const {
         auto* e = this;
         do {
@@ -84,6 +88,20 @@ public:
         while (e != this);
         return true;
     }
+
+
+    static bool contains(T* list, T* elem) {
+        if (!list)
+            return false;
+        T* first = list;
+        do {
+            if (list == elem)
+                return true;
+            list = list->m_next;
+        }         
+        while (list != first);
+        return false;
+    }
 };