Merged bit-vector and uf proof branch.

1 files changed, 22 insertions, 4 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2491aef3a..d5c12457a 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -22,6 +22,7 @@
 #include "base/cvc4_assert.h"
 #include "smt/logic_exception.h"
 #include "theory/interrupted.h"
+#include "proof/proof_manager.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -99,8 +100,10 @@ public:
    * assigned false), or else a literal by itself (in the case of a
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
+   * @param pf - a proof of the conflict. This is only non-null if proofs
+   * are enabled. 
    */
-  virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
+  virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -115,16 +118,31 @@ public:
    * been detected.  (This requests a split.)
    *
    * @param n - a theory lemma valid at decision level 0
+   * @param rule - the proof rule for this lemma
    * @param removable - whether the lemma can be removed at any point
    * @param preprocess - whether to apply more aggressive preprocessing
    * @param sendAtoms - whether to ensure atoms are sent to the theory
    * @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 LemmaStatus lemma(TNode n, bool removable = false,
-                            bool preprocess = false, bool sendAtoms = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0;
+  virtual LemmaStatus lemma(TNode n, ProofRule rule,
+                            bool removable = false,
+                            bool preprocess = false,
+                            bool sendAtoms = false)
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
+
+  /**
+   * Variant of the lemma function that does not require providing a proof rule.
+   */
+  virtual LemmaStatus lemma(TNode n, 
+                            bool removable = false,
+                            bool preprocess = false,
+                            bool sendAtoms = false)
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+    return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms);
+  }
 
+  
   /**
    * Request a split on a new theory atom.  This is equivalent to
    * calling lemma({OR n (NOT n)}).