summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/prop/cnf_stream_black.h293
-rw-r--r--test/unit/theory/theory_arith_white.h7
-rw-r--r--test/unit/theory/theory_black.h13
-rw-r--r--test/unit/theory/theory_engine_white.h13
4 files changed, 170 insertions, 156 deletions
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index c9a2196a5..62117d4c1 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -99,154 +99,159 @@ class CnfStreamBlack : public CxxTest::TestSuite {
/** The context */
Context* d_context;
+ /** The user context */
+ UserContext* d_userContext;
+
/** The node manager */
NodeManager* d_nodeManager;
-void setUp() {
- d_context = new Context;
- d_nodeManager = new NodeManager(d_context, NULL);
- NodeManagerScope nms(d_nodeManager);
- d_satSolver = new FakeSatSolver;
- d_theoryEngine = new TheoryEngine(d_context);
- d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
- d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
- d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
- theory::Registrar registrar(d_theoryEngine);
- d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
-}
-
-void tearDown() {
- NodeManagerScope nms(d_nodeManager);
- delete d_cnfStream;
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
- delete d_satSolver;
- delete d_nodeManager;
- delete d_context;
-}
+ void setUp() {
+ d_context = new Context();
+ d_userContext = new UserContext();
+ d_nodeManager = new NodeManager(d_context, NULL);
+ NodeManagerScope nms(d_nodeManager);
+ d_satSolver = new FakeSatSolver();
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+ d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
+ d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
+ d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
+ theory::Registrar registrar(d_theoryEngine);
+ d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
+ }
+
+ void tearDown() {
+ NodeManagerScope nms(d_nodeManager);
+ delete d_cnfStream;
+ d_theoryEngine->shutdown();
+ delete d_theoryEngine;
+ delete d_satSolver;
+ delete d_nodeManager;
+ delete d_userContext;
+ delete d_context;
+ }
public:
-/* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
- * deep structure of the CNF conversion. Firstly, we just want to make sure
- * that the conversion doesn't choke on any boolean Exprs. We'll also check
- * that addClause got called. We won't check that it gets called a particular
- * number of times, or with what.
- */
-
-void testAnd() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testComplexExpr() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(
- kind::IMPLIES,
- d_nodeManager->mkNode(kind::AND, a, b),
- d_nodeManager->mkNode(
- kind::IFF,
- d_nodeManager->mkNode(kind::OR, c, d),
- d_nodeManager->mkNode(
- kind::NOT,
- d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testFalse() {
- NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testIff() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IFF, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testImplies() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-// ITEs should be removed before going to CNF
-//void testIte() {
-// NodeManagerScope nms(d_nodeManager);
-// d_cnfStream->convertAndAssert(
-// d_nodeManager->mkNode(
-// kind::EQUAL,
-// d_nodeManager->mkNode(
-// kind::ITE,
-// d_nodeManager->mkVar(d_nodeManager->booleanType()),
-// d_nodeManager->mkVar(d_nodeManager->integerType()),
-// d_nodeManager->mkVar(d_nodeManager->integerType())
-// ),
-// d_nodeManager->mkVar(d_nodeManager->integerType())
-// ), false, false);
-//
-//}
-
-void testNot() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::NOT, a), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testOr() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testTrue() {
- NodeManagerScope nms(d_nodeManager);
- d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testVar() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(a, false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
- d_satSolver->reset();
- d_cnfStream->convertAndAssert(b, false, false);
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
-
-void testXor() {
- NodeManagerScope nms(d_nodeManager);
- Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
- Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
- d_cnfStream->convertAndAssert(
- d_nodeManager->mkNode(kind::XOR, a, b), false, false );
- TS_ASSERT( d_satSolver->addClauseCalled() );
-}
+ /* [chris 5/26/2010] In the tests below, we don't attempt to delve into the
+ * deep structure of the CNF conversion. Firstly, we just want to make sure
+ * that the conversion doesn't choke on any boolean Exprs. We'll also check
+ * that addClause got called. We won't check that it gets called a particular
+ * number of times, or with what.
+ */
+
+ void testAnd() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testComplexExpr() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node d = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node e = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(
+ kind::IMPLIES,
+ d_nodeManager->mkNode(kind::AND, a, b),
+ d_nodeManager->mkNode(
+ kind::IFF,
+ d_nodeManager->mkNode(kind::OR, c, d),
+ d_nodeManager->mkNode(
+ kind::NOT,
+ d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testFalse() {
+ NodeManagerScope nms(d_nodeManager);
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testIff() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::IFF, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testImplies() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ // ITEs should be removed before going to CNF
+ //void testIte() {
+ // NodeManagerScope nms(d_nodeManager);
+ // d_cnfStream->convertAndAssert(
+ // d_nodeManager->mkNode(
+ // kind::EQUAL,
+ // d_nodeManager->mkNode(
+ // kind::ITE,
+ // d_nodeManager->mkVar(d_nodeManager->booleanType()),
+ // d_nodeManager->mkVar(d_nodeManager->integerType()),
+ // d_nodeManager->mkVar(d_nodeManager->integerType())
+ // ),
+ // d_nodeManager->mkVar(d_nodeManager->integerType())
+ // ), false, false);
+ //
+ //}
+
+ void testNot() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::NOT, a), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testOr() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testTrue() {
+ NodeManagerScope nms(d_nodeManager);
+ d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testVar() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(a, false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ d_satSolver->reset();
+ d_cnfStream->convertAndAssert(b, false, false);
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
+
+ void testXor() {
+ NodeManagerScope nms(d_nodeManager);
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
+ d_cnfStream->convertAndAssert(
+ d_nodeManager->mkNode(kind::XOR, a, b), false, false );
+ TS_ASSERT( d_satSolver->addClauseCalled() );
+ }
};
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index ded7cee97..f0073cc0b 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -43,6 +43,7 @@ using namespace std;
class TheoryArithWhite : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
@@ -92,11 +93,12 @@ public:
}
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
d_outputChannel.clear();
- d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));
+ d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
preregistered = new std::set<Node>();
@@ -115,6 +117,7 @@ public:
d_outputChannel.clear();
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 2c3ff0bb1..63900c19c 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -95,8 +95,8 @@ public:
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) :
- Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) {
+ DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation) {
}
void registerTerm(TNode n) {
@@ -135,11 +135,12 @@ public:
void explain(TNode n, Effort level) {}
Node getValue(TNode n) { return Node::null(); }
string identify() const { return "DummyTheory"; }
-};
+};/* class DummyTheory */
class TheoryBlack : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
@@ -153,10 +154,11 @@ class TheoryBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
- d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
+ d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL));
d_outputChannel.clear();
atom0 = d_nm->mkConst(true);
atom1 = d_nm->mkConst(false);
@@ -168,6 +170,7 @@ public:
delete d_dummy;
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index e33efb597..7132d9b17 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -104,8 +104,8 @@ class FakeTheory : public Theory {
// static std::deque<RewriteItem> s_expected;
public:
- FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) :
- Theory(theoryId, ctxt, out, valuation)
+ FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation) :
+ Theory(theoryId, ctxt, uctxt, out, valuation)
{ }
/** Register an expected rewrite call */
@@ -222,6 +222,7 @@ public:
*/
class TheoryEngineWhite : public CxxTest::TestSuite {
Context* d_ctxt;
+ UserContext* d_uctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
@@ -231,15 +232,16 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
+ d_ctxt = new Context();
+ d_uctxt = new UserContext();
d_nm = new NodeManager(d_ctxt, NULL);
d_scope = new NodeManagerScope(d_nm);
- d_nullChannel = new FakeOutputChannel;
+ d_nullChannel = new FakeOutputChannel();
// create the TheoryEngine
- d_theoryEngine = new TheoryEngine(d_ctxt);
+ d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt);
d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
@@ -260,6 +262,7 @@ public:
delete d_scope;
delete d_nm;
+ delete d_uctxt;
delete d_ctxt;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback