diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-17 11:07:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-17 18:07:48 +0000 |
commit | bbf9eee55db6851c0923252cdda8946030c3c75a (patch) | |
tree | 52d3f04010f61784a3494e5de27d6e70c20b9abb /test/unit/node | |
parent | fe72d5a3fce499092c842b48df997eb0aa54fc05 (diff) |
Rename test/unit/expr to test/unit/node. (#6156)
This is in preparation for renaming src/expr to src/node.
Diffstat (limited to 'test/unit/node')
-rw-r--r-- | test/unit/node/CMakeLists.txt | 28 | ||||
-rw-r--r-- | test/unit/node/attribute_black.cpp | 128 | ||||
-rw-r--r-- | test/unit/node/attribute_white.cpp | 448 | ||||
-rw-r--r-- | test/unit/node/kind_black.cpp | 90 | ||||
-rw-r--r-- | test/unit/node/kind_map_black.cpp | 48 | ||||
-rw-r--r-- | test/unit/node/node_algorithm_black.cpp | 202 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 787 | ||||
-rw-r--r-- | test/unit/node/node_builder_black.cpp | 590 | ||||
-rw-r--r-- | test/unit/node/node_manager_black.cpp | 333 | ||||
-rw-r--r-- | test/unit/node/node_manager_white.cpp | 84 | ||||
-rw-r--r-- | test/unit/node/node_self_iterator_black.cpp | 57 | ||||
-rw-r--r-- | test/unit/node/node_traversal_black.cpp | 296 | ||||
-rw-r--r-- | test/unit/node/node_white.cpp | 82 | ||||
-rw-r--r-- | test/unit/node/symbol_table_black.cpp | 149 | ||||
-rw-r--r-- | test/unit/node/type_cardinality_black.cpp | 335 | ||||
-rw-r--r-- | test/unit/node/type_node_white.cpp | 97 |
16 files changed, 3754 insertions, 0 deletions
diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt new file mode 100644 index 000000000..52e591aeb --- /dev/null +++ b/test/unit/node/CMakeLists.txt @@ -0,0 +1,28 @@ +##################### +## CMakeLists.txt +## Top contributors (to current version): +## Aina Niemetz +## This file is part of the CVC4 project. +## Copyright (c) 2009-2021 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. +## +#-----------------------------------------------------------------------------# +# Add unit tests + +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_unit_test_black(node_black expr) +cvc4_add_unit_test_black(node_algorithm_black expr) +cvc4_add_unit_test_black(node_builder_black expr) +cvc4_add_unit_test_black(node_manager_black expr) +cvc4_add_unit_test_white(node_manager_white expr) +cvc4_add_unit_test_black(node_self_iterator_black expr) +cvc4_add_unit_test_black(node_traversal_black expr) +cvc4_add_unit_test_white(node_white expr) +cvc4_add_unit_test_black(symbol_table_black expr) +cvc4_add_unit_test_black(type_cardinality_black expr) +cvc4_add_unit_test_white(type_node_white expr) diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp new file mode 100644 index 000000000..487798e49 --- /dev/null +++ b/test/unit/node/attribute_black.cpp @@ -0,0 +1,128 @@ +/********************* */ +/*! \file attribute_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::Attribute. + ** + ** Black box testing of CVC4::Attribute. + **/ + +#include <sstream> +#include <vector> + +#include "expr/attribute.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_value.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace smt; + +namespace test { + +class TestNodeBlackAttribute : public TestNode +{ + protected: + struct PrimitiveIntAttributeId + { + }; + using PrimitiveIntAttribute = + expr::Attribute<PrimitiveIntAttributeId, uint64_t>; + struct TNodeAttributeId + { + }; + using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>; + struct StringAttributeId + { + }; + using StringAttribute = expr::Attribute<StringAttributeId, std::string>; + struct BoolAttributeId + { + }; + using BoolAttribute = expr::Attribute<BoolAttributeId, bool>; +}; + +TEST_F(TestNodeBlackAttribute, ints) +{ + TypeNode booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + const uint64_t val = 63489; + uint64_t data0 = 0; + uint64_t data1 = 0; + + PrimitiveIntAttribute attr; + ASSERT_FALSE(node->getAttribute(attr, data0)); + node->setAttribute(attr, val); + ASSERT_TRUE(node->getAttribute(attr, data1)); + ASSERT_EQ(data1, val); + + delete node; +} + +TEST_F(TestNodeBlackAttribute, tnodes) +{ + TypeNode booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + + Node val(d_nodeManager->mkSkolem("b", booleanType)); + TNode data0; + TNode data1; + + TNodeAttribute attr; + ASSERT_FALSE(node->getAttribute(attr, data0)); + node->setAttribute(attr, val); + ASSERT_TRUE(node->getAttribute(attr, data1)); + ASSERT_EQ(data1, val); + + delete node; +} + +TEST_F(TestNodeBlackAttribute, strings) +{ + TypeNode booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + + std::string val("63489"); + std::string data0; + std::string data1; + + StringAttribute attr; + ASSERT_FALSE(node->getAttribute(attr, data0)); + node->setAttribute(attr, val); + ASSERT_TRUE(node->getAttribute(attr, data1)); + ASSERT_EQ(data1, val); + + delete node; +} + +TEST_F(TestNodeBlackAttribute, bools) +{ + TypeNode booleanType = d_nodeManager->booleanType(); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); + + bool val = true; + bool data0 = false; + bool data1 = false; + + BoolAttribute attr; + ASSERT_TRUE(node->getAttribute(attr, data0)); + ASSERT_EQ(false, data0); + node->setAttribute(attr, val); + ASSERT_TRUE(node->getAttribute(attr, data1)); + ASSERT_EQ(data1, val); + + delete node; +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp new file mode 100644 index 000000000..fccb587db --- /dev/null +++ b/test/unit/node/attribute_white.cpp @@ -0,0 +1,448 @@ +/********************* */ +/*! \file attribute_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 White box testing of Node attributes. + ** + ** White box testing of Node attributes. + **/ + +#include <string> + +#include "base/check.h" +#include "expr/attribute.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" +#include "expr/node_value.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test_node.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" + +namespace CVC4 { + +using namespace kind; +using namespace smt; +using namespace expr; +using namespace expr::attr; + +namespace test { + +struct Test1; +struct Test2; +struct Test3; +struct Test4; +struct Test5; + +typedef Attribute<Test1, std::string> TestStringAttr1; +typedef Attribute<Test2, std::string> TestStringAttr2; + +using TestFlag1 = Attribute<Test1, bool>; +using TestFlag2 = Attribute<Test2, bool>; +using TestFlag3 = Attribute<Test3, bool>; +using TestFlag4 = Attribute<Test4, bool>; +using TestFlag5 = Attribute<Test5, bool>; + +class TestNodeWhiteAttribute : public TestNode +{ + protected: + void SetUp() override + { + TestNode::SetUp(); + d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); + } + std::unique_ptr<TypeNode> d_booleanType; +}; + +TEST_F(TestNodeWhiteAttribute, attribute_ids) +{ + // Test that IDs for (a subset of) attributes in the system are + // unique and that the LastAttributeId (which would be the next ID + // to assign) is greater than all attribute IDs. + + // We used to check ID assignments explicitly. However, between + // compilation modules, you don't get a strong guarantee + // (initialization order is somewhat implementation-specific, and + // anyway you'd have to change the tests anytime you add an + // attribute). So we back off, and just test that they're unique + // and that the next ID to be assigned is strictly greater than + // those that have already been assigned. + + unsigned lastId = attr::LastAttributeId<std::string, false>::getId(); + ASSERT_LT(VarNameAttr::s_id, lastId); + ASSERT_LT(TestStringAttr1::s_id, lastId); + ASSERT_LT(TestStringAttr2::s_id, lastId); + + ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id); + ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); + ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); + + lastId = attr::LastAttributeId<bool, false>::getId(); + ASSERT_LT(TestFlag1::s_id, lastId); + ASSERT_LT(TestFlag2::s_id, lastId); + ASSERT_LT(TestFlag3::s_id, lastId); + ASSERT_LT(TestFlag4::s_id, lastId); + ASSERT_LT(TestFlag5::s_id, lastId); + ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id); + ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id); + ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id); + + lastId = attr::LastAttributeId<TypeNode, false>::getId(); + ASSERT_LT(TypeAttr::s_id, lastId); +} + +TEST_F(TestNodeWhiteAttribute, attributes) +{ + Node a = d_nodeManager->mkVar(*d_booleanType); + Node b = d_nodeManager->mkVar(*d_booleanType); + Node c = d_nodeManager->mkVar(*d_booleanType); + Node unnamed = d_nodeManager->mkVar(*d_booleanType); + + a.setAttribute(VarNameAttr(), "a"); + b.setAttribute(VarNameAttr(), "b"); + c.setAttribute(VarNameAttr(), "c"); + + // test that all boolean flags are FALSE to start + Debug("boolattr") << "get flag 1 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag1())); + + Debug("boolattr") << "get flag 2 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag2())); + + Debug("boolattr") << "get flag 3 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag3())); + + Debug("boolattr") << "get flag 4 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag4())); + + Debug("boolattr") << "get flag 5 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag5())); + + // test that they all HAVE the boolean attributes + ASSERT_TRUE(a.hasAttribute(TestFlag1())); + ASSERT_TRUE(b.hasAttribute(TestFlag1())); + ASSERT_TRUE(c.hasAttribute(TestFlag1())); + ASSERT_TRUE(unnamed.hasAttribute(TestFlag1())); + + ASSERT_TRUE(a.hasAttribute(TestFlag2())); + ASSERT_TRUE(b.hasAttribute(TestFlag2())); + ASSERT_TRUE(c.hasAttribute(TestFlag2())); + ASSERT_TRUE(unnamed.hasAttribute(TestFlag2())); + + ASSERT_TRUE(a.hasAttribute(TestFlag3())); + ASSERT_TRUE(b.hasAttribute(TestFlag3())); + ASSERT_TRUE(c.hasAttribute(TestFlag3())); + ASSERT_TRUE(unnamed.hasAttribute(TestFlag3())); + + ASSERT_TRUE(a.hasAttribute(TestFlag4())); + ASSERT_TRUE(b.hasAttribute(TestFlag4())); + ASSERT_TRUE(c.hasAttribute(TestFlag4())); + ASSERT_TRUE(unnamed.hasAttribute(TestFlag4())); + + ASSERT_TRUE(a.hasAttribute(TestFlag5())); + ASSERT_TRUE(b.hasAttribute(TestFlag5())); + ASSERT_TRUE(c.hasAttribute(TestFlag5())); + ASSERT_TRUE(unnamed.hasAttribute(TestFlag5())); + + // test two-arg version of hasAttribute() + bool bb = false; + Debug("boolattr") << "get flag 1 on a (should be F)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag1(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag1(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag1(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag1(), bb)); + ASSERT_FALSE(bb); + + Debug("boolattr") << "get flag 2 on a (should be F)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag2(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 2 on b (should be F)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag2(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 2 on c (should be F)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag2(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag2(), bb)); + ASSERT_FALSE(bb); + + Debug("boolattr") << "get flag 3 on a (should be F)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag3(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 3 on b (should be F)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag3(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 3 on c (should be F)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag3(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag3(), bb)); + ASSERT_FALSE(bb); + + Debug("boolattr") << "get flag 4 on a (should be F)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag4(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 4 on b (should be F)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag4(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 4 on c (should be F)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag4(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag4(), bb)); + ASSERT_FALSE(bb); + + Debug("boolattr") << "get flag 5 on a (should be F)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag5(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 5 on b (should be F)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag5(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag5(), bb)); + ASSERT_FALSE(bb); + Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag5(), bb)); + ASSERT_FALSE(bb); + + // setting boolean flags + Debug("boolattr") << "set flag 1 on a to T\n"; + a.setAttribute(TestFlag1(), true); + Debug("boolattr") << "set flag 1 on b to F\n"; + b.setAttribute(TestFlag1(), false); + Debug("boolattr") << "set flag 1 on c to F\n"; + c.setAttribute(TestFlag1(), false); + Debug("boolattr") << "set flag 1 on unnamed to T\n"; + unnamed.setAttribute(TestFlag1(), true); + + Debug("boolattr") << "set flag 2 on a to F\n"; + a.setAttribute(TestFlag2(), false); + Debug("boolattr") << "set flag 2 on b to T\n"; + b.setAttribute(TestFlag2(), true); + Debug("boolattr") << "set flag 2 on c to T\n"; + c.setAttribute(TestFlag2(), true); + Debug("boolattr") << "set flag 2 on unnamed to F\n"; + unnamed.setAttribute(TestFlag2(), false); + + Debug("boolattr") << "set flag 3 on a to T\n"; + a.setAttribute(TestFlag3(), true); + Debug("boolattr") << "set flag 3 on b to T\n"; + b.setAttribute(TestFlag3(), true); + Debug("boolattr") << "set flag 3 on c to T\n"; + c.setAttribute(TestFlag3(), true); + Debug("boolattr") << "set flag 3 on unnamed to T\n"; + unnamed.setAttribute(TestFlag3(), true); + + Debug("boolattr") << "set flag 4 on a to T\n"; + a.setAttribute(TestFlag4(), true); + Debug("boolattr") << "set flag 4 on b to T\n"; + b.setAttribute(TestFlag4(), true); + Debug("boolattr") << "set flag 4 on c to T\n"; + c.setAttribute(TestFlag4(), true); + Debug("boolattr") << "set flag 4 on unnamed to T\n"; + unnamed.setAttribute(TestFlag4(), true); + + Debug("boolattr") << "set flag 5 on a to T\n"; + a.setAttribute(TestFlag5(), true); + Debug("boolattr") << "set flag 5 on b to T\n"; + b.setAttribute(TestFlag5(), true); + Debug("boolattr") << "set flag 5 on c to F\n"; + c.setAttribute(TestFlag5(), false); + Debug("boolattr") << "set flag 5 on unnamed to T\n"; + unnamed.setAttribute(TestFlag5(), true); + + ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + + ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); + + ASSERT_FALSE(a.hasAttribute(TestStringAttr1())); + ASSERT_FALSE(b.hasAttribute(TestStringAttr1())); + ASSERT_FALSE(c.hasAttribute(TestStringAttr1())); + ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1())); + + ASSERT_FALSE(a.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(b.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(c.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2())); + + Debug("boolattr") << "get flag 1 on a (should be T)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on b (should be F)\n"; + ASSERT_FALSE(b.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag1())); + Debug("boolattr") << "get flag 1 on unnamed (should be T)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag1())); + + Debug("boolattr") << "get flag 2 on a (should be F)\n"; + ASSERT_FALSE(a.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on b (should be T)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on c (should be T)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag2())); + Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; + ASSERT_FALSE(unnamed.getAttribute(TestFlag2())); + + Debug("boolattr") << "get flag 3 on a (should be T)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on b (should be T)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on c (should be T)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag3())); + Debug("boolattr") << "get flag 3 on unnamed (should be T)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag3())); + + Debug("boolattr") << "get flag 4 on a (should be T)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on b (should be T)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on c (should be T)\n"; + ASSERT_TRUE(c.getAttribute(TestFlag4())); + Debug("boolattr") << "get flag 4 on unnamed (should be T)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag4())); + + Debug("boolattr") << "get flag 5 on a (should be T)\n"; + ASSERT_TRUE(a.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on b (should be T)\n"; + ASSERT_TRUE(b.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on c (should be F)\n"; + ASSERT_FALSE(c.getAttribute(TestFlag5())); + Debug("boolattr") << "get flag 5 on unnamed (should be T)\n"; + ASSERT_TRUE(unnamed.getAttribute(TestFlag5())); + + a.setAttribute(TestStringAttr1(), "foo"); + b.setAttribute(TestStringAttr1(), "bar"); + c.setAttribute(TestStringAttr1(), "baz"); + + ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + + ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); + + ASSERT_TRUE(a.hasAttribute(TestStringAttr1())); + ASSERT_TRUE(b.hasAttribute(TestStringAttr1())); + ASSERT_TRUE(c.hasAttribute(TestStringAttr1())); + ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1())); + + ASSERT_FALSE(a.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(b.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(c.hasAttribute(TestStringAttr2())); + ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2())); + + a.setAttribute(VarNameAttr(), "b"); + b.setAttribute(VarNameAttr(), "c"); + c.setAttribute(VarNameAttr(), "a"); + + ASSERT_EQ(c.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(c.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(c.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(a.getAttribute(VarNameAttr()), "a"); + ASSERT_EQ(a.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(a.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(b.getAttribute(VarNameAttr()), "b"); + ASSERT_EQ(b.getAttribute(VarNameAttr()), "c"); + ASSERT_NE(b.getAttribute(VarNameAttr()), ""); + + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + + ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp new file mode 100644 index 000000000..a33955152 --- /dev/null +++ b/test/unit/node/kind_black.cpp @@ -0,0 +1,90 @@ +/********************* */ +/*! \file kind_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::Kind. + ** + ** Black box testing of CVC4::Kind. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/kind.h" +#include "test.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestNodeBlackKind : public TestInternal +{ + protected: + void SetUp() override + { + d_undefined = UNDEFINED_KIND; + d_null = NULL_EXPR; + d_last = LAST_KIND; + d_beyond = ((int32_t)LAST_KIND) + 1; + d_unknown = (Kind)d_beyond; + } + + bool string_is_as_expected(Kind k, const char* s) + { + std::stringstream act; + std::stringstream exp; + act << k; + exp << s; + return act.str() == exp.str(); + } + + Kind d_undefined; + Kind d_unknown; + Kind d_null; + Kind d_last; + int32_t d_beyond; +}; + +TEST_F(TestNodeBlackKind, equality) +{ + ASSERT_EQ(d_undefined, UNDEFINED_KIND); + ASSERT_EQ(d_last, LAST_KIND); +} + +TEST_F(TestNodeBlackKind, order) +{ + ASSERT_LT((int32_t)d_undefined, (int32_t)d_null); + ASSERT_LT((int32_t)d_null, (int32_t)d_last); + ASSERT_LT((int32_t)d_undefined, (int32_t)d_last); + ASSERT_LT((int32_t)d_last, (int32_t)d_unknown); +} + +TEST_F(TestNodeBlackKind, output) +{ + ASSERT_TRUE(string_is_as_expected(d_undefined, "UNDEFINED_KIND")); + ASSERT_TRUE(string_is_as_expected(d_null, "NULL")); + ASSERT_TRUE(string_is_as_expected(d_last, "LAST_KIND")); +} + +TEST_F(TestNodeBlackKind, output_concat) +{ + std::stringstream act, exp; + act << d_undefined << d_null << d_last << d_unknown; + exp << "UNDEFINED_KIND" + << "NULL" + << "LAST_KIND" + << "?"; + ASSERT_EQ(act.str(), exp.str()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp new file mode 100644 index 000000000..8e1c45d79 --- /dev/null +++ b/test/unit/node/kind_map_black.cpp @@ -0,0 +1,48 @@ +/********************* */ +/*! \file kind_map_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Gereon Kremer + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::KindMap + ** + ** Black box testing of CVC4::KindMap. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/kind_map.h" +#include "test.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestNodeBlackKindMap : public TestInternal +{ +}; + +TEST_F(TestNodeBlackKindMap, simple) +{ + KindMap map; + ASSERT_FALSE(map.test(AND)); + map.set(AND); + ASSERT_TRUE(map.test(AND)); + map.reset(AND); + ASSERT_FALSE(map.test(AND)); +#ifdef CVC4_ASSERTIONS + ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException); +#endif +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp new file mode 100644 index 000000000..bd243e0fd --- /dev/null +++ b/test/unit/node/node_algorithm_black.cpp @@ -0,0 +1,202 @@ +/********************* */ +/*! \file node_algorithm_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 utility functions in node_algorithm.{h,cpp} + ** + ** Black box testing of node_algorithm.{h,cpp} + **/ + +#include <string> +#include <vector> + +#include "base/output.h" +#include "expr/node_algorithm.h" +#include "expr/node_manager.h" +#include "test_node.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace expr; +using namespace kind; + +namespace test { + +class TestNodeBlackNodeAlgorithm : public TestNode +{ +}; + +TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1) +{ + // The only symbol in ~x (x is a boolean varible) should be x + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node n = d_nodeManager->mkNode(NOT, x); + std::unordered_set<Node, NodeHashFunction> syms; + getSymbols(n, syms); + ASSERT_EQ(syms.size(), 1); + ASSERT_NE(syms.find(x), syms.end()); +} + +TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2) +{ + // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because + // "var" is bound. + + // left conjunct + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType()); + Node left = d_nodeManager->mkNode(EQUAL, x, y); + + // right conjunct + Node var = d_nodeManager->mkBoundVar(*d_intTypeNode); + std::vector<Node> vars; + vars.push_back(var); + Node sum = d_nodeManager->mkNode(PLUS, var, var); + Node qeq = d_nodeManager->mkNode(EQUAL, x, sum); + Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars); + Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq); + + // conjunction + Node res = d_nodeManager->mkNode(AND, left, right); + + // symbols + std::unordered_set<Node, NodeHashFunction> syms; + getSymbols(res, syms); + + // assertions + ASSERT_EQ(syms.size(), 2); + ASSERT_NE(syms.find(x), syms.end()); + ASSERT_NE(syms.find(y), syms.end()); + ASSERT_EQ(syms.find(var), syms.end()); +} + +TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map) +{ + // map to store result + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result = + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >(); + + // create test formula + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node plus = d_nodeManager->mkNode(PLUS, x, x); + Node mul = d_nodeManager->mkNode(MULT, x, x); + Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul); + + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4)); + Node ext1 = theory::bv::utils::mkExtract(y, 1, 0); + Node ext2 = theory::bv::utils::mkExtract(y, 3, 2); + Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2); + + Node formula = d_nodeManager->mkNode(AND, eq1, eq2); + + // call function + expr::getOperatorsMap(formula, result); + + // Verify result + // We should have only integer, bv and boolean as types + ASSERT_EQ(result.size(), 3); + ASSERT_NE(result.find(*d_intTypeNode), result.end()); + ASSERT_NE(result.find(*d_boolTypeNode), result.end()); + ASSERT_NE(result.find(*d_bvTypeNode), result.end()); + + // in integers, we should only have plus and mult as operators + ASSERT_EQ(result[*d_intTypeNode].size(), 2); + ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)), + result[*d_intTypeNode].end()); + ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)), + result[*d_intTypeNode].end()); + + // in booleans, we should only have "=" and "and" as an operator. + ASSERT_EQ(result[*d_boolTypeNode].size(), 2); + ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)), + result[*d_boolTypeNode].end()); + ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)), + result[*d_boolTypeNode].end()); + + // in bv, we should only have "extract" as an operator. + ASSERT_EQ(result[*d_boolTypeNode].size(), 2); + Node extractOp1 = + d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0)); + Node extractOp2 = + d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2)); + ASSERT_NE(result[*d_bvTypeNode].find(extractOp1), + result[*d_bvTypeNode].end()); + ASSERT_NE(result[*d_bvTypeNode].find(extractOp2), + result[*d_bvTypeNode].end()); +} + +TEST_F(TestNodeBlackNodeAlgorithm, match) +{ + TypeNode integer = d_nodeManager->integerType(); + + Node one = d_nodeManager->mkConst(Rational(1)); + Node two = d_nodeManager->mkConst(Rational(2)); + + Node x = d_nodeManager->mkBoundVar(integer); + Node a = d_nodeManager->mkSkolem("a", integer); + + Node n1 = d_nodeManager->mkNode(MULT, two, x); + std::unordered_map<Node, Node, NodeHashFunction> subs; + + // check reflexivity + ASSERT_TRUE(match(n1, n1, subs)); + ASSERT_EQ(subs.size(), 0); + + Node n2 = d_nodeManager->mkNode(MULT, two, a); + subs.clear(); + + // check instance + ASSERT_TRUE(match(n1, n2, subs)); + ASSERT_EQ(subs.size(), 1); + ASSERT_EQ(subs[x], a); + + // should return false for flipped arguments (match is not symmetric) + ASSERT_FALSE(match(n2, n1, subs)); + + n2 = d_nodeManager->mkNode(MULT, one, a); + + // should return false since n2 is not an instance of n1 + ASSERT_FALSE(match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a); + + // should return false for similar operators + ASSERT_FALSE(match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(MULT, two, a, one); + + // should return false for different number of arguments + ASSERT_FALSE(match(n1, n2, subs)); + + n1 = x; + n2 = d_nodeManager->mkConst(true); + + // should return false for different types + ASSERT_FALSE(match(n1, n2, subs)); + + n1 = d_nodeManager->mkNode(MULT, x, x); + n2 = d_nodeManager->mkNode(MULT, two, a); + + // should return false for contradictory substitutions + ASSERT_FALSE(match(n1, n2, subs)); + + n2 = d_nodeManager->mkNode(MULT, a, a); + subs.clear(); + + // implementation: check if the cache works correctly + ASSERT_TRUE(match(n1, n2, subs)); + ASSERT_EQ(subs.size(), 1); + ASSERT_EQ(subs[x], a); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp new file mode 100644 index 000000000..3c1651155 --- /dev/null +++ b/test/unit/node/node_black.cpp @@ -0,0 +1,787 @@ +/********************* */ +/*! \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-2021 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 <algorithm> +#include <sstream> +#include <string> +#include <vector> + +#include "api/cvc4cpp.h" +#include "expr/dtype.h" +#include "expr/dtype_cons.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 "theory/rewriter.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +namespace { +/** Returns N skolem nodes from 'nodeManager' with the same `type`. */ +std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, + uint32_t n, + TypeNode type) +{ + std::vector<Node> 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 TestNode +{ + protected: + void SetUp() override + { + TestNode::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<SmtEngine> 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 = nullptr; + ASSERT_NO_FATAL_FAILURE(n = new Node()); + if (n) + { + 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<Node> 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_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED"); + ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED"); +#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::getMinArityForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(AND, 1), + "getNumChildren\\(\\) >= " + "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(NOT, 0), + "getNumChildren\\(\\) >= " + "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); + ASSERT_DEATH(testNaryExpForSize(NOT, 2), + "getNumChildren\\(\\) <= " + "kind::metakind::getMaxArityForKind\\(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<Node> skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector<Node> 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<Node> skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector<TNode> 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<Node> 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<Node> 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<Node> 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<TNode> 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<DTypeConstructor> consC = + std::make_shared<DTypeConstructor>("cons"); + consC->addArg("car", d_nodeManager->integerType()); + consC->addArgSelf("cdr"); + list.addConstructor(consC); + list.addConstructor(std::make_shared<DTypeConstructor>("nil")); + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const std::vector<std::shared_ptr<DTypeConstructor> >& 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/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp new file mode 100644 index 000000000..7e38dd899 --- /dev/null +++ b/test/unit/node/node_builder_black.cpp @@ -0,0 +1,590 @@ +/********************* */ +/*! \file node_builder_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::NodeBuilder. + ** + ** Black box testing of CVC4::NodeBuilder. + **/ + +#include <limits.h> + +#include <sstream> +#include <vector> + +#include "base/check.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "test_node.h" +#include "util/rational.h" + +#define K 30u +#define LARGE_K UINT_MAX / 40 + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestNodeBlackNodeBuilder : public TestNode +{ + protected: + template <unsigned N> + void push_back(NodeBuilder<N>& nb, uint32_t n) + { + for (uint32_t i = 0; i < n; ++i) + { + nb << d_nodeManager->mkConst(true); + } + } + Kind d_specKind = AND; +}; + +/** Tests just constructors. No modification is done to the node. */ +TEST_F(TestNodeBlackNodeBuilder, ctors) +{ + /* Default size tests. */ + NodeBuilder<> def; + ASSERT_EQ(def.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<> spec(d_specKind); + ASSERT_EQ(spec.getKind(), d_specKind); + ASSERT_EQ(spec.getNumChildren(), 0u); + ASSERT_EQ(spec.begin(), spec.end()); + + NodeBuilder<> from_nm(d_nodeManager.get()); + ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(from_nm.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind); + ASSERT_EQ(from_nm_kind.getKind(), d_specKind); + ASSERT_EQ(from_nm_kind.getNumChildren(), 0u); + ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end()); + + /* Non-default size tests */ + NodeBuilder<K> ws; + ASSERT_EQ(ws.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<K> ws_kind(d_specKind); + ASSERT_EQ(ws_kind.getKind(), d_specKind); + ASSERT_EQ(ws_kind.getNumChildren(), 0u); + ASSERT_EQ(ws_kind.begin(), ws_kind.end()); + + NodeBuilder<K> ws_from_nm(d_nodeManager.get()); + ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(ws_from_nm.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind); + ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind); + ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u); + ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end()); + + /* Extreme size tests */ + NodeBuilder<0> ws_size_0; + + /* Allocating on the heap instead of the stack. */ + NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>; + delete ws_size_large; + + /* Copy constructors */ + NodeBuilder<> copy(def); + ASSERT_EQ(copy.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<K> cp_ws(ws); + ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<K - 10> cp_from_larger(ws); + ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_from_larger.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + NodeBuilder<K + 10> cp_from_smaller(ws); + ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(cp_from_smaller.getNumChildren(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_smaller.begin(), + "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif +} + +TEST_F(TestNodeBlackNodeBuilder, dtor) +{ + NodeBuilder<K>* nb = new NodeBuilder<K>(); + delete nb; +} + +TEST_F(TestNodeBlackNodeBuilder, begin_end) +{ + /* Test begin() and end() without resizing. */ + NodeBuilder<K> ws(d_specKind); + ASSERT_EQ(ws.begin(), ws.end()); + + push_back(ws, K); + ASSERT_NE(ws.begin(), ws.end()); + + NodeBuilder<K>::iterator iter = ws.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(iter, ws.end()); + ++iter; + } + ASSERT_EQ(iter, ws.end()); + + NodeBuilder<K>::const_iterator citer = ws.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(citer, ws.end()); + ++citer; + } + ASSERT_EQ(citer, ws.end()); + + /* Repeat same tests and make sure that resizing occurs. */ + NodeBuilder<> smaller(d_specKind); + ASSERT_EQ(smaller.begin(), smaller.end()); + + push_back(smaller, K); + ASSERT_NE(smaller.begin(), smaller.end()); + + NodeBuilder<>::iterator smaller_iter = smaller.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(smaller_iter, smaller.end()); + ++smaller_iter; + } + ASSERT_EQ(iter, ws.end()); + + NodeBuilder<>::const_iterator smaller_citer = smaller.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(smaller_citer, smaller.end()); + ++smaller_citer; + } + ASSERT_EQ(smaller_citer, smaller.end()); +} + +TEST_F(TestNodeBlackNodeBuilder, iterator) +{ + NodeBuilder<> b; + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + b << x << y << z << AND; + + { + NodeBuilder<>::iterator i = b.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, b.end()); + } + + { + const NodeBuilder<>& c = b; + NodeBuilder<>::const_iterator i = c.begin(); + ASSERT_EQ(*i++, x); + ASSERT_EQ(*i++, y); + ASSERT_EQ(*i++, z); + ASSERT_EQ(i, b.end()); + } +} + +TEST_F(TestNodeBlackNodeBuilder, getKind) +{ + NodeBuilder<> noKind; + ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); + + Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + noKind << x << x; + ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); + + noKind << PLUS; + + ASSERT_EQ(noKind.getKind(), PLUS); + + Node n = noKind; + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)"); +#endif + + NodeBuilder<> spec(PLUS); + ASSERT_EQ(spec.getKind(), PLUS); + spec << x << x; + ASSERT_EQ(spec.getKind(), PLUS); +} + +TEST_F(TestNodeBlackNodeBuilder, getNumChildren) +{ + Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); + + NodeBuilder<> nb; +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + nb << PLUS << x << x; + + ASSERT_EQ(nb.getNumChildren(), 2u); + + nb << x << x; + ASSERT_EQ(nb.getNumChildren(), 4u); + + nb.clear(); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + nb.clear(PLUS); + ASSERT_EQ(nb.getNumChildren(), 0u); + nb << x << x << x; + + ASSERT_EQ(nb.getNumChildren(), 3u); + + nb << x << x << x; + ASSERT_EQ(nb.getNumChildren(), 6u); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND"); + Node n = nb; + ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBlackNodeBuilder, operator_square) +{ + NodeBuilder<> arr(d_specKind); + + Node i_0 = d_nodeManager->mkConst(false); + Node i_2 = d_nodeManager->mkConst(true); + Node i_K = d_nodeManager->mkNode(NOT, i_0); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(arr[-1], "index out of range"); + ASSERT_DEATH(arr[0], "index out of range"); +#endif + + arr << i_0; + + ASSERT_EQ(arr[0], i_0); + + push_back(arr, 1); + + arr << i_2; + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + + push_back(arr, K - 3); + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + for (unsigned i = 3; i < K; ++i) + { + ASSERT_EQ(arr[i], d_nodeManager->mkConst(true)); + } + + arr << i_K; + + ASSERT_EQ(arr[0], i_0); + ASSERT_EQ(arr[2], i_2); + for (unsigned i = 3; i < K; ++i) + { + ASSERT_EQ(arr[i], d_nodeManager->mkConst(true)); + } + ASSERT_EQ(arr[K], i_K); + +#ifdef CVC4_ASSERTIONS + Node n = arr; + ASSERT_DEATH(arr[0], "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBlackNodeBuilder, clear) +{ + NodeBuilder<> nb; + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + nb << d_specKind; + push_back(nb, K); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + + nb.clear(); + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif + + nb << d_specKind; + push_back(nb, K); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + + nb.clear(d_specKind); + + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), 0u); + ASSERT_EQ(nb.begin(), nb.end()); + + push_back(nb, K); + nb.clear(); + + ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); + ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); +#endif +} + +TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) +{ +#ifdef CVC4_ASSERTIONS + NodeBuilder<> spec(d_specKind); + ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> noSpec; + noSpec << d_specKind; + ASSERT_EQ(noSpec.getKind(), d_specKind); + + NodeBuilder<> modified; + push_back(modified, K); + modified << d_specKind; + ASSERT_EQ(modified.getKind(), d_specKind); + + NodeBuilder<> nb(d_specKind); + nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false); + nb.clear(PLUS); + +#ifdef CVC4_ASSERTIONS + Node n; + ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children"); + nb.clear(PLUS); +#endif + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> testRef; + ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind); + +#ifdef CVC4_ASSERTIONS + NodeBuilder<> testTwo; + ASSERT_DEATH(testTwo << d_specKind << PLUS, + "can't redefine the Kind of a NodeBuilder"); +#endif + + NodeBuilder<> testMixOrder1; + ASSERT_EQ( + (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(), + d_specKind); + NodeBuilder<> testMixOrder2; + ASSERT_EQ( + (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(), + d_specKind); +} + +TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node) +{ + NodeBuilder<K> nb(d_specKind); + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), 0u); + ASSERT_EQ(nb.begin(), nb.end()); + push_back(nb, K); + ASSERT_EQ(nb.getKind(), d_specKind); + ASSERT_EQ(nb.getNumChildren(), K); + ASSERT_NE(nb.begin(), nb.end()); + +#ifdef CVC4_ASSERTIONS + Node n = nb; + ASSERT_DEATH(nb << n, "!isUsed\\(\\)"); +#endif + + NodeBuilder<> overflow(d_specKind); + ASSERT_EQ(overflow.getKind(), d_specKind); + ASSERT_EQ(overflow.getNumChildren(), 0u); + ASSERT_EQ(overflow.begin(), overflow.end()); + + push_back(overflow, 5 * K + 1); + + ASSERT_EQ(overflow.getKind(), d_specKind); + ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1); + ASSERT_NE(overflow.begin(), overflow.end()); +} + +TEST_F(TestNodeBlackNodeBuilder, append) +{ + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode); + Node m = d_nodeManager->mkNode(AND, y, z, x); + Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z); + Node o = d_nodeManager->mkNode(XOR, y, x); + + Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode); + Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode); + Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode); + + Node p = d_nodeManager->mkNode( + EQUAL, + d_nodeManager->mkConst<Rational>(0), + d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); + Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x), + "Nodes with kind XOR must have at most 2 children"); +#endif + + NodeBuilder<> b(d_specKind); + + /* test append(TNode) */ + b.append(n).append(o).append(q); + + ASSERT_EQ(b.getNumChildren(), 3); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + + std::vector<Node> v; + v.push_back(m); + v.push_back(p); + v.push_back(q); + + /* test append(vector<Node>) */ + b.append(v); + + ASSERT_EQ(b.getNumChildren(), 6); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + ASSERT_EQ(b[3], m); + ASSERT_EQ(b[4], p); + ASSERT_EQ(b[5], q); + + /* test append(iterator, iterator) */ + b.append(v.rbegin(), v.rend()); + + ASSERT_EQ(b.getNumChildren(), 9); + ASSERT_EQ(b[0], n); + ASSERT_EQ(b[1], o); + ASSERT_EQ(b[2], q); + ASSERT_EQ(b[3], m); + ASSERT_EQ(b[4], p); + ASSERT_EQ(b[5], q); + ASSERT_EQ(b[6], q); + ASSERT_EQ(b[7], p); + ASSERT_EQ(b[8], m); +} + +TEST_F(TestNodeBlackNodeBuilder, operator_node_cast) +{ + NodeBuilder<K> implicit(d_specKind); + NodeBuilder<K> explic(d_specKind); + + push_back(implicit, K); + push_back(explic, K); + + Node nimpl = implicit; + Node nexplicit = (Node)explic; + + ASSERT_EQ(nimpl.getKind(), d_specKind); + ASSERT_EQ(nimpl.getNumChildren(), K); + + ASSERT_EQ(nexplicit.getKind(), d_specKind); + ASSERT_EQ(nexplicit.getNumChildren(), K); + +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)"); +#endif +} + +TEST_F(TestNodeBlackNodeBuilder, leftist_building) +{ + NodeBuilder<> nb; + + Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode); + + Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode); + Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode); + + Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode); + Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode); + + nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE; + + Node n = nb; + ASSERT_EQ(n.getNumChildren(), 3u); + ASSERT_EQ(n.getType(), *d_realTypeNode); + ASSERT_EQ(n[0].getType(), *d_boolTypeNode); + ASSERT_EQ(n[1].getType(), *d_realTypeNode); + ASSERT_EQ(n[2].getType(), *d_realTypeNode); + + Node nota = d_nodeManager->mkNode(NOT, a); + Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c); + Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a); + Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e); + + ASSERT_EQ(nexpected, n); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp new file mode 100644 index 000000000..a2ede3ed0 --- /dev/null +++ b/test/unit/node/node_manager_black.cpp @@ -0,0 +1,333 @@ +/********************* */ +/*! \file node_manager_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Christopher L. Conway, Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::NodeManager. + ** + ** Black box testing of CVC4::NodeManager. + **/ + +#include <string> +#include <vector> + +#include "base/output.h" +#include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" +#include "test_node.h" +#include "util/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace kind; +using namespace expr; + +namespace test { + +class TestNodeBlackNodeManager : public TestNode +{ +}; + +TEST_F(TestNodeBlackNodeManager, mkNode_not) +{ + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node n = d_nodeManager->mkNode(NOT, x); + ASSERT_EQ(n.getNumChildren(), 1u); + ASSERT_EQ(n.getKind(), NOT); + ASSERT_EQ(n[0], x); +} + +TEST_F(TestNodeBlackNodeManager, mkNode_binary) +{ + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node n = d_nodeManager->mkNode(IMPLIES, x, y); + ASSERT_EQ(n.getNumChildren(), 2u); + ASSERT_EQ(n.getKind(), IMPLIES); + ASSERT_EQ(n[0], x); + ASSERT_EQ(n[1], y); +} + +TEST_F(TestNodeBlackNodeManager, mkNode_three_children) +{ + 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 = d_nodeManager->mkNode(AND, x, y, z); + ASSERT_EQ(n.getNumChildren(), 3u); + ASSERT_EQ(n.getKind(), AND); + ASSERT_EQ(n[0], x); + ASSERT_EQ(n[1], y); + ASSERT_EQ(n[2], z); +} + +TEST_F(TestNodeBlackNodeManager, mkNode_four_children) +{ + Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); + Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4); + ASSERT_EQ(n.getNumChildren(), 4u); + ASSERT_EQ(n.getKind(), AND); + ASSERT_EQ(n[0], x1); + ASSERT_EQ(n[1], x2); + ASSERT_EQ(n[2], x3); + ASSERT_EQ(n[3], x4); +} + +TEST_F(TestNodeBlackNodeManager, mkNode_five_children) +{ + Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType()); + Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType()); + Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5); + ASSERT_EQ(n.getNumChildren(), 5u); + ASSERT_EQ(n.getKind(), AND); + ASSERT_EQ(n[0], x1); + ASSERT_EQ(n[1], x2); + ASSERT_EQ(n[2], x3); + ASSERT_EQ(n[3], x4); + ASSERT_EQ(n[4], x5); +} + +TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node) +{ + Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + std::vector<Node> args; + args.push_back(x1); + args.push_back(x2); + args.push_back(x3); + Node n = d_nodeManager->mkNode(AND, args); + ASSERT_EQ(n.getNumChildren(), args.size()); + ASSERT_EQ(n.getKind(), AND); + for (unsigned i = 0; i < args.size(); ++i) + { + ASSERT_EQ(n[i], args[i]); + } +} + +TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode) +{ + Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType()); + Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType()); + Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType()); + std::vector<TNode> args; + args.push_back(x1); + args.push_back(x2); + args.push_back(x3); + Node n = d_nodeManager->mkNode(AND, args); + ASSERT_EQ(n.getNumChildren(), args.size()); + ASSERT_EQ(n.getKind(), AND); + for (unsigned i = 0; i < args.size(); ++i) + { + ASSERT_EQ(n[i], args[i]); + } +} + +TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name) +{ + Node x = d_nodeManager->mkSkolem( + "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME); + ASSERT_EQ(x.getKind(), SKOLEM); + ASSERT_EQ(x.getNumChildren(), 0u); + ASSERT_EQ(x.getAttribute(VarNameAttr()), "x"); + ASSERT_EQ(x.getType(), *d_boolTypeNode); +} + +TEST_F(TestNodeBlackNodeManager, mkConst_bool) +{ + Node tt = d_nodeManager->mkConst(true); + ASSERT_EQ(tt.getConst<bool>(), true); + Node ff = d_nodeManager->mkConst(false); + ASSERT_EQ(ff.getConst<bool>(), false); +} + +TEST_F(TestNodeBlackNodeManager, mkConst_rational) +{ + Rational r("3/2"); + Node n = d_nodeManager->mkConst(r); + ASSERT_EQ(n.getConst<Rational>(), r); +} + +TEST_F(TestNodeBlackNodeManager, hasOperator) +{ + ASSERT_TRUE(NodeManager::hasOperator(AND)); + ASSERT_TRUE(NodeManager::hasOperator(OR)); + ASSERT_TRUE(NodeManager::hasOperator(NOT)); + ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF)); + ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE)); +} + +TEST_F(TestNodeBlackNodeManager, booleanType) +{ + TypeNode t = d_nodeManager->booleanType(); + TypeNode t2 = d_nodeManager->booleanType(); + TypeNode t3 = d_nodeManager->mkSort("T"); + ASSERT_TRUE(t.isBoolean()); + ASSERT_FALSE(t.isFunction()); + ASSERT_FALSE(t.isNull()); + ASSERT_FALSE(t.isPredicate()); + ASSERT_FALSE(t.isSort()); + ASSERT_EQ(t, t2); + ASSERT_NE(t, t3); + + TypeNode bt = t; + ASSERT_EQ(bt, t); +} + +TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool) +{ + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType); + TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType); + + ASSERT_FALSE(t.isBoolean()); + ASSERT_TRUE(t.isFunction()); + ASSERT_FALSE(t.isNull()); + ASSERT_TRUE(t.isPredicate()); + ASSERT_FALSE(t.isSort()); + + ASSERT_EQ(t, t2); + + TypeNode ft = t; + ASSERT_EQ(ft, t); + ASSERT_EQ(ft.getArgTypes().size(), 1u); + ASSERT_EQ(ft.getArgTypes()[0], booleanType); + ASSERT_EQ(ft.getRangeType(), booleanType); +} + +TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type) +{ + TypeNode a = d_nodeManager->mkSort(); + TypeNode b = d_nodeManager->mkSort(); + TypeNode c = d_nodeManager->mkSort(); + + std::vector<TypeNode> argTypes; + argTypes.push_back(a); + argTypes.push_back(b); + + TypeNode t = d_nodeManager->mkFunctionType(argTypes, c); + TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c); + + ASSERT_FALSE(t.isBoolean()); + ASSERT_TRUE(t.isFunction()); + ASSERT_FALSE(t.isNull()); + ASSERT_FALSE(t.isPredicate()); + ASSERT_FALSE(t.isSort()); + + ASSERT_EQ(t, t2); + + TypeNode ft = t; + ASSERT_EQ(ft, t); + ASSERT_EQ(ft.getArgTypes().size(), argTypes.size()); + ASSERT_EQ(ft.getArgTypes()[0], a); + ASSERT_EQ(ft.getArgTypes()[1], b); + ASSERT_EQ(ft.getRangeType(), c); +} + +TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments) +{ + TypeNode a = d_nodeManager->mkSort(); + TypeNode b = d_nodeManager->mkSort(); + TypeNode c = d_nodeManager->mkSort(); + + std::vector<TypeNode> types; + types.push_back(a); + types.push_back(b); + types.push_back(c); + + TypeNode t = d_nodeManager->mkFunctionType(types); + TypeNode t2 = d_nodeManager->mkFunctionType(types); + + ASSERT_FALSE(t.isBoolean()); + ASSERT_TRUE(t.isFunction()); + ASSERT_FALSE(t.isNull()); + ASSERT_FALSE(t.isPredicate()); + ASSERT_FALSE(t.isSort()); + + ASSERT_EQ(t, t2); + + TypeNode ft = t; + ASSERT_EQ(ft, t); + ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1); + ASSERT_EQ(ft.getArgTypes()[0], a); + ASSERT_EQ(ft.getArgTypes()[1], b); + ASSERT_EQ(ft.getRangeType(), c); +} + +TEST_F(TestNodeBlackNodeManager, mkPredicateType) +{ + TypeNode a = d_nodeManager->mkSort("a"); + TypeNode b = d_nodeManager->mkSort("b"); + TypeNode c = d_nodeManager->mkSort("c"); + TypeNode booleanType = d_nodeManager->booleanType(); + + std::vector<TypeNode> argTypes; + argTypes.push_back(a); + argTypes.push_back(b); + argTypes.push_back(c); + + TypeNode t = d_nodeManager->mkPredicateType(argTypes); + TypeNode t2 = d_nodeManager->mkPredicateType(argTypes); + + ASSERT_FALSE(t.isBoolean()); + ASSERT_TRUE(t.isFunction()); + ASSERT_FALSE(t.isNull()); + ASSERT_TRUE(t.isPredicate()); + ASSERT_FALSE(t.isSort()); + + ASSERT_EQ(t, t2); + + TypeNode ft = t; + ASSERT_EQ(ft, t); + ASSERT_EQ(ft.getArgTypes().size(), argTypes.size()); + ASSERT_EQ(ft.getArgTypes()[0], a); + ASSERT_EQ(ft.getArgTypes()[1], b); + ASSERT_EQ(ft.getArgTypes()[2], c); + ASSERT_EQ(ft.getRangeType(), booleanType); +} + +/* This test is only valid if assertions are enabled. */ +TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children) +{ +#ifdef CVC4_ASSERTIONS + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + ASSERT_DEATH(d_nodeManager->mkNode(AND, x), + "Nodes with kind AND must have at least 2 children"); +#endif +} + +/* This test is only valid if assertions are enabled. */ +TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) +{ +#ifdef CVC4_ASSERTIONS + std::vector<Node> vars; + const uint32_t max = metakind::getMaxArityForKind(AND); + TypeNode boolType = d_nodeManager->booleanType(); + Node skolem_i = d_nodeManager->mkSkolem("i", boolType); + Node skolem_j = d_nodeManager->mkSkolem("j", boolType); + Node andNode = skolem_i.andNode(skolem_j); + Node orNode = skolem_i.orNode(skolem_j); + while (vars.size() <= max) + { + vars.push_back(andNode); + vars.push_back(skolem_j); + vars.push_back(orNode); + } + ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren"); +#endif +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp new file mode 100644 index 000000000..daf211b78 --- /dev/null +++ b/test/unit/node/node_manager_white.cpp @@ -0,0 +1,84 @@ +/********************* */ +/*! \file node_manager_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 White box testing of CVC4::NodeManager. + ** + ** White box testing of CVC4::NodeManager. + **/ + +#include <string> + +#include "expr/node_manager.h" +#include "test_node.h" +#include "util/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +using namespace CVC4::expr; + +namespace test { + +class TestNodeWhiteNodeManager : public TestNode +{ +}; + +TEST_F(TestNodeWhiteNodeManager, mkConst_rational) +{ + Rational i("3"); + Node n = d_nodeManager->mkConst(i); + Node m = d_nodeManager->mkConst(i); + ASSERT_EQ(n.getId(), m.getId()); +} + +TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) +{ + NodeBuilder<> nb; + + ASSERT_NO_THROW(nb.realloc(15)); + ASSERT_NO_THROW(nb.realloc(25)); + ASSERT_NO_THROW(nb.realloc(256)); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren"); +#endif /* CVC4_ASSERTIONS */ + ASSERT_NO_THROW(nb.realloc(257)); + ASSERT_NO_THROW(nb.realloc(4000)); + ASSERT_NO_THROW(nb.realloc(20000)); + ASSERT_NO_THROW(nb.realloc(60000)); + ASSERT_NO_THROW(nb.realloc(65535)); + ASSERT_NO_THROW(nb.realloc(65536)); + ASSERT_NO_THROW(nb.realloc(67108863)); +#ifdef CVC4_ASSERTIONS + ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren"); +#endif /* CVC4_ASSERTIONS */ +} + +TEST_F(TestNodeWhiteNodeManager, topological_sort) +{ + TypeNode boolType = d_nodeManager->booleanType(); + Node i = d_nodeManager->mkSkolem("i", boolType); + Node j = d_nodeManager->mkSkolem("j", boolType); + Node n1 = d_nodeManager->mkNode(kind::AND, j, j); + Node n2 = d_nodeManager->mkNode(kind::AND, i, n1); + + { + std::vector<NodeValue*> roots = {n1.d_nv}; + ASSERT_EQ(NodeManager::TopologicalSort(roots), roots); + } + + { + std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv}; + std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv}; + ASSERT_EQ(NodeManager::TopologicalSort(roots), result); + } +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp new file mode 100644 index 000000000..34ab5f09b --- /dev/null +++ b/test/unit/node/node_self_iterator_black.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file node_self_iterator_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::expr::NodeSelfIterator + ** + ** Black box testing of CVC4::expr::NodeSelfIterator + **/ + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_self_iterator.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace expr; + +namespace test { + +class TestNodeBlackNodeSelfIterator : public TestNode +{ +}; + +TEST_F(TestNodeBlackNodeSelfIterator, iteration) +{ + Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); + Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode); + Node x_and_y = x.andNode(y); + NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); + ASSERT_NE(i, x_and_y.end()); + ASSERT_NE(j, x_and_y.end()); + ASSERT_EQ(*i, x_and_y); + ASSERT_EQ(*j, x_and_y); + ASSERT_EQ(*i++, x_and_y); + ASSERT_EQ(*j++, x_and_y); + ASSERT_EQ(i, NodeSelfIterator::selfEnd(x_and_y)); + ASSERT_EQ(j, NodeSelfIterator::selfEnd(x_and_y)); + ASSERT_EQ(i, x_and_y.end()); + ASSERT_EQ(j, x_and_y.end()); + + i = x_and_y.begin(); + ASSERT_NE(i, x_and_y.end()); + ASSERT_EQ(*i, x); + ASSERT_EQ(*++i, y); + ASSERT_EQ(++i, x_and_y.end()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp new file mode 100644 index 000000000..e443ff685 --- /dev/null +++ b/test/unit/node/node_traversal_black.cpp @@ -0,0 +1,296 @@ +/********************* */ +/*! \file node_traversal_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Alex Ozdemir, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 node traversal iterators. + **/ + +#include <algorithm> +#include <cstddef> +#include <iterator> +#include <sstream> +#include <string> +#include <vector> + +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node_traversal.h" +#include "expr/node_value.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestNodeBlackNodeTraversalPostorder : public TestNode +{ +}; + +class TestNodeBlackNodeTraversalPreorder : public TestNode +{ +}; + +TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER); + NodeDfsIterator i = traversal.begin(); + NodeDfsIterator end = traversal.end(); + ASSERT_EQ(*i, tb); + ASSERT_FALSE(i == end); + ++i; + ASSERT_EQ(*i, eb); + ASSERT_FALSE(i == end); + ++i; + ASSERT_EQ(*i, cnd); + ASSERT_FALSE(i == end); + ++i; + ASSERT_TRUE(i == end); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER); + NodeDfsIterator i = traversal.begin(); + NodeDfsIterator end = traversal.end(); + ASSERT_EQ(*(i++), tb); + ASSERT_EQ(*(i++), eb); + ASSERT_EQ(*(i++), cnd); + ASSERT_TRUE(i == end); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + auto traversal = NodeDfsIterable(cnd); + NodeDfsIterator i = traversal.begin(); + NodeDfsIterator end = traversal.end(); + ASSERT_EQ(*i, tb); + ASSERT_FALSE(i == end); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + size_t count = 0; + for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER)) + { + ++count; + } + ASSERT_EQ(count, 3); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + size_t count = 0; + for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER)) + { + if (i.isConst()) + { + ++count; + } + } + ASSERT_EQ(count, 2); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); + + size_t count = std::count_if( + traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); }); + ASSERT_EQ(count, 2); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {tb, eb, cnd, top}; + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + ASSERT_EQ(actual, expected); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {top}; + + auto traversal = NodeDfsIterable( + top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; }); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + ASSERT_EQ(actual, expected); +} + +TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {}; + + auto traversal = + NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; }); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + ASSERT_EQ(actual, expected); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER); + NodeDfsIterator i = traversal.begin(); + NodeDfsIterator end = traversal.end(); + ASSERT_EQ(*i, cnd); + ASSERT_FALSE(i == end); + ++i; + ASSERT_EQ(*i, tb); + ASSERT_FALSE(i == end); + ++i; + ASSERT_EQ(*i, eb); + ASSERT_FALSE(i == end); + ++i; + ASSERT_TRUE(i == end); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER); + NodeDfsIterator i = traversal.begin(); + NodeDfsIterator end = traversal.end(); + ASSERT_EQ(*(i++), cnd); + ASSERT_EQ(*(i++), tb); + ASSERT_EQ(*(i++), eb); + ASSERT_TRUE(i == end); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + size_t count = 0; + for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER)) + { + ++count; + } + ASSERT_EQ(count, 3); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + + size_t count = 0; + for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER)) + { + if (i.isConst()) + { + ++count; + } + } + ASSERT_EQ(count, 2); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + + auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); + + size_t count = std::count_if( + traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); }); + ASSERT_EQ(count, 2); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {top, cnd, tb, eb}; + + auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + ASSERT_EQ(actual, expected); +} + +TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if) +{ + const Node tb = d_nodeManager->mkConst(true); + const Node eb = d_nodeManager->mkConst(false); + const Node cnd = d_nodeManager->mkNode(XOR, tb, eb); + const Node top = d_nodeManager->mkNode(XOR, cnd, cnd); + std::vector<TNode> expected = {top, cnd, eb}; + + auto traversal = NodeDfsIterable( + top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; }); + + std::vector<TNode> actual; + std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); + ASSERT_EQ(actual, expected); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp new file mode 100644 index 000000000..651dd1990 --- /dev/null +++ b/test/unit/node/node_white.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file node_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 White box testing of CVC4::Node. + ** + ** White box testing of CVC4::Node. + **/ + +#include <string> + +#include "base/check.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace expr; + +namespace test { + +class TestNodeWhiteNode : public TestNode +{ +}; + +TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); } + +TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); } + +TEST_F(TestNodeWhiteNode, builder) +{ + NodeBuilder<> b; + ASSERT_TRUE(b.d_nv->getId() == 0); + ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND); + ASSERT_EQ(b.d_nv->d_nchildren, 0u); + /* etc. */ +} + +TEST_F(TestNodeWhiteNode, iterators) +{ + Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType()); + Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType()); + Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y); + Node two = d_nodeManager->mkConst(Rational(2)); + Node x_times_2 = d_nodeManager->mkNode(MULT, x, two); + + Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y); + + Node::iterator i; + + i = std::find(n.begin(), n.end(), x_plus_y); + ASSERT_TRUE(i != n.end()); + ASSERT_TRUE(*i == x_plus_y); + + i = std::find(n.begin(), n.end(), x); + ASSERT_TRUE(i == n.end()); + + i = std::find(x_times_2.begin(), x_times_2.end(), two); + ASSERT_TRUE(i != x_times_2.end()); + ASSERT_TRUE(*i == two); + + i = std::find(n.begin(), n.end(), y); + ASSERT_TRUE(i != n.end()); + ASSERT_TRUE(*i == y); + + std::vector<Node> v; + copy(n.begin(), n.end(), back_inserter(v)); + ASSERT_EQ(n.getNumChildren(), v.size()); + ASSERT_EQ(3, v.size()); + ASSERT_EQ(v[0], x_times_2); + ASSERT_EQ(v[1], x_plus_y); + ASSERT_EQ(v[2], y); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp new file mode 100644 index 000000000..c1865eaa9 --- /dev/null +++ b/test/unit/node/symbol_table_black.cpp @@ -0,0 +1,149 @@ +/********************* */ +/*! \file symbol_table_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Christopher L. Conway + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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::SymbolTable + ** + ** Black box testing of CVC4::SymbolTable. + **/ + +#include <sstream> +#include <string> + +#include "base/check.h" +#include "base/exception.h" +#include "context/context.h" +#include "expr/kind.h" +#include "expr/symbol_table.h" +#include "test_api.h" + +namespace CVC4 { + +using namespace kind; +using namespace context; + +namespace test { + +class TestNodeBlackSymbolTable : public TestApi +{ +}; + +TEST_F(TestNodeBlackSymbolTable, bind1) +{ + SymbolTable symtab; + api::Sort booleanType = d_solver.getBooleanSort(); + api::Term x = d_solver.mkConst(booleanType); + symtab.bind("x", x); + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), x); +} + +TEST_F(TestNodeBlackSymbolTable, bind2) +{ + SymbolTable symtab; + api::Sort booleanType = d_solver.getBooleanSort(); + // var name attribute shouldn't matter + api::Term y = d_solver.mkConst(booleanType, "y"); + symtab.bind("x", y); + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), y); +} + +TEST_F(TestNodeBlackSymbolTable, bind3) +{ + SymbolTable symtab; + api::Sort booleanType = d_solver.getBooleanSort(); + api::Term x = d_solver.mkConst(booleanType); + symtab.bind("x", x); + api::Term y = d_solver.mkConst(booleanType); + // new binding covers old + symtab.bind("x", y); + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), y); +} + +TEST_F(TestNodeBlackSymbolTable, bind4) +{ + SymbolTable symtab; + api::Sort booleanType = d_solver.getBooleanSort(); + api::Term x = d_solver.mkConst(booleanType); + symtab.bind("x", x); + + api::Sort t = d_solver.mkUninterpretedSort("T"); + // duplicate binding for type is OK + symtab.bindType("x", t); + + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), x); + ASSERT_TRUE(symtab.isBoundType("x")); + ASSERT_EQ(symtab.lookupType("x"), t); +} + +TEST_F(TestNodeBlackSymbolTable, bind_type1) +{ + SymbolTable symtab; + api::Sort s = d_solver.mkUninterpretedSort("S"); + symtab.bindType("S", s); + ASSERT_TRUE(symtab.isBoundType("S")); + ASSERT_EQ(symtab.lookupType("S"), s); +} + +TEST_F(TestNodeBlackSymbolTable, bind_type2) +{ + SymbolTable symtab; + // type name attribute shouldn't matter + api::Sort s = d_solver.mkUninterpretedSort("S"); + symtab.bindType("T", s); + ASSERT_TRUE(symtab.isBoundType("T")); + ASSERT_EQ(symtab.lookupType("T"), s); +} + +TEST_F(TestNodeBlackSymbolTable, bind_type3) +{ + SymbolTable symtab; + api::Sort s = d_solver.mkUninterpretedSort("S"); + symtab.bindType("S", s); + api::Sort t = d_solver.mkUninterpretedSort("T"); + // new binding covers old + symtab.bindType("S", t); + ASSERT_TRUE(symtab.isBoundType("S")); + ASSERT_EQ(symtab.lookupType("S"), t); +} + +TEST_F(TestNodeBlackSymbolTable, push_scope) +{ + SymbolTable symtab; + api::Sort booleanType = d_solver.getBooleanSort(); + api::Term x = d_solver.mkConst(booleanType); + symtab.bind("x", x); + symtab.pushScope(); + + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), x); + + api::Term y = d_solver.mkConst(booleanType); + symtab.bind("x", y); + + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), y); + + symtab.popScope(); + ASSERT_TRUE(symtab.isBound("x")); + ASSERT_EQ(symtab.lookup("x"), x); +} + +TEST_F(TestNodeBlackSymbolTable, bad_pop) +{ + SymbolTable symtab; + ASSERT_THROW(symtab.popScope(), ScopeException); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp new file mode 100644 index 000000000..55936df0d --- /dev/null +++ b/test/unit/node/type_cardinality_black.cpp @@ -0,0 +1,335 @@ +/********************* */ +/*! \file type_cardinality_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 Public box testing of Type::getCardinality() for various Types + ** + ** Public box testing of Type::getCardinality() for various Types. + **/ + +#include <string> + +#include "expr/kind.h" +#include "expr/node_manager.h" +#include "test_node.h" +#include "util/cardinality.h" + +namespace CVC4 { + +using namespace kind; + +namespace test { + +class TestNodeBlackTypeCardinality : public TestNode +{ +}; + +TEST_F(TestNodeBlackTypeCardinality, basics) +{ + ASSERT_EQ(d_nodeManager->booleanType().getCardinality().compare(2), + Cardinality::EQUAL); + ASSERT_EQ(d_nodeManager->integerType().getCardinality().compare( + Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ( + d_nodeManager->realType().getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); +} + +TEST_F(TestNodeBlackTypeCardinality, arrays) +{ + TypeNode intToInt = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + TypeNode realToReal = d_nodeManager->mkArrayType(d_nodeManager->realType(), + d_nodeManager->realType()); + TypeNode realToInt = d_nodeManager->mkArrayType(d_nodeManager->realType(), + d_nodeManager->integerType()); + TypeNode intToReal = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->realType()); + TypeNode intToBool = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->booleanType()); + TypeNode realToBool = d_nodeManager->mkArrayType( + d_nodeManager->realType(), d_nodeManager->booleanType()); + TypeNode boolToReal = d_nodeManager->mkArrayType(d_nodeManager->booleanType(), + d_nodeManager->realType()); + TypeNode boolToInt = d_nodeManager->mkArrayType(d_nodeManager->booleanType(), + d_nodeManager->integerType()); + TypeNode boolToBool = d_nodeManager->mkArrayType( + d_nodeManager->booleanType(), d_nodeManager->booleanType()); + + ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL); +} + +TEST_F(TestNodeBlackTypeCardinality, unary_functions) +{ + TypeNode intToInt = d_nodeManager->mkFunctionType( + d_nodeManager->integerType(), d_nodeManager->integerType()); + TypeNode realToReal = d_nodeManager->mkFunctionType( + d_nodeManager->realType(), d_nodeManager->realType()); + TypeNode realToInt = d_nodeManager->mkFunctionType( + d_nodeManager->realType(), d_nodeManager->integerType()); + TypeNode intToReal = d_nodeManager->mkFunctionType( + d_nodeManager->integerType(), d_nodeManager->realType()); + TypeNode intToBool = d_nodeManager->mkFunctionType( + d_nodeManager->integerType(), d_nodeManager->booleanType()); + TypeNode realToBool = d_nodeManager->mkFunctionType( + d_nodeManager->realType(), d_nodeManager->booleanType()); + TypeNode boolToReal = d_nodeManager->mkFunctionType( + d_nodeManager->booleanType(), d_nodeManager->realType()); + TypeNode boolToInt = d_nodeManager->mkFunctionType( + d_nodeManager->booleanType(), d_nodeManager->integerType()); + TypeNode boolToBool = d_nodeManager->mkFunctionType( + d_nodeManager->booleanType(), d_nodeManager->booleanType()); + + ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL); +} + +TEST_F(TestNodeBlackTypeCardinality, binary_functions) +{ + std::vector<TypeNode> boolbool; + boolbool.push_back(d_nodeManager->booleanType()); + boolbool.push_back(d_nodeManager->booleanType()); + std::vector<TypeNode> boolint; + boolint.push_back(d_nodeManager->booleanType()); + boolint.push_back(d_nodeManager->integerType()); + std::vector<TypeNode> intbool; + intbool.push_back(d_nodeManager->integerType()); + intbool.push_back(d_nodeManager->booleanType()); + std::vector<TypeNode> intint; + intint.push_back(d_nodeManager->integerType()); + intint.push_back(d_nodeManager->integerType()); + std::vector<TypeNode> intreal; + intreal.push_back(d_nodeManager->integerType()); + intreal.push_back(d_nodeManager->realType()); + std::vector<TypeNode> realint; + realint.push_back(d_nodeManager->realType()); + realint.push_back(d_nodeManager->integerType()); + std::vector<TypeNode> realreal; + realreal.push_back(d_nodeManager->realType()); + realreal.push_back(d_nodeManager->realType()); + std::vector<TypeNode> realbool; + realbool.push_back(d_nodeManager->realType()); + realbool.push_back(d_nodeManager->booleanType()); + std::vector<TypeNode> boolreal; + boolreal.push_back(d_nodeManager->booleanType()); + boolreal.push_back(d_nodeManager->realType()); + + TypeNode boolboolToBool = + d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType()); + TypeNode boolboolToInt = + d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType()); + TypeNode boolboolToReal = + d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType()); + + TypeNode boolintToBool = + d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType()); + TypeNode boolintToInt = + d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType()); + TypeNode boolintToReal = + d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType()); + + TypeNode intboolToBool = + d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType()); + TypeNode intboolToInt = + d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType()); + TypeNode intboolToReal = + d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType()); + + TypeNode intintToBool = + d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType()); + TypeNode intintToInt = + d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType()); + TypeNode intintToReal = + d_nodeManager->mkFunctionType(intint, d_nodeManager->realType()); + + TypeNode intrealToBool = + d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType()); + TypeNode intrealToInt = + d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType()); + TypeNode intrealToReal = + d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType()); + + TypeNode realintToBool = + d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType()); + TypeNode realintToInt = + d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType()); + TypeNode realintToReal = + d_nodeManager->mkFunctionType(realint, d_nodeManager->realType()); + + TypeNode realrealToBool = + d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType()); + TypeNode realrealToInt = + d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType()); + TypeNode realrealToReal = + d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType()); + + TypeNode realboolToBool = + d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType()); + TypeNode realboolToInt = + d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType()); + TypeNode realboolToReal = + d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType()); + + TypeNode boolrealToBool = + d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType()); + TypeNode boolrealToInt = + d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType()); + TypeNode boolrealToReal = + d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType()); + + ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL); + ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS), + Cardinality::EQUAL); + ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::EQUAL); + + ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + + ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); + ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS), + Cardinality::GREATER); +} + +TEST_F(TestNodeBlackTypeCardinality, ternary_functions) +{ + std::vector<TypeNode> boolbool; + boolbool.push_back(d_nodeManager->booleanType()); + boolbool.push_back(d_nodeManager->booleanType()); + std::vector<TypeNode> boolboolbool = boolbool; + boolboolbool.push_back(d_nodeManager->booleanType()); + + TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool); + TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool); + + TypeNode boolboolboolToBool = + d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType()); + TypeNode boolboolToBoolbool = + d_nodeManager->mkFunctionType(boolbool, boolboolTuple); + TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType( + d_nodeManager->booleanType(), boolboolboolTuple); + + ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8), + Cardinality::EQUAL); + ASSERT_EQ( + boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4), + Cardinality::EQUAL); + ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8), + Cardinality::EQUAL); +} + +TEST_F(TestNodeBlackTypeCardinality, undefined_sorts) +{ + TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE); + // We've currently assigned them a specific Beth number, which + // isn't really correct, but... + ASSERT_FALSE(foo.getCardinality().isFinite()); +} + +TEST_F(TestNodeBlackTypeCardinality, bitvectors) +{ + ASSERT_EQ(d_nodeManager->mkBitVectorType(0).getCardinality().compare(0), + Cardinality::EQUAL); + Cardinality lastCard = 0; + for (unsigned i = 1; i <= 65; ++i) + { + Cardinality card = Cardinality(2) ^ i; + Cardinality typeCard = d_nodeManager->mkBitVectorType(i).getCardinality(); + ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER + || (typeCard.isLargeFinite() && lastCard.isLargeFinite())); + ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL + || typeCard.isLargeFinite()); + lastCard = typeCard; + } +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp new file mode 100644 index 000000000..f364e40fc --- /dev/null +++ b/test/unit/node/type_node_white.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file type_node_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 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 White box testing of TypeNode + ** + ** White box testing of TypeNode. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/node_manager.h" +#include "expr/type_node.h" +#include "smt/smt_engine.h" +#include "test_node.h" + +namespace CVC4 { + +using namespace kind; +using namespace context; + +namespace test { + +class TestNodeWhiteTypeNode : public TestNode +{ + protected: + void SetUp() override + { + TestNode::SetUp(); + d_smt.reset(new SmtEngine(d_nodeManager.get())); + } + std::unique_ptr<SmtEngine> d_smt; +}; + +TEST_F(TestNodeWhiteTypeNode, sub_types) +{ + TypeNode realType = d_nodeManager->realType(); + TypeNode integerType = d_nodeManager->realType(); + TypeNode booleanType = d_nodeManager->booleanType(); + TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType); + TypeNode bvType = d_nodeManager->mkBitVectorType(32); + + Node x = d_nodeManager->mkBoundVar("x", realType); + Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0))); + TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType); + Node lambda = d_nodeManager->mkVar("lambda", funtype); + std::vector<Node> formals; + formals.push_back(x); + d_smt->defineFunction(lambda, formals, xPos); + + ASSERT_FALSE(realType.isComparableTo(booleanType)); + ASSERT_TRUE(realType.isComparableTo(integerType)); + ASSERT_TRUE(realType.isComparableTo(realType)); + ASSERT_FALSE(realType.isComparableTo(arrayType)); + ASSERT_FALSE(realType.isComparableTo(bvType)); + + ASSERT_FALSE(booleanType.isComparableTo(integerType)); + ASSERT_FALSE(booleanType.isComparableTo(realType)); + ASSERT_TRUE(booleanType.isComparableTo(booleanType)); + ASSERT_FALSE(booleanType.isComparableTo(arrayType)); + ASSERT_FALSE(booleanType.isComparableTo(bvType)); + + ASSERT_TRUE(integerType.isComparableTo(realType)); + ASSERT_TRUE(integerType.isComparableTo(integerType)); + ASSERT_FALSE(integerType.isComparableTo(booleanType)); + ASSERT_FALSE(integerType.isComparableTo(arrayType)); + ASSERT_FALSE(integerType.isComparableTo(bvType)); + + ASSERT_FALSE(arrayType.isComparableTo(booleanType)); + ASSERT_FALSE(arrayType.isComparableTo(integerType)); + ASSERT_FALSE(arrayType.isComparableTo(realType)); + ASSERT_TRUE(arrayType.isComparableTo(arrayType)); + ASSERT_FALSE(arrayType.isComparableTo(bvType)); + + ASSERT_FALSE(bvType.isComparableTo(booleanType)); + ASSERT_FALSE(bvType.isComparableTo(integerType)); + ASSERT_FALSE(bvType.isComparableTo(realType)); + ASSERT_FALSE(bvType.isComparableTo(arrayType)); + ASSERT_TRUE(bvType.isComparableTo(bvType)); + + ASSERT_TRUE(realType.getBaseType() == realType); + ASSERT_TRUE(integerType.getBaseType() == realType); + ASSERT_TRUE(booleanType.getBaseType() == booleanType); + ASSERT_TRUE(arrayType.getBaseType() == arrayType); + ASSERT_TRUE(bvType.getBaseType() == bvType); +} +} // namespace test +} // namespace CVC4 |