From b212e64555954532b93db2b64a863d107a4a127d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 12 Jan 2021 09:36:46 -0800 Subject: [PATCH] google test: expr: Migrate node_black. (#5764) --- test/unit/expr/CMakeLists.txt | 2 +- test/unit/expr/node_black.cpp | 785 ++++++++++++++++++++++++++++++++++ test/unit/expr/node_black.h | 783 --------------------------------- 3 files changed, 786 insertions(+), 784 deletions(-) create mode 100644 test/unit/expr/node_black.cpp delete mode 100644 test/unit/expr/node_black.h diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 440874166..aa7e06ef0 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -15,7 +15,7 @@ cvc4_add_unit_test_black(attribute_black expr) cvc4_add_unit_test_white(attribute_white expr) cvc4_add_unit_test_black(kind_black expr) cvc4_add_unit_test_black(kind_map_black expr) -cvc4_add_cxx_unit_test_black(node_black expr) +cvc4_add_unit_test_black(node_black expr) cvc4_add_unit_test_black(node_algorithm_black expr) cvc4_add_cxx_unit_test_black(node_builder_black expr) cvc4_add_cxx_unit_test_black(node_manager_black expr) diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp new file mode 100644 index 000000000..d45cf603f --- /dev/null +++ b/test/unit/expr/node_black.cpp @@ -0,0 +1,785 @@ +/********************* */ +/*! \file node_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of CVC4::Node. + ** + ** Black box testing of CVC4::Node. + **/ + +#include +#include +#include +#include + +#include "api/cvc4cpp.h" +#include "expr/dtype.h" +#include "expr/expr_manager.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node_value.h" +#include "smt/smt_engine.h" +#include "test_node.h" +#include "test_utils.h" +#include "theory/rewriter.h" + +namespace CVC4 { + +using namespace CVC4::kind; + +namespace test { + +namespace { +/** Returns N skolem nodes from 'nodeManager' with the same `type`. */ +std::vector makeNSkolemNodes(NodeManager* nodeManager, + uint32_t n, + TypeNode type) +{ + std::vector skolems; + for (uint32_t i = 0; i < n; i++) + { + skolems.push_back(nodeManager->mkSkolem( + "skolem_", type, "Created by makeNSkolemNodes()")); + } + return skolems; +} +} // namespace + +class TestNodeBlackNode : public TestNodeBlack +{ + protected: + void SetUp() override + { + TestNodeBlack::SetUp(); + // setup an SMT engine so that options are in scope + Options opts; + char* argv[2]; + argv[0] = strdup(""); + argv[1] = strdup("--output-lang=ast"); + Options::parseOptions(&opts, 2, argv); + free(argv[0]); + free(argv[1]); + d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts)); + } + + std::unique_ptr d_smt; + + bool imp(bool a, bool b) const { return (!a) || (b); } + bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); } + + void testNaryExpForSize(Kind k, uint32_t n) + { + NodeBuilder<> nbz(k); + Node trueNode = d_nodeManager->mkConst(true); + for (uint32_t i = 0; i < n; ++i) + { + nbz << trueNode; + } + Node result = nbz; + ASSERT_EQ(n, result.getNumChildren()); + } +}; + +TEST_F(TestNodeBlackNode, null) { Node::null(); } + +TEST_F(TestNodeBlackNode, is_null) +{ + Node a = Node::null(); + ASSERT_TRUE(a.isNull()); + + Node b = Node(); + ASSERT_TRUE(b.isNull()); + + Node c = b; + ASSERT_TRUE(c.isNull()); +} + +TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); } + +TEST_F(TestNodeBlackNode, dtor) +{ + /* No access to internals? Only test that this is crash free. */ + Node* n; + ASSERT_NO_FATAL_FAILURE(n = new Node()); + delete n; +} + +/* operator== */ +TEST_F(TestNodeBlackNode, operator_equals) +{ + Node a, b, c; + + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + + a = b; + c = a; + + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + + ASSERT_TRUE(a == a); + ASSERT_TRUE(a == b); + ASSERT_TRUE(a == c); + + ASSERT_TRUE(b == a); + ASSERT_TRUE(b == b); + ASSERT_TRUE(b == c); + + ASSERT_TRUE(c == a); + ASSERT_TRUE(c == b); + ASSERT_TRUE(c == c); + + ASSERT_TRUE(d == d); + + ASSERT_FALSE(d == a); + ASSERT_FALSE(d == b); + ASSERT_FALSE(d == c); + + ASSERT_FALSE(a == d); + ASSERT_FALSE(b == d); + ASSERT_FALSE(c == d); +} + +/* operator!= */ +TEST_F(TestNodeBlackNode, operator_not_equals) +{ + Node a, b, c; + + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + + a = b; + c = a; + + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + + /*structed assuming operator == works */ + ASSERT_TRUE(iff(a != a, !(a == a))); + ASSERT_TRUE(iff(a != b, !(a == b))); + ASSERT_TRUE(iff(a != c, !(a == c))); + + ASSERT_TRUE(iff(b != a, !(b == a))); + ASSERT_TRUE(iff(b != b, !(b == b))); + ASSERT_TRUE(iff(b != c, !(b == c))); + + ASSERT_TRUE(iff(c != a, !(c == a))); + ASSERT_TRUE(iff(c != b, !(c == b))); + ASSERT_TRUE(iff(c != c, !(c == c))); + + ASSERT_TRUE(!(d != d)); + + ASSERT_TRUE(d != a); + ASSERT_TRUE(d != b); + ASSERT_TRUE(d != c); +} + +/* operator[] */ +TEST_F(TestNodeBlackNode, operator_square) +{ +#ifdef CVC4_ASSERTIONS + // Basic bounds check on a node w/out children + ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren"); + ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren"); +#endif + + // Basic access check + Node tb = d_nodeManager->mkConst(true); + Node eb = d_nodeManager->mkConst(false); + Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + Node ite = cnd.iteNode(tb, eb); + + ASSERT_EQ(tb, cnd[0]); + ASSERT_EQ(eb, cnd[1]); + + ASSERT_EQ(cnd, ite[0]); + ASSERT_EQ(tb, ite[1]); + ASSERT_EQ(eb, ite[2]); + +#ifdef CVC4_ASSERTIONS + // Bounds check on a node with children + ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren"); + ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren"); +#endif +} + +/* operator= */ +TEST_F(TestNodeBlackNode, operator_assign) +{ + Node a, b; + Node c = d_nodeManager->mkNode( + NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); + + b = c; + ASSERT_EQ(b, c); + + a = b = c; + + ASSERT_EQ(a, b); + ASSERT_EQ(a, c); +} + +/* operator< */ +TEST_F(TestNodeBlackNode, operator_less_than) +{ + // We don't have access to the ids so we can't test the implementation + // in the black box tests. + + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + + ASSERT_TRUE(a < b || b < a); + ASSERT_TRUE(!(a < b && b < a)); + + Node c = d_nodeManager->mkNode(AND, a, b); + Node d = d_nodeManager->mkNode(AND, a, b); + + ASSERT_FALSE(c < d); + ASSERT_FALSE(d < c); + + // simple test of descending descendant property + Node child = d_nodeManager->mkConst(true); + Node parent = d_nodeManager->mkNode(NOT, child); + + ASSERT_TRUE(child < parent); + + // slightly less simple test of DD property + std::vector chain; + const int N = 500; + Node curr = d_nodeManager->mkNode(OR, a, b); + chain.push_back(curr); + 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]; + ASSERT_TRUE(chain_i < chain_j); + } + } +} + +TEST_F(TestNodeBlackNode, eqNode) +{ + TypeNode t = d_nodeManager->mkSort(); + Node left = d_nodeManager->mkSkolem("left", t); + Node right = d_nodeManager->mkSkolem("right", t); + Node eq = left.eqNode(right); + + ASSERT_EQ(EQUAL, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(eq[0], left); + ASSERT_EQ(eq[1], right); +} + +TEST_F(TestNodeBlackNode, notNode) +{ + Node child = d_nodeManager->mkConst(true); + Node parent = child.notNode(); + + ASSERT_EQ(NOT, parent.getKind()); + ASSERT_EQ(1, parent.getNumChildren()); + + ASSERT_EQ(parent[0], child); +} + +TEST_F(TestNodeBlackNode, andNode) +{ + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); + Node eq = left.andNode(right); + + ASSERT_EQ(AND, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(*(eq.begin()), left); + ASSERT_EQ(*(++eq.begin()), right); +} + +TEST_F(TestNodeBlackNode, orNode) +{ + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); + Node eq = left.orNode(right); + + ASSERT_EQ(OR, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(*(eq.begin()), left); + ASSERT_EQ(*(++eq.begin()), right); +} + +TEST_F(TestNodeBlackNode, iteNode) +{ + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + + Node cnd = d_nodeManager->mkNode(OR, a, b); + Node thenBranch = d_nodeManager->mkConst(true); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); + Node ite = cnd.iteNode(thenBranch, elseBranch); + + ASSERT_EQ(ITE, ite.getKind()); + ASSERT_EQ(3, ite.getNumChildren()); + + ASSERT_EQ(*(ite.begin()), cnd); + ASSERT_EQ(*(++ite.begin()), thenBranch); + ASSERT_EQ(*(++(++ite.begin())), elseBranch); +} + +TEST_F(TestNodeBlackNode, iffNode) +{ + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); + Node eq = left.eqNode(right); + + ASSERT_EQ(EQUAL, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(*(eq.begin()), left); + ASSERT_EQ(*(++eq.begin()), right); +} + +TEST_F(TestNodeBlackNode, impNode) +{ + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); + Node eq = left.impNode(right); + + ASSERT_EQ(IMPLIES, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(*(eq.begin()), left); + ASSERT_EQ(*(++eq.begin()), right); +} + +TEST_F(TestNodeBlackNode, xorNode) +{ + Node left = d_nodeManager->mkConst(true); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false))); + Node eq = left.xorNode(right); + + ASSERT_EQ(XOR, eq.getKind()); + ASSERT_EQ(2, eq.getNumChildren()); + + ASSERT_EQ(*(eq.begin()), left); + ASSERT_EQ(*(++eq.begin()), right); +} + +TEST_F(TestNodeBlackNode, getKind) +{ + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + + Node n = d_nodeManager->mkNode(NOT, a); + ASSERT_EQ(NOT, n.getKind()); + + n = d_nodeManager->mkNode(EQUAL, a, b); + ASSERT_EQ(EQUAL, n.getKind()); + + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); + + n = d_nodeManager->mkNode(PLUS, x, y); + ASSERT_EQ(PLUS, n.getKind()); + + n = d_nodeManager->mkNode(UMINUS, x); + ASSERT_EQ(UMINUS, n.getKind()); +} + +TEST_F(TestNodeBlackNode, getOperator) +{ + TypeNode sort = d_nodeManager->mkSort("T"); + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); + + Node f = d_nodeManager->mkSkolem("f", predType); + Node a = d_nodeManager->mkSkolem("a", sort); + Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); + + ASSERT_TRUE(fa.hasOperator()); + ASSERT_FALSE(f.hasOperator()); + ASSERT_FALSE(a.hasOperator()); + + ASSERT_EQ(fa.getNumChildren(), 1); + ASSERT_EQ(f.getNumChildren(), 0); + ASSERT_EQ(a.getNumChildren(), 0); + + ASSERT_EQ(f, fa.getOperator()); +#ifdef CVC4_ASSERTIONS + ASSERT_THROW(f.getOperator(), IllegalArgumentException); + ASSERT_THROW(a.getOperator(), IllegalArgumentException); +#endif +} + +TEST_F(TestNodeBlackNode, getNumChildren) +{ + Node trueNode = d_nodeManager->mkConst(true); + + ASSERT_EQ(0, (Node::null()).getNumChildren()); + ASSERT_EQ(1, trueNode.notNode().getNumChildren()); + ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren()); + + srand(0); + for (uint32_t i = 0; i < 500; ++i) + { + uint32_t n = rand() % 1000 + 2; + testNaryExpForSize(AND, n); + } + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(testNaryExpForSize(AND, 0), + "getNumChildren\\(\\) >= " + "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(AND, 1), + "getNumChildren\\(\\) >= " + "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(NOT, 0), + "getNumChildren\\(\\) >= " + "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(NOT, 2), + "getNumChildren\\(\\) <= " + "kind::metakind::getUpperBoundForKind\\(getKind\\(\\)\\)"); +#endif /* CVC4_ASSERTIONS */ +} + +TEST_F(TestNodeBlackNode, iterator) +{ + NodeBuilder<> b; + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); + Node n = b << x << y << z << kind::AND; + + { // iterator + Node::iterator i = n.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, n.end()); + } + + { // same for const iterator + const Node& c = n; + Node::const_iterator i = c.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, n.end()); + } +} + +TEST_F(TestNodeBlackNode, kinded_iterator) +{ + TypeNode integerType = d_nodeManager->integerType(); + + Node x = d_nodeManager->mkSkolem("x", integerType); + Node y = d_nodeManager->mkSkolem("y", integerType); + Node z = d_nodeManager->mkSkolem("z", integerType); + 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 + Node::kinded_iterator i = plus_x_y_z.begin(PLUS); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_TRUE(i == plus_x_y_z.end(PLUS)); + + i = x.begin(PLUS); + ASSERT_EQ(*i++, x); + ASSERT_TRUE(i == x.end(PLUS)); + } +} + +TEST_F(TestNodeBlackNode, toString) +{ + 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 m = NodeBuilder<>() << w << x << kind::OR; + Node n = NodeBuilder<>() << m << y << z << kind::AND; + + ASSERT_EQ(n.toString(), "(AND (OR w x) y z)"); +} + +TEST_F(TestNodeBlackNode, toStream) +{ + 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 m = NodeBuilder<>() << x << y << kind::OR; + Node n = NodeBuilder<>() << w << m << z << kind::AND; + Node o = NodeBuilder<>() << n << n << kind::XOR; + + std::stringstream sstr; + sstr << Node::dag(false); + n.toStream(sstr); + ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)"); + + sstr.str(std::string()); + o.toStream(sstr, -1, 0); + ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(std::string()); + sstr << n; + ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)"); + + sstr.str(std::string()); + sstr << o; + ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(std::string()); + sstr << Node::setdepth(0) << n; + ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)"); + + sstr.str(std::string()); + sstr << Node::setdepth(0) << o; + ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(std::string()); + sstr << Node::setdepth(1) << n; + ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)"); + + sstr.str(std::string()); + sstr << Node::setdepth(1) << o; + ASSERT_EQ(sstr.str(), + "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); + + sstr.str(std::string()); + sstr << Node::setdepth(2) << n; + ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)"); + + sstr.str(std::string()); + sstr << Node::setdepth(2) << o; + ASSERT_EQ(sstr.str(), + "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); + + sstr.str(std::string()); + sstr << Node::setdepth(3) << n; + ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)"); + + sstr.str(std::string()); + sstr << Node::setdepth(3) << o; + ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); +} + +TEST_F(TestNodeBlackNode, dagifier) +{ + 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 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); + Node gy = d_nodeManager->mkNode(APPLY_UF, g, y); + Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx); + Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx); + Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx); + Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x); + Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y); + Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx); + 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); + + std::stringstream sstr; + sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4); + sstr << Node::dag(false) << n; // never dagify + ASSERT_EQ(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))"); +} + +TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (Node child : add) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (TNode child : add) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 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); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 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); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, isConst) +{ + // more complicated "constants" exist in datatypes and arrays theories + DType list("list"); + std::shared_ptr consC = + std::make_shared("cons"); + consC->addArg("car", d_nodeManager->integerType()); + consC->addArgSelf("cdr"); + list.addConstructor(consC); + list.addConstructor(std::make_shared("nil")); + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const std::vector >& lcons = + listType.getDType().getConstructors(); + Node cons = lcons[0]->getConstructor(); + Node nil = lcons[1]->getConstructor(); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node cons_x_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + x, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_cons_2_nil = d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); + ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); + ASSERT_FALSE(cons_x_nil.isConst()); + ASSERT_TRUE(cons_1_nil.isConst()); + ASSERT_TRUE(cons_1_cons_2_nil.isConst()); + + TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + ASSERT_TRUE(arr.isConst()); + Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), + d_nodeManager->mkBitVectorType(1)); + zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); + one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + ASSERT_TRUE(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); +} + +namespace { +Node level0(NodeManager* nm) +{ + NodeBuilder<> nb(kind::AND); + Node x = nm->mkSkolem("x", nm->booleanType()); + nb << x; + nb << x; + return Node(nb.constructNode()); +} +TNode level1(NodeManager* nm) { return level0(nm); } +} // namespace + +/** + * This is for demonstrating what a certain type of user error looks like. + */ +TEST_F(TestNodeBlackNode, node_tnode_usage) +{ + Node n; + ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get())); + ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0"); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h deleted file mode 100644 index 4e4a39654..000000000 --- a/test/unit/expr/node_black.h +++ /dev/null @@ -1,783 +0,0 @@ -/********************* */ -/*! \file node_black.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Morgan Deters, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of CVC4::Node. - ** - ** Black box testing of CVC4::Node. - **/ - -#include - -// Used in some of the tests -#include -#include -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/dtype.h" -#include "expr/expr_manager.h" -#include "expr/node.h" -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "expr/node_value.h" -#include "smt/smt_engine.h" -#include "test_utils.h" -#include "theory/rewriter.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace std; - -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: - NodeManager* d_nodeManager; - api::Solver* d_slv; - public: - void setUp() override - { - // setup a SMT engine so that options are in scope - Options opts; - char* argv[2]; - argv[0] = strdup(""); - argv[1] = strdup("--output-lang=ast"); - Options::parseOptions(&opts, 2, argv); - free(argv[0]); - free(argv[1]); - - d_slv = new api::Solver(&opts); - d_nodeManager = d_slv->getSmtEngine()->getNodeManager(); - } - - void tearDown() override { - delete d_slv; - } - - 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 testIsNull() { - /* bool isNull() const; */ - - Node a = Node::null(); - TS_ASSERT(a.isNull()); - - Node b = Node(); - TS_ASSERT(b.isNull()); - - Node c = b; - - TS_ASSERT(c.isNull()); - } - - 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(); - delete n; - } - - /*tests: bool operator==(const Node& e) const */ - void testOperatorEquals() { - Node a, b, c; - - b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - - a = b; - c = a; - - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->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(d == 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_nodeManager->booleanType()); - - a = b; - c = a; - - Node d = d_nodeManager->mkSkolem("d", d_nodeManager->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(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(!(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 - TS_UTILS_EXPECT_ABORT(Node::null()[-1]); - TS_UTILS_EXPECT_ABORT(Node::null()[0]); -#endif /* CVC4_ASSERTIONS */ - - // Basic access check - Node tb = d_nodeManager->mkConst(true); - Node eb = d_nodeManager->mkConst(false); - Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - Node ite = cnd.iteNode(tb, eb); - - TS_ASSERT(tb == cnd[0]); - TS_ASSERT(eb == cnd[1]); - - TS_ASSERT(cnd == ite[0]); - TS_ASSERT(tb == ite[1]); - TS_ASSERT(eb == ite[2]); - -#ifdef CVC4_ASSERTIONS - // Bounds check on a node with children - TS_UTILS_EXPECT_ABORT(ite == ite[-1]); - TS_UTILS_EXPECT_ABORT(ite == ite[4]); -#endif /* CVC4_ASSERTIONS */ - } - - /*tests: Node& operator=(const Node&); */ - void testOperatorAssign() { - Node a, b; - Node c = d_nodeManager->mkNode( - NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); - - b = c; - TS_ASSERT(b == c); - - a = b = c; - - TS_ASSERT(a == b); - TS_ASSERT(a == c); - } - - void testOperatorLessThan() { - /* We don't have access to the ids so we can't test the implementation - * in the black box tests. */ - - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - - TS_ASSERT(a < b || b < a); - TS_ASSERT(!(a < b && b < a)); - - Node c = d_nodeManager->mkNode(AND, a, b); - Node d = d_nodeManager->mkNode(AND, a, b); - - TS_ASSERT(!(c < d)); - TS_ASSERT(!(d < c)); - - /* TODO: - * Less than has the rather difficult to test property that subexpressions - * are less than enclosing expressions. - * - * But what would be a convincing test of this property? - */ - - // simple test of descending descendant property - Node child = d_nodeManager->mkConst(true); - Node parent = d_nodeManager->mkNode(NOT, child); - - TS_ASSERT(child < parent); - - // slightly less simple test of DD property - std::vector chain; - const int N = 500; - Node curr = d_nodeManager->mkNode(OR, a, b); - chain.push_back(curr); - 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); - } - } - } - - void testEqNode() { - /* Node eqNode(const Node& right) const; */ - - TypeNode t = d_nodeManager->mkSort(); - Node left = d_nodeManager->mkSkolem("left", t); - Node right = d_nodeManager->mkSkolem("right", t); - Node eq = left.eqNode(right); - - TS_ASSERT(EQUAL == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); - - TS_ASSERT(eq[0] == left); - TS_ASSERT(eq[1] == right); - } - - void testNotNode() { - /* Node notNode() const; */ - - Node child = d_nodeManager->mkConst(true); - Node parent = child.notNode(); - - TS_ASSERT(NOT == parent.getKind()); - TS_ASSERT(1 == parent.getNumChildren()); - - TS_ASSERT(parent[0] == child); - } - void testAndNode() { - /*Node andNode(const Node& right) const;*/ - - Node left = d_nodeManager->mkConst(true); - 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(*(eq.begin()) == left); - TS_ASSERT(*(++eq.begin()) == right); - } - - void testOrNode() { - /*Node orNode(const Node& right) const;*/ - - Node left = d_nodeManager->mkConst(true); - 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(*(eq.begin()) == left); - TS_ASSERT(*(++eq.begin()) == right); - } - - void testIteNode() { - /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - - Node cnd = d_nodeManager->mkNode(OR, a, b); - Node thenBranch = d_nodeManager->mkConst(true); - Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false)); - Node ite = cnd.iteNode(thenBranch, elseBranch); - - TS_ASSERT(ITE == ite.getKind()); - TS_ASSERT(3 == ite.getNumChildren()); - - TS_ASSERT(*(ite.begin()) == cnd); - TS_ASSERT(*(++ite.begin()) == thenBranch); - TS_ASSERT(*(++(++ite.begin())) == elseBranch); - } - - void testIffNode() { - /* Node eqNode(const Node& right) const; */ - - Node left = d_nodeManager->mkConst(true); - 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(*(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()); - - TS_ASSERT(*(eq.begin()) == left); - TS_ASSERT(*(++eq.begin()) == right); - } - - void testXorNode() { - /*Node xorNode(const Node& right) const;*/ - Node left = d_nodeManager->mkConst(true); - 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(*(eq.begin()) == left); - TS_ASSERT(*(++eq.begin()) == right); - } - - void testGetKind() { - /*inline Kind getKind() const; */ - - Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); - Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); - - Node n = d_nodeManager->mkNode(NOT, a); - TS_ASSERT(NOT == n.getKind()); - - n = d_nodeManager->mkNode(EQUAL, a, b); - TS_ASSERT(EQUAL == n.getKind()); - - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); - - n = d_nodeManager->mkNode(PLUS, x, y); - TS_ASSERT(PLUS == n.getKind()); - - n = d_nodeManager->mkNode(UMINUS, x); - TS_ASSERT(UMINUS == n.getKind()); - } - - void testGetOperator() { - TypeNode sort = d_nodeManager->mkSort("T"); - TypeNode booleanType = d_nodeManager->booleanType(); - TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType); - - Node f = d_nodeManager->mkSkolem("f", predType); - 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.getNumChildren() == 1); - TS_ASSERT(f.getNumChildren() == 0); - TS_ASSERT(a.getNumChildren() == 0); - - TS_ASSERT(f == fa.getOperator()); -#ifdef CVC4_ASSERTIONS - 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) { - nbz << trueNode; - } - Node result = nbz; - TS_ASSERT(N == result.getNumChildren()); - } - - void testNumChildren() { - /*inline size_t getNumChildren() const;*/ - - Node trueNode = d_nodeManager->mkConst(true); - - // test 0 - TS_ASSERT(0 == (Node::null()).getNumChildren()); - - // test 1 - TS_ASSERT(1 == trueNode.notNode().getNumChildren()); - - // test 2 - TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren()); - - // Bigger tests - - srand(0); - int trials = 500; - for (int i = 0; i < trials; ++i) { - unsigned N = rand() % 1000 + 2; - testNaryExpForSize(AND, N); - } - -#ifdef CVC4_ASSERTIONS - TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 0)); - TS_UTILS_EXPECT_ABORT(testNaryExpForSize(AND, 1)); - TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 0)); - TS_UTILS_EXPECT_ABORT(testNaryExpForSize(NOT, 2)); -#endif /* CVC4_ASSERTIONS */ - } - - // test iterators - void testIterator() { - NodeBuilder<> b; - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); - Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); - Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); - Node n = b << x << y << z << kind::AND; - - { // iterator - Node::iterator i = n.begin(); - TS_ASSERT(*i++ == x); - TS_ASSERT(*i++ == y); - TS_ASSERT(*i++ == z); - TS_ASSERT(i == n.end()); - } - - { // same for const iterator - const Node& c = n; - Node::const_iterator i = c.begin(); - TS_ASSERT(*i++ == x); - TS_ASSERT(*i++ == y); - TS_ASSERT(*i++ == z); - TS_ASSERT(i == n.end()); - } - } - - // test the special "kinded-iterator" - void testKindedIterator() { - TypeNode integerType = d_nodeManager->integerType(); - - Node x = d_nodeManager->mkSkolem("x", integerType); - Node y = d_nodeManager->mkSkolem("y", integerType); - Node z = d_nodeManager->mkSkolem("z", integerType); - 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 - Node::kinded_iterator i = plus_x_y_z.begin(PLUS); - TS_ASSERT(*i++ == x); - TS_ASSERT(*i++ == y); - TS_ASSERT(*i++ == z); - TS_ASSERT(i == plus_x_y_z.end(PLUS)); - - i = x.begin(PLUS); - TS_ASSERT(*i++ == x); - TS_ASSERT(i == x.end(PLUS)); - } - } - - 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 m = NodeBuilder<>() << w << x << kind::OR; - Node n = NodeBuilder<>() << m << y << z << kind::AND; - - TS_ASSERT(n.toString() == "(AND (OR w x) y z)"); - } - - 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 m = NodeBuilder<>() << x << y << kind::OR; - Node n = NodeBuilder<>() << w << m << z << kind::AND; - Node o = NodeBuilder<>() << n << n << kind::XOR; - - stringstream sstr; - sstr << Node::dag(false); - n.toStream(sstr); - TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); - - sstr.str(string()); - o.toStream(sstr, -1, 0); - TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); - - sstr.str(string()); - sstr << n; - TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); - - sstr.str(string()); - sstr << o; - TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); - - sstr.str(string()); - sstr << Node::setdepth(0) << n; - TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); - - sstr.str(string()); - sstr << Node::setdepth(0) << o; - TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); - - sstr.str(string()); - sstr << Node::setdepth(1) << n; - TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)"); - - sstr.str(string()); - sstr << Node::setdepth(1) << o; - TS_ASSERT(sstr.str() == - "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); - - sstr.str(string()); - sstr << Node::setdepth(2) << n; - TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); - - sstr.str(string()); - sstr << Node::setdepth(2) << o; - TS_ASSERT(sstr.str() == - "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); - - sstr.str(string()); - sstr << Node::setdepth(3) << n; - TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); - - sstr.str(string()); - sstr << Node::setdepth(3) << o; - TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); - } - - void testDagifier() { - 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 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); - Node gy = d_nodeManager->mkNode(APPLY_UF, g, y); - Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx); - Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx); - Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx); - Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x); - Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y); - Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx); - 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); - - 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))"); - } - - 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())); - } - - void testIsConst() - { - // more complicated "constants" exist in datatypes and arrays theories - DType list("list"); - std::shared_ptr consC = - std::make_shared("cons"); - consC->addArg("car", d_nodeManager->integerType()); - consC->addArgSelf("cdr"); - list.addConstructor(consC); - list.addConstructor(std::make_shared("nil")); - TypeNode listType = d_nodeManager->mkDatatypeType(list); - const std::vector >& lcons = - listType.getDType().getConstructors(); - Node cons = lcons[0]->getConstructor(); - Node nil = lcons[1]->getConstructor(); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); - Node cons_x_nil = - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - x, - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); - Node cons_1_nil = - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); - Node cons_1_cons_2_nil = d_nodeManager->mkNode( - APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(2)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); - TS_ASSERT(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); - TS_ASSERT(!cons_x_nil.isConst()); - TS_ASSERT(cons_1_nil.isConst()); - TS_ASSERT(cons_1_cons_2_nil.isConst()); - - TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), - d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); - TS_ASSERT(storeAll.isConst()); - - Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); - TS_ASSERT(!arr.isConst()); - arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); - TS_ASSERT(arr.isConst()); - Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - TS_ASSERT(!arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - TS_ASSERT(!arr2.isConst()); - - arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), - d_nodeManager->mkBitVectorType(1)); - zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); - one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); - storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); - TS_ASSERT(storeAll.isConst()); - - arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); - TS_ASSERT(!arr.isConst()); - arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); - TS_ASSERT(arr.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - TS_ASSERT(!arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, one, one); - TS_ASSERT(!arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - TS_ASSERT(!arr2.isConst()); - } - - // 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_nodeManager->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; - // } -}; -- 2.30.2