From e926fd162c6cee95d31044305e3b4df90b59f9fc Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 3 Jul 2014 18:37:51 -0400 Subject: [PATCH] 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 --- src/theory/sets/theory_sets_private.cpp | 14 +++++++++----- 1 file 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(); } -- 2.30.2