diff options
author | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2016-01-26 16:04:26 -0800 |
commit | 42b665f2a00643c81b42932fab1441987628c5a5 (patch) | |
tree | aa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /test/unit | |
parent | 7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff) |
Merged bit-vector and uf proof branch.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 5 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 7 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 18 |
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); |