diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-08 20:16:58 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-14 16:41:17 -0400 |
commit | ef000094d2d6a024c7eac490b241259b38e07225 (patch) | |
tree | 395250d07c9e589b1ba42316516deddfe1486018 /test | |
parent | 7df24c61c7998e1485ab75219078deaf1455bd71 (diff) |
Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/context/stacking_map_black.h | 4 | ||||
-rw-r--r-- | test/unit/context/stacking_vector_black.h | 4 | ||||
-rw-r--r-- | test/unit/expr/attribute_black.h | 20 | ||||
-rw-r--r-- | test/unit/expr/attribute_white.h | 41 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 6 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 7 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 7 | ||||
-rw-r--r-- | test/unit/expr/node_manager_white.h | 7 | ||||
-rw-r--r-- | test/unit/expr/node_self_iterator_black.h | 7 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 7 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.h | 7 |
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() { |