diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-03 18:37:51 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-03 18:37:51 -0400 |
commit | e926fd162c6cee95d31044305e3b4df90b59f9fc (patch) | |
tree | 8dc282bb4887fc5ee04c9f5be1a742863c44ba2d | |
parent | a5df93270d53400687d64822a9f2a7e9412a55f5 (diff) |
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
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
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(); } |