From: Tim King <taking@cs.nyu.edu>
Date: Fri, 3 May 2013 20:32:11 +0000 (-0400)
Subject: Fixing compilation of unit tests. These problems were due to splitLemma() being pure... 
X-Git-Tag: cvc5-1.0.0~7287^2~157
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a490befefedfd40b7abab5080e84fb7c0540f86;p=cvc5.git

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

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 237b09bc1..e4921b163 100644
--- 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 c9bea1795..4035b85da 100644
--- 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 126f57060..d9df2912b 100644
--- 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();