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
@@ -28,6 +28,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.
  */
 class OutputChannel {
@@ -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<Node> 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) {