From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 3 Jul 2014 22:37:51 +0000 (-0400)
Subject: change lemma generation behavior
X-Git-Tag: cvc5-1.0.0~6702
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e926fd162c6cee95d31044305e3b4df90b59f9fc;p=cvc5.git

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 5d3ec5fc5..592b4bc37 100644
--- 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();
 }