Fixing compilation of unit tests. These problems were due to splitLemma() being pure...

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 237b09bc11fc0cb2bcea7d18caccb03bb32b65e2..e4921b163d3abe2cf6533311ca913cc5e243781d 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -107,6 +107,11 @@ public:
     d_callHistory.clear();
   }
 
+  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){
+    push(LEMMA, n);
+    return LemmaStatus(Node::null(), 0);
+  }
+
   Node getIthNode(int i) {
     Node tmp = (d_callHistory[i]).second;
     return tmp;

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index c9bea179544eed74eb984a0ff2ef1b5fb1a37065..4035b85daa75eefa3395c40c639edd48f98967ed 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -76,6 +76,9 @@ class FakeOutputChannel : public OutputChannel {
   void handleUserAttribute( const char* attr, Theory* t ){
     Unimplemented();
   }
+  LemmaStatus splitLemma(TNode n, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException){
+    Unimplemented();
+  }
 };/* class FakeOutputChannel */
 
 template<TheoryId theory>

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 126f57060a18239e1a0fda0f09abdb512fea0a9e..d9df2912b4c4ea1869e80bbd4767422a08ed20a8 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -76,6 +76,11 @@ public:
     return LemmaStatus(Node::null(), 0);
   }
 
+  LemmaStatus splitLemma(TNode n, bool removable) throw (TypeCheckingExceptionPrivate, AssertionException){
+    push(LEMMA, n);
+    return LemmaStatus(Node::null(), 0);
+  }
+
   void requirePhase(TNode, bool)
     throw(Interrupted, AssertionException) {
     Unreachable();