diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-03 16:32:11 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-03 16:32:11 -0400 |
commit | 9a490befefedfd40b7abab5080e84fb7c0540f86 (patch) | |
tree | d7d73eadd61af32c9cdc08a461198edbc5e38d90 | |
parent | 4c20ab57d70c4812d75af037e95c371c65418333 (diff) |
Fixing compilation of unit tests. These problems were due to splitLemma() being pure virtual.
-rw-r--r-- | src/theory/theory_test_utils.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 3 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 5 |
3 files changed, 13 insertions, 0 deletions
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(); |