change lemma generation behavior

don't store lemmas in a pending queue, instead generate them right away

doing with pending queue is tricky, needs rethinking to do it properly

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 5d3ec5fc5edf269ab402d71ec0d7df9fe05bfda2..592b4bc37fd870f1691b5644511f11df8df23f44 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -814,15 +814,19 @@ void TheorySetsPrivate::addToPending(Node n) {
       Assert(n.getKind() == kind::EQUAL);
       d_pendingDisequal.push(n);
     }
+    d_external.d_out->lemma(getLemma());
+    Assert(isComplete());
   }
 }
 
 bool TheorySetsPrivate::isComplete() {
-  while(!d_pending.empty() && present(d_pending.front())) {
-    Debug("sets-pending") << "[sets-pending] removing as already present: "
-                          << d_pending.front() << std::endl;
-    d_pending.pop();
-  }
+  // while(!d_pending.empty() &&
+  //       (d_pendingEverInserted.find(d_pending.front()) != d_pendingEverInserted.end()
+  //        || present(d_pending.front()) ) ) {
+  //   Debug("sets-pending") << "[sets-pending] removing as already present: "
+  //                         << d_pending.front() << std::endl;
+  //   d_pending.pop();
+  // }
   return d_pending.empty() && d_pendingDisequal.empty();
 }