summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/unit/context/stacking_map_black.h4
-rw-r--r--test/unit/context/stacking_vector_black.h4
-rw-r--r--test/unit/expr/attribute_black.h20
-rw-r--r--test/unit/expr/attribute_white.h41
-rw-r--r--test/unit/expr/node_black.h6
-rw-r--r--test/unit/expr/node_builder_black.h7
-rw-r--r--test/unit/expr/node_manager_black.h7
-rw-r--r--test/unit/expr/node_manager_white.h7
-rw-r--r--test/unit/expr/node_self_iterator_black.h7
-rw-r--r--test/unit/expr/node_white.h7
-rw-r--r--test/unit/util/boolean_simplification_black.h7
11 files changed, 43 insertions, 74 deletions
diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
index 91e12a25e..4daab5cce 100644
--- a/test/unit/context/stacking_map_black.h
+++ b/test/unit/context/stacking_map_black.h
@@ -39,8 +39,8 @@ class StackingMapBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_ctxt = new Context();
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
d_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(d_ctxt);
diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
index c7e185735..35305e469 100644
--- a/test/unit/context/stacking_vector_black.h
+++ b/test/unit/context/stacking_vector_black.h
@@ -39,8 +39,8 @@ class StackingVectorBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_ctxt = new Context();
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
d_vectorPtr = new StackingVector<TNode>(d_ctxt);
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 8fee6571d..5f9a7ebce 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -26,31 +26,35 @@
#include "expr/node_manager.h"
#include "expr/node.h"
#include "expr/attribute.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
+using namespace CVC4::smt;
using namespace std;
class AttributeBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
+ ExprManager* d_exprManager;
NodeManager* d_nodeManager;
- NodeManagerScope* d_scope;
+ SmtEngine* d_smtEngine;
+ SmtScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context;
- d_nodeManager = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nodeManager);
+ d_exprManager = new ExprManager();
+ d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+ d_smtEngine = new SmtEngine(d_exprManager);
+ d_scope = new SmtScope(d_smtEngine);
}
void tearDown() {
delete d_scope;
- delete d_nodeManager;
- delete d_ctxt;
+ delete d_smtEngine;
+ delete d_exprManager;
}
class MyData {
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 11063cd1b..00ebc8b8d 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -18,7 +18,6 @@
#include <string>
-#include "context/context.h"
#include "expr/node_value.h"
#include "expr/node_builder.h"
#include "expr/node_manager.h"
@@ -29,10 +28,12 @@
#include "theory/theory_engine.h"
#include "theory/uf/theory_uf.h"
#include "util/cvc4_assert.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
+using namespace CVC4::smt;
using namespace CVC4::expr;
using namespace CVC4::expr::attr;
using namespace std;
@@ -60,26 +61,27 @@ typedef CDAttribute<Test2, bool> TestFlag2cd;
class AttributeWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
+ ExprManager* d_em;
NodeManager* d_nm;
- NodeManagerScope* d_scope;
+ SmtScope* d_scope;
TypeNode* d_booleanType;
+ SmtEngine* d_smtEngine;
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
-
+ d_em = new ExprManager();
+ d_nm = NodeManager::fromExprManager(d_em);
+ d_smtEngine = new SmtEngine(d_em);
+ d_scope = new SmtScope(d_smtEngine);
d_booleanType = new TypeNode(d_nm->booleanType());
}
void tearDown() {
delete d_booleanType;
delete d_scope;
- delete d_nm;
- delete d_ctxt;
+ delete d_smtEngine;
+ delete d_em;
}
void testAttributeIds() {
@@ -145,7 +147,6 @@ public:
lastId = attr::LastAttributeId<TypeNode, false>::getId();
TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId);
-
}
void testCDAttributes() {
@@ -162,7 +163,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 1
+ d_smtEngine->push(); // level 1
// test that all boolean flags are FALSE to start
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
@@ -204,7 +205,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 2
+ d_smtEngine->push(); // level 2
Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
TS_ASSERT(a.getAttribute(TestFlag1cd()));
@@ -225,7 +226,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->push(); // level 3
+ d_smtEngine->push(); // level 3
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -244,7 +245,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be T)\n";
TS_ASSERT(c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 2
+ d_smtEngine->pop(); // level 2
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -253,7 +254,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 1
+ d_smtEngine->pop(); // level 1
Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
TS_ASSERT(a.getAttribute(TestFlag1cd()));
@@ -262,7 +263,7 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
- d_ctxt->pop(); // level 0
+ d_smtEngine->pop(); // level 0
Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -271,13 +272,11 @@ public:
Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-#ifdef CVC4_ASSERTIONS
- TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException );
-#endif /* CVC4_ASSERTIONS */
+ TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException );
}
void testAttributes() {
- //Debug.on("bootattr");
+ //Debug.on("boolattr");
Node a = d_nm->mkVar(*d_booleanType);
Node b = d_nm->mkVar(*d_booleanType);
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 9f8ecb69e..7d6ee523a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -28,14 +28,12 @@
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace std;
class NodeBlack : public CxxTest::TestSuite {
private:
Options opts;
- Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -51,8 +49,7 @@ public:
free(argv[0]);
free(argv[1]);
- d_ctxt = new Context();
- d_nodeManager = new NodeManager(d_ctxt, NULL, opts);
+ d_nodeManager = new NodeManager(NULL, opts);
d_scope = new NodeManagerScope(d_nodeManager);
d_booleanType = new TypeNode(d_nodeManager->booleanType());
d_realType = new TypeNode(d_nodeManager->realType());
@@ -62,7 +59,6 @@ public:
delete d_booleanType;
delete d_scope;
delete d_nodeManager;
- delete d_ctxt;
}
bool imp(bool a, bool b) const {
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index c71ba48c5..9bac0d818 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -25,19 +25,16 @@
#include "expr/node_manager.h"
#include "expr/node.h"
#include "expr/kind.h"
-#include "context/context.h"
#include "util/cvc4_assert.h"
#include "util/rational.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace std;
class NodeBuilderBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -47,8 +44,7 @@ private:
public:
void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
specKind = AND;
@@ -63,7 +59,6 @@ public:
delete d_realType;
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 9ca086d06..b94e6a691 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -21,7 +21,6 @@
#include "expr/node_manager.h"
#include "expr/node_manager_attributes.h"
-#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
@@ -29,26 +28,22 @@
using namespace CVC4;
using namespace CVC4::expr;
using namespace CVC4::kind;
-using namespace CVC4::context;
class NodeManagerBlack : public CxxTest::TestSuite {
- Context* d_context;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_context = new Context;
- d_nodeManager = new NodeManager(d_context, NULL);
+ d_nodeManager = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nodeManager);
}
void tearDown() {
delete d_scope;
delete d_nodeManager;
- delete d_context;
}
void testMkNodeNot() {
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 7bc279f47..aaa3256dd 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -19,33 +19,28 @@
#include <string>
#include "expr/node_manager.h"
-#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
using namespace CVC4;
using namespace CVC4::expr;
-using namespace CVC4::context;
class NodeManagerWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context();
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
}
void tearDown() {
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
void testMkConstRational() {
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 9f90bd1b0..7240deed5 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -16,14 +16,12 @@
#include <cxxtest/TestSuite.h>
-#include "context/context.h"
#include "expr/node.h"
#include "expr/node_self_iterator.h"
#include "expr/node_builder.h"
#include "expr/convenience_node_builders.h"
using namespace CVC4;
-using namespace CVC4::context;
using namespace CVC4::kind;
using namespace CVC4::expr;
using namespace std;
@@ -31,7 +29,6 @@ using namespace std;
class NodeSelfIteratorBlack : public CxxTest::TestSuite {
private:
- Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
TypeNode* d_booleanType;
@@ -40,8 +37,7 @@ private:
public:
void setUp() {
- d_ctxt = new Context;
- d_nodeManager = new NodeManager(d_ctxt, NULL);
+ d_nodeManager = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nodeManager);
d_booleanType = new TypeNode(d_nodeManager->booleanType());
d_realType = new TypeNode(d_nodeManager->realType());
@@ -51,7 +47,6 @@ public:
delete d_booleanType;
delete d_scope;
delete d_nodeManager;
- delete d_ctxt;
}
void testSelfIteration() {
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index bcb3155e1..8a68db269 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -22,33 +22,28 @@
#include "expr/node_builder.h"
#include "expr/node_manager.h"
#include "expr/node.h"
-#include "context/context.h"
#include "util/cvc4_assert.h"
using namespace CVC4;
using namespace CVC4::kind;
-using namespace CVC4::context;
using namespace CVC4::expr;
using namespace std;
class NodeWhite : public CxxTest::TestSuite {
- Context* d_ctxt;
NodeManager* d_nm;
NodeManagerScope* d_scope;
public:
void setUp() {
- d_ctxt = new Context();
- d_nm = new NodeManager(d_ctxt, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
}
void tearDown() {
delete d_scope;
delete d_nm;
- delete d_ctxt;
}
void testNull() {
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index e2937ccb2..db02ce207 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -14,7 +14,6 @@
** Black box testing of CVC4::BooleanSimplification.
**/
-#include "context/context.h"
#include "util/language.h"
#include "expr/node.h"
#include "expr/kind.h"
@@ -26,12 +25,10 @@
#include <set>
using namespace CVC4;
-using namespace CVC4::context;
using namespace std;
class BooleanSimplificationBlack : public CxxTest::TestSuite {
- Context* d_context;
NodeManager* d_nm;
NodeManagerScope* d_scope;
@@ -70,8 +67,7 @@ class BooleanSimplificationBlack : public CxxTest::TestSuite {
public:
void setUp() {
- d_context = new Context();
- d_nm = new NodeManager(d_context, NULL);
+ d_nm = new NodeManager(NULL);
d_scope = new NodeManagerScope(d_nm);
a = d_nm->mkSkolem("a", d_nm->booleanType());
@@ -116,7 +112,6 @@ public:
delete d_scope;
delete d_nm;
- delete d_context;
}
void testNegate() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback