diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-02 20:33:26 +0000 |
commit | 2b87789ee57a738cccd89dd9d2d81b065875dc29 (patch) | |
tree | f5376c532490088e5dcc7a37ed318127a0dc8c40 /test | |
parent | 7f5036bb37e13dbc7e176d4fa82ee0736d11e913 (diff) |
* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/node_builder_black.h | 88 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 89 |
2 files changed, 117 insertions, 60 deletions
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 8aff0faf0..871e93dca 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -15,7 +15,6 @@ #include <cxxtest/TestSuite.h> -//Used in some of the tests #include <vector> #include <limits.h> #include <sstream> @@ -65,7 +64,7 @@ public: /** * Tests just constructors. No modification is done to the node. */ - void testNodeConstructors(){ + void testNodeConstructors() { //inline NodeBuilder(); //inline NodeBuilder(Kind k); @@ -151,14 +150,14 @@ public: } - void testDestructor(){ + void testDestructor() { //inline ~NodeBuilder(); NodeBuilder<K>* nb = new NodeBuilder<K>(); delete nb; //Not sure what to test other than survival } - void testBeginEnd(){ + void testBeginEnd() { /* Test begin and ends without resizing */ NodeBuilder<K> ws; TS_ASSERT_EQUALS(ws.begin(), ws.end()); @@ -203,12 +202,12 @@ public: TS_ASSERT_EQUALS(smaller_citer, smaller.end()); } - void testIterator(){ + void testIterator() { NodeBuilder<> b; Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); - b << x << y << z << kind::AND; + b << x << y << z << AND; { NodeBuilder<>::iterator i = b.begin(); @@ -228,7 +227,7 @@ public: } } - void testGetKind(){ + void testGetKind() { /* Kind getKind() const; */ NodeBuilder<> noKind; TS_ASSERT_EQUALS(noKind.getKind(), UNDEFINED_KIND); @@ -244,15 +243,13 @@ public: TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); #endif - NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); push_back(spec, K); TS_ASSERT_EQUALS(spec.getKind(), specKind); - } - void testGetNumChildren(){ + void testGetNumChildren() { /* unsigned getNumChildren() const; */ NodeBuilder<> noKind; @@ -282,7 +279,7 @@ public: #endif } - void testOperatorSquare(){ + void testOperatorSquare() { /* Node operator[](int i) const { Assert(i >= 0 && i < d_ev->getNumChildren()); @@ -332,7 +329,7 @@ public: #endif } - void testClear(){ + void testClear() { /* void clear(Kind k = UNDEFINED_KIND); */ NodeBuilder<> nb; @@ -378,7 +375,7 @@ public: } - void testStreamInsertionKind(){ + void testStreamInsertionKind() { /* NodeBuilder& operator<<(const Kind& k); */ #ifdef CVC4_DEBUG @@ -420,7 +417,7 @@ public: specKind); } - void testStreamInsertionNode(){ + void testStreamInsertionNode() { /* NodeBuilder& operator<<(const Node& n); */ NodeBuilder<K> nb(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -449,7 +446,7 @@ public: } - void testAppend(){ + void testAppend() { Node x = d_nm->mkVar(); Node y = d_nm->mkVar(); Node z = d_nm->mkVar(); @@ -499,7 +496,7 @@ public: TS_ASSERT(b[8] == m); } - void testOperatorNodeCast(){ + void testOperatorNodeCast() { /* operator Node();*/ NodeBuilder<K> implicit(specKind); NodeBuilder<K> explic(specKind); @@ -521,7 +518,7 @@ public: #endif } - void testToStream(){ + void testToStream() { /* inline void toStream(std::ostream& out) const { d_ev->toStream(out); } @@ -571,4 +568,61 @@ public: TS_ASSERT_EQUALS(astr, bstr); TS_ASSERT_DIFFERS(astr, cstr); } + + void testConvenienceBuilders() { + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node d = d_nm->mkVar(); + Node e = d_nm->mkVar(); + Node f = d_nm->mkVar(); + + Node m = a && b; + Node n = a && b || c; + Node o = d + e - b; + Node p = a && o || c; + + Node x = d + e + o - m; + Node y = f - a - c + e; + + Node q = a && b && c; + + Node r = e && d && b && a || x && y || f || q && a; + + TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); + TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); + TS_ASSERT_EQUALS(o, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, b))); + TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, o), c)); + + TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, o, d_nm->mkNode(UMINUS, m))); + TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS, + f, + d_nm->mkNode(UMINUS, a), + d_nm->mkNode(UMINUS, c), + e)); + + TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c)); + + TS_ASSERT_EQUALS(r, d_nm->mkNode(OR, + d_nm->mkNode(AND, e, d, b, a), + d_nm->mkNode(AND, x, y), + 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)); + } }; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index ee914090e..17fefd07b 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -29,17 +29,17 @@ using namespace CVC4::context; 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, PROPAGATE, LEMMA, EXPLANATION}; class TestOutputChannel : public OutputChannel { private: - void push(OutputChannelCallType call, TNode n){ - d_callHistory.push_back(make_pair(call,n)); + void push(OutputChannelCallType call, TNode n) { + d_callHistory.push_back(make_pair(call, n)); } + public: vector< pair<OutputChannelCallType, Node> > d_callHistory; @@ -49,71 +49,78 @@ 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){ - push(PROPOGATE, n); + void propagate(TNode n, bool safe = false) throw(Interrupted) { + push(PROPAGATE, 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 DummyTheory : public TheoryImpl<DummyTheory> { public: - vector<Node> d_registerSequence; + set<Node> d_registered; vector<Node> d_getSequence; DummyTheory(context::Context* ctxt, OutputChannel& out) : TheoryImpl<DummyTheory>(ctxt, out) {} - void registerTerm(TNode n){ - d_registerSequence.push_back(n); - } + void registerTerm(TNode n) { + // check that we registerTerm() a term only once + TS_ASSERT(d_registered.find(n) == d_registered.end()); + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + // check that registerTerm() is called in reverse topological order + TS_ASSERT(d_registered.find(*i) != d_registered.end()); + } + + d_registered.insert(n); + } - Node getWrapper(){ + Node getWrapper() { Node n = get(); d_getSequence.push_back(n); return n; } - bool doneWrapper(){ + bool doneWrapper() { return done(); } - void check(Effort e){ - while(!done()){ + void check(Effort e) { + while(!done()) { getWrapper(); } } - void preRegisterTerm(TNode n ){} - void propagate(Effort level = FULL_EFFORT){} - void explain(TNode n, Effort level = FULL_EFFORT){} - + void preRegisterTerm(TNode n) {} + void propagate(Effort level) {} + void explain(TNode n, Effort level) {} }; class TheoryBlack : public CxxTest::TestSuite { @@ -132,7 +139,7 @@ class TheoryBlack : public CxxTest::TestSuite { public: - TheoryBlack() { } + TheoryBlack() {} void setUp() { d_nm = new NodeManager(); @@ -187,15 +194,13 @@ public: TS_ASSERT( Theory::quickCheckOrMore(s)); TS_ASSERT( Theory::quickCheckOrMore(f)); - TS_ASSERT(!Theory::standardEffortOrMore(m)); TS_ASSERT(!Theory::standardEffortOrMore(q)); TS_ASSERT( Theory::standardEffortOrMore(s)); TS_ASSERT( Theory::standardEffortOrMore(f)); - } - void testDone(){ + void testDone() { TS_ASSERT(d_dummy->doneWrapper()); d_dummy->assertFact(atom0); @@ -208,7 +213,7 @@ public: TS_ASSERT(d_dummy->doneWrapper()); } - void testRegisterSequence(){ + void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); Node x = d_nm->mkVar(); @@ -218,7 +223,6 @@ public: Node f_x_eq_x = f_x.eqNode(x); Node x_eq_f_f_x = x.eqNode(f_f_x); - d_dummy->assertFact(f_x_eq_x); d_dummy->assertFact(x_eq_f_f_x); @@ -226,11 +230,13 @@ public: TS_ASSERT_EQUALS(got, f_x_eq_x); - TS_ASSERT_EQUALS(4, d_dummy-> d_registerSequence.size()); - TS_ASSERT_EQUALS(x, d_dummy-> d_registerSequence[0]); - TS_ASSERT_EQUALS(f, d_dummy-> d_registerSequence[1]); - TS_ASSERT_EQUALS(f_x, d_dummy-> d_registerSequence[2]); - TS_ASSERT_EQUALS(f_x_eq_x, d_dummy-> d_registerSequence[3]); + TS_ASSERT_EQUALS(4, d_dummy->d_registered.size()); + TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end()); TS_ASSERT(!d_dummy->doneWrapper()); @@ -238,15 +244,14 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(6, d_dummy-> d_registerSequence.size()); - TS_ASSERT_EQUALS(f_f_x, d_dummy-> d_registerSequence[4]); - TS_ASSERT_EQUALS(x_eq_f_f_x, d_dummy-> d_registerSequence[5]); + TS_ASSERT_EQUALS(6, d_dummy->d_registered.size()); + TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->doneWrapper()); } - - void testOutputChannelAccessors(){ + void testOutputChannelAccessors() { /* void setOutputChannel(OutputChannel& out) */ /* OutputChannel& getOutputChannel() */ @@ -261,7 +266,5 @@ public: const OutputChannel& oc = d_dummy->getOutputChannel(); TS_ASSERT_EQUALS(&oc, &theOtherChannel); - } - }; |