From: Aina Niemetz Date: Wed, 17 Mar 2021 18:07:48 +0000 (-0700) Subject: Rename test/unit/expr to test/unit/node. (#6156) X-Git-Tag: cvc5-1.0.0~2063 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bbf9eee55db6851c0923252cdda8946030c3c75a;p=cvc5.git Rename test/unit/expr to test/unit/node. (#6156) This is in preparation for renaming src/expr to src/node. --- diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 350127a14..71568e337 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -84,7 +84,7 @@ endmacro() add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) -add_subdirectory(expr) +add_subdirectory(node) add_subdirectory(main) add_subdirectory(parser) add_subdirectory(printer) diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt deleted file mode 100644 index 52e591aeb..000000000 --- a/test/unit/expr/CMakeLists.txt +++ /dev/null @@ -1,28 +0,0 @@ -##################### -## 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/expr/attribute_black.cpp b/test/unit/expr/attribute_black.cpp deleted file mode 100644 index 64605bdb9..000000000 --- a/test/unit/expr/attribute_black.cpp +++ /dev/null @@ -1,128 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 TestExprBlackAttribute : public TestNode -{ - protected: - struct PrimitiveIntAttributeId - { - }; - using PrimitiveIntAttribute = - expr::Attribute; - struct TNodeAttributeId - { - }; - using TNodeAttribute = expr::Attribute; - struct StringAttributeId - { - }; - using StringAttribute = expr::Attribute; - struct BoolAttributeId - { - }; - using BoolAttribute = expr::Attribute; -}; - -TEST_F(TestExprBlackAttribute, 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(TestExprBlackAttribute, 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(TestExprBlackAttribute, 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(TestExprBlackAttribute, 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/expr/attribute_white.cpp b/test/unit/expr/attribute_white.cpp deleted file mode 100644 index e9a12261b..000000000 --- a/test/unit/expr/attribute_white.cpp +++ /dev/null @@ -1,448 +0,0 @@ -/********************* */ -/*! \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 - -#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 TestStringAttr1; -typedef Attribute TestStringAttr2; - -using TestFlag1 = Attribute; -using TestFlag2 = Attribute; -using TestFlag3 = Attribute; -using TestFlag4 = Attribute; -using TestFlag5 = Attribute; - -class TestExprWhiteAttribute : public TestNode -{ - protected: - void SetUp() override - { - TestNode::SetUp(); - d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); - } - std::unique_ptr d_booleanType; -}; - -TEST_F(TestExprWhiteAttribute, 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::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::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::getId(); - ASSERT_LT(TypeAttr::s_id, lastId); -} - -TEST_F(TestExprWhiteAttribute, 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/expr/kind_black.cpp b/test/unit/expr/kind_black.cpp deleted file mode 100644 index b8e764726..000000000 --- a/test/unit/expr/kind_black.cpp +++ /dev/null @@ -1,90 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#include "expr/kind.h" -#include "test.h" - -namespace CVC4 { - -using namespace kind; - -namespace test { - -class TestExprBlackKind : 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(TestExprBlackKind, equality) -{ - ASSERT_EQ(d_undefined, UNDEFINED_KIND); - ASSERT_EQ(d_last, LAST_KIND); -} - -TEST_F(TestExprBlackKind, 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(TestExprBlackKind, 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(TestExprBlackKind, 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/expr/kind_map_black.cpp b/test/unit/expr/kind_map_black.cpp deleted file mode 100644 index ac40d8ed6..000000000 --- a/test/unit/expr/kind_map_black.cpp +++ /dev/null @@ -1,48 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#include "expr/kind_map.h" -#include "test.h" - -namespace CVC4 { - -using namespace kind; - -namespace test { - -class TestExprBlackKindMap : public TestInternal -{ -}; - -TEST_F(TestExprBlackKindMap, 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/expr/node_algorithm_black.cpp b/test/unit/expr/node_algorithm_black.cpp deleted file mode 100644 index bd243e0fd..000000000 --- a/test/unit/expr/node_algorithm_black.cpp +++ /dev/null @@ -1,202 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 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 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 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 > result = - std::map >(); - - // 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(1, 0)); - Node extractOp2 = - d_nodeManager->mkConst(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 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/expr/node_black.cpp b/test/unit/expr/node_black.cpp deleted file mode 100644 index 3c1651155..000000000 --- a/test/unit/expr/node_black.cpp +++ /dev/null @@ -1,787 +0,0 @@ -/********************* */ -/*! \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 -#include -#include -#include - -#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 makeNSkolemNodes(NodeManager* nodeManager, - uint32_t n, - TypeNode type) -{ - std::vector skolems; - for (uint32_t i = 0; i < n; i++) - { - skolems.push_back(nodeManager->mkSkolem( - "skolem_", type, "Created by makeNSkolemNodes()")); - } - return skolems; -} -} // namespace - -class TestNodeBlackNode : public 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 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 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 skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); - Node add = d_nodeManager->mkNode(kind::PLUS, skolems); - std::vector children; - for (Node child : add) - { - children.push_back(child); - } - ASSERT_TRUE(children.size() == skolems.size() - && std::equal(children.begin(), children.end(), skolems.begin())); -} - -TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) -{ - const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); - Node add = d_nodeManager->mkNode(kind::PLUS, skolems); - std::vector children; - for (TNode child : add) - { - children.push_back(child); - } - ASSERT_TRUE(children.size() == skolems.size() - && std::equal(children.begin(), children.end(), skolems.begin())); -} - -TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) -{ - const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); - Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); - TNode add_tnode = add_node; - std::vector children; - for (Node child : add_tnode) - { - children.push_back(child); - } - ASSERT_TRUE(children.size() == skolems.size() - && std::equal(children.begin(), children.end(), skolems.begin())); -} - -TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode) -{ - const std::vector skolems = - makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); - Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); - TNode add_tnode = add_node; - std::vector children; - for (TNode child : add_tnode) - { - children.push_back(child); - } - ASSERT_TRUE(children.size() == skolems.size() - && std::equal(children.begin(), children.end(), skolems.begin())); -} - -TEST_F(TestNodeBlackNode, isConst) -{ - // more complicated "constants" exist in datatypes and arrays theories - DType list("list"); - std::shared_ptr consC = - std::make_shared("cons"); - consC->addArg("car", d_nodeManager->integerType()); - consC->addArgSelf("cdr"); - list.addConstructor(consC); - list.addConstructor(std::make_shared("nil")); - TypeNode listType = d_nodeManager->mkDatatypeType(list); - const std::vector >& lcons = - listType.getDType().getConstructors(); - Node cons = lcons[0]->getConstructor(); - Node nil = lcons[1]->getConstructor(); - Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); - Node cons_x_nil = - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - x, - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); - Node cons_1_nil = - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); - Node cons_1_cons_2_nil = d_nodeManager->mkNode( - APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(1)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, - cons, - d_nodeManager->mkConst(Rational(2)), - d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); - ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); - ASSERT_FALSE(cons_x_nil.isConst()); - ASSERT_TRUE(cons_1_nil.isConst()); - ASSERT_TRUE(cons_1_cons_2_nil.isConst()); - - TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), - d_nodeManager->integerType()); - Node zero = d_nodeManager->mkConst(Rational(0)); - Node one = d_nodeManager->mkConst(Rational(1)); - Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); - ASSERT_TRUE(storeAll.isConst()); - - Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); - ASSERT_FALSE(arr.isConst()); - arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); - ASSERT_TRUE(arr.isConst()); - Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - ASSERT_FALSE(arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - ASSERT_FALSE(arr2.isConst()); - - arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), - d_nodeManager->mkBitVectorType(1)); - zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); - one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); - storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); - ASSERT_TRUE(storeAll.isConst()); - - arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); - ASSERT_FALSE(arr.isConst()); - arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); - ASSERT_TRUE(arr.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); - ASSERT_FALSE(arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, one, one); - ASSERT_FALSE(arr2.isConst()); - arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); - ASSERT_FALSE(arr2.isConst()); -} - -namespace { -Node level0(NodeManager* nm) -{ - NodeBuilder<> nb(kind::AND); - Node x = nm->mkSkolem("x", nm->booleanType()); - nb << x; - nb << x; - return Node(nb.constructNode()); -} -TNode level1(NodeManager* nm) { return level0(nm); } -} // namespace - -/** - * This is for demonstrating what a certain type of user error looks like. - */ -TEST_F(TestNodeBlackNode, node_tnode_usage) -{ - Node n; - ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get())); - ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0"); -} - -} // namespace test -} // namespace CVC4 diff --git a/test/unit/expr/node_builder_black.cpp b/test/unit/expr/node_builder_black.cpp deleted file mode 100644 index 7e38dd899..000000000 --- a/test/unit/expr/node_builder_black.cpp +++ /dev/null @@ -1,590 +0,0 @@ -/********************* */ -/*! \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 - -#include -#include - -#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 - void push_back(NodeBuilder& 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 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 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 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 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* ws_size_large = new NodeBuilder; - 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 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 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 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* nb = new NodeBuilder(); - delete nb; -} - -TEST_F(TestNodeBlackNodeBuilder, begin_end) -{ - /* Test begin() and end() without resizing. */ - NodeBuilder ws(d_specKind); - ASSERT_EQ(ws.begin(), ws.end()); - - push_back(ws, K); - ASSERT_NE(ws.begin(), ws.end()); - - NodeBuilder::iterator iter = ws.begin(); - for (uint32_t i = 0; i < K; ++i) - { - ASSERT_NE(iter, ws.end()); - ++iter; - } - ASSERT_EQ(iter, ws.end()); - - NodeBuilder::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 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(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 v; - v.push_back(m); - v.push_back(p); - v.push_back(q); - - /* test append(vector) */ - 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 implicit(d_specKind); - NodeBuilder 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/expr/node_manager_black.cpp b/test/unit/expr/node_manager_black.cpp deleted file mode 100644 index a2ede3ed0..000000000 --- a/test/unit/expr/node_manager_black.cpp +++ /dev/null @@ -1,333 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 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 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(), true); - Node ff = d_nodeManager->mkConst(false); - ASSERT_EQ(ff.getConst(), false); -} - -TEST_F(TestNodeBlackNodeManager, mkConst_rational) -{ - Rational r("3/2"); - Node n = d_nodeManager->mkConst(r); - ASSERT_EQ(n.getConst(), 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 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 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 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 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/expr/node_manager_white.cpp b/test/unit/expr/node_manager_white.cpp deleted file mode 100644 index daf211b78..000000000 --- a/test/unit/expr/node_manager_white.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \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 - -#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 roots = {n1.d_nv}; - ASSERT_EQ(NodeManager::TopologicalSort(roots), roots); - } - - { - std::vector roots = {n2.d_nv, n1.d_nv}; - std::vector result = {n1.d_nv, n2.d_nv}; - ASSERT_EQ(NodeManager::TopologicalSort(roots), result); - } -} -} // namespace test -} // namespace CVC4 diff --git a/test/unit/expr/node_self_iterator_black.cpp b/test/unit/expr/node_self_iterator_black.cpp deleted file mode 100644 index 34ab5f09b..000000000 --- a/test/unit/expr/node_self_iterator_black.cpp +++ /dev/null @@ -1,57 +0,0 @@ -/********************* */ -/*! \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/expr/node_traversal_black.cpp b/test/unit/expr/node_traversal_black.cpp deleted file mode 100644 index e443ff685..000000000 --- a/test/unit/expr/node_traversal_black.cpp +++ /dev/null @@ -1,296 +0,0 @@ -/********************* */ -/*! \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 -#include -#include -#include -#include -#include - -#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 expected = {tb, eb, cnd, top}; - - auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); - - std::vector 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 expected = {top}; - - auto traversal = NodeDfsIterable( - top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; }); - - std::vector 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 expected = {}; - - auto traversal = - NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; }); - - std::vector 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 expected = {top, cnd, tb, eb}; - - auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); - - std::vector 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 expected = {top, cnd, eb}; - - auto traversal = NodeDfsIterable( - top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; }); - - std::vector actual; - std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual)); - ASSERT_EQ(actual, expected); -} -} // namespace test -} // namespace CVC4 diff --git a/test/unit/expr/node_white.cpp b/test/unit/expr/node_white.cpp deleted file mode 100644 index 651dd1990..000000000 --- a/test/unit/expr/node_white.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \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 - -#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 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/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp deleted file mode 100644 index 10fb52f6d..000000000 --- a/test/unit/expr/symbol_table_black.cpp +++ /dev/null @@ -1,149 +0,0 @@ -/********************* */ -/*! \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 -#include - -#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 TestSymbolTableBlack : public TestApi -{ -}; - -TEST_F(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, 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(TestSymbolTableBlack, bad_pop) -{ - SymbolTable symtab; - ASSERT_THROW(symtab.popScope(), ScopeException); -} - -} // namespace test -} // namespace CVC4 diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp deleted file mode 100644 index 58024fa53..000000000 --- a/test/unit/expr/type_cardinality_black.cpp +++ /dev/null @@ -1,335 +0,0 @@ -/********************* */ -/*! \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 - -#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 TestTypeCardinalityBlack : public TestNode -{ -}; - -TEST_F(TestTypeCardinalityBlack, 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(TestTypeCardinalityBlack, 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(TestTypeCardinalityBlack, 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(TestTypeCardinalityBlack, binary_functions) -{ - std::vector boolbool; - boolbool.push_back(d_nodeManager->booleanType()); - boolbool.push_back(d_nodeManager->booleanType()); - std::vector boolint; - boolint.push_back(d_nodeManager->booleanType()); - boolint.push_back(d_nodeManager->integerType()); - std::vector intbool; - intbool.push_back(d_nodeManager->integerType()); - intbool.push_back(d_nodeManager->booleanType()); - std::vector intint; - intint.push_back(d_nodeManager->integerType()); - intint.push_back(d_nodeManager->integerType()); - std::vector intreal; - intreal.push_back(d_nodeManager->integerType()); - intreal.push_back(d_nodeManager->realType()); - std::vector realint; - realint.push_back(d_nodeManager->realType()); - realint.push_back(d_nodeManager->integerType()); - std::vector realreal; - realreal.push_back(d_nodeManager->realType()); - realreal.push_back(d_nodeManager->realType()); - std::vector realbool; - realbool.push_back(d_nodeManager->realType()); - realbool.push_back(d_nodeManager->booleanType()); - std::vector 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(TestTypeCardinalityBlack, ternary_functions) -{ - std::vector boolbool; - boolbool.push_back(d_nodeManager->booleanType()); - boolbool.push_back(d_nodeManager->booleanType()); - std::vector 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(TestTypeCardinalityBlack, 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(TestTypeCardinalityBlack, 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/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp deleted file mode 100644 index f364e40fc..000000000 --- a/test/unit/expr/type_node_white.cpp +++ /dev/null @@ -1,97 +0,0 @@ -/********************* */ -/*! \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 -#include -#include - -#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 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 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 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 +#include + +#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; + struct TNodeAttributeId + { + }; + using TNodeAttribute = expr::Attribute; + struct StringAttributeId + { + }; + using StringAttribute = expr::Attribute; + struct BoolAttributeId + { + }; + using BoolAttribute = expr::Attribute; +}; + +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 + +#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 TestStringAttr1; +typedef Attribute TestStringAttr2; + +using TestFlag1 = Attribute; +using TestFlag2 = Attribute; +using TestFlag3 = Attribute; +using TestFlag4 = Attribute; +using TestFlag5 = Attribute; + +class TestNodeWhiteAttribute : public TestNode +{ + protected: + void SetUp() override + { + TestNode::SetUp(); + d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); + } + std::unique_ptr 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::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::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::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 +#include +#include + +#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 +#include +#include + +#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 +#include + +#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 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 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 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 > result = + std::map >(); + + // 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(1, 0)); + Node extractOp2 = + d_nodeManager->mkConst(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 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 +#include +#include +#include + +#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 makeNSkolemNodes(NodeManager* nodeManager, + uint32_t n, + TypeNode type) +{ + std::vector skolems; + for (uint32_t i = 0; i < n; i++) + { + skolems.push_back(nodeManager->mkSkolem( + "skolem_", type, "Created by makeNSkolemNodes()")); + } + return skolems; +} +} // namespace + +class TestNodeBlackNode : public 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 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 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 skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (Node child : add) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add = d_nodeManager->mkNode(kind::PLUS, skolems); + std::vector children; + for (TNode child : add) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + TNode add_tnode = add_node; + std::vector children; + for (Node child : add_tnode) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode) +{ + const std::vector skolems = + makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType()); + Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems); + TNode add_tnode = add_node; + std::vector children; + for (TNode child : add_tnode) + { + children.push_back(child); + } + ASSERT_TRUE(children.size() == skolems.size() + && std::equal(children.begin(), children.end(), skolems.begin())); +} + +TEST_F(TestNodeBlackNode, isConst) +{ + // more complicated "constants" exist in datatypes and arrays theories + DType list("list"); + std::shared_ptr consC = + std::make_shared("cons"); + consC->addArg("car", d_nodeManager->integerType()); + consC->addArgSelf("cdr"); + list.addConstructor(consC); + list.addConstructor(std::make_shared("nil")); + TypeNode listType = d_nodeManager->mkDatatypeType(list); + const std::vector >& lcons = + listType.getDType().getConstructors(); + Node cons = lcons[0]->getConstructor(); + Node nil = lcons[1]->getConstructor(); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType()); + Node cons_x_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + x, + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_nil = + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)); + Node cons_1_cons_2_nil = d_nodeManager->mkNode( + APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(1)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, + cons, + d_nodeManager->mkConst(Rational(2)), + d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil))); + ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst()); + ASSERT_FALSE(cons_x_nil.isConst()); + ASSERT_TRUE(cons_1_nil.isConst()); + ASSERT_TRUE(cons_1_cons_2_nil.isConst()); + + TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), + d_nodeManager->integerType()); + Node zero = d_nodeManager->mkConst(Rational(0)); + Node one = d_nodeManager->mkConst(Rational(1)); + Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + ASSERT_TRUE(arr.isConst()); + Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); + + arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), + d_nodeManager->mkBitVectorType(1)); + zero = d_nodeManager->mkConst(BitVector(1, unsigned(0))); + one = d_nodeManager->mkConst(BitVector(1, unsigned(1))); + storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); + ASSERT_TRUE(storeAll.isConst()); + + arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); + ASSERT_FALSE(arr.isConst()); + arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); + ASSERT_TRUE(arr.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, one, one); + ASSERT_FALSE(arr2.isConst()); + arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); + ASSERT_FALSE(arr2.isConst()); +} + +namespace { +Node level0(NodeManager* nm) +{ + NodeBuilder<> nb(kind::AND); + Node x = nm->mkSkolem("x", nm->booleanType()); + nb << x; + nb << x; + return Node(nb.constructNode()); +} +TNode level1(NodeManager* nm) { return level0(nm); } +} // namespace + +/** + * This is for demonstrating what a certain type of user error looks like. + */ +TEST_F(TestNodeBlackNode, node_tnode_usage) +{ + Node n; + ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get())); + ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0"); +} + +} // namespace test +} // namespace CVC4 diff --git a/test/unit/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 + +#include +#include + +#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 + void push_back(NodeBuilder& 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 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 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 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 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* ws_size_large = new NodeBuilder; + 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 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 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 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* nb = new NodeBuilder(); + delete nb; +} + +TEST_F(TestNodeBlackNodeBuilder, begin_end) +{ + /* Test begin() and end() without resizing. */ + NodeBuilder ws(d_specKind); + ASSERT_EQ(ws.begin(), ws.end()); + + push_back(ws, K); + ASSERT_NE(ws.begin(), ws.end()); + + NodeBuilder::iterator iter = ws.begin(); + for (uint32_t i = 0; i < K; ++i) + { + ASSERT_NE(iter, ws.end()); + ++iter; + } + ASSERT_EQ(iter, ws.end()); + + NodeBuilder::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 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(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 v; + v.push_back(m); + v.push_back(p); + v.push_back(q); + + /* test append(vector) */ + 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 implicit(d_specKind); + NodeBuilder 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 +#include + +#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 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 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(), true); + Node ff = d_nodeManager->mkConst(false); + ASSERT_EQ(ff.getConst(), false); +} + +TEST_F(TestNodeBlackNodeManager, mkConst_rational) +{ + Rational r("3/2"); + Node n = d_nodeManager->mkConst(r); + ASSERT_EQ(n.getConst(), 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 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 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 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 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 + +#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 roots = {n1.d_nv}; + ASSERT_EQ(NodeManager::TopologicalSort(roots), roots); + } + + { + std::vector roots = {n2.d_nv, n1.d_nv}; + std::vector 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 +#include +#include +#include +#include +#include + +#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 expected = {tb, eb, cnd, top}; + + auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER); + + std::vector 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 expected = {top}; + + auto traversal = NodeDfsIterable( + top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; }); + + std::vector 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 expected = {}; + + auto traversal = + NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; }); + + std::vector 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 expected = {top, cnd, tb, eb}; + + auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER); + + std::vector 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 expected = {top, cnd, eb}; + + auto traversal = NodeDfsIterable( + top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; }); + + std::vector 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 + +#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 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 +#include + +#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 + +#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 boolbool; + boolbool.push_back(d_nodeManager->booleanType()); + boolbool.push_back(d_nodeManager->booleanType()); + std::vector boolint; + boolint.push_back(d_nodeManager->booleanType()); + boolint.push_back(d_nodeManager->integerType()); + std::vector intbool; + intbool.push_back(d_nodeManager->integerType()); + intbool.push_back(d_nodeManager->booleanType()); + std::vector intint; + intint.push_back(d_nodeManager->integerType()); + intint.push_back(d_nodeManager->integerType()); + std::vector intreal; + intreal.push_back(d_nodeManager->integerType()); + intreal.push_back(d_nodeManager->realType()); + std::vector realint; + realint.push_back(d_nodeManager->realType()); + realint.push_back(d_nodeManager->integerType()); + std::vector realreal; + realreal.push_back(d_nodeManager->realType()); + realreal.push_back(d_nodeManager->realType()); + std::vector realbool; + realbool.push_back(d_nodeManager->realType()); + realbool.push_back(d_nodeManager->booleanType()); + std::vector 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 boolbool; + boolbool.push_back(d_nodeManager->booleanType()); + boolbool.push_back(d_nodeManager->booleanType()); + std::vector 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 +#include +#include + +#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 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 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