Merged bit-vector and uf proof branch.

3 files changed, 20 insertions, 10 deletions

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index bab71d8b2..0736ec052 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -64,8 +64,9 @@ public:
     return d_nextVar++;
   }
 
-  void addClause(SatClause& c, bool lemma, uint64_t) {
+  ClauseId addClause(SatClause& c, bool lemma) {
     d_addClauseCalled = true;
+    return ClauseIdUndef;
   }
 
   void reset() {
@@ -117,6 +118,8 @@ public:
     return true;
   }
 
+  bool ok() const { return true; }
+
 };/* class FakeSatSolver */
 
 class CnfStreamWhite : public CxxTest::TestSuite {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 2ecb4e225..62ed96900 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -49,7 +49,7 @@ using namespace CVC4::smt;
 using namespace std;
 
 class FakeOutputChannel : public OutputChannel {
-  void conflict(TNode n) throw(AssertionException) {
+  void conflict(TNode n, Proof* pf = NULL) throw(AssertionException) {
     Unimplemented();
   }
   bool propagate(TNode n) throw(AssertionException) {
@@ -58,7 +58,10 @@ class FakeOutputChannel : public OutputChannel {
   void propagateAsDecision(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  LemmaStatus lemma(TNode n, bool removable, bool preprocess, bool sendAtoms) throw(AssertionException) {
+  LemmaStatus lemma(TNode n, ProofRule rule,
+                    bool removable,
+                    bool preprocess,
+                    bool sendAtoms) throw(AssertionException) {
     Unimplemented();
   }
   void requirePhase(TNode, bool) throw(AssertionException) {
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 429e72fc6..daa98855a 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -15,16 +15,17 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+#include <vector>
 
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
+// taking: Add include for Proof*.
+#include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "context/context.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
 
-#include <vector>
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -56,7 +57,7 @@ public:
       throw(Interrupted, UnsafeInterruptException, AssertionException)
   {}
 
-  void conflict(TNode n)
+  void conflict(TNode n, Proof* pf = NULL)
     throw(AssertionException) {
     push(CONFLICT, n);
   }
@@ -72,7 +73,10 @@ public:
     // ignore
   }
 
-  LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false, bool sendAtoms = false)
+  LemmaStatus lemma(TNode n, ProofRule rule,
+                    bool removable = false,
+                    bool preprocess = false,
+                    bool sendAtoms = false)
     throw(AssertionException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
@@ -305,7 +309,7 @@ public:
 
   void testOutputChannel() {
     Node n = atom0.orNode(atom1);
-    d_outputChannel.lemma(n);
+    d_outputChannel.lemma(n, RULE_INVALID);
     d_outputChannel.split(atom0);
     Node s = atom0.orNode(atom0.notNode());
     TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);