LemmaStatus changes, as agreed to during 12/2 meeting.

1 files changed, 34 insertions, 5 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()));
   }
 
   /**