From df5f7fe03fda041429548bcb39abb8916ca2e291 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Tue, 9 Nov 2010 21:57:06 +0000 Subject: Lemmas on demand work, push-pop, some cleanup. --- test/unit/prop/cnf_stream_black.h | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'test/unit/prop/cnf_stream_black.h') diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index cee8a6a64..7258e630d 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -30,7 +30,6 @@ #include "prop/prop_engine.h" #include "prop/sat.h" #include "smt/smt_engine.h" -#include "util/decision_engine.h" using namespace CVC4; using namespace CVC4::context; @@ -63,6 +62,17 @@ public: unsigned int addClauseCalled() { return d_addClauseCalled; } + + int getLevel() const { + return 0; + } + + void unregisterVar(SatLiteral lit) { + } + + void renewVar(SatLiteral lit, int level = -1) { + } + }; class CnfStreamBlack : public CxxTest::TestSuite { -- cgit v1.2.3