diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /test/unit | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 3 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_black.h | 6 | ||||
-rw-r--r-- | test/unit/theory/shared_term_manager_black.h | 148 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 25 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 23 |
5 files changed, 22 insertions, 183 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 608d6335b..b8e4c1679 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -1,12 +1,11 @@ # All unit tests UNIT_TESTS = \ - theory/shared_term_manager_black \ theory/theory_engine_white \ theory/theory_black \ theory/theory_arith_white \ theory/union_find_black \ expr/expr_public \ - expr/expr_manager_public \ + expr/expr_manager_public \ expr/node_white \ expr/node_black \ expr/kind_black \ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index 8fb96c74a..c9a2196a5 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -108,9 +108,9 @@ void setUp() { NodeManagerScope nms(d_nodeManager); d_satSolver = new FakeSatSolver; d_theoryEngine = new TheoryEngine(d_context); - d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(); - d_theoryEngine->addTheory<theory::booleans::TheoryBool>(); - d_theoryEngine->addTheory<theory::arith::TheoryArith>(); + 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); } diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h deleted file mode 100644 index 1be116517..000000000 --- a/test/unit/theory/shared_term_manager_black.h +++ /dev/null @@ -1,148 +0,0 @@ -/********************* */ -/*! \file shared_term_manager_black.h - ** \verbatim - ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): cconway, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Black box testing of CVC4::SharedTermManager. - ** - ** Black box testing of CVC4::SharedTermManager. - **/ - -#include <cxxtest/TestSuite.h> - -#include <iostream> -#include <string> -#include <deque> - -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "expr/kind.h" -#include "context/context.h" -#include "util/rational.h" -#include "util/integer.h" -#include "util/options.h" -#include "util/Assert.h" - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::expr; -using namespace CVC4::context; -using namespace CVC4::kind; - -using namespace std; - -/** - * Test the SharedTermManager. - */ -class SharedTermManagerBlack : public CxxTest::TestSuite { - Context* d_ctxt; - - NodeManager* d_nm; - NodeManagerScope* d_scope; - TheoryEngine* d_theoryEngine; - -public: - - void setUp() { - d_ctxt = new Context; - - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); - - d_theoryEngine = new TheoryEngine(d_ctxt); - } - - void tearDown() { - d_theoryEngine->shutdown(); - delete d_theoryEngine; - - delete d_scope; - delete d_nm; - - delete d_ctxt; - } - - void testExplanation() { - // Example from Barcelogic paper - SharedTermManager* stm = d_theoryEngine->getSharedTermManager(); - - Node x1 = d_nm->mkVar("x1", d_nm->integerType()); - Node x2 = d_nm->mkVar("x2", d_nm->integerType()); - Node x3 = d_nm->mkVar("x3", d_nm->integerType()); - Node x4 = d_nm->mkVar("x4", d_nm->integerType()); - Node x5 = d_nm->mkVar("x5", d_nm->integerType()); - Node x6 = d_nm->mkVar("x6", d_nm->integerType()); - Node x7 = d_nm->mkVar("x7", d_nm->integerType()); - Node x8 = d_nm->mkVar("x8", d_nm->integerType()); - Node x9 = d_nm->mkVar("x9", d_nm->integerType()); - Node x10 = d_nm->mkVar("x10", d_nm->integerType()); - Node x11 = d_nm->mkVar("x11", d_nm->integerType()); - Node x12 = d_nm->mkVar("x12", d_nm->integerType()); - Node x13 = d_nm->mkVar("x13", d_nm->integerType()); - Node x14 = d_nm->mkVar("x14", d_nm->integerType()); - - Node a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12; - - d_ctxt->push(); - - stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8)); - stm->addEq(a2 = d_nm->mkNode(EQUAL, x7, x2)); - stm->addEq(a3 = d_nm->mkNode(EQUAL, x3, x13)); - stm->addEq(a4 = d_nm->mkNode(EQUAL, x7, x1)); - stm->addEq(a5 = d_nm->mkNode(EQUAL, x6, x7)); - stm->addEq(a6 = d_nm->mkNode(EQUAL, x9, x5)); - stm->addEq(a7 = d_nm->mkNode(EQUAL, x9, x3)); - stm->addEq(a8 = d_nm->mkNode(EQUAL, x14, x11)); - stm->addEq(a9 = d_nm->mkNode(EQUAL, x10, x4)); - stm->addEq(a10 = d_nm->mkNode(EQUAL, x12, x9)); - stm->addEq(a11 = d_nm->mkNode(EQUAL, x4, x11)); - stm->addEq(a12 = d_nm->mkNode(EQUAL, x10, x7)); - - Node explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x4)); - - TS_ASSERT(explanation.getNumChildren() == 3); - - Node e0 = explanation[0]; - Node e1 = explanation[1]; - Node e2 = explanation[2]; - - TS_ASSERT(e0 == a4 && e1 == a9 && e2 == a12); - - TS_ASSERT(stm->getRep(x8) == stm->getRep(x14)); - TS_ASSERT(stm->getRep(x2) != stm->getRep(x12)); - - d_ctxt->pop(); - - TS_ASSERT(stm->getRep(x8) != stm->getRep(x14)); - - d_ctxt->push(); - - stm->addEq(a1 = d_nm->mkNode(EQUAL, x1, x8)); - stm->addEq(a2 = d_nm->mkNode(EQUAL, x8, x2)); - stm->addEq(a3 = d_nm->mkNode(EQUAL, x2, x3)); - - explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x3)); - TS_ASSERT(explanation.getNumChildren() == 3); - - e0 = explanation[0]; - e1 = explanation[1]; - e2 = explanation[2]; - - TS_ASSERT(e0 == a1 && e1 == a2 && e2 == a3); - - TS_ASSERT(stm->getRep(x8) == stm->getRep(x2)); - - d_ctxt->pop(); - } - -}; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index ff6b352d0..2c3ff0bb1 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -52,32 +52,23 @@ public: void safePoint() throw(Interrupted, AssertionException) {} - void conflict(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void conflict(TNode n) + throw(AssertionException) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void propagate(TNode n) + throw(AssertionException) { push(PROPAGATE, n); } - void lemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { + void lemma(TNode n, bool removable) + throw(AssertionException) { push(LEMMA, n); } - void augmentingLemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { - Unreachable(); - } - - void explanation(TNode n, bool safe = false) - throw(Interrupted, AssertionException) { - push(EXPLANATION, n); - } void setIncomplete() - throw(Interrupted, AssertionException) { + throw(AssertionException) { Unreachable(); } @@ -292,7 +283,7 @@ public: void testOutputChannel() { Node n = atom0.orNode(atom1); - d_outputChannel.lemma(n); + d_outputChannel.lemma(n, false); d_outputChannel.split(atom0); Node s = atom0.orNode(atom0.notNode()); TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index a1b058eeb..e33efb597 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -48,19 +48,16 @@ using namespace CVC4::kind; using namespace std; class FakeOutputChannel : public OutputChannel { - void conflict(TNode n, bool safe) throw(AssertionException) { + void conflict(TNode n) throw(AssertionException) { Unimplemented(); } - void propagate(TNode n, bool safe) throw(AssertionException) { + void propagate(TNode n) throw(AssertionException) { Unimplemented(); } - void lemma(TNode n, bool safe) throw(AssertionException) { + void lemma(TNode n, bool removable) throw(AssertionException) { Unimplemented(); } - void augmentingLemma(TNode n, bool safe) throw(AssertionException) { - Unimplemented(); - } - void explanation(TNode n, bool safe) throw(AssertionException) { + void explanation(TNode n) throw(AssertionException) { Unimplemented(); } void setIncomplete() throw(AssertionException) { @@ -244,12 +241,12 @@ public: // create the TheoryEngine d_theoryEngine = new TheoryEngine(d_ctxt); - d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(); - d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(); - d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(); - d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(); - d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(); - d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(); + d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); + d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL); + d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF); + d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH); + d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY); + d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV); //Debug.on("theory-rewrite"); } |