From 2fcaf83bd8d93399cb1fb4bbfe3a252398d314c6 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 16 Oct 2017 11:22:21 -0700 Subject: Adds unit test that show Node and TNode work with for each loops. (#1230) Extends test/unit/expr/node_black.h with tests that show Node and TNode can work with C++11 for each loops. --- test/unit/expr/node_black.h | 401 ++++++++++++++++++++++++++------------------ 1 file changed, 234 insertions(+), 167 deletions(-) diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 618dd9e3d..49c7f4aa0 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -16,33 +16,48 @@ #include -//Used in some of the tests -#include +// Used in some of the tests +#include #include +#include +#include #include "expr/expr_manager.h" -#include "expr/node_value.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" +#include "expr/node_value.h" using namespace CVC4; using namespace CVC4::kind; using namespace std; -class NodeBlack : public CxxTest::TestSuite { -private: +namespace { +// Returns N skolem nodes from 'nodeManager' with the same `type`. +std::vector makeNSkolemNodes(NodeManager* nodeManager, int N, + TypeNode type) { + std::vector skolems; + for (int i = 0; i < N; i++) { + skolems.push_back(nodeManager->mkSkolem(/*prefix=*/"skolem_", type, + "Created by makeNSkolemNodes()")); + } + return skolems; +} + +} // namespace + +class NodeBlack : public CxxTest::TestSuite { + private: Options opts; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; TypeNode* d_realType; -public: - + public: void setUp() { - char *argv[2]; + char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); Options::parseOptions(&opts, 2, argv); @@ -62,16 +77,10 @@ public: delete d_nodeManager; } - bool imp(bool a, bool b) const { - return (!a) || (b); - } - bool iff(bool a, bool b) const { - return (a && b) || ((!a)&&(!b)); - } + bool imp(bool a, bool b) const { return (!a) || (b); } + bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); } - void testNull() { - Node::null(); - } + void testNull() { Node::null(); } void testIsNull() { /* bool isNull() const; */ @@ -87,18 +96,15 @@ public: TS_ASSERT(c.isNull()); } - void testCopyCtor() { - Node e(Node::null()); - } + void testCopyCtor() { Node e(Node::null()); } void testDestructor() { /* No access to internals ? * Makes sense to only test that this is crash free. */ - Node *n = new Node(); + Node* n = new Node(); delete n; - } /*tests: bool operator==(const Node& e) const */ @@ -112,37 +118,31 @@ public: Node d = d_nodeManager->mkSkolem("d", *d_booleanType); - TS_ASSERT(a==a); - TS_ASSERT(a==b); - TS_ASSERT(a==c); - - TS_ASSERT(b==a); - TS_ASSERT(b==b); - TS_ASSERT(b==c); - - - - TS_ASSERT(c==a); - TS_ASSERT(c==b); - TS_ASSERT(c==c); + TS_ASSERT(a == a); + TS_ASSERT(a == b); + TS_ASSERT(a == c); + TS_ASSERT(b == a); + TS_ASSERT(b == b); + TS_ASSERT(b == c); - TS_ASSERT(d==d); + TS_ASSERT(c == a); + TS_ASSERT(c == b); + TS_ASSERT(c == c); - TS_ASSERT(!(d==a)); - TS_ASSERT(!(d==b)); - TS_ASSERT(!(d==c)); + TS_ASSERT(d == d); - TS_ASSERT(!(a==d)); - TS_ASSERT(!(b==d)); - TS_ASSERT(!(c==d)); + TS_ASSERT(!(d == a)); + TS_ASSERT(!(d == b)); + TS_ASSERT(!(d == c)); + TS_ASSERT(!(a == d)); + TS_ASSERT(!(b == d)); + TS_ASSERT(!(c == d)); } /* operator!= */ void testOperatorNotEquals() { - - Node a, b, c; b = d_nodeManager->mkSkolem("b", *d_booleanType); @@ -153,38 +153,35 @@ public: Node d = d_nodeManager->mkSkolem("d", *d_booleanType); /*structed assuming operator == works */ - TS_ASSERT(iff(a!=a, !(a==a))); - TS_ASSERT(iff(a!=b, !(a==b))); - TS_ASSERT(iff(a!=c, !(a==c))); - + TS_ASSERT(iff(a != a, !(a == a))); + TS_ASSERT(iff(a != b, !(a == b))); + TS_ASSERT(iff(a != c, !(a == c))); - TS_ASSERT(iff(b!=a, !(b==a))); - TS_ASSERT(iff(b!=b, !(b==b))); - TS_ASSERT(iff(b!=c, !(b==c))); + TS_ASSERT(iff(b != a, !(b == a))); + TS_ASSERT(iff(b != b, !(b == b))); + TS_ASSERT(iff(b != c, !(b == c))); + TS_ASSERT(iff(c != a, !(c == a))); + TS_ASSERT(iff(c != b, !(c == b))); + TS_ASSERT(iff(c != c, !(c == c))); - TS_ASSERT(iff(c!=a, !(c==a))); - TS_ASSERT(iff(c!=b, !(c==b))); - TS_ASSERT(iff(c!=c, !(c==c))); - - TS_ASSERT(!(d!=d)); - - TS_ASSERT(d!=a); - TS_ASSERT(d!=b); - TS_ASSERT(d!=c); + TS_ASSERT(!(d != d)); + TS_ASSERT(d != a); + TS_ASSERT(d != b); + TS_ASSERT(d != c); } void testOperatorSquare() { /*Node operator[](int i) const */ #ifdef CVC4_ASSERTIONS - //Basic bounds check on a node w/out children + // Basic bounds check on a node w/out children TS_ASSERT_THROWS(Node::null()[-1], AssertionException); TS_ASSERT_THROWS(Node::null()[0], AssertionException); #endif /* CVC4_ASSERTIONS */ - //Basic access check + // Basic access check Node tb = d_nodeManager->mkConst(true); Node eb = d_nodeManager->mkConst(false); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); @@ -198,7 +195,7 @@ public: TS_ASSERT(eb == ite[2]); #ifdef CVC4_ASSERTIONS - //Bounds check on a node with children + // Bounds check on a node with children TS_ASSERT_THROWS(ite == ite[-1], AssertionException); TS_ASSERT_THROWS(ite == ite[4], AssertionException); #endif /* CVC4_ASSERTIONS */ @@ -207,16 +204,16 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkSkolem("c", *d_booleanType)); + Node c = d_nodeManager->mkNode( + NOT, d_nodeManager->mkSkolem("c", *d_booleanType)); b = c; - TS_ASSERT(b==c); - + TS_ASSERT(b == c); a = b = c; - TS_ASSERT(a==b); - TS_ASSERT(a==c); + TS_ASSERT(a == b); + TS_ASSERT(a == c); } void testOperatorLessThan() { @@ -226,14 +223,14 @@ public: Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - TS_ASSERT(amkNode(AND, a, b); Node d = d_nodeManager->mkNode(AND, a, b); - TS_ASSERT(!(cmkNode(OR, a, b); chain.push_back(curr); - for(int i = 0; i < N; ++i) { + for (int i = 0; i < N; ++i) { curr = d_nodeManager->mkNode(AND, curr, curr); chain.push_back(curr); } - for(int i = 0; i < N; ++i) { - for(int j = i + 1; j < N; ++j) { - Node chain_i = chain[i]; - Node chain_j = chain[j]; - TS_ASSERT(chain_i < chain_j); + for (int i = 0; i < N; ++i) { + for (int j = i + 1; j < N; ++j) { + Node chain_i = chain[i]; + Node chain_j = chain[j]; + TS_ASSERT(chain_i < chain_j); } } } @@ -289,10 +286,9 @@ public: Node parent = child.notNode(); TS_ASSERT(NOT == parent.getKind()); - TS_ASSERT(1 == parent.getNumChildren()); + TS_ASSERT(1 == parent.getNumChildren()); TS_ASSERT(parent[0] == child); - } void testAndNode() { /*Node andNode(const Node& right) const;*/ @@ -301,13 +297,11 @@ public: Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.andNode(right); - TS_ASSERT(AND == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); - } void testOrNode() { @@ -317,13 +311,11 @@ public: Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.orNode(right); - - TS_ASSERT(OR == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(OR == eq.getKind()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); - } void testIteNode() { @@ -352,22 +344,19 @@ public: Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.eqNode(right); - TS_ASSERT(EQUAL == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); } - void testImpNode() { /* Node impNode(const Node& right) const; */ Node left = d_nodeManager->mkConst(true); Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.impNode(right); - TS_ASSERT(IMPLIES == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -381,9 +370,8 @@ public: Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); Node eq = left.xorNode(right); - TS_ASSERT(XOR == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); @@ -420,29 +408,29 @@ public: Node a = d_nodeManager->mkSkolem("a", sort); Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); - TS_ASSERT( fa.hasOperator() ); - TS_ASSERT( !f.hasOperator() ); - TS_ASSERT( !a.hasOperator() ); + TS_ASSERT(fa.hasOperator()); + TS_ASSERT(!f.hasOperator()); + TS_ASSERT(!a.hasOperator()); - TS_ASSERT( fa.getNumChildren() == 1 ); - TS_ASSERT( f.getNumChildren() == 0 ); - TS_ASSERT( a.getNumChildren() == 0 ); + TS_ASSERT(fa.getNumChildren() == 1); + TS_ASSERT(f.getNumChildren() == 0); + TS_ASSERT(a.getNumChildren() == 0); - TS_ASSERT( f == fa.getOperator() ); + TS_ASSERT(f == fa.getOperator()); #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( f.getOperator(), IllegalArgumentException ); - TS_ASSERT_THROWS( a.getOperator(), IllegalArgumentException ); + TS_ASSERT_THROWS(f.getOperator(), IllegalArgumentException); + TS_ASSERT_THROWS(a.getOperator(), IllegalArgumentException); #endif /* CVC4_ASSERTIONS */ } void testNaryExpForSize(Kind k, unsigned N) { NodeBuilder<> nbz(k); Node trueNode = d_nodeManager->mkConst(true); - for(unsigned i = 0; i < N; ++i) { + for (unsigned i = 0; i < N; ++i) { nbz << trueNode; } Node result = nbz; - TS_ASSERT( N == result.getNumChildren() ); + TS_ASSERT(N == result.getNumChildren()); } void testNumChildren() { @@ -450,29 +438,29 @@ public: Node trueNode = d_nodeManager->mkConst(true); - //test 0 + // test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); - //test 1 + // test 1 TS_ASSERT(1 == trueNode.notNode().getNumChildren()); - //test 2 + // test 2 TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren()); - //Bigger tests + // Bigger tests srand(0); int trials = 500; - for(int i = 0; i < trials; ++i) { + for (int i = 0; i < trials; ++i) { unsigned N = rand() % 1000 + 2; testNaryExpForSize(AND, N); } #ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( testNaryExpForSize(AND, 0), AssertionException ); - TS_ASSERT_THROWS( testNaryExpForSize(AND, 1), AssertionException ); - TS_ASSERT_THROWS( testNaryExpForSize(NOT, 0), AssertionException ); - TS_ASSERT_THROWS( testNaryExpForSize(NOT, 2), AssertionException ); + TS_ASSERT_THROWS(testNaryExpForSize(AND, 0), AssertionException); + TS_ASSERT_THROWS(testNaryExpForSize(AND, 1), AssertionException); + TS_ASSERT_THROWS(testNaryExpForSize(NOT, 0), AssertionException); + TS_ASSERT_THROWS(testNaryExpForSize(NOT, 2), AssertionException); #endif /* CVC4_ASSERTIONS */ } @@ -484,7 +472,7 @@ public: Node z = d_nodeManager->mkSkolem("z", *d_booleanType); Node n = b << x << y << z << kind::AND; - { // iterator + { // iterator Node::iterator i = n.begin(); TS_ASSERT(*i++ == x); TS_ASSERT(*i++ == y); @@ -492,7 +480,7 @@ public: TS_ASSERT(i == n.end()); } - { // same for const iterator + { // same for const iterator const Node& c = n; Node::const_iterator i = c.begin(); TS_ASSERT(*i++ == x); @@ -512,7 +500,7 @@ public: Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z); Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y); - { // iterator + { // iterator Node::kinded_iterator i = plus_x_y_z.begin(PLUS); TS_ASSERT(*i++ == x); TS_ASSERT(*i++ == y); @@ -528,10 +516,14 @@ public: void testToString() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node w = d_nodeManager->mkSkolem("w", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node x = d_nodeManager->mkSkolem("x", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node z = d_nodeManager->mkSkolem("z", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -541,10 +533,14 @@ public: void testToStream() { TypeNode booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkSkolem("w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node x = d_nodeManager->mkSkolem("x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem("y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node z = d_nodeManager->mkSkolem("z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); + Node w = d_nodeManager->mkSkolem("w", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node x = d_nodeManager->mkSkolem("x", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node z = d_nodeManager->mkSkolem("z", booleanType, "", + NodeManager::SKOLEM_EXACT_NAME); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; @@ -580,7 +576,8 @@ public: sstr.str(string()); sstr << Node::setdepth(1) << o; - TS_ASSERT(sstr.str() == "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); + TS_ASSERT(sstr.str() == + "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); sstr.str(string()); sstr << Node::setdepth(2) << n; @@ -588,7 +585,8 @@ public: sstr.str(string()); sstr << Node::setdepth(2) << o; - TS_ASSERT(sstr.str() == "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); + TS_ASSERT(sstr.str() == + "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); sstr.str(string()); sstr << Node::setdepth(3) << n; @@ -603,10 +601,14 @@ public: TypeNode intType = d_nodeManager->integerType(); TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType); - Node x = d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node y = d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME); - Node f = d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME); - Node g = d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME); + Node x = d_nodeManager->mkSkolem("x", intType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node y = d_nodeManager->mkSkolem("y", intType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node f = d_nodeManager->mkSkolem("f", fnType, "", + NodeManager::SKOLEM_EXACT_NAME); + Node g = d_nodeManager->mkSkolem("g", fnType, "", + NodeManager::SKOLEM_EXACT_NAME); Node fx = d_nodeManager->mkNode(APPLY_UF, f, x); Node fy = d_nodeManager->mkNode(APPLY_UF, f, y); Node gx = d_nodeManager->mkNode(APPLY_UF, g, x); @@ -620,49 +622,114 @@ public: Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y); Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy); - Node n = d_nodeManager->mkNode(OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy); + Node n = d_nodeManager->mkNode(OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, + fgx_eq_gy); stringstream sstr; - sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4); - sstr << Node::dag(false) << n; // never dagify - TS_ASSERT(sstr.str() == "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = y) OR (f(g(x)) = g(y))"); + sstr << Node::setdepth(-1) + << Node::setlanguage(language::output::LANG_CVC4); + sstr << Node::dag(false) << n; // never dagify + TS_ASSERT(sstr.str() == + "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = " + "y) OR (f(g(x)) = g(y))"); sstr.str(string()); - sstr << Node::dag(true) << n; // always dagify - TS_ASSERT(sstr.str() == "LET _let_0 = f(x), _let_1 = g(x), _let_2 = f(f(_let_0)) IN (_let_2 = x) OR (_let_2 = y) OR (_let_0 = _let_1) OR (x = y) OR (f(_let_1) = g(y))"); + sstr << Node::dag(true) << n; // always dagify + TS_ASSERT(sstr.str() == + "LET _let_0 = f(x), _let_1 = g(x), _let_2 = f(f(_let_0)) IN " + "(_let_2 = x) OR (_let_2 = y) OR (_let_0 = _let_1) OR (x = y) OR " + "(f(_let_1) = g(y))"); sstr.str(string()); - sstr << Node::dag(2) << n; // dagify subexprs occurring > 2 times - TS_ASSERT(sstr.str() == "LET _let_0 = f(x) IN (f(f(_let_0)) = x) OR (f(f(_let_0)) = y) OR (_let_0 = g(x)) OR (x = y) OR (f(g(x)) = g(y))"); - - Warning() << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) << n << std::endl; + sstr << Node::dag(2) << n; // dagify subexprs occurring > 2 times + TS_ASSERT(sstr.str() == + "LET _let_0 = f(x) IN (f(f(_let_0)) = x) OR (f(f(_let_0)) = y) " + "OR (_let_0 = g(x)) OR (x = y) OR (f(g(x)) = g(y))"); + + Warning() << Node::setdepth(-1) + << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) + << n << std::endl; sstr.str(string()); - sstr << Node::dag(3) << n; // dagify subexprs occurring > 3 times - TS_ASSERT(sstr.str() == "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = y) OR (f(g(x)) = g(y))"); - Warning() << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) << n << std::endl; + sstr << Node::dag(3) << n; // dagify subexprs occurring > 3 times + TS_ASSERT(sstr.str() == + "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = " + "y) OR (f(g(x)) = g(y))"); + Warning() << Node::setdepth(-1) + << Node::setlanguage(language::output::LANG_CVC4) << Node::dag(2) + << n << std::endl; + } + + void testForEachOverNodeAsNodes() { + const std::vector skolems = + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (Node child : add) { + children.push_back(child); + } + TS_ASSERT(children.size() == skolems.size() && + std::equal(children.begin(), children.end(), skolems.begin())); + } + + void testForEachOverNodeAsTNodes() { + const std::vector skolems = + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (TNode child : add) { + children.push_back(child); + } + TS_ASSERT(children.size() == skolems.size() && + std::equal(children.begin(), children.end(), skolems.begin())); + } + + void testForEachOverTNodeAsNode() { + const std::vector skolems = + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); + Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + TNode add_tnode = add_node; + std::vector children; + for (Node child : add_tnode) { + children.push_back(child); + } + TS_ASSERT(children.size() == skolems.size() && + std::equal(children.begin(), children.end(), skolems.begin())); + } + + void testForEachOverTNodeAsTNodes() { + const std::vector skolems = + makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType()); + Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + TNode add_tnode = add_node; + std::vector children; + for (TNode child : add_tnode) { + children.push_back(child); + } + TS_ASSERT(children.size() == skolems.size() && + std::equal(children.begin(), children.end(), skolems.begin())); } -// This Test is designed to fail in a way that will cause a segfault, -// so it is commented out. -// This is for demonstrating what a certain type of user error looks like. -// Node level0(){ -// NodeBuilder<> nb(kind::AND); -// Node x = d_nodeManager->mkSkolem("x", *d_booleanType); -// nb << x; -// nb << x; -// return Node(nb.constructNode()); -// } - -// TNode level1(){ -// return level0(); -// } - -// void testChaining() { -// Node res = level1(); - -// TS_ASSERT(res.getKind() == kind::NULL_EXPR); -// TS_ASSERT(res != Node::null()); - -// cerr << "I finished both tests now watch as I crash" << endl; -// } + // This Test is designed to fail in a way that will cause a segfault, + // so it is commented out. + // This is for demonstrating what a certain type of user error looks like. + // Node level0(){ + // NodeBuilder<> nb(kind::AND); + // Node x = d_nodeManager->mkSkolem("x", *d_booleanType); + // nb << x; + // nb << x; + // return Node(nb.constructNode()); + // } + + // TNode level1(){ + // return level0(); + // } + + // void testChaining() { + // Node res = level1(); + + // TS_ASSERT(res.getKind() == kind::NULL_EXPR); + // TS_ASSERT(res != Node::null()); + + // cerr << "I finished both tests now watch as I crash" << endl; + // } }; -- cgit v1.2.3