summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/context/cdlist_black.h72
-rw-r--r--test/unit/context/context_black.h45
-rw-r--r--test/unit/expr/node_black.h10
-rw-r--r--test/unit/expr/node_builder_black.h60
-rw-r--r--test/unit/expr/node_white.h183
-rw-r--r--test/unit/theory/theory_black.h29
-rw-r--r--test/unit/theory/theory_uf_white.h92
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);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback