diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/context/cdlist_black.h | 72 | ||||
-rw-r--r-- | test/unit/context/context_black.h | 45 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 10 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 60 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 183 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 29 | ||||
-rw-r--r-- | test/unit/theory/theory_uf_white.h | 92 |
8 files changed, 333 insertions, 159 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 8caec4f40..967d6a8c8 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -7,6 +7,7 @@ UNIT_TESTS = \ parser/parser_black \ context/context_black \ context/context_mm_black \ + context/cdlist_black \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h new file mode 100644 index 000000000..560c70722 --- /dev/null +++ b/test/unit/context/cdlist_black.h @@ -0,0 +1,72 @@ +/********************* */ +/** cdlist_black.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Black box testing of CVC4::context::CDList<>. + **/ + +#include <cxxtest/TestSuite.h> + +#include <vector> +#include <iostream> +#include "context/context.h" +#include "context/cdlist.h" + +using namespace std; +using namespace CVC4::context; + +class CDListBlack : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context(); + } + + // test at different sizes. this triggers grow() behavior differently. + // grow() is completely broken in revision 256; fix forthcoming by Tim + void testCDList10() { listTest(10); } + void testCDList15() { listTest(15); } + void testCDList20() { listTest(20); } + void testCDList35() { listTest(35); } + void testCDList50() { listTest(50); } + void testCDList99() { listTest(99); } + + void listTest(int N) { + CDList<int> list(d_context); + + TS_ASSERT(list.empty()); + for(int i = 0; i < N; ++i) { + TS_ASSERT(list.size() == i); + list.push_back(i); + TS_ASSERT(!list.empty()); + TS_ASSERT(list.back() == i); + int i2 = 0; + for(CDList<int>::const_iterator j = list.begin(); + j != list.end(); + ++j) { + TS_ASSERT(*j == i2++); + } + } + TS_ASSERT(list.size() == N); + + for(int i = 0; i < N; ++i) { + TS_ASSERT(list[i] == i); + } + } + + void tearDown() { + delete d_context; + } +}; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 64ad2d7f7..f06ed9f42 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -10,17 +10,20 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Black box testing of CVC4::Node. + ** Black box testing of CVC4::context::Context. **/ #include <cxxtest/TestSuite.h> -//Used in some of the tests #include <vector> #include <iostream> #include "context/context.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "util/Assert.h" using namespace std; +using namespace CVC4; using namespace CVC4::context; class ContextBlack : public CxxTest::TestSuite { @@ -31,7 +34,7 @@ private: public: void setUp() { - d_context = new Context(); + d_context = new Context; } void testIntCDO() { @@ -53,40 +56,8 @@ public: // the interface doesn't declare any exceptions d_context->push(); d_context->pop(); -// d_context->pop(); -// d_context->pop(); - } - - // test at different sizes. this triggers grow() behavior differently. - // grow() is completely broken in revision 256; fix forthcoming by Tim - void testCDList10() { listTest(10); } - void testCDList15() { listTest(15); } - void testCDList20() { listTest(20); } - void testCDList35() { listTest(35); } - void testCDList50() { listTest(50); } - void testCDList99() { listTest(99); } - - void listTest(int N) { - CDList<int> list(d_context); - - TS_ASSERT(list.empty()); - for(int i = 0; i < N; ++i) { - TS_ASSERT(list.size() == i); - list.push_back(i); - TS_ASSERT(!list.empty()); - TS_ASSERT(list.back() == i); - int i2 = 0; - for(CDList<int>::const_iterator j = list.begin(); - j != list.end(); - ++j) { - TS_ASSERT(*j == i2++); - } - } - TS_ASSERT(list.size() == N); - - for(int i = 0; i < N; ++i) { - TS_ASSERT(list[i] == i); - } + TS_ASSERT_THROWS( d_context->pop(), AssertionException ); + TS_ASSERT_THROWS( d_context->pop(), AssertionException ); } void tearDown() { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c11d5cf86..96f02c489 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -27,24 +27,28 @@ using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace std; class NodeBlack : public CxxTest::TestSuite { private: - NodeManager *d_nodeManager; - NodeManagerScope *d_scope; + Context* d_ctxt; + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; public: void setUp() { - d_nodeManager = new NodeManager(); + d_ctxt = new Context; + d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { 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 871e93dca..ab3c1c842 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -23,29 +23,34 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" +#include "context/context.h" #include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { private: - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; public: void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); specKind = PLUS; } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; + delete d_ctxt; } @@ -609,20 +614,37 @@ public: f, d_nm->mkNode(AND, q, a))); - Node assoc1 = (a && b) && c; - Node assoc2 = a && (b && c); - - TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c)); - TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); - - Node prec1 = (a && b) || c; - Node prec2 = a || (b && c); - Node prec3 = a && (b || c); - Node prec4 = (a || b) && c; - - TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); - TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); - TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c)); + TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); + TS_ASSERT_EQUALS(Node((a || b) || c), d_nm->mkNode(OR, a, b, c)); + TS_ASSERT_EQUALS(Node(a || (b || c)), d_nm->mkNode(OR, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(Node((a && b) || c), d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); + TS_ASSERT_EQUALS(Node(a && (b || c)), d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); + + TS_ASSERT_EQUALS(Node((a + b) + c), d_nm->mkNode(PLUS, a, b, c)); + TS_ASSERT_EQUALS(Node(a + (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, c))); + TS_ASSERT_EQUALS(Node((a - b) - c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a - (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))))); + TS_ASSERT_EQUALS(Node((a * b) * c), d_nm->mkNode(MULT, a, b, c)); + TS_ASSERT_EQUALS(Node(a * (b * c)), d_nm->mkNode(MULT, a, d_nm->mkNode(MULT, b, c))); + TS_ASSERT_EQUALS(Node((a + b) - c), d_nm->mkNode(PLUS, a, b, d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a + (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))); + TS_ASSERT_EQUALS(Node((a - b) + c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), c)); + TS_ASSERT_EQUALS(Node(a - (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, c)))); + TS_ASSERT_EQUALS(Node((a + b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, b), c)); + TS_ASSERT_EQUALS(Node(a + (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(MULT, b, c))); + TS_ASSERT_EQUALS(Node((a - b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b)), c)); + TS_ASSERT_EQUALS(Node(a - (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, b, c)))); + TS_ASSERT_EQUALS(Node((a * b) + c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), c)); + TS_ASSERT_EQUALS(Node(a * (b + c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, c))); + TS_ASSERT_EQUALS(Node((a * b) - c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a * (b - c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))); + + TS_ASSERT_EQUALS(Node(-a), d_nm->mkNode(UMINUS, a)); + TS_ASSERT_EQUALS(Node(- a - b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), d_nm->mkNode(UMINUS, b))); + TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b)); + TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b)); } }; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 871abe232..88ae5253f 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -22,9 +22,12 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/attribute.h" +#include "context/context.h" +#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace CVC4::expr; using namespace CVC4::expr::attr; using namespace std; @@ -41,39 +44,33 @@ typedef Attribute<Test2, std::string> TestStringAttr2; // it would be nice to have CDAttribute<> for context-dependence typedef CDAttribute<Test1, bool> TestCDFlag; -struct ecdata; -struct cleanupfcn { - static void cleanup(ecdata* ec) { /* clean up */ } -}; - -// ManagedAttribute<> has a cleanup function deleting the value -typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr; - typedef Attribute<Test1, bool> TestFlag1; typedef Attribute<Test2, bool> TestFlag2; typedef Attribute<Test3, bool> TestFlag3; typedef Attribute<Test4, bool> TestFlag4; typedef Attribute<Test5, bool> TestFlag5; -struct FooBar {}; -struct Test6; -typedef Attribute<Test6, FooBar> TestFlag6; +typedef CDAttribute<Test1, bool> TestFlag1cd; +typedef CDAttribute<Test2, bool> TestFlag2cd; class NodeWhite : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; public: void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; + delete d_ctxt; } void testNull() { @@ -96,16 +93,149 @@ public: TS_ASSERT(VarNameAttr::s_id == 0); TS_ASSERT(TestStringAttr1::s_id == 1); TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT(attr::LastAttributeId<string>::s_id == 3); + TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3)); TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1); + TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1)); TS_ASSERT(TestFlag1::s_id == 0); TS_ASSERT(TestFlag2::s_id == 1); TS_ASSERT(TestFlag3::s_id == 2); TS_ASSERT(TestFlag4::s_id == 3); TS_ASSERT(TestFlag5::s_id == 4); + TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5)); + + TS_ASSERT(TestFlag1cd::s_id == 0); + TS_ASSERT(TestFlag2cd::s_id == 1); + TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2)); + } + + void testCDAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 1 + + // test that all boolean flags are FALSE to start + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + // test that they all HAVE the boolean attributes + TS_ASSERT(a.hasAttribute(TestFlag1cd())); + TS_ASSERT(b.hasAttribute(TestFlag1cd())); + TS_ASSERT(c.hasAttribute(TestFlag1cd())); + + // test two-arg version of hasAttribute() + bool bb; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + + // setting boolean flags + Debug("boolattr", "set flag 1 on a to T\n"); + a.setAttribute(TestFlag1cd(), true); + Debug("boolattr", "set flag 1 on b to F\n"); + b.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on c to F\n"); + c.setAttribute(TestFlag1cd(), false); + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on a to F\n"); + a.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on b to T\n"); + b.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 3 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on c to T\n"); + c.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 1 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 0 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); } void testAttributes() { @@ -169,49 +299,29 @@ public: TS_ASSERT(! unnamed.getAttribute(TestFlag5())); // test that they all HAVE the boolean attributes - Debug("boolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 2 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 3 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 4 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 5 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag5())); // test two-arg version of hasAttribute() @@ -465,6 +575,5 @@ public: TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - } }; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 17fefd07b..908ab81fc 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -87,8 +87,9 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(context::Context* ctxt, OutputChannel& out) : - TheoryImpl<DummyTheory>(ctxt, out) {} + DummyTheory(Context* ctxt, OutputChannel& out) : + TheoryImpl<DummyTheory>(ctxt, out) { + } void registerTerm(TNode n) { // check that we registerTerm() a term only once @@ -125,13 +126,12 @@ public: class TheoryBlack : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; TestOutputChannel d_outputChannel; - Context* d_context; - DummyTheory* d_dummy; Node atom0; @@ -139,28 +139,23 @@ class TheoryBlack : public CxxTest::TestSuite { public: - TheoryBlack() {} - void setUp() { - d_nm = new NodeManager(); - + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - - d_context = new Context(); - - d_dummy = new DummyTheory(d_context, d_outputChannel); - + d_dummy = new DummyTheory(d_ctxt, d_outputChannel); d_outputChannel.clear(); - atom0 = d_nm->mkNode(kind::TRUE); atom1 = d_nm->mkNode(kind::FALSE); } void tearDown() { + atom1 = Node::null(); + atom0 = Node::null(); delete d_dummy; - delete d_context; delete d_scope; delete d_nm; + delete d_ctxt; } void testEffort(){ diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index fe2c8d821..86266e923 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -36,10 +36,10 @@ using namespace std; * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel */ -enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION}; +enum OutputChannelCallType { CONFLICT, PROPOGATE, LEMMA, EXPLANATION }; class TestOutputChannel : public OutputChannel { private: - void push(OutputChannelCallType call, TNode n){ + void push(OutputChannelCallType call, TNode n) { d_callHistory.push_back(make_pair(call,n)); } public: @@ -51,71 +51,71 @@ public: void safePoint() throw(Interrupted) {} - void conflict(TNode n, bool safe = false) throw(Interrupted){ + void conflict(TNode n, bool safe = false) throw(Interrupted) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted){ + void propagate(TNode n, bool safe = false) throw(Interrupted) { push(PROPOGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted){ + void lemma(TNode n, bool safe = false) throw(Interrupted) { push(LEMMA, n); } - void explanation(TNode n, bool safe = false) throw(Interrupted){ + void explanation(TNode n, bool safe = false) throw(Interrupted) { push(EXPLANATION, n); } - void clear(){ + void clear() { d_callHistory.clear(); } - Node getIthNode(int i){ + + Node getIthNode(int i) { Node tmp = (d_callHistory[i]).second; return tmp; } - OutputChannelCallType getIthCallType(int i){ + OutputChannelCallType getIthCallType(int i) { return (d_callHistory[i]).first; } - unsigned getNumCalls(){ + unsigned getNumCalls() { return d_callHistory.size(); } }; class TheoryUFWhite : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; TestOutputChannel d_outputChannel; - Theory::Effort level; + Theory::Effort d_level; - Context* d_context; TheoryUF* d_euf; public: - TheoryUFWhite(): level(Theory::FULL_EFFORT) { } + TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - - d_context = new Context(); - d_outputChannel.clear(); - d_euf = new TheoryUF(d_context, d_outputChannel); + d_euf = new TheoryUF(d_ctxt, d_outputChannel); } void tearDown() { delete d_euf; - delete d_context; + d_outputChannel.clear(); delete d_scope; delete d_nm; + delete d_ctxt; } - void testPushPopChain(){ + void testPushPopChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -140,26 +140,26 @@ public: d_euf->assertFact( f3_x_eq_x ); d_euf->assertFact( f1_x_neq_x ); - d_euf->check(level); - d_context->push(); + d_euf->check(d_level); + d_ctxt->push(); d_euf->assertFact( f5_x_eq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); - d_context->pop(); - d_euf->check(level); + d_ctxt->pop(); + d_euf->check(d_level); //Test that no additional calls to the output channel occurred. TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); d_euf->assertFact( f5_x_eq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -174,7 +174,7 @@ public: /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ - void testSimpleChain(){ + void testSimpleChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -188,7 +188,7 @@ public: d_euf->assertFact(f_f_x_eq_x); d_euf->assertFact(f_f_f_x_neq_f_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -199,13 +199,13 @@ public: } /* test that !(x == x) is inconsistent */ - void testSelfInconsistent(){ + void testSelfInconsistent() { Node x = d_nm->mkVar(); Node x_neq_x = (x.eqNode(x)).notNode(); Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x); d_euf->assertFact(x_neq_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0)); @@ -213,12 +213,12 @@ public: } /* test that (x == x) is consistent */ - void testSelfConsistent(){ + void testSelfConsistent() { Node x = d_nm->mkVar(); Node x_eq_x = x.eqNode(x); d_euf->assertFact(x_eq_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls()); } @@ -229,7 +229,7 @@ public: f(f(f(f(f(x))))) = x, f(x) != x } is inconsistent */ - void testChain(){ + void testChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -251,7 +251,7 @@ public: d_euf->assertFact( f3_x_eq_x ); d_euf->assertFact( f5_x_eq_x ); d_euf->assertFact( f1_x_neq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -260,28 +260,28 @@ public: } - void testPushPopA(){ + void testPushPopA() { Node x = d_nm->mkVar(); Node x_eq_x = x.eqNode(x); - d_context->push(); + d_ctxt->push(); d_euf->assertFact( x_eq_x ); - d_euf->check(level); - d_context->pop(); - d_euf->check(level); + d_euf->check(d_level); + d_ctxt->pop(); + d_euf->check(d_level); } - void testPushPopB(){ + void testPushPopB() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); Node f_x_eq_x = f_x.eqNode(x); d_euf->assertFact( f_x_eq_x ); - d_context->push(); - d_euf->check(level); - d_context->pop(); - d_euf->check(level); + d_ctxt->push(); + d_euf->check(d_level); + d_ctxt->pop(); + d_euf->check(d_level); } |