summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/system/Makefile.am3
-rw-r--r--test/system/boilerplate.cpp1
-rw-r--r--test/system/two_smt_engines.cpp37
-rw-r--r--test/unit/Makefile.am4
-rw-r--r--test/unit/prop/cnf_stream_white.h (renamed from test/unit/prop/cnf_stream_black.h)52
-rw-r--r--test/unit/theory/theory_arith_white.h35
-rw-r--r--test/unit/theory/theory_engine_white.h41
-rw-r--r--test/unit/theory/theory_white.h (renamed from test/unit/theory/theory_black.h)30
8 files changed, 132 insertions, 71 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 7fa7b4a68..070f69639 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -2,7 +2,8 @@ TESTS_ENVIRONMENT =
TEST_EXTENSIONS = .class
CPLUSPLUS_TESTS = \
boilerplate \
- ouroborous
+ ouroborous \
+ two_smt_engines
# cvc3_main
TESTS = $(CPLUSPLUS_TESTS)
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index c64c1463e..18a560c0e 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -30,6 +30,7 @@ using namespace std;
int main() {
ExprManager em;
Options opts;
+ cout << "foo: " << opts.threadArgv.size() << endl;
SmtEngine smt(&em);
Result r = smt.query(em.mkConst(true));
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp
new file mode 100644
index 000000000..35d6c92cf
--- /dev/null
+++ b/test/system/two_smt_engines.cpp
@@ -0,0 +1,37 @@
+/********************* */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+ ExprManager em;
+ Options opts;
+ SmtEngine smt(&em);
+ SmtEngine smt2(&em);
+ Result r = smt.query(em.mkConst(true));
+
+ return r == Result::VALID ? 0 : 1;
+}
+
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index bb8cdf7fe..dc53bff61 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -2,7 +2,7 @@
UNIT_TESTS = \
theory/logic_info_white \
theory/theory_engine_white \
- theory/theory_black \
+ theory/theory_white \
theory/theory_arith_white \
theory/union_find_black \
theory/theory_bv_white \
@@ -24,7 +24,7 @@ UNIT_TESTS = \
expr/type_node_white \
parser/parser_black \
parser/parser_builder_black \
- prop/cnf_stream_black \
+ prop/cnf_stream_white \
context/context_black \
context/context_white \
context/context_mm_black \
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_white.h
index 70c306a6d..cc7ea9bf6 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -1,5 +1,5 @@
/********************* */
-/*! \file cnf_stream_black.h
+/*! \file cnf_stream_white.h
** \verbatim
** Original author: cconway
** Major contributors: mdeters
@@ -22,7 +22,6 @@
#include "util/Assert.h"
-
#include "expr/expr_manager.h"
#include "expr/node_manager.h"
#include "context/context.h"
@@ -30,6 +29,7 @@
#include "prop/prop_engine.h"
#include "prop/theory_proxy.h"
#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
@@ -42,6 +42,8 @@
using namespace CVC4;
using namespace CVC4::context;
using namespace CVC4::prop;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
using namespace std;
/* This fake class relies on the face that a MiniSat variable is just an int. */
@@ -118,19 +120,13 @@ public:
};/* class FakeSatSolver */
-class CnfStreamBlack : public CxxTest::TestSuite {
+class CnfStreamWhite : public CxxTest::TestSuite {
/** The SAT solver proxy */
FakeSatSolver* d_satSolver;
- /** The logic info */
- LogicInfo* d_logicInfo;
-
/** The theory engine */
TheoryEngine* d_theoryEngine;
- /** The output channel */
- theory::OutputChannel* d_outputChannel;
-
/** The CNF converter in use */
CnfStream* d_cnfStream;
@@ -143,31 +139,32 @@ class CnfStreamBlack : public CxxTest::TestSuite {
/** The node manager */
NodeManager* d_nodeManager;
+ ExprManager* d_exprManager;
+ SmtScope* d_scope;
+ SmtEngine* d_smt;
+
void setUp() {
- d_context = new Context();
- d_userContext = new UserContext();
- d_nodeManager = new NodeManager(d_context, NULL);
- NodeManagerScope nms(d_nodeManager);
+ d_exprManager = new ExprManager();
+ d_smt = new SmtEngine(d_exprManager);
+ d_smt->d_logic.lock();
+ d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+ d_scope = new SmtScope(d_smt);
+
+ d_context = d_smt->d_context;
+ d_userContext = d_smt->d_userContext;
+
+ d_theoryEngine = d_smt->d_theoryEngine;
+
d_satSolver = new FakeSatSolver();
- d_logicInfo = new LogicInfo();
- d_logicInfo->lock();
- d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
- 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);
d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
}
void tearDown() {
- NodeManagerScope nms(d_nodeManager);
delete d_cnfStream;
- d_theoryEngine->shutdown();
- delete d_theoryEngine;
- delete d_logicInfo;
delete d_satSolver;
- delete d_nodeManager;
- delete d_userContext;
- delete d_context;
+ delete d_scope;
+ delete d_smt;
+ delete d_exprManager;
}
public:
@@ -291,8 +288,7 @@ public:
Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
d_cnfStream->ensureLiteral(a_and_b);
- // Clauses are necessary to "literal-ize" a_and_b; this perhaps
- // doesn't belong in a black-box test though...
+ // Clauses are necessary to "literal-ize" a_and_b
TS_ASSERT( d_satSolver->addClauseCalled() );
TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) );
}
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(){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback