diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
commit | 36615c5e7332e26645b33ce9b6bab25439a5108e (patch) | |
tree | 166efefced107009f4a68ff3d0c6623540dfa435 /test/unit/theory | |
parent | 25396f93b7df85c80a39ed207483e28a8c86ff26 (diff) |
Support for having two SmtEngines with the same ExprManager.
Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine. Otherwise, theories register the
same statistic twice. This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed. Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
Diffstat (limited to 'test/unit/theory')
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 35 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 41 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h (renamed from test/unit/theory/theory_black.h) | 30 |
3 files changed, 66 insertions, 40 deletions
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 48b9b2d35..fe922a6e1 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -21,12 +21,15 @@ #include <cxxtest/TestSuite.h> #include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/arith/theory_arith.h" #include "theory/quantifiers_engine.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" #include "util/rational.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/theory_test_utils.h" @@ -38,6 +41,7 @@ using namespace CVC4::theory::arith; using namespace CVC4::expr; using namespace CVC4::context; using namespace CVC4::kind; +using namespace CVC4::smt; using namespace std; @@ -45,14 +49,15 @@ class TheoryArithWhite : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtScope* d_scope; + SmtEngine* d_smt; TestOutputChannel d_outputChannel; LogicInfo d_logicInfo; Theory::Effort d_level; - QuantifiersEngine* d_quantifiersEngine; TheoryArith* d_arith; TypeNode* d_booleanType; @@ -96,14 +101,22 @@ public: } void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; + d_scope = new SmtScope(d_smt); d_outputChannel.clear(); d_logicInfo.lock(); - d_quantifiersEngine = new QuantifiersEngine(d_ctxt, NULL); - d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_quantifiersEngine); + + // guard against duplicate statistics assertion errors + delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]; + delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH]; + d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; + d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL; + + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine); preregistered = new std::set<Node>(); @@ -119,12 +132,10 @@ public: delete preregistered; delete d_arith; - delete d_quantifiersEngine; d_outputChannel.clear(); delete d_scope; - delete d_nm; - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testAssert() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ae61bd0d3..ee637daac 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -34,6 +34,8 @@ #include "expr/node_manager.h" #include "expr/kind.h" #include "context/context.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "util/rational.h" #include "util/integer.h" #include "util/options.h" @@ -44,6 +46,7 @@ using namespace CVC4::theory; using namespace CVC4::expr; using namespace CVC4::context; using namespace CVC4::kind; +using namespace CVC4::smt; using namespace std; @@ -233,49 +236,47 @@ class TheoryEngineWhite : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtEngine* d_smt; + SmtScope* d_scope; FakeOutputChannel *d_nullChannel; TheoryEngine* d_theoryEngine; - LogicInfo* d_logicInfo; public: void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); + d_em = new ExprManager(); + d_smt = new SmtEngine(d_em); + d_nm = NodeManager::fromExprManager(d_em); + d_scope = new SmtScope(d_smt); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; d_nullChannel = new FakeOutputChannel(); - // create the TheoryEngine - d_logicInfo = new LogicInfo(); - d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo); - + d_theoryEngine = d_smt->d_theoryEngine; + for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { + delete d_theoryEngine->d_theoryOut[id]; + delete d_theoryEngine->d_theoryTable[id]; + d_theoryEngine->d_theoryOut[id] = NULL; + d_theoryEngine->d_theoryTable[id] = NULL; + } 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"); } void tearDown() { - d_theoryEngine->shutdown(); - delete d_theoryEngine; - delete d_logicInfo; - delete d_nullChannel; delete d_scope; - delete d_nm; - - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testRewriterSimple() { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_white.h index 74f5870a3..5b46aee4f 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_white.h @@ -19,9 +19,12 @@ #include <cxxtest/TestSuite.h> #include "theory/theory.h" +#include "theory/theory_engine.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 <vector> @@ -29,6 +32,7 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::expr; using namespace CVC4::context; +using namespace CVC4::smt; using namespace std; @@ -159,7 +163,9 @@ class TheoryBlack : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; NodeManager* d_nm; - NodeManagerScope* d_scope; + ExprManager* d_em; + SmtScope* d_scope; + SmtEngine* d_smt; LogicInfo* d_logicInfo; TestOutputChannel d_outputChannel; @@ -172,12 +178,21 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; + d_scope = new SmtScope(d_smt); d_logicInfo = new LogicInfo(); d_logicInfo->lock(); + + // guard against duplicate statistics assertion errors + delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; + delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN]; + d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; + d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); @@ -190,9 +205,8 @@ public: delete d_dummy; delete d_logicInfo; delete d_scope; - delete d_nm; - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testEffort(){ |