From e3484f9960bb40518e7db4869f5722ec1cf0b4ed Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 6 Dec 2011 02:01:06 +0000 Subject: [PATCH] LemmaStatus changes, as agreed to during 12/2 meeting. --- src/theory/output_channel.h | 39 ++++++++++++++++++++++---- src/theory/theory_engine.h | 20 +++++++------ src/theory/theory_test_utils.h | 4 +-- test/unit/theory/theory_black.h | 4 +-- test/unit/theory/theory_engine_white.h | 2 +- 5 files changed, 51 insertions(+), 18 deletions(-) diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index aaad25bd5..0e47cd7f2 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -27,6 +27,33 @@ namespace CVC4 { namespace theory { +/** + * A LemmaStatus, returned from OutputChannel::lemma(), provides information + * about the lemma added. In particular, it contains the T-rewritten lemma + * for inspection and the user-level at which the lemma will reside. + */ +class LemmaStatus { + Node d_rewrittenLemma; + unsigned d_level; + +public: + LemmaStatus(TNode rewrittenLemma, unsigned level) : + d_rewrittenLemma(rewrittenLemma), + d_level(level) { + } + + /** Get the T-rewritten form of the lemma. */ + TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; } + + /** + * Get the user-level at which the lemma resides. After this user level + * is popped, the lemma is un-asserted from the SAT layer. This level + * will be 0 if the lemma didn't reach the SAT layer at all. + */ + unsigned getLevel() const throw() { return d_level; } + +};/* class LemmaStatus */ + /** * Generic "theory output channel" interface. */ @@ -85,10 +112,11 @@ public: * * @param n - a theory lemma valid at decision level 0 * @param removable - whether the lemma can be removed at any point - * @return the user level at which the lemma resides; it will be - * removed when this user level pops + * @return the "status" of the lemma, including user level at which + * the lemma resides; the lemma will be removed when this user level pops */ - virtual unsigned lemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) = 0; + virtual LemmaStatus lemma(TNode n, bool removable = false) + throw(TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to @@ -96,8 +124,9 @@ public: * * @param n - a theory atom; must be of Boolean type */ - void split(TNode n) throw(TypeCheckingExceptionPrivate, AssertionException) { - lemma(n.orNode(n.notNode())); + LemmaStatus split(TNode n) + throw(TypeCheckingExceptionPrivate, AssertionException) { + return lemma(n.orNode(n.notNode())); } /** diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0d9500996..387468b14 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -202,7 +202,7 @@ class TheoryEngine { d_engine->propagate(literal, d_theory); } - unsigned lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; @@ -356,21 +356,23 @@ class TheoryEngine { bool d_outputChannelUsed; /** - * Adds a new lemma + * Adds a new lemma, returning its status. */ - unsigned lemma(TNode node, bool negated, bool removable) { - + theory::LemmaStatus lemma(TNode node, bool negated, bool removable) { if(Dump.isOn("t-lemmas")) { - Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") + << std::endl << QueryCommand(node.toExpr()) << std::endl; } // Remove the ITEs and assert to prop engine std::vector additionalLemmas; additionalLemmas.push_back(node); RemoveITE::run(additionalLemmas); - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable); + additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { - d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable); + additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); + d_propEngine->assertLemma(additionalLemmas[i], false, removable); } // Mark that we added some lemmas @@ -378,7 +380,9 @@ class TheoryEngine { // Lemma analysis isn't online yet; this lemma may only live for this // user level. - return d_userContext->getLevel(); + Node finalForm = + negated ? additionalLemmas[0].notNode() : additionalLemmas[0]; + return theory::LemmaStatus(finalForm, d_userContext->getLevel()); } public: diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 49ed16788..96bd02b5a 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -81,9 +81,9 @@ public: push(PROPAGATE, n); } - unsigned lemma(TNode n, bool removable) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); - return 0; + return LemmaStatus(Node::null(), 0); } void setIncomplete() throw(AssertionException) {} diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index e5577d2c2..60e090d16 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -62,10 +62,10 @@ public: push(PROPAGATE, n); } - unsigned lemma(TNode n, bool removable) + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); - return 0; + return LemmaStatus(Node::null(), 0); } void setIncomplete() diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index fbac6f4ee..2363e4906 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -54,7 +54,7 @@ class FakeOutputChannel : public OutputChannel { void propagate(TNode n) throw(AssertionException) { Unimplemented(); } - unsigned lemma(TNode n, bool removable) throw(AssertionException) { + LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) { Unimplemented(); } void explanation(TNode n) throw(AssertionException) { -- 2.30.2