This is in preparation for renaming src/expr to src/node.
add_subdirectory(api)
add_subdirectory(base)
add_subdirectory(context)
-add_subdirectory(expr)
+add_subdirectory(node)
add_subdirectory(main)
add_subdirectory(parser)
add_subdirectory(printer)
+++ /dev/null
-#####################
-## 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)
+++ /dev/null
-/********************* */
-/*! \file attribute_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::Attribute.
- **
- ** Black box testing of CVC4::Attribute.
- **/
-
-#include <sstream>
-#include <vector>
-
-#include "expr/attribute.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_value.h"
-#include "test_node.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace smt;
-
-namespace test {
-
-class TestExprBlackAttribute : public TestNode
-{
- protected:
- struct PrimitiveIntAttributeId
- {
- };
- using PrimitiveIntAttribute =
- expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
- struct TNodeAttributeId
- {
- };
- using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
- struct StringAttributeId
- {
- };
- using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
- struct BoolAttributeId
- {
- };
- using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
-};
-
-TEST_F(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
+++ /dev/null
-/********************* */
-/*! \file attribute_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief White box testing of Node attributes.
- **
- ** White box testing of Node attributes.
- **/
-
-#include <string>
-
-#include "base/check.h"
-#include "expr/attribute.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_manager_attributes.h"
-#include "expr/node_value.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "test_node.h"
-#include "theory/theory.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/theory_uf.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace smt;
-using namespace expr;
-using namespace expr::attr;
-
-namespace test {
-
-struct Test1;
-struct Test2;
-struct Test3;
-struct Test4;
-struct Test5;
-
-typedef Attribute<Test1, std::string> TestStringAttr1;
-typedef Attribute<Test2, std::string> TestStringAttr2;
-
-using TestFlag1 = Attribute<Test1, bool>;
-using TestFlag2 = Attribute<Test2, bool>;
-using TestFlag3 = Attribute<Test3, bool>;
-using TestFlag4 = Attribute<Test4, bool>;
-using TestFlag5 = Attribute<Test5, bool>;
-
-class TestExprWhiteAttribute : public TestNode
-{
- protected:
- void SetUp() override
- {
- TestNode::SetUp();
- d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
- }
- std::unique_ptr<TypeNode> 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<std::string, false>::getId();
- ASSERT_LT(VarNameAttr::s_id, lastId);
- ASSERT_LT(TestStringAttr1::s_id, lastId);
- ASSERT_LT(TestStringAttr2::s_id, lastId);
-
- ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id);
- ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
- ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
-
- lastId = attr::LastAttributeId<bool, false>::getId();
- ASSERT_LT(TestFlag1::s_id, lastId);
- ASSERT_LT(TestFlag2::s_id, lastId);
- ASSERT_LT(TestFlag3::s_id, lastId);
- ASSERT_LT(TestFlag4::s_id, lastId);
- ASSERT_LT(TestFlag5::s_id, lastId);
- ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id);
- ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id);
- ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id);
- ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id);
- ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id);
- ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id);
- ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id);
- ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id);
- ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id);
- ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id);
-
- lastId = attr::LastAttributeId<TypeNode, false>::getId();
- ASSERT_LT(TypeAttr::s_id, lastId);
-}
-
-TEST_F(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
+++ /dev/null
-/********************* */
-/*! \file kind_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::Kind.
- **
- ** Black box testing of CVC4::Kind.
- **/
-
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "expr/kind.h"
-#include "test.h"
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-class 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
+++ /dev/null
-/********************* */
-/*! \file kind_map_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Gereon Kremer
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::KindMap
- **
- ** Black box testing of CVC4::KindMap.
- **/
-
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "expr/kind_map.h"
-#include "test.h"
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-class 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
+++ /dev/null
-/********************* */
-/*! \file node_algorithm_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of utility functions in node_algorithm.{h,cpp}
- **
- ** Black box testing of node_algorithm.{h,cpp}
- **/
-
-#include <string>
-#include <vector>
-
-#include "base/output.h"
-#include "expr/node_algorithm.h"
-#include "expr/node_manager.h"
-#include "test_node.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "util/integer.h"
-#include "util/rational.h"
-
-namespace CVC4 {
-
-using namespace expr;
-using namespace kind;
-
-namespace test {
-
-class TestNodeBlackNodeAlgorithm : public TestNode
-{
-};
-
-TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
-{
- // The only symbol in ~x (x is a boolean varible) should be x
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(NOT, x);
- std::unordered_set<Node, NodeHashFunction> syms;
- getSymbols(n, syms);
- ASSERT_EQ(syms.size(), 1);
- ASSERT_NE(syms.find(x), syms.end());
-}
-
-TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
-{
- // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because
- // "var" is bound.
-
- // left conjunct
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType());
- Node left = d_nodeManager->mkNode(EQUAL, x, y);
-
- // right conjunct
- Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
- std::vector<Node> vars;
- vars.push_back(var);
- Node sum = d_nodeManager->mkNode(PLUS, var, var);
- Node qeq = d_nodeManager->mkNode(EQUAL, x, sum);
- Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars);
- Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq);
-
- // conjunction
- Node res = d_nodeManager->mkNode(AND, left, right);
-
- // symbols
- std::unordered_set<Node, NodeHashFunction> syms;
- getSymbols(res, syms);
-
- // assertions
- ASSERT_EQ(syms.size(), 2);
- ASSERT_NE(syms.find(x), syms.end());
- ASSERT_NE(syms.find(y), syms.end());
- ASSERT_EQ(syms.find(var), syms.end());
-}
-
-TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
-{
- // map to store result
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
- std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
-
- // create test formula
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
- Node plus = d_nodeManager->mkNode(PLUS, x, x);
- Node mul = d_nodeManager->mkNode(MULT, x, x);
- Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
-
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4));
- Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
- Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
- Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
-
- Node formula = d_nodeManager->mkNode(AND, eq1, eq2);
-
- // call function
- expr::getOperatorsMap(formula, result);
-
- // Verify result
- // We should have only integer, bv and boolean as types
- ASSERT_EQ(result.size(), 3);
- ASSERT_NE(result.find(*d_intTypeNode), result.end());
- ASSERT_NE(result.find(*d_boolTypeNode), result.end());
- ASSERT_NE(result.find(*d_bvTypeNode), result.end());
-
- // in integers, we should only have plus and mult as operators
- ASSERT_EQ(result[*d_intTypeNode].size(), 2);
- ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
- result[*d_intTypeNode].end());
- ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
- result[*d_intTypeNode].end());
-
- // in booleans, we should only have "=" and "and" as an operator.
- ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
- ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
- result[*d_boolTypeNode].end());
- ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
- result[*d_boolTypeNode].end());
-
- // in bv, we should only have "extract" as an operator.
- ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
- Node extractOp1 =
- d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
- Node extractOp2 =
- d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
- ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
- result[*d_bvTypeNode].end());
- ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
- result[*d_bvTypeNode].end());
-}
-
-TEST_F(TestNodeBlackNodeAlgorithm, match)
-{
- TypeNode integer = d_nodeManager->integerType();
-
- Node one = d_nodeManager->mkConst(Rational(1));
- Node two = d_nodeManager->mkConst(Rational(2));
-
- Node x = d_nodeManager->mkBoundVar(integer);
- Node a = d_nodeManager->mkSkolem("a", integer);
-
- Node n1 = d_nodeManager->mkNode(MULT, two, x);
- std::unordered_map<Node, Node, NodeHashFunction> subs;
-
- // check reflexivity
- ASSERT_TRUE(match(n1, n1, subs));
- ASSERT_EQ(subs.size(), 0);
-
- Node n2 = d_nodeManager->mkNode(MULT, two, a);
- subs.clear();
-
- // check instance
- ASSERT_TRUE(match(n1, n2, subs));
- ASSERT_EQ(subs.size(), 1);
- ASSERT_EQ(subs[x], a);
-
- // should return false for flipped arguments (match is not symmetric)
- ASSERT_FALSE(match(n2, n1, subs));
-
- n2 = d_nodeManager->mkNode(MULT, one, a);
-
- // should return false since n2 is not an instance of n1
- ASSERT_FALSE(match(n1, n2, subs));
-
- n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);
-
- // should return false for similar operators
- ASSERT_FALSE(match(n1, n2, subs));
-
- n2 = d_nodeManager->mkNode(MULT, two, a, one);
-
- // should return false for different number of arguments
- ASSERT_FALSE(match(n1, n2, subs));
-
- n1 = x;
- n2 = d_nodeManager->mkConst(true);
-
- // should return false for different types
- ASSERT_FALSE(match(n1, n2, subs));
-
- n1 = d_nodeManager->mkNode(MULT, x, x);
- n2 = d_nodeManager->mkNode(MULT, two, a);
-
- // should return false for contradictory substitutions
- ASSERT_FALSE(match(n1, n2, subs));
-
- n2 = d_nodeManager->mkNode(MULT, a, a);
- subs.clear();
-
- // implementation: check if the cache works correctly
- ASSERT_TRUE(match(n1, n2, subs));
- ASSERT_EQ(subs.size(), 1);
- ASSERT_EQ(subs[x], a);
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file node_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::Node.
- **
- ** Black box testing of CVC4::Node.
- **/
-
-#include <algorithm>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "api/cvc4cpp.h"
-#include "expr/dtype.h"
-#include "expr/dtype_cons.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "smt/smt_engine.h"
-#include "test_node.h"
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-namespace {
-/** Returns N skolem nodes from 'nodeManager' with the same `type`. */
-std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
- uint32_t n,
- TypeNode type)
-{
- std::vector<Node> skolems;
- for (uint32_t i = 0; i < n; i++)
- {
- skolems.push_back(nodeManager->mkSkolem(
- "skolem_", type, "Created by makeNSkolemNodes()"));
- }
- return skolems;
-}
-} // namespace
-
-class TestNodeBlackNode : public TestNode
-{
- protected:
- void SetUp() override
- {
- TestNode::SetUp();
- // setup an SMT engine so that options are in scope
- Options opts;
- char* argv[2];
- argv[0] = strdup("");
- argv[1] = strdup("--output-lang=ast");
- Options::parseOptions(&opts, 2, argv);
- free(argv[0]);
- free(argv[1]);
- d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
- }
-
- std::unique_ptr<SmtEngine> d_smt;
-
- bool imp(bool a, bool b) const { return (!a) || (b); }
- bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
-
- void testNaryExpForSize(Kind k, uint32_t n)
- {
- NodeBuilder<> nbz(k);
- Node trueNode = d_nodeManager->mkConst(true);
- for (uint32_t i = 0; i < n; ++i)
- {
- nbz << trueNode;
- }
- Node result = nbz;
- ASSERT_EQ(n, result.getNumChildren());
- }
-};
-
-TEST_F(TestNodeBlackNode, null) { Node::null(); }
-
-TEST_F(TestNodeBlackNode, is_null)
-{
- Node a = Node::null();
- ASSERT_TRUE(a.isNull());
-
- Node b = Node();
- ASSERT_TRUE(b.isNull());
-
- Node c = b;
- ASSERT_TRUE(c.isNull());
-}
-
-TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
-
-TEST_F(TestNodeBlackNode, dtor)
-{
- /* No access to internals? Only test that this is crash free. */
- Node* n = nullptr;
- ASSERT_NO_FATAL_FAILURE(n = new Node());
- if (n)
- {
- delete n;
- }
-}
-
-/* operator== */
-TEST_F(TestNodeBlackNode, operator_equals)
-{
- Node a, b, c;
-
- b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
- a = b;
- c = a;
-
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
-
- ASSERT_TRUE(a == a);
- ASSERT_TRUE(a == b);
- ASSERT_TRUE(a == c);
-
- ASSERT_TRUE(b == a);
- ASSERT_TRUE(b == b);
- ASSERT_TRUE(b == c);
-
- ASSERT_TRUE(c == a);
- ASSERT_TRUE(c == b);
- ASSERT_TRUE(c == c);
-
- ASSERT_TRUE(d == d);
-
- ASSERT_FALSE(d == a);
- ASSERT_FALSE(d == b);
- ASSERT_FALSE(d == c);
-
- ASSERT_FALSE(a == d);
- ASSERT_FALSE(b == d);
- ASSERT_FALSE(c == d);
-}
-
-/* operator!= */
-TEST_F(TestNodeBlackNode, operator_not_equals)
-{
- Node a, b, c;
-
- b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
- a = b;
- c = a;
-
- Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
-
- /*structed assuming operator == works */
- ASSERT_TRUE(iff(a != a, !(a == a)));
- ASSERT_TRUE(iff(a != b, !(a == b)));
- ASSERT_TRUE(iff(a != c, !(a == c)));
-
- ASSERT_TRUE(iff(b != a, !(b == a)));
- ASSERT_TRUE(iff(b != b, !(b == b)));
- ASSERT_TRUE(iff(b != c, !(b == c)));
-
- ASSERT_TRUE(iff(c != a, !(c == a)));
- ASSERT_TRUE(iff(c != b, !(c == b)));
- ASSERT_TRUE(iff(c != c, !(c == c)));
-
- ASSERT_TRUE(!(d != d));
-
- ASSERT_TRUE(d != a);
- ASSERT_TRUE(d != b);
- ASSERT_TRUE(d != c);
-}
-
-/* operator[] */
-TEST_F(TestNodeBlackNode, operator_square)
-{
-#ifdef CVC4_ASSERTIONS
- // Basic bounds check on a node w/out children
- ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
- ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
-#endif
-
- // Basic access check
- Node tb = d_nodeManager->mkConst(true);
- Node eb = d_nodeManager->mkConst(false);
- Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- Node ite = cnd.iteNode(tb, eb);
-
- ASSERT_EQ(tb, cnd[0]);
- ASSERT_EQ(eb, cnd[1]);
-
- ASSERT_EQ(cnd, ite[0]);
- ASSERT_EQ(tb, ite[1]);
- ASSERT_EQ(eb, ite[2]);
-
-#ifdef CVC4_ASSERTIONS
- // Bounds check on a node with children
- ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
- ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
-#endif
-}
-
-/* operator= */
-TEST_F(TestNodeBlackNode, operator_assign)
-{
- Node a, b;
- Node c = d_nodeManager->mkNode(
- NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
-
- b = c;
- ASSERT_EQ(b, c);
-
- a = b = c;
-
- ASSERT_EQ(a, b);
- ASSERT_EQ(a, c);
-}
-
-/* operator< */
-TEST_F(TestNodeBlackNode, operator_less_than)
-{
- // We don't have access to the ids so we can't test the implementation
- // in the black box tests.
-
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
- ASSERT_TRUE(a < b || b < a);
- ASSERT_TRUE(!(a < b && b < a));
-
- Node c = d_nodeManager->mkNode(AND, a, b);
- Node d = d_nodeManager->mkNode(AND, a, b);
-
- ASSERT_FALSE(c < d);
- ASSERT_FALSE(d < c);
-
- // simple test of descending descendant property
- Node child = d_nodeManager->mkConst(true);
- Node parent = d_nodeManager->mkNode(NOT, child);
-
- ASSERT_TRUE(child < parent);
-
- // slightly less simple test of DD property
- std::vector<Node> chain;
- const int N = 500;
- Node curr = d_nodeManager->mkNode(OR, a, b);
- chain.push_back(curr);
- for (int i = 0; i < N; ++i)
- {
- curr = d_nodeManager->mkNode(AND, curr, curr);
- chain.push_back(curr);
- }
-
- for (int i = 0; i < N; ++i)
- {
- for (int j = i + 1; j < N; ++j)
- {
- Node chain_i = chain[i];
- Node chain_j = chain[j];
- ASSERT_TRUE(chain_i < chain_j);
- }
- }
-}
-
-TEST_F(TestNodeBlackNode, eqNode)
-{
- TypeNode t = d_nodeManager->mkSort();
- Node left = d_nodeManager->mkSkolem("left", t);
- Node right = d_nodeManager->mkSkolem("right", t);
- Node eq = left.eqNode(right);
-
- ASSERT_EQ(EQUAL, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(eq[0], left);
- ASSERT_EQ(eq[1], right);
-}
-
-TEST_F(TestNodeBlackNode, notNode)
-{
- Node child = d_nodeManager->mkConst(true);
- Node parent = child.notNode();
-
- ASSERT_EQ(NOT, parent.getKind());
- ASSERT_EQ(1, parent.getNumChildren());
-
- ASSERT_EQ(parent[0], child);
-}
-
-TEST_F(TestNodeBlackNode, andNode)
-{
- Node left = d_nodeManager->mkConst(true);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.andNode(right);
-
- ASSERT_EQ(AND, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(*(eq.begin()), left);
- ASSERT_EQ(*(++eq.begin()), right);
-}
-
-TEST_F(TestNodeBlackNode, orNode)
-{
- Node left = d_nodeManager->mkConst(true);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.orNode(right);
-
- ASSERT_EQ(OR, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(*(eq.begin()), left);
- ASSERT_EQ(*(++eq.begin()), right);
-}
-
-TEST_F(TestNodeBlackNode, iteNode)
-{
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
- Node cnd = d_nodeManager->mkNode(OR, a, b);
- Node thenBranch = d_nodeManager->mkConst(true);
- Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
- Node ite = cnd.iteNode(thenBranch, elseBranch);
-
- ASSERT_EQ(ITE, ite.getKind());
- ASSERT_EQ(3, ite.getNumChildren());
-
- ASSERT_EQ(*(ite.begin()), cnd);
- ASSERT_EQ(*(++ite.begin()), thenBranch);
- ASSERT_EQ(*(++(++ite.begin())), elseBranch);
-}
-
-TEST_F(TestNodeBlackNode, iffNode)
-{
- Node left = d_nodeManager->mkConst(true);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.eqNode(right);
-
- ASSERT_EQ(EQUAL, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(*(eq.begin()), left);
- ASSERT_EQ(*(++eq.begin()), right);
-}
-
-TEST_F(TestNodeBlackNode, impNode)
-{
- Node left = d_nodeManager->mkConst(true);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.impNode(right);
-
- ASSERT_EQ(IMPLIES, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(*(eq.begin()), left);
- ASSERT_EQ(*(++eq.begin()), right);
-}
-
-TEST_F(TestNodeBlackNode, xorNode)
-{
- Node left = d_nodeManager->mkConst(true);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
- Node eq = left.xorNode(right);
-
- ASSERT_EQ(XOR, eq.getKind());
- ASSERT_EQ(2, eq.getNumChildren());
-
- ASSERT_EQ(*(eq.begin()), left);
- ASSERT_EQ(*(++eq.begin()), right);
-}
-
-TEST_F(TestNodeBlackNode, getKind)
-{
- Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
- Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
-
- Node n = d_nodeManager->mkNode(NOT, a);
- ASSERT_EQ(NOT, n.getKind());
-
- n = d_nodeManager->mkNode(EQUAL, a, b);
- ASSERT_EQ(EQUAL, n.getKind());
-
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
-
- n = d_nodeManager->mkNode(PLUS, x, y);
- ASSERT_EQ(PLUS, n.getKind());
-
- n = d_nodeManager->mkNode(UMINUS, x);
- ASSERT_EQ(UMINUS, n.getKind());
-}
-
-TEST_F(TestNodeBlackNode, getOperator)
-{
- TypeNode sort = d_nodeManager->mkSort("T");
- TypeNode booleanType = d_nodeManager->booleanType();
- TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
-
- Node f = d_nodeManager->mkSkolem("f", predType);
- Node a = d_nodeManager->mkSkolem("a", sort);
- Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
-
- ASSERT_TRUE(fa.hasOperator());
- ASSERT_FALSE(f.hasOperator());
- ASSERT_FALSE(a.hasOperator());
-
- ASSERT_EQ(fa.getNumChildren(), 1);
- ASSERT_EQ(f.getNumChildren(), 0);
- ASSERT_EQ(a.getNumChildren(), 0);
-
- ASSERT_EQ(f, fa.getOperator());
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
- ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
-#endif
-}
-
-TEST_F(TestNodeBlackNode, getNumChildren)
-{
- Node trueNode = d_nodeManager->mkConst(true);
-
- ASSERT_EQ(0, (Node::null()).getNumChildren());
- ASSERT_EQ(1, trueNode.notNode().getNumChildren());
- ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
-
- srand(0);
- for (uint32_t i = 0; i < 500; ++i)
- {
- uint32_t n = rand() % 1000 + 2;
- testNaryExpForSize(AND, n);
- }
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(testNaryExpForSize(AND, 0),
- "getNumChildren\\(\\) >= "
- "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
- ASSERT_DEATH(testNaryExpForSize(AND, 1),
- "getNumChildren\\(\\) >= "
- "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
- ASSERT_DEATH(testNaryExpForSize(NOT, 0),
- "getNumChildren\\(\\) >= "
- "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
- ASSERT_DEATH(testNaryExpForSize(NOT, 2),
- "getNumChildren\\(\\) <= "
- "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
-#endif /* CVC4_ASSERTIONS */
-}
-
-TEST_F(TestNodeBlackNode, iterator)
-{
- NodeBuilder<> b;
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
- Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
- Node n = b << x << y << z << kind::AND;
-
- { // iterator
- Node::iterator i = n.begin();
- ASSERT_EQ(*i++, x);
- ASSERT_EQ(*i++, y);
- ASSERT_EQ(*i++, z);
- ASSERT_EQ(i, n.end());
- }
-
- { // same for const iterator
- const Node& c = n;
- Node::const_iterator i = c.begin();
- ASSERT_EQ(*i++, x);
- ASSERT_EQ(*i++, y);
- ASSERT_EQ(*i++, z);
- ASSERT_EQ(i, n.end());
- }
-}
-
-TEST_F(TestNodeBlackNode, kinded_iterator)
-{
- TypeNode integerType = d_nodeManager->integerType();
-
- Node x = d_nodeManager->mkSkolem("x", integerType);
- Node y = d_nodeManager->mkSkolem("y", integerType);
- Node z = d_nodeManager->mkSkolem("z", integerType);
- Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
- Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
-
- { // iterator
- Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
- ASSERT_EQ(*i++, x);
- ASSERT_EQ(*i++, y);
- ASSERT_EQ(*i++, z);
- ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
-
- i = x.begin(PLUS);
- ASSERT_EQ(*i++, x);
- ASSERT_TRUE(i == x.end(PLUS));
- }
-}
-
-TEST_F(TestNodeBlackNode, toString)
-{
- TypeNode booleanType = d_nodeManager->booleanType();
-
- Node w = d_nodeManager->mkSkolem(
- "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node x = d_nodeManager->mkSkolem(
- "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y = d_nodeManager->mkSkolem(
- "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node z = d_nodeManager->mkSkolem(
- "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node m = NodeBuilder<>() << w << x << kind::OR;
- Node n = NodeBuilder<>() << m << y << z << kind::AND;
-
- ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
-}
-
-TEST_F(TestNodeBlackNode, toStream)
-{
- TypeNode booleanType = d_nodeManager->booleanType();
-
- Node w = d_nodeManager->mkSkolem(
- "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node x = d_nodeManager->mkSkolem(
- "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y = d_nodeManager->mkSkolem(
- "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node z = d_nodeManager->mkSkolem(
- "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node m = NodeBuilder<>() << x << y << kind::OR;
- Node n = NodeBuilder<>() << w << m << z << kind::AND;
- Node o = NodeBuilder<>() << n << n << kind::XOR;
-
- std::stringstream sstr;
- sstr << Node::dag(false);
- n.toStream(sstr);
- ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
-
- sstr.str(std::string());
- o.toStream(sstr, -1, 0);
- ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
- sstr.str(std::string());
- sstr << n;
- ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
-
- sstr.str(std::string());
- sstr << o;
- ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
- sstr.str(std::string());
- sstr << Node::setdepth(0) << n;
- ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
-
- sstr.str(std::string());
- sstr << Node::setdepth(0) << o;
- ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-
- sstr.str(std::string());
- sstr << Node::setdepth(1) << n;
- ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
-
- sstr.str(std::string());
- sstr << Node::setdepth(1) << o;
- ASSERT_EQ(sstr.str(),
- "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
-
- sstr.str(std::string());
- sstr << Node::setdepth(2) << n;
- ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
-
- sstr.str(std::string());
- sstr << Node::setdepth(2) << o;
- ASSERT_EQ(sstr.str(),
- "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
-
- sstr.str(std::string());
- sstr << Node::setdepth(3) << n;
- ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
-
- sstr.str(std::string());
- sstr << Node::setdepth(3) << o;
- ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
-}
-
-TEST_F(TestNodeBlackNode, dagifier)
-{
- TypeNode intType = d_nodeManager->integerType();
- TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
-
- Node x =
- d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node y =
- d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node f =
- d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node g =
- d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
- Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
- Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
- Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
- Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
- Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
- Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
- Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
- Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
- Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
- Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
- Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
- Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
-
- Node n = d_nodeManager->mkNode(
- OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
-
- std::stringstream sstr;
- sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
- sstr << Node::dag(false) << n; // never dagify
- ASSERT_EQ(sstr.str(),
- "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
- "y) OR (f(g(x)) = g(y))");
-}
-
-TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
-{
- const std::vector<Node> skolems =
- makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
- Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
- std::vector<Node> children;
- for (Node child : add)
- {
- children.push_back(child);
- }
- ASSERT_TRUE(children.size() == skolems.size()
- && std::equal(children.begin(), children.end(), skolems.begin()));
-}
-
-TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
-{
- const std::vector<Node> skolems =
- makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
- Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
- std::vector<TNode> children;
- for (TNode child : add)
- {
- children.push_back(child);
- }
- ASSERT_TRUE(children.size() == skolems.size()
- && std::equal(children.begin(), children.end(), skolems.begin()));
-}
-
-TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
-{
- const std::vector<Node> skolems =
- makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
- Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
- TNode add_tnode = add_node;
- std::vector<Node> children;
- for (Node child : add_tnode)
- {
- children.push_back(child);
- }
- ASSERT_TRUE(children.size() == skolems.size()
- && std::equal(children.begin(), children.end(), skolems.begin()));
-}
-
-TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
-{
- const std::vector<Node> skolems =
- makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
- Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
- TNode add_tnode = add_node;
- std::vector<TNode> children;
- for (TNode child : add_tnode)
- {
- children.push_back(child);
- }
- ASSERT_TRUE(children.size() == skolems.size()
- && std::equal(children.begin(), children.end(), skolems.begin()));
-}
-
-TEST_F(TestNodeBlackNode, isConst)
-{
- // more complicated "constants" exist in datatypes and arrays theories
- DType list("list");
- std::shared_ptr<DTypeConstructor> consC =
- std::make_shared<DTypeConstructor>("cons");
- consC->addArg("car", d_nodeManager->integerType());
- consC->addArgSelf("cdr");
- list.addConstructor(consC);
- list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
- TypeNode listType = d_nodeManager->mkDatatypeType(list);
- const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
- listType.getDType().getConstructors();
- Node cons = lcons[0]->getConstructor();
- Node nil = lcons[1]->getConstructor();
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
- Node cons_x_nil =
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
- cons,
- x,
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
- Node cons_1_nil =
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
- cons,
- d_nodeManager->mkConst(Rational(1)),
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
- Node cons_1_cons_2_nil = d_nodeManager->mkNode(
- APPLY_CONSTRUCTOR,
- cons,
- d_nodeManager->mkConst(Rational(1)),
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
- cons,
- d_nodeManager->mkConst(Rational(2)),
- d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
- ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
- ASSERT_FALSE(cons_x_nil.isConst());
- ASSERT_TRUE(cons_1_nil.isConst());
- ASSERT_TRUE(cons_1_cons_2_nil.isConst());
-
- TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
- d_nodeManager->integerType());
- Node zero = d_nodeManager->mkConst(Rational(0));
- Node one = d_nodeManager->mkConst(Rational(1));
- Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
- ASSERT_TRUE(storeAll.isConst());
-
- Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
- ASSERT_FALSE(arr.isConst());
- arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
- ASSERT_TRUE(arr.isConst());
- Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
- ASSERT_FALSE(arr2.isConst());
- arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
- ASSERT_FALSE(arr2.isConst());
-
- arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
- d_nodeManager->mkBitVectorType(1));
- zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
- one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
- storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
- ASSERT_TRUE(storeAll.isConst());
-
- arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
- ASSERT_FALSE(arr.isConst());
- arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
- ASSERT_TRUE(arr.isConst());
- arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
- ASSERT_FALSE(arr2.isConst());
- arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
- ASSERT_FALSE(arr2.isConst());
- arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
- ASSERT_FALSE(arr2.isConst());
-}
-
-namespace {
-Node level0(NodeManager* nm)
-{
- NodeBuilder<> nb(kind::AND);
- Node x = nm->mkSkolem("x", nm->booleanType());
- nb << x;
- nb << x;
- return Node(nb.constructNode());
-}
-TNode level1(NodeManager* nm) { return level0(nm); }
-} // namespace
-
-/**
- * This is for demonstrating what a certain type of user error looks like.
- */
-TEST_F(TestNodeBlackNode, node_tnode_usage)
-{
- Node n;
- ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
- ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
-}
-
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file node_builder_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Tim King, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::NodeBuilder.
- **
- ** Black box testing of CVC4::NodeBuilder.
- **/
-
-#include <limits.h>
-
-#include <sstream>
-#include <vector>
-
-#include "base/check.h"
-#include "expr/kind.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "test_node.h"
-#include "util/rational.h"
-
-#define K 30u
-#define LARGE_K UINT_MAX / 40
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-class TestNodeBlackNodeBuilder : public TestNode
-{
- protected:
- template <unsigned N>
- void push_back(NodeBuilder<N>& nb, uint32_t n)
- {
- for (uint32_t i = 0; i < n; ++i)
- {
- nb << d_nodeManager->mkConst(true);
- }
- }
- Kind d_specKind = AND;
-};
-
-/** Tests just constructors. No modification is done to the node. */
-TEST_F(TestNodeBlackNodeBuilder, ctors)
-{
- /* Default size tests. */
- NodeBuilder<> def;
- ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<> spec(d_specKind);
- ASSERT_EQ(spec.getKind(), d_specKind);
- ASSERT_EQ(spec.getNumChildren(), 0u);
- ASSERT_EQ(spec.begin(), spec.end());
-
- NodeBuilder<> from_nm(d_nodeManager.get());
- ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(from_nm.getNumChildren(),
- "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind);
- ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
- ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
- ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end());
-
- /* Non-default size tests */
- NodeBuilder<K> ws;
- ASSERT_EQ(ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<K> ws_kind(d_specKind);
- ASSERT_EQ(ws_kind.getKind(), d_specKind);
- ASSERT_EQ(ws_kind.getNumChildren(), 0u);
- ASSERT_EQ(ws_kind.begin(), ws_kind.end());
-
- NodeBuilder<K> ws_from_nm(d_nodeManager.get());
- ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(ws_from_nm.getNumChildren(),
- "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind);
- ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind);
- ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u);
- ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
-
- /* Extreme size tests */
- NodeBuilder<0> ws_size_0;
-
- /* Allocating on the heap instead of the stack. */
- NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
- delete ws_size_large;
-
- /* Copy constructors */
- NodeBuilder<> copy(def);
- ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<K> cp_ws(ws);
- ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<K - 10> cp_from_larger(ws);
- ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(cp_from_larger.getNumChildren(),
- "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- NodeBuilder<K + 10> cp_from_smaller(ws);
- ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(cp_from_smaller.getNumChildren(),
- "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_from_smaller.begin(),
- "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-}
-
-TEST_F(TestNodeBlackNodeBuilder, dtor)
-{
- NodeBuilder<K>* nb = new NodeBuilder<K>();
- delete nb;
-}
-
-TEST_F(TestNodeBlackNodeBuilder, begin_end)
-{
- /* Test begin() and end() without resizing. */
- NodeBuilder<K> ws(d_specKind);
- ASSERT_EQ(ws.begin(), ws.end());
-
- push_back(ws, K);
- ASSERT_NE(ws.begin(), ws.end());
-
- NodeBuilder<K>::iterator iter = ws.begin();
- for (uint32_t i = 0; i < K; ++i)
- {
- ASSERT_NE(iter, ws.end());
- ++iter;
- }
- ASSERT_EQ(iter, ws.end());
-
- NodeBuilder<K>::const_iterator citer = ws.begin();
- for (uint32_t i = 0; i < K; ++i)
- {
- ASSERT_NE(citer, ws.end());
- ++citer;
- }
- ASSERT_EQ(citer, ws.end());
-
- /* Repeat same tests and make sure that resizing occurs. */
- NodeBuilder<> smaller(d_specKind);
- ASSERT_EQ(smaller.begin(), smaller.end());
-
- push_back(smaller, K);
- ASSERT_NE(smaller.begin(), smaller.end());
-
- NodeBuilder<>::iterator smaller_iter = smaller.begin();
- for (uint32_t i = 0; i < K; ++i)
- {
- ASSERT_NE(smaller_iter, smaller.end());
- ++smaller_iter;
- }
- ASSERT_EQ(iter, ws.end());
-
- NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
- for (uint32_t i = 0; i < K; ++i)
- {
- ASSERT_NE(smaller_citer, smaller.end());
- ++smaller_citer;
- }
- ASSERT_EQ(smaller_citer, smaller.end());
-}
-
-TEST_F(TestNodeBlackNodeBuilder, iterator)
-{
- NodeBuilder<> b;
- Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
- Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
- Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
- b << x << y << z << AND;
-
- {
- NodeBuilder<>::iterator i = b.begin();
- ASSERT_EQ(*i++, x);
- ASSERT_EQ(*i++, y);
- ASSERT_EQ(*i++, z);
- ASSERT_EQ(i, b.end());
- }
-
- {
- const NodeBuilder<>& c = b;
- NodeBuilder<>::const_iterator i = c.begin();
- ASSERT_EQ(*i++, x);
- ASSERT_EQ(*i++, y);
- ASSERT_EQ(*i++, z);
- ASSERT_EQ(i, b.end());
- }
-}
-
-TEST_F(TestNodeBlackNodeBuilder, getKind)
-{
- NodeBuilder<> noKind;
- ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
-
- Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
- noKind << x << x;
- ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
-
- noKind << PLUS;
-
- ASSERT_EQ(noKind.getKind(), PLUS);
-
- Node n = noKind;
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
-#endif
-
- NodeBuilder<> spec(PLUS);
- ASSERT_EQ(spec.getKind(), PLUS);
- spec << x << x;
- ASSERT_EQ(spec.getKind(), PLUS);
-}
-
-TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
-{
- Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
-
- NodeBuilder<> nb;
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
- nb << PLUS << x << x;
-
- ASSERT_EQ(nb.getNumChildren(), 2u);
-
- nb << x << x;
- ASSERT_EQ(nb.getNumChildren(), 4u);
-
- nb.clear();
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
- nb.clear(PLUS);
- ASSERT_EQ(nb.getNumChildren(), 0u);
- nb << x << x << x;
-
- ASSERT_EQ(nb.getNumChildren(), 3u);
-
- nb << x << x << x;
- ASSERT_EQ(nb.getNumChildren(), 6u);
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
- Node n = nb;
- ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
-#endif
-}
-
-TEST_F(TestNodeBlackNodeBuilder, operator_square)
-{
- NodeBuilder<> arr(d_specKind);
-
- Node i_0 = d_nodeManager->mkConst(false);
- Node i_2 = d_nodeManager->mkConst(true);
- Node i_K = d_nodeManager->mkNode(NOT, i_0);
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(arr[-1], "index out of range");
- ASSERT_DEATH(arr[0], "index out of range");
-#endif
-
- arr << i_0;
-
- ASSERT_EQ(arr[0], i_0);
-
- push_back(arr, 1);
-
- arr << i_2;
-
- ASSERT_EQ(arr[0], i_0);
- ASSERT_EQ(arr[2], i_2);
-
- push_back(arr, K - 3);
-
- ASSERT_EQ(arr[0], i_0);
- ASSERT_EQ(arr[2], i_2);
- for (unsigned i = 3; i < K; ++i)
- {
- ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
- }
-
- arr << i_K;
-
- ASSERT_EQ(arr[0], i_0);
- ASSERT_EQ(arr[2], i_2);
- for (unsigned i = 3; i < K; ++i)
- {
- ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
- }
- ASSERT_EQ(arr[K], i_K);
-
-#ifdef CVC4_ASSERTIONS
- Node n = arr;
- ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
-#endif
-}
-
-TEST_F(TestNodeBlackNodeBuilder, clear)
-{
- NodeBuilder<> nb;
-
- ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- nb << d_specKind;
- push_back(nb, K);
-
- ASSERT_EQ(nb.getKind(), d_specKind);
- ASSERT_EQ(nb.getNumChildren(), K);
- ASSERT_NE(nb.begin(), nb.end());
-
- nb.clear();
-
- ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-
- nb << d_specKind;
- push_back(nb, K);
-
- ASSERT_EQ(nb.getKind(), d_specKind);
- ASSERT_EQ(nb.getNumChildren(), K);
- ASSERT_NE(nb.begin(), nb.end());
-
- nb.clear(d_specKind);
-
- ASSERT_EQ(nb.getKind(), d_specKind);
- ASSERT_EQ(nb.getNumChildren(), 0u);
- ASSERT_EQ(nb.begin(), nb.end());
-
- push_back(nb, K);
- nb.clear();
-
- ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
- ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
-#endif
-}
-
-TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
-{
-#ifdef CVC4_ASSERTIONS
- NodeBuilder<> spec(d_specKind);
- ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
-#endif
-
- NodeBuilder<> noSpec;
- noSpec << d_specKind;
- ASSERT_EQ(noSpec.getKind(), d_specKind);
-
- NodeBuilder<> modified;
- push_back(modified, K);
- modified << d_specKind;
- ASSERT_EQ(modified.getKind(), d_specKind);
-
- NodeBuilder<> nb(d_specKind);
- nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
- nb.clear(PLUS);
-
-#ifdef CVC4_ASSERTIONS
- Node n;
- ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
- nb.clear(PLUS);
-#endif
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
-#endif
-
- NodeBuilder<> testRef;
- ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
-
-#ifdef CVC4_ASSERTIONS
- NodeBuilder<> testTwo;
- ASSERT_DEATH(testTwo << d_specKind << PLUS,
- "can't redefine the Kind of a NodeBuilder");
-#endif
-
- NodeBuilder<> testMixOrder1;
- ASSERT_EQ(
- (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
- d_specKind);
- NodeBuilder<> testMixOrder2;
- ASSERT_EQ(
- (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
- d_specKind);
-}
-
-TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
-{
- NodeBuilder<K> nb(d_specKind);
- ASSERT_EQ(nb.getKind(), d_specKind);
- ASSERT_EQ(nb.getNumChildren(), 0u);
- ASSERT_EQ(nb.begin(), nb.end());
- push_back(nb, K);
- ASSERT_EQ(nb.getKind(), d_specKind);
- ASSERT_EQ(nb.getNumChildren(), K);
- ASSERT_NE(nb.begin(), nb.end());
-
-#ifdef CVC4_ASSERTIONS
- Node n = nb;
- ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
-#endif
-
- NodeBuilder<> overflow(d_specKind);
- ASSERT_EQ(overflow.getKind(), d_specKind);
- ASSERT_EQ(overflow.getNumChildren(), 0u);
- ASSERT_EQ(overflow.begin(), overflow.end());
-
- push_back(overflow, 5 * K + 1);
-
- ASSERT_EQ(overflow.getKind(), d_specKind);
- ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
- ASSERT_NE(overflow.begin(), overflow.end());
-}
-
-TEST_F(TestNodeBlackNodeBuilder, append)
-{
- Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
- Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
- Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
- Node m = d_nodeManager->mkNode(AND, y, z, x);
- Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
- Node o = d_nodeManager->mkNode(XOR, y, x);
-
- Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
- Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
- Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
-
- Node p = d_nodeManager->mkNode(
- EQUAL,
- d_nodeManager->mkConst<Rational>(0),
- d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
- Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
- "Nodes with kind XOR must have at most 2 children");
-#endif
-
- NodeBuilder<> b(d_specKind);
-
- /* test append(TNode) */
- b.append(n).append(o).append(q);
-
- ASSERT_EQ(b.getNumChildren(), 3);
- ASSERT_EQ(b[0], n);
- ASSERT_EQ(b[1], o);
- ASSERT_EQ(b[2], q);
-
- std::vector<Node> v;
- v.push_back(m);
- v.push_back(p);
- v.push_back(q);
-
- /* test append(vector<Node>) */
- b.append(v);
-
- ASSERT_EQ(b.getNumChildren(), 6);
- ASSERT_EQ(b[0], n);
- ASSERT_EQ(b[1], o);
- ASSERT_EQ(b[2], q);
- ASSERT_EQ(b[3], m);
- ASSERT_EQ(b[4], p);
- ASSERT_EQ(b[5], q);
-
- /* test append(iterator, iterator) */
- b.append(v.rbegin(), v.rend());
-
- ASSERT_EQ(b.getNumChildren(), 9);
- ASSERT_EQ(b[0], n);
- ASSERT_EQ(b[1], o);
- ASSERT_EQ(b[2], q);
- ASSERT_EQ(b[3], m);
- ASSERT_EQ(b[4], p);
- ASSERT_EQ(b[5], q);
- ASSERT_EQ(b[6], q);
- ASSERT_EQ(b[7], p);
- ASSERT_EQ(b[8], m);
-}
-
-TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
-{
- NodeBuilder<K> implicit(d_specKind);
- NodeBuilder<K> explic(d_specKind);
-
- push_back(implicit, K);
- push_back(explic, K);
-
- Node nimpl = implicit;
- Node nexplicit = (Node)explic;
-
- ASSERT_EQ(nimpl.getKind(), d_specKind);
- ASSERT_EQ(nimpl.getNumChildren(), K);
-
- ASSERT_EQ(nexplicit.getKind(), d_specKind);
- ASSERT_EQ(nexplicit.getNumChildren(), K);
-
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
-#endif
-}
-
-TEST_F(TestNodeBlackNodeBuilder, leftist_building)
-{
- NodeBuilder<> nb;
-
- Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
-
- Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
- Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
-
- Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
- Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
-
- nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
-
- Node n = nb;
- ASSERT_EQ(n.getNumChildren(), 3u);
- ASSERT_EQ(n.getType(), *d_realTypeNode);
- ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
- ASSERT_EQ(n[1].getType(), *d_realTypeNode);
- ASSERT_EQ(n[2].getType(), *d_realTypeNode);
-
- Node nota = d_nodeManager->mkNode(NOT, a);
- Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c);
- Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a);
- Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e);
-
- ASSERT_EQ(nexpected, n);
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file node_manager_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Christopher L. Conway, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::NodeManager.
- **
- ** Black box testing of CVC4::NodeManager.
- **/
-
-#include <string>
-#include <vector>
-
-#include "base/output.h"
-#include "expr/node_manager.h"
-#include "expr/node_manager_attributes.h"
-#include "test_node.h"
-#include "util/integer.h"
-#include "util/rational.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace expr;
-
-namespace test {
-
-class TestNodeBlackNodeManager : public TestNode
-{
-};
-
-TEST_F(TestNodeBlackNodeManager, mkNode_not)
-{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(NOT, x);
- ASSERT_EQ(n.getNumChildren(), 1u);
- ASSERT_EQ(n.getKind(), NOT);
- ASSERT_EQ(n[0], x);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_binary)
-{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(IMPLIES, x, y);
- ASSERT_EQ(n.getNumChildren(), 2u);
- ASSERT_EQ(n.getKind(), IMPLIES);
- ASSERT_EQ(n[0], x);
- ASSERT_EQ(n[1], y);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
-{
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
- Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(AND, x, y, z);
- ASSERT_EQ(n.getNumChildren(), 3u);
- ASSERT_EQ(n.getKind(), AND);
- ASSERT_EQ(n[0], x);
- ASSERT_EQ(n[1], y);
- ASSERT_EQ(n[2], z);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
-{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
- ASSERT_EQ(n.getNumChildren(), 4u);
- ASSERT_EQ(n.getKind(), AND);
- ASSERT_EQ(n[0], x1);
- ASSERT_EQ(n[1], x2);
- ASSERT_EQ(n[2], x3);
- ASSERT_EQ(n[3], x4);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
-{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
- Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType());
- Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
- ASSERT_EQ(n.getNumChildren(), 5u);
- ASSERT_EQ(n.getKind(), AND);
- ASSERT_EQ(n[0], x1);
- ASSERT_EQ(n[1], x2);
- ASSERT_EQ(n[2], x3);
- ASSERT_EQ(n[3], x4);
- ASSERT_EQ(n[4], x5);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
-{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- std::vector<Node> args;
- args.push_back(x1);
- args.push_back(x2);
- args.push_back(x3);
- Node n = d_nodeManager->mkNode(AND, args);
- ASSERT_EQ(n.getNumChildren(), args.size());
- ASSERT_EQ(n.getKind(), AND);
- for (unsigned i = 0; i < args.size(); ++i)
- {
- ASSERT_EQ(n[i], args[i]);
- }
-}
-
-TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
-{
- Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
- Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
- Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
- std::vector<TNode> args;
- args.push_back(x1);
- args.push_back(x2);
- args.push_back(x3);
- Node n = d_nodeManager->mkNode(AND, args);
- ASSERT_EQ(n.getNumChildren(), args.size());
- ASSERT_EQ(n.getKind(), AND);
- for (unsigned i = 0; i < args.size(); ++i)
- {
- ASSERT_EQ(n[i], args[i]);
- }
-}
-
-TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
-{
- Node x = d_nodeManager->mkSkolem(
- "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
- ASSERT_EQ(x.getKind(), SKOLEM);
- ASSERT_EQ(x.getNumChildren(), 0u);
- ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
- ASSERT_EQ(x.getType(), *d_boolTypeNode);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkConst_bool)
-{
- Node tt = d_nodeManager->mkConst(true);
- ASSERT_EQ(tt.getConst<bool>(), true);
- Node ff = d_nodeManager->mkConst(false);
- ASSERT_EQ(ff.getConst<bool>(), false);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkConst_rational)
-{
- Rational r("3/2");
- Node n = d_nodeManager->mkConst(r);
- ASSERT_EQ(n.getConst<Rational>(), r);
-}
-
-TEST_F(TestNodeBlackNodeManager, hasOperator)
-{
- ASSERT_TRUE(NodeManager::hasOperator(AND));
- ASSERT_TRUE(NodeManager::hasOperator(OR));
- ASSERT_TRUE(NodeManager::hasOperator(NOT));
- ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
- ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
-}
-
-TEST_F(TestNodeBlackNodeManager, booleanType)
-{
- TypeNode t = d_nodeManager->booleanType();
- TypeNode t2 = d_nodeManager->booleanType();
- TypeNode t3 = d_nodeManager->mkSort("T");
- ASSERT_TRUE(t.isBoolean());
- ASSERT_FALSE(t.isFunction());
- ASSERT_FALSE(t.isNull());
- ASSERT_FALSE(t.isPredicate());
- ASSERT_FALSE(t.isSort());
- ASSERT_EQ(t, t2);
- ASSERT_NE(t, t3);
-
- TypeNode bt = t;
- ASSERT_EQ(bt, t);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
-{
- TypeNode booleanType = d_nodeManager->booleanType();
- TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
- TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
-
- ASSERT_FALSE(t.isBoolean());
- ASSERT_TRUE(t.isFunction());
- ASSERT_FALSE(t.isNull());
- ASSERT_TRUE(t.isPredicate());
- ASSERT_FALSE(t.isSort());
-
- ASSERT_EQ(t, t2);
-
- TypeNode ft = t;
- ASSERT_EQ(ft, t);
- ASSERT_EQ(ft.getArgTypes().size(), 1u);
- ASSERT_EQ(ft.getArgTypes()[0], booleanType);
- ASSERT_EQ(ft.getRangeType(), booleanType);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
-{
- TypeNode a = d_nodeManager->mkSort();
- TypeNode b = d_nodeManager->mkSort();
- TypeNode c = d_nodeManager->mkSort();
-
- std::vector<TypeNode> argTypes;
- argTypes.push_back(a);
- argTypes.push_back(b);
-
- TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
- TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
-
- ASSERT_FALSE(t.isBoolean());
- ASSERT_TRUE(t.isFunction());
- ASSERT_FALSE(t.isNull());
- ASSERT_FALSE(t.isPredicate());
- ASSERT_FALSE(t.isSort());
-
- ASSERT_EQ(t, t2);
-
- TypeNode ft = t;
- ASSERT_EQ(ft, t);
- ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
- ASSERT_EQ(ft.getArgTypes()[0], a);
- ASSERT_EQ(ft.getArgTypes()[1], b);
- ASSERT_EQ(ft.getRangeType(), c);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
-{
- TypeNode a = d_nodeManager->mkSort();
- TypeNode b = d_nodeManager->mkSort();
- TypeNode c = d_nodeManager->mkSort();
-
- std::vector<TypeNode> types;
- types.push_back(a);
- types.push_back(b);
- types.push_back(c);
-
- TypeNode t = d_nodeManager->mkFunctionType(types);
- TypeNode t2 = d_nodeManager->mkFunctionType(types);
-
- ASSERT_FALSE(t.isBoolean());
- ASSERT_TRUE(t.isFunction());
- ASSERT_FALSE(t.isNull());
- ASSERT_FALSE(t.isPredicate());
- ASSERT_FALSE(t.isSort());
-
- ASSERT_EQ(t, t2);
-
- TypeNode ft = t;
- ASSERT_EQ(ft, t);
- ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
- ASSERT_EQ(ft.getArgTypes()[0], a);
- ASSERT_EQ(ft.getArgTypes()[1], b);
- ASSERT_EQ(ft.getRangeType(), c);
-}
-
-TEST_F(TestNodeBlackNodeManager, mkPredicateType)
-{
- TypeNode a = d_nodeManager->mkSort("a");
- TypeNode b = d_nodeManager->mkSort("b");
- TypeNode c = d_nodeManager->mkSort("c");
- TypeNode booleanType = d_nodeManager->booleanType();
-
- std::vector<TypeNode> argTypes;
- argTypes.push_back(a);
- argTypes.push_back(b);
- argTypes.push_back(c);
-
- TypeNode t = d_nodeManager->mkPredicateType(argTypes);
- TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
-
- ASSERT_FALSE(t.isBoolean());
- ASSERT_TRUE(t.isFunction());
- ASSERT_FALSE(t.isNull());
- ASSERT_TRUE(t.isPredicate());
- ASSERT_FALSE(t.isSort());
-
- ASSERT_EQ(t, t2);
-
- TypeNode ft = t;
- ASSERT_EQ(ft, t);
- ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
- ASSERT_EQ(ft.getArgTypes()[0], a);
- ASSERT_EQ(ft.getArgTypes()[1], b);
- ASSERT_EQ(ft.getArgTypes()[2], c);
- ASSERT_EQ(ft.getRangeType(), booleanType);
-}
-
-/* This test is only valid if assertions are enabled. */
-TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
-{
-#ifdef CVC4_ASSERTIONS
- Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
- ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
- "Nodes with kind AND must have at least 2 children");
-#endif
-}
-
-/* This test is only valid if assertions are enabled. */
-TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
-{
-#ifdef CVC4_ASSERTIONS
- std::vector<Node> vars;
- const uint32_t max = metakind::getMaxArityForKind(AND);
- TypeNode boolType = d_nodeManager->booleanType();
- Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
- Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
- Node andNode = skolem_i.andNode(skolem_j);
- Node orNode = skolem_i.orNode(skolem_j);
- while (vars.size() <= max)
- {
- vars.push_back(andNode);
- vars.push_back(skolem_j);
- vars.push_back(orNode);
- }
- ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
-#endif
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file node_manager_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief White box testing of CVC4::NodeManager.
- **
- ** White box testing of CVC4::NodeManager.
- **/
-
-#include <string>
-
-#include "expr/node_manager.h"
-#include "test_node.h"
-#include "util/integer.h"
-#include "util/rational.h"
-
-namespace CVC4 {
-
-using namespace CVC4::expr;
-
-namespace test {
-
-class TestNodeWhiteNodeManager : public TestNode
-{
-};
-
-TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
-{
- Rational i("3");
- Node n = d_nodeManager->mkConst(i);
- Node m = d_nodeManager->mkConst(i);
- ASSERT_EQ(n.getId(), m.getId());
-}
-
-TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
-{
- NodeBuilder<> nb;
-
- ASSERT_NO_THROW(nb.realloc(15));
- ASSERT_NO_THROW(nb.realloc(25));
- ASSERT_NO_THROW(nb.realloc(256));
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren");
-#endif /* CVC4_ASSERTIONS */
- ASSERT_NO_THROW(nb.realloc(257));
- ASSERT_NO_THROW(nb.realloc(4000));
- ASSERT_NO_THROW(nb.realloc(20000));
- ASSERT_NO_THROW(nb.realloc(60000));
- ASSERT_NO_THROW(nb.realloc(65535));
- ASSERT_NO_THROW(nb.realloc(65536));
- ASSERT_NO_THROW(nb.realloc(67108863));
-#ifdef CVC4_ASSERTIONS
- ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren");
-#endif /* CVC4_ASSERTIONS */
-}
-
-TEST_F(TestNodeWhiteNodeManager, topological_sort)
-{
- TypeNode boolType = d_nodeManager->booleanType();
- Node i = d_nodeManager->mkSkolem("i", boolType);
- Node j = d_nodeManager->mkSkolem("j", boolType);
- Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
- Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
-
- {
- std::vector<NodeValue*> roots = {n1.d_nv};
- ASSERT_EQ(NodeManager::TopologicalSort(roots), roots);
- }
-
- {
- std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
- std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
- ASSERT_EQ(NodeManager::TopologicalSort(roots), result);
- }
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \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
+++ /dev/null
-/********************* */
-/*! \file node_traversal_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of node traversal iterators.
- **/
-
-#include <algorithm>
-#include <cstddef>
-#include <iterator>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_traversal.h"
-#include "expr/node_value.h"
-#include "test_node.h"
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-class TestNodeBlackNodeTraversalPostorder : public TestNode
-{
-};
-
-class TestNodeBlackNodeTraversalPreorder : public TestNode
-{
-};
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
- NodeDfsIterator i = traversal.begin();
- NodeDfsIterator end = traversal.end();
- ASSERT_EQ(*i, tb);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_EQ(*i, eb);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_EQ(*i, cnd);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_TRUE(i == end);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
- NodeDfsIterator i = traversal.begin();
- NodeDfsIterator end = traversal.end();
- ASSERT_EQ(*(i++), tb);
- ASSERT_EQ(*(i++), eb);
- ASSERT_EQ(*(i++), cnd);
- ASSERT_TRUE(i == end);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- auto traversal = NodeDfsIterable(cnd);
- NodeDfsIterator i = traversal.begin();
- NodeDfsIterator end = traversal.end();
- ASSERT_EQ(*i, tb);
- ASSERT_FALSE(i == end);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- size_t count = 0;
- for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
- {
- ++count;
- }
- ASSERT_EQ(count, 3);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- size_t count = 0;
- for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
- {
- if (i.isConst())
- {
- ++count;
- }
- }
- ASSERT_EQ(count, 2);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-
- auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
-
- size_t count = std::count_if(
- traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
- ASSERT_EQ(count, 2);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
- std::vector<TNode> expected = {tb, eb, cnd, top};
-
- auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
-
- std::vector<TNode> actual;
- std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
- ASSERT_EQ(actual, expected);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
- std::vector<TNode> expected = {top};
-
- auto traversal = NodeDfsIterable(
- top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
-
- std::vector<TNode> actual;
- std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
- ASSERT_EQ(actual, expected);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
- std::vector<TNode> expected = {};
-
- auto traversal =
- NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; });
-
- std::vector<TNode> actual;
- std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
- ASSERT_EQ(actual, expected);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
- NodeDfsIterator i = traversal.begin();
- NodeDfsIterator end = traversal.end();
- ASSERT_EQ(*i, cnd);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_EQ(*i, tb);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_EQ(*i, eb);
- ASSERT_FALSE(i == end);
- ++i;
- ASSERT_TRUE(i == end);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
- NodeDfsIterator i = traversal.begin();
- NodeDfsIterator end = traversal.end();
- ASSERT_EQ(*(i++), cnd);
- ASSERT_EQ(*(i++), tb);
- ASSERT_EQ(*(i++), eb);
- ASSERT_TRUE(i == end);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- size_t count = 0;
- for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
- {
- ++count;
- }
- ASSERT_EQ(count, 3);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
-
- size_t count = 0;
- for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
- {
- if (i.isConst())
- {
- ++count;
- }
- }
- ASSERT_EQ(count, 2);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
-
- auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
-
- size_t count = std::count_if(
- traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
- ASSERT_EQ(count, 2);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
- std::vector<TNode> expected = {top, cnd, tb, eb};
-
- auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
-
- std::vector<TNode> actual;
- std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
- ASSERT_EQ(actual, expected);
-}
-
-TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
-{
- const Node tb = d_nodeManager->mkConst(true);
- const Node eb = d_nodeManager->mkConst(false);
- const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
- const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
- std::vector<TNode> expected = {top, cnd, eb};
-
- auto traversal = NodeDfsIterable(
- top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
-
- std::vector<TNode> actual;
- std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
- ASSERT_EQ(actual, expected);
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file node_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief White box testing of CVC4::Node.
- **
- ** White box testing of CVC4::Node.
- **/
-
-#include <string>
-
-#include "base/check.h"
-#include "test_node.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace expr;
-
-namespace test {
-
-class TestNodeWhiteNode : public TestNode
-{
-};
-
-TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); }
-
-TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
-
-TEST_F(TestNodeWhiteNode, builder)
-{
- NodeBuilder<> b;
- ASSERT_TRUE(b.d_nv->getId() == 0);
- ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
- ASSERT_EQ(b.d_nv->d_nchildren, 0u);
- /* etc. */
-}
-
-TEST_F(TestNodeWhiteNode, iterators)
-{
- Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
- Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
- Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
- Node two = d_nodeManager->mkConst(Rational(2));
- Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
-
- Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
-
- Node::iterator i;
-
- i = std::find(n.begin(), n.end(), x_plus_y);
- ASSERT_TRUE(i != n.end());
- ASSERT_TRUE(*i == x_plus_y);
-
- i = std::find(n.begin(), n.end(), x);
- ASSERT_TRUE(i == n.end());
-
- i = std::find(x_times_2.begin(), x_times_2.end(), two);
- ASSERT_TRUE(i != x_times_2.end());
- ASSERT_TRUE(*i == two);
-
- i = std::find(n.begin(), n.end(), y);
- ASSERT_TRUE(i != n.end());
- ASSERT_TRUE(*i == y);
-
- std::vector<Node> v;
- copy(n.begin(), n.end(), back_inserter(v));
- ASSERT_EQ(n.getNumChildren(), v.size());
- ASSERT_EQ(3, v.size());
- ASSERT_EQ(v[0], x_times_2);
- ASSERT_EQ(v[1], x_plus_y);
- ASSERT_EQ(v[2], y);
-}
-} // namespace test
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \file symbol_table_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters, Christopher L. Conway
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::SymbolTable
- **
- ** Black box testing of CVC4::SymbolTable.
- **/
-
-#include <sstream>
-#include <string>
-
-#include "base/check.h"
-#include "base/exception.h"
-#include "context/context.h"
-#include "expr/kind.h"
-#include "expr/symbol_table.h"
-#include "test_api.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
-
-namespace test {
-
-class 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
+++ /dev/null
-/********************* */
-/*! \file type_cardinality_black.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Public box testing of Type::getCardinality() for various Types
- **
- ** Public box testing of Type::getCardinality() for various Types.
- **/
-
-#include <string>
-
-#include "expr/kind.h"
-#include "expr/node_manager.h"
-#include "test_node.h"
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-using namespace kind;
-
-namespace test {
-
-class 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<TypeNode> boolbool;
- boolbool.push_back(d_nodeManager->booleanType());
- boolbool.push_back(d_nodeManager->booleanType());
- std::vector<TypeNode> boolint;
- boolint.push_back(d_nodeManager->booleanType());
- boolint.push_back(d_nodeManager->integerType());
- std::vector<TypeNode> intbool;
- intbool.push_back(d_nodeManager->integerType());
- intbool.push_back(d_nodeManager->booleanType());
- std::vector<TypeNode> intint;
- intint.push_back(d_nodeManager->integerType());
- intint.push_back(d_nodeManager->integerType());
- std::vector<TypeNode> intreal;
- intreal.push_back(d_nodeManager->integerType());
- intreal.push_back(d_nodeManager->realType());
- std::vector<TypeNode> realint;
- realint.push_back(d_nodeManager->realType());
- realint.push_back(d_nodeManager->integerType());
- std::vector<TypeNode> realreal;
- realreal.push_back(d_nodeManager->realType());
- realreal.push_back(d_nodeManager->realType());
- std::vector<TypeNode> realbool;
- realbool.push_back(d_nodeManager->realType());
- realbool.push_back(d_nodeManager->booleanType());
- std::vector<TypeNode> boolreal;
- boolreal.push_back(d_nodeManager->booleanType());
- boolreal.push_back(d_nodeManager->realType());
-
- TypeNode boolboolToBool =
- d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType());
- TypeNode boolboolToInt =
- d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType());
- TypeNode boolboolToReal =
- d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType());
-
- TypeNode boolintToBool =
- d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType());
- TypeNode boolintToInt =
- d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType());
- TypeNode boolintToReal =
- d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType());
-
- TypeNode intboolToBool =
- d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType());
- TypeNode intboolToInt =
- d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType());
- TypeNode intboolToReal =
- d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType());
-
- TypeNode intintToBool =
- d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType());
- TypeNode intintToInt =
- d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType());
- TypeNode intintToReal =
- d_nodeManager->mkFunctionType(intint, d_nodeManager->realType());
-
- TypeNode intrealToBool =
- d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType());
- TypeNode intrealToInt =
- d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType());
- TypeNode intrealToReal =
- d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType());
-
- TypeNode realintToBool =
- d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType());
- TypeNode realintToInt =
- d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType());
- TypeNode realintToReal =
- d_nodeManager->mkFunctionType(realint, d_nodeManager->realType());
-
- TypeNode realrealToBool =
- d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType());
- TypeNode realrealToInt =
- d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType());
- TypeNode realrealToReal =
- d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType());
-
- TypeNode realboolToBool =
- d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType());
- TypeNode realboolToInt =
- d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType());
- TypeNode realboolToReal =
- d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType());
-
- TypeNode boolrealToBool =
- d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType());
- TypeNode boolrealToInt =
- d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType());
- TypeNode boolrealToReal =
- d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType());
-
- ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL);
- ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS),
- Cardinality::EQUAL);
- ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
-
- ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
-
- ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
-
- ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
- ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::EQUAL);
-
- ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
-
- ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
-
- ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
-
- ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
-
- ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
- ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS),
- Cardinality::GREATER);
-}
-
-TEST_F(TestTypeCardinalityBlack, ternary_functions)
-{
- std::vector<TypeNode> boolbool;
- boolbool.push_back(d_nodeManager->booleanType());
- boolbool.push_back(d_nodeManager->booleanType());
- std::vector<TypeNode> boolboolbool = boolbool;
- boolboolbool.push_back(d_nodeManager->booleanType());
-
- TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool);
- TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool);
-
- TypeNode boolboolboolToBool =
- d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType());
- TypeNode boolboolToBoolbool =
- d_nodeManager->mkFunctionType(boolbool, boolboolTuple);
- TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType(
- d_nodeManager->booleanType(), boolboolboolTuple);
-
- ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8),
- Cardinality::EQUAL);
- ASSERT_EQ(
- boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4),
- Cardinality::EQUAL);
- ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8),
- Cardinality::EQUAL);
-}
-
-TEST_F(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
+++ /dev/null
-/********************* */
-/*! \file type_node_white.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief White box testing of TypeNode
- **
- ** White box testing of TypeNode.
- **/
-
-#include <iostream>
-#include <sstream>
-#include <string>
-
-#include "expr/node_manager.h"
-#include "expr/type_node.h"
-#include "smt/smt_engine.h"
-#include "test_node.h"
-
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
-
-namespace test {
-
-class TestNodeWhiteTypeNode : public TestNode
-{
- protected:
- void SetUp() override
- {
- TestNode::SetUp();
- d_smt.reset(new SmtEngine(d_nodeManager.get()));
- }
- std::unique_ptr<SmtEngine> d_smt;
-};
-
-TEST_F(TestNodeWhiteTypeNode, sub_types)
-{
- TypeNode realType = d_nodeManager->realType();
- TypeNode integerType = d_nodeManager->realType();
- TypeNode booleanType = d_nodeManager->booleanType();
- TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType);
- TypeNode bvType = d_nodeManager->mkBitVectorType(32);
-
- Node x = d_nodeManager->mkBoundVar("x", realType);
- Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
- TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
- Node lambda = d_nodeManager->mkVar("lambda", funtype);
- std::vector<Node> formals;
- formals.push_back(x);
- d_smt->defineFunction(lambda, formals, xPos);
-
- ASSERT_FALSE(realType.isComparableTo(booleanType));
- ASSERT_TRUE(realType.isComparableTo(integerType));
- ASSERT_TRUE(realType.isComparableTo(realType));
- ASSERT_FALSE(realType.isComparableTo(arrayType));
- ASSERT_FALSE(realType.isComparableTo(bvType));
-
- ASSERT_FALSE(booleanType.isComparableTo(integerType));
- ASSERT_FALSE(booleanType.isComparableTo(realType));
- ASSERT_TRUE(booleanType.isComparableTo(booleanType));
- ASSERT_FALSE(booleanType.isComparableTo(arrayType));
- ASSERT_FALSE(booleanType.isComparableTo(bvType));
-
- ASSERT_TRUE(integerType.isComparableTo(realType));
- ASSERT_TRUE(integerType.isComparableTo(integerType));
- ASSERT_FALSE(integerType.isComparableTo(booleanType));
- ASSERT_FALSE(integerType.isComparableTo(arrayType));
- ASSERT_FALSE(integerType.isComparableTo(bvType));
-
- ASSERT_FALSE(arrayType.isComparableTo(booleanType));
- ASSERT_FALSE(arrayType.isComparableTo(integerType));
- ASSERT_FALSE(arrayType.isComparableTo(realType));
- ASSERT_TRUE(arrayType.isComparableTo(arrayType));
- ASSERT_FALSE(arrayType.isComparableTo(bvType));
-
- ASSERT_FALSE(bvType.isComparableTo(booleanType));
- ASSERT_FALSE(bvType.isComparableTo(integerType));
- ASSERT_FALSE(bvType.isComparableTo(realType));
- ASSERT_FALSE(bvType.isComparableTo(arrayType));
- ASSERT_TRUE(bvType.isComparableTo(bvType));
-
- ASSERT_TRUE(realType.getBaseType() == realType);
- ASSERT_TRUE(integerType.getBaseType() == realType);
- ASSERT_TRUE(booleanType.getBaseType() == booleanType);
- ASSERT_TRUE(arrayType.getBaseType() == arrayType);
- ASSERT_TRUE(bvType.getBaseType() == bvType);
-}
-} // namespace test
-} // namespace CVC4
--- /dev/null
+#####################
+## 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)
--- /dev/null
+/********************* */
+/*! \file attribute_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Attribute.
+ **
+ ** Black box testing of CVC4::Attribute.
+ **/
+
+#include <sstream>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_value.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace smt;
+
+namespace test {
+
+class TestNodeBlackAttribute : public TestNode
+{
+ protected:
+ struct PrimitiveIntAttributeId
+ {
+ };
+ using PrimitiveIntAttribute =
+ expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
+ struct TNodeAttributeId
+ {
+ };
+ using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
+ struct StringAttributeId
+ {
+ };
+ using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
+ struct BoolAttributeId
+ {
+ };
+ using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
+};
+
+TEST_F(TestNodeBlackAttribute, ints)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+ const uint64_t val = 63489;
+ uint64_t data0 = 0;
+ uint64_t data1 = 0;
+
+ PrimitiveIntAttribute attr;
+ ASSERT_FALSE(node->getAttribute(attr, data0));
+ node->setAttribute(attr, val);
+ ASSERT_TRUE(node->getAttribute(attr, data1));
+ ASSERT_EQ(data1, val);
+
+ delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, tnodes)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+ Node val(d_nodeManager->mkSkolem("b", booleanType));
+ TNode data0;
+ TNode data1;
+
+ TNodeAttribute attr;
+ ASSERT_FALSE(node->getAttribute(attr, data0));
+ node->setAttribute(attr, val);
+ ASSERT_TRUE(node->getAttribute(attr, data1));
+ ASSERT_EQ(data1, val);
+
+ delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, strings)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+ std::string val("63489");
+ std::string data0;
+ std::string data1;
+
+ StringAttribute attr;
+ ASSERT_FALSE(node->getAttribute(attr, data0));
+ node->setAttribute(attr, val);
+ ASSERT_TRUE(node->getAttribute(attr, data1));
+ ASSERT_EQ(data1, val);
+
+ delete node;
+}
+
+TEST_F(TestNodeBlackAttribute, bools)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+ Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
+
+ bool val = true;
+ bool data0 = false;
+ bool data1 = false;
+
+ BoolAttribute attr;
+ ASSERT_TRUE(node->getAttribute(attr, data0));
+ ASSERT_EQ(false, data0);
+ node->setAttribute(attr, val);
+ ASSERT_TRUE(node->getAttribute(attr, data1));
+ ASSERT_EQ(data1, val);
+
+ delete node;
+}
+
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file attribute_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of Node attributes.
+ **
+ ** White box testing of Node attributes.
+ **/
+
+#include <string>
+
+#include "base/check.h"
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "test_node.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace smt;
+using namespace expr;
+using namespace expr::attr;
+
+namespace test {
+
+struct Test1;
+struct Test2;
+struct Test3;
+struct Test4;
+struct Test5;
+
+typedef Attribute<Test1, std::string> TestStringAttr1;
+typedef Attribute<Test2, std::string> TestStringAttr2;
+
+using TestFlag1 = Attribute<Test1, bool>;
+using TestFlag2 = Attribute<Test2, bool>;
+using TestFlag3 = Attribute<Test3, bool>;
+using TestFlag4 = Attribute<Test4, bool>;
+using TestFlag5 = Attribute<Test5, bool>;
+
+class TestNodeWhiteAttribute : public TestNode
+{
+ protected:
+ void SetUp() override
+ {
+ TestNode::SetUp();
+ d_booleanType.reset(new TypeNode(d_nodeManager->booleanType()));
+ }
+ std::unique_ptr<TypeNode> d_booleanType;
+};
+
+TEST_F(TestNodeWhiteAttribute, attribute_ids)
+{
+ // Test that IDs for (a subset of) attributes in the system are
+ // unique and that the LastAttributeId (which would be the next ID
+ // to assign) is greater than all attribute IDs.
+
+ // We used to check ID assignments explicitly. However, between
+ // compilation modules, you don't get a strong guarantee
+ // (initialization order is somewhat implementation-specific, and
+ // anyway you'd have to change the tests anytime you add an
+ // attribute). So we back off, and just test that they're unique
+ // and that the next ID to be assigned is strictly greater than
+ // those that have already been assigned.
+
+ unsigned lastId = attr::LastAttributeId<std::string, false>::getId();
+ ASSERT_LT(VarNameAttr::s_id, lastId);
+ ASSERT_LT(TestStringAttr1::s_id, lastId);
+ ASSERT_LT(TestStringAttr2::s_id, lastId);
+
+ ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id);
+ ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
+ ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
+
+ lastId = attr::LastAttributeId<bool, false>::getId();
+ ASSERT_LT(TestFlag1::s_id, lastId);
+ ASSERT_LT(TestFlag2::s_id, lastId);
+ ASSERT_LT(TestFlag3::s_id, lastId);
+ ASSERT_LT(TestFlag4::s_id, lastId);
+ ASSERT_LT(TestFlag5::s_id, lastId);
+ ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id);
+ ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id);
+ ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id);
+ ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id);
+ ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id);
+ ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id);
+ ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id);
+ ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id);
+ ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id);
+ ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id);
+
+ lastId = attr::LastAttributeId<TypeNode, false>::getId();
+ ASSERT_LT(TypeAttr::s_id, lastId);
+}
+
+TEST_F(TestNodeWhiteAttribute, attributes)
+{
+ Node a = d_nodeManager->mkVar(*d_booleanType);
+ Node b = d_nodeManager->mkVar(*d_booleanType);
+ Node c = d_nodeManager->mkVar(*d_booleanType);
+ Node unnamed = d_nodeManager->mkVar(*d_booleanType);
+
+ a.setAttribute(VarNameAttr(), "a");
+ b.setAttribute(VarNameAttr(), "b");
+ c.setAttribute(VarNameAttr(), "c");
+
+ // test that all boolean flags are FALSE to start
+ Debug("boolattr") << "get flag 1 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag1()));
+
+ Debug("boolattr") << "get flag 2 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag2()));
+
+ Debug("boolattr") << "get flag 3 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag3()));
+
+ Debug("boolattr") << "get flag 4 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag4()));
+
+ Debug("boolattr") << "get flag 5 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag5()));
+
+ // test that they all HAVE the boolean attributes
+ ASSERT_TRUE(a.hasAttribute(TestFlag1()));
+ ASSERT_TRUE(b.hasAttribute(TestFlag1()));
+ ASSERT_TRUE(c.hasAttribute(TestFlag1()));
+ ASSERT_TRUE(unnamed.hasAttribute(TestFlag1()));
+
+ ASSERT_TRUE(a.hasAttribute(TestFlag2()));
+ ASSERT_TRUE(b.hasAttribute(TestFlag2()));
+ ASSERT_TRUE(c.hasAttribute(TestFlag2()));
+ ASSERT_TRUE(unnamed.hasAttribute(TestFlag2()));
+
+ ASSERT_TRUE(a.hasAttribute(TestFlag3()));
+ ASSERT_TRUE(b.hasAttribute(TestFlag3()));
+ ASSERT_TRUE(c.hasAttribute(TestFlag3()));
+ ASSERT_TRUE(unnamed.hasAttribute(TestFlag3()));
+
+ ASSERT_TRUE(a.hasAttribute(TestFlag4()));
+ ASSERT_TRUE(b.hasAttribute(TestFlag4()));
+ ASSERT_TRUE(c.hasAttribute(TestFlag4()));
+ ASSERT_TRUE(unnamed.hasAttribute(TestFlag4()));
+
+ ASSERT_TRUE(a.hasAttribute(TestFlag5()));
+ ASSERT_TRUE(b.hasAttribute(TestFlag5()));
+ ASSERT_TRUE(c.hasAttribute(TestFlag5()));
+ ASSERT_TRUE(unnamed.hasAttribute(TestFlag5()));
+
+ // test two-arg version of hasAttribute()
+ bool bb = false;
+ Debug("boolattr") << "get flag 1 on a (should be F)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag1(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 1 on b (should be F)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag1(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 1 on c (should be F)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag1(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 1 on unnamed (should be F)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag1(), bb));
+ ASSERT_FALSE(bb);
+
+ Debug("boolattr") << "get flag 2 on a (should be F)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag2(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 2 on b (should be F)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag2(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 2 on c (should be F)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag2(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag2(), bb));
+ ASSERT_FALSE(bb);
+
+ Debug("boolattr") << "get flag 3 on a (should be F)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag3(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 3 on b (should be F)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag3(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 3 on c (should be F)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag3(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 3 on unnamed (should be F)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag3(), bb));
+ ASSERT_FALSE(bb);
+
+ Debug("boolattr") << "get flag 4 on a (should be F)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag4(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 4 on b (should be F)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag4(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 4 on c (should be F)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag4(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 4 on unnamed (should be F)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag4(), bb));
+ ASSERT_FALSE(bb);
+
+ Debug("boolattr") << "get flag 5 on a (should be F)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag5(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 5 on b (should be F)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag5(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 5 on c (should be F)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag5(), bb));
+ ASSERT_FALSE(bb);
+ Debug("boolattr") << "get flag 5 on unnamed (should be F)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag5(), bb));
+ ASSERT_FALSE(bb);
+
+ // setting boolean flags
+ Debug("boolattr") << "set flag 1 on a to T\n";
+ a.setAttribute(TestFlag1(), true);
+ Debug("boolattr") << "set flag 1 on b to F\n";
+ b.setAttribute(TestFlag1(), false);
+ Debug("boolattr") << "set flag 1 on c to F\n";
+ c.setAttribute(TestFlag1(), false);
+ Debug("boolattr") << "set flag 1 on unnamed to T\n";
+ unnamed.setAttribute(TestFlag1(), true);
+
+ Debug("boolattr") << "set flag 2 on a to F\n";
+ a.setAttribute(TestFlag2(), false);
+ Debug("boolattr") << "set flag 2 on b to T\n";
+ b.setAttribute(TestFlag2(), true);
+ Debug("boolattr") << "set flag 2 on c to T\n";
+ c.setAttribute(TestFlag2(), true);
+ Debug("boolattr") << "set flag 2 on unnamed to F\n";
+ unnamed.setAttribute(TestFlag2(), false);
+
+ Debug("boolattr") << "set flag 3 on a to T\n";
+ a.setAttribute(TestFlag3(), true);
+ Debug("boolattr") << "set flag 3 on b to T\n";
+ b.setAttribute(TestFlag3(), true);
+ Debug("boolattr") << "set flag 3 on c to T\n";
+ c.setAttribute(TestFlag3(), true);
+ Debug("boolattr") << "set flag 3 on unnamed to T\n";
+ unnamed.setAttribute(TestFlag3(), true);
+
+ Debug("boolattr") << "set flag 4 on a to T\n";
+ a.setAttribute(TestFlag4(), true);
+ Debug("boolattr") << "set flag 4 on b to T\n";
+ b.setAttribute(TestFlag4(), true);
+ Debug("boolattr") << "set flag 4 on c to T\n";
+ c.setAttribute(TestFlag4(), true);
+ Debug("boolattr") << "set flag 4 on unnamed to T\n";
+ unnamed.setAttribute(TestFlag4(), true);
+
+ Debug("boolattr") << "set flag 5 on a to T\n";
+ a.setAttribute(TestFlag5(), true);
+ Debug("boolattr") << "set flag 5 on b to T\n";
+ b.setAttribute(TestFlag5(), true);
+ Debug("boolattr") << "set flag 5 on c to F\n";
+ c.setAttribute(TestFlag5(), false);
+ Debug("boolattr") << "set flag 5 on unnamed to T\n";
+ unnamed.setAttribute(TestFlag5(), true);
+
+ ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+ ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+ ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+ ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+ ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+
+ ASSERT_FALSE(a.hasAttribute(TestStringAttr1()));
+ ASSERT_FALSE(b.hasAttribute(TestStringAttr1()));
+ ASSERT_FALSE(c.hasAttribute(TestStringAttr1()));
+ ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1()));
+
+ ASSERT_FALSE(a.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(b.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(c.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2()));
+
+ Debug("boolattr") << "get flag 1 on a (should be T)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on b (should be F)\n";
+ ASSERT_FALSE(b.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag1()));
+ Debug("boolattr") << "get flag 1 on unnamed (should be T)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag1()));
+
+ Debug("boolattr") << "get flag 2 on a (should be F)\n";
+ ASSERT_FALSE(a.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on b (should be T)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on c (should be T)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag2()));
+ Debug("boolattr") << "get flag 2 on unnamed (should be F)\n";
+ ASSERT_FALSE(unnamed.getAttribute(TestFlag2()));
+
+ Debug("boolattr") << "get flag 3 on a (should be T)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on b (should be T)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on c (should be T)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag3()));
+ Debug("boolattr") << "get flag 3 on unnamed (should be T)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag3()));
+
+ Debug("boolattr") << "get flag 4 on a (should be T)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on b (should be T)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on c (should be T)\n";
+ ASSERT_TRUE(c.getAttribute(TestFlag4()));
+ Debug("boolattr") << "get flag 4 on unnamed (should be T)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag4()));
+
+ Debug("boolattr") << "get flag 5 on a (should be T)\n";
+ ASSERT_TRUE(a.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on b (should be T)\n";
+ ASSERT_TRUE(b.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on c (should be F)\n";
+ ASSERT_FALSE(c.getAttribute(TestFlag5()));
+ Debug("boolattr") << "get flag 5 on unnamed (should be T)\n";
+ ASSERT_TRUE(unnamed.getAttribute(TestFlag5()));
+
+ a.setAttribute(TestStringAttr1(), "foo");
+ b.setAttribute(TestStringAttr1(), "bar");
+ c.setAttribute(TestStringAttr1(), "baz");
+
+ ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+ ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+ ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+ ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+ ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+
+ ASSERT_TRUE(a.hasAttribute(TestStringAttr1()));
+ ASSERT_TRUE(b.hasAttribute(TestStringAttr1()));
+ ASSERT_TRUE(c.hasAttribute(TestStringAttr1()));
+ ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1()));
+
+ ASSERT_FALSE(a.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(b.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(c.hasAttribute(TestStringAttr2()));
+ ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2()));
+
+ a.setAttribute(VarNameAttr(), "b");
+ b.setAttribute(VarNameAttr(), "c");
+ c.setAttribute(VarNameAttr(), "a");
+
+ ASSERT_EQ(c.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "a");
+ ASSERT_EQ(a.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "b");
+ ASSERT_EQ(b.getAttribute(VarNameAttr()), "c");
+ ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+ ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+ ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+
+ ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file kind_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Kind.
+ **
+ ** Black box testing of CVC4::Kind.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackKind : public TestInternal
+{
+ protected:
+ void SetUp() override
+ {
+ d_undefined = UNDEFINED_KIND;
+ d_null = NULL_EXPR;
+ d_last = LAST_KIND;
+ d_beyond = ((int32_t)LAST_KIND) + 1;
+ d_unknown = (Kind)d_beyond;
+ }
+
+ bool string_is_as_expected(Kind k, const char* s)
+ {
+ std::stringstream act;
+ std::stringstream exp;
+ act << k;
+ exp << s;
+ return act.str() == exp.str();
+ }
+
+ Kind d_undefined;
+ Kind d_unknown;
+ Kind d_null;
+ Kind d_last;
+ int32_t d_beyond;
+};
+
+TEST_F(TestNodeBlackKind, equality)
+{
+ ASSERT_EQ(d_undefined, UNDEFINED_KIND);
+ ASSERT_EQ(d_last, LAST_KIND);
+}
+
+TEST_F(TestNodeBlackKind, order)
+{
+ ASSERT_LT((int32_t)d_undefined, (int32_t)d_null);
+ ASSERT_LT((int32_t)d_null, (int32_t)d_last);
+ ASSERT_LT((int32_t)d_undefined, (int32_t)d_last);
+ ASSERT_LT((int32_t)d_last, (int32_t)d_unknown);
+}
+
+TEST_F(TestNodeBlackKind, output)
+{
+ ASSERT_TRUE(string_is_as_expected(d_undefined, "UNDEFINED_KIND"));
+ ASSERT_TRUE(string_is_as_expected(d_null, "NULL"));
+ ASSERT_TRUE(string_is_as_expected(d_last, "LAST_KIND"));
+}
+
+TEST_F(TestNodeBlackKind, output_concat)
+{
+ std::stringstream act, exp;
+ act << d_undefined << d_null << d_last << d_unknown;
+ exp << "UNDEFINED_KIND"
+ << "NULL"
+ << "LAST_KIND"
+ << "?";
+ ASSERT_EQ(act.str(), exp.str());
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file kind_map_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::KindMap
+ **
+ ** Black box testing of CVC4::KindMap.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/kind_map.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackKindMap : public TestInternal
+{
+};
+
+TEST_F(TestNodeBlackKindMap, simple)
+{
+ KindMap map;
+ ASSERT_FALSE(map.test(AND));
+ map.set(AND);
+ ASSERT_TRUE(map.test(AND));
+ map.reset(AND);
+ ASSERT_FALSE(map.test(AND));
+#ifdef CVC4_ASSERTIONS
+ ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException);
+#endif
+}
+
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_algorithm_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Yoni Zohar, Abdalrhman Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of utility functions in node_algorithm.{h,cpp}
+ **
+ ** Black box testing of node_algorithm.{h,cpp}
+ **/
+
+#include <string>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node_algorithm.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace expr;
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeAlgorithm : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
+{
+ // The only symbol in ~x (x is a boolean varible) should be x
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(NOT, x);
+ std::unordered_set<Node, NodeHashFunction> syms;
+ getSymbols(n, syms);
+ ASSERT_EQ(syms.size(), 1);
+ ASSERT_NE(syms.find(x), syms.end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
+{
+ // the only symbols in x=y ^ (exists var. var+var = x) are x and y, because
+ // "var" is bound.
+
+ // left conjunct
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->integerType());
+ Node left = d_nodeManager->mkNode(EQUAL, x, y);
+
+ // right conjunct
+ Node var = d_nodeManager->mkBoundVar(*d_intTypeNode);
+ std::vector<Node> vars;
+ vars.push_back(var);
+ Node sum = d_nodeManager->mkNode(PLUS, var, var);
+ Node qeq = d_nodeManager->mkNode(EQUAL, x, sum);
+ Node bvl = d_nodeManager->mkNode(BOUND_VAR_LIST, vars);
+ Node right = d_nodeManager->mkNode(EXISTS, bvl, qeq);
+
+ // conjunction
+ Node res = d_nodeManager->mkNode(AND, left, right);
+
+ // symbols
+ std::unordered_set<Node, NodeHashFunction> syms;
+ getSymbols(res, syms);
+
+ // assertions
+ ASSERT_EQ(syms.size(), 2);
+ ASSERT_NE(syms.find(x), syms.end());
+ ASSERT_NE(syms.find(y), syms.end());
+ ASSERT_EQ(syms.find(var), syms.end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
+{
+ // map to store result
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > result =
+ std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> >();
+
+ // create test formula
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+ Node plus = d_nodeManager->mkNode(PLUS, x, x);
+ Node mul = d_nodeManager->mkNode(MULT, x, x);
+ Node eq1 = d_nodeManager->mkNode(EQUAL, plus, mul);
+
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->mkBitVectorType(4));
+ Node ext1 = theory::bv::utils::mkExtract(y, 1, 0);
+ Node ext2 = theory::bv::utils::mkExtract(y, 3, 2);
+ Node eq2 = d_nodeManager->mkNode(EQUAL, ext1, ext2);
+
+ Node formula = d_nodeManager->mkNode(AND, eq1, eq2);
+
+ // call function
+ expr::getOperatorsMap(formula, result);
+
+ // Verify result
+ // We should have only integer, bv and boolean as types
+ ASSERT_EQ(result.size(), 3);
+ ASSERT_NE(result.find(*d_intTypeNode), result.end());
+ ASSERT_NE(result.find(*d_boolTypeNode), result.end());
+ ASSERT_NE(result.find(*d_bvTypeNode), result.end());
+
+ // in integers, we should only have plus and mult as operators
+ ASSERT_EQ(result[*d_intTypeNode].size(), 2);
+ ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
+ result[*d_intTypeNode].end());
+ ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
+ result[*d_intTypeNode].end());
+
+ // in booleans, we should only have "=" and "and" as an operator.
+ ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
+ ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
+ result[*d_boolTypeNode].end());
+ ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
+ result[*d_boolTypeNode].end());
+
+ // in bv, we should only have "extract" as an operator.
+ ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
+ Node extractOp1 =
+ d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
+ Node extractOp2 =
+ d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
+ ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
+ result[*d_bvTypeNode].end());
+ ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
+ result[*d_bvTypeNode].end());
+}
+
+TEST_F(TestNodeBlackNodeAlgorithm, match)
+{
+ TypeNode integer = d_nodeManager->integerType();
+
+ Node one = d_nodeManager->mkConst(Rational(1));
+ Node two = d_nodeManager->mkConst(Rational(2));
+
+ Node x = d_nodeManager->mkBoundVar(integer);
+ Node a = d_nodeManager->mkSkolem("a", integer);
+
+ Node n1 = d_nodeManager->mkNode(MULT, two, x);
+ std::unordered_map<Node, Node, NodeHashFunction> subs;
+
+ // check reflexivity
+ ASSERT_TRUE(match(n1, n1, subs));
+ ASSERT_EQ(subs.size(), 0);
+
+ Node n2 = d_nodeManager->mkNode(MULT, two, a);
+ subs.clear();
+
+ // check instance
+ ASSERT_TRUE(match(n1, n2, subs));
+ ASSERT_EQ(subs.size(), 1);
+ ASSERT_EQ(subs[x], a);
+
+ // should return false for flipped arguments (match is not symmetric)
+ ASSERT_FALSE(match(n2, n1, subs));
+
+ n2 = d_nodeManager->mkNode(MULT, one, a);
+
+ // should return false since n2 is not an instance of n1
+ ASSERT_FALSE(match(n1, n2, subs));
+
+ n2 = d_nodeManager->mkNode(NONLINEAR_MULT, two, a);
+
+ // should return false for similar operators
+ ASSERT_FALSE(match(n1, n2, subs));
+
+ n2 = d_nodeManager->mkNode(MULT, two, a, one);
+
+ // should return false for different number of arguments
+ ASSERT_FALSE(match(n1, n2, subs));
+
+ n1 = x;
+ n2 = d_nodeManager->mkConst(true);
+
+ // should return false for different types
+ ASSERT_FALSE(match(n1, n2, subs));
+
+ n1 = d_nodeManager->mkNode(MULT, x, x);
+ n2 = d_nodeManager->mkNode(MULT, two, a);
+
+ // should return false for contradictory substitutions
+ ASSERT_FALSE(match(n1, n2, subs));
+
+ n2 = d_nodeManager->mkNode(MULT, a, a);
+ subs.clear();
+
+ // implementation: check if the cache works correctly
+ ASSERT_TRUE(match(n1, n2, subs));
+ ASSERT_EQ(subs.size(), 1);
+ ASSERT_EQ(subs[x], a);
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::Node.
+ **
+ ** Black box testing of CVC4::Node.
+ **/
+
+#include <algorithm>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "api/cvc4cpp.h"
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+namespace {
+/** Returns N skolem nodes from 'nodeManager' with the same `type`. */
+std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
+ uint32_t n,
+ TypeNode type)
+{
+ std::vector<Node> skolems;
+ for (uint32_t i = 0; i < n; i++)
+ {
+ skolems.push_back(nodeManager->mkSkolem(
+ "skolem_", type, "Created by makeNSkolemNodes()"));
+ }
+ return skolems;
+}
+} // namespace
+
+class TestNodeBlackNode : public TestNode
+{
+ protected:
+ void SetUp() override
+ {
+ TestNode::SetUp();
+ // setup an SMT engine so that options are in scope
+ Options opts;
+ char* argv[2];
+ argv[0] = strdup("");
+ argv[1] = strdup("--output-lang=ast");
+ Options::parseOptions(&opts, 2, argv);
+ free(argv[0]);
+ free(argv[1]);
+ d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
+ }
+
+ std::unique_ptr<SmtEngine> d_smt;
+
+ bool imp(bool a, bool b) const { return (!a) || (b); }
+ bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
+
+ void testNaryExpForSize(Kind k, uint32_t n)
+ {
+ NodeBuilder<> nbz(k);
+ Node trueNode = d_nodeManager->mkConst(true);
+ for (uint32_t i = 0; i < n; ++i)
+ {
+ nbz << trueNode;
+ }
+ Node result = nbz;
+ ASSERT_EQ(n, result.getNumChildren());
+ }
+};
+
+TEST_F(TestNodeBlackNode, null) { Node::null(); }
+
+TEST_F(TestNodeBlackNode, is_null)
+{
+ Node a = Node::null();
+ ASSERT_TRUE(a.isNull());
+
+ Node b = Node();
+ ASSERT_TRUE(b.isNull());
+
+ Node c = b;
+ ASSERT_TRUE(c.isNull());
+}
+
+TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
+
+TEST_F(TestNodeBlackNode, dtor)
+{
+ /* No access to internals? Only test that this is crash free. */
+ Node* n = nullptr;
+ ASSERT_NO_FATAL_FAILURE(n = new Node());
+ if (n)
+ {
+ delete n;
+ }
+}
+
+/* operator== */
+TEST_F(TestNodeBlackNode, operator_equals)
+{
+ Node a, b, c;
+
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+ a = b;
+ c = a;
+
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+ ASSERT_TRUE(a == a);
+ ASSERT_TRUE(a == b);
+ ASSERT_TRUE(a == c);
+
+ ASSERT_TRUE(b == a);
+ ASSERT_TRUE(b == b);
+ ASSERT_TRUE(b == c);
+
+ ASSERT_TRUE(c == a);
+ ASSERT_TRUE(c == b);
+ ASSERT_TRUE(c == c);
+
+ ASSERT_TRUE(d == d);
+
+ ASSERT_FALSE(d == a);
+ ASSERT_FALSE(d == b);
+ ASSERT_FALSE(d == c);
+
+ ASSERT_FALSE(a == d);
+ ASSERT_FALSE(b == d);
+ ASSERT_FALSE(c == d);
+}
+
+/* operator!= */
+TEST_F(TestNodeBlackNode, operator_not_equals)
+{
+ Node a, b, c;
+
+ b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+ a = b;
+ c = a;
+
+ Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
+
+ /*structed assuming operator == works */
+ ASSERT_TRUE(iff(a != a, !(a == a)));
+ ASSERT_TRUE(iff(a != b, !(a == b)));
+ ASSERT_TRUE(iff(a != c, !(a == c)));
+
+ ASSERT_TRUE(iff(b != a, !(b == a)));
+ ASSERT_TRUE(iff(b != b, !(b == b)));
+ ASSERT_TRUE(iff(b != c, !(b == c)));
+
+ ASSERT_TRUE(iff(c != a, !(c == a)));
+ ASSERT_TRUE(iff(c != b, !(c == b)));
+ ASSERT_TRUE(iff(c != c, !(c == c)));
+
+ ASSERT_TRUE(!(d != d));
+
+ ASSERT_TRUE(d != a);
+ ASSERT_TRUE(d != b);
+ ASSERT_TRUE(d != c);
+}
+
+/* operator[] */
+TEST_F(TestNodeBlackNode, operator_square)
+{
+#ifdef CVC4_ASSERTIONS
+ // Basic bounds check on a node w/out children
+ ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+ ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+
+ // Basic access check
+ Node tb = d_nodeManager->mkConst(true);
+ Node eb = d_nodeManager->mkConst(false);
+ Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ Node ite = cnd.iteNode(tb, eb);
+
+ ASSERT_EQ(tb, cnd[0]);
+ ASSERT_EQ(eb, cnd[1]);
+
+ ASSERT_EQ(cnd, ite[0]);
+ ASSERT_EQ(tb, ite[1]);
+ ASSERT_EQ(eb, ite[2]);
+
+#ifdef CVC4_ASSERTIONS
+ // Bounds check on a node with children
+ ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+ ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
+#endif
+}
+
+/* operator= */
+TEST_F(TestNodeBlackNode, operator_assign)
+{
+ Node a, b;
+ Node c = d_nodeManager->mkNode(
+ NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
+
+ b = c;
+ ASSERT_EQ(b, c);
+
+ a = b = c;
+
+ ASSERT_EQ(a, b);
+ ASSERT_EQ(a, c);
+}
+
+/* operator< */
+TEST_F(TestNodeBlackNode, operator_less_than)
+{
+ // We don't have access to the ids so we can't test the implementation
+ // in the black box tests.
+
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+ ASSERT_TRUE(a < b || b < a);
+ ASSERT_TRUE(!(a < b && b < a));
+
+ Node c = d_nodeManager->mkNode(AND, a, b);
+ Node d = d_nodeManager->mkNode(AND, a, b);
+
+ ASSERT_FALSE(c < d);
+ ASSERT_FALSE(d < c);
+
+ // simple test of descending descendant property
+ Node child = d_nodeManager->mkConst(true);
+ Node parent = d_nodeManager->mkNode(NOT, child);
+
+ ASSERT_TRUE(child < parent);
+
+ // slightly less simple test of DD property
+ std::vector<Node> chain;
+ const int N = 500;
+ Node curr = d_nodeManager->mkNode(OR, a, b);
+ chain.push_back(curr);
+ for (int i = 0; i < N; ++i)
+ {
+ curr = d_nodeManager->mkNode(AND, curr, curr);
+ chain.push_back(curr);
+ }
+
+ for (int i = 0; i < N; ++i)
+ {
+ for (int j = i + 1; j < N; ++j)
+ {
+ Node chain_i = chain[i];
+ Node chain_j = chain[j];
+ ASSERT_TRUE(chain_i < chain_j);
+ }
+ }
+}
+
+TEST_F(TestNodeBlackNode, eqNode)
+{
+ TypeNode t = d_nodeManager->mkSort();
+ Node left = d_nodeManager->mkSkolem("left", t);
+ Node right = d_nodeManager->mkSkolem("right", t);
+ Node eq = left.eqNode(right);
+
+ ASSERT_EQ(EQUAL, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(eq[0], left);
+ ASSERT_EQ(eq[1], right);
+}
+
+TEST_F(TestNodeBlackNode, notNode)
+{
+ Node child = d_nodeManager->mkConst(true);
+ Node parent = child.notNode();
+
+ ASSERT_EQ(NOT, parent.getKind());
+ ASSERT_EQ(1, parent.getNumChildren());
+
+ ASSERT_EQ(parent[0], child);
+}
+
+TEST_F(TestNodeBlackNode, andNode)
+{
+ Node left = d_nodeManager->mkConst(true);
+ Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+ Node eq = left.andNode(right);
+
+ ASSERT_EQ(AND, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(*(eq.begin()), left);
+ ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, orNode)
+{
+ Node left = d_nodeManager->mkConst(true);
+ Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+ Node eq = left.orNode(right);
+
+ ASSERT_EQ(OR, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(*(eq.begin()), left);
+ ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, iteNode)
+{
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+ Node cnd = d_nodeManager->mkNode(OR, a, b);
+ Node thenBranch = d_nodeManager->mkConst(true);
+ Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkConst(false));
+ Node ite = cnd.iteNode(thenBranch, elseBranch);
+
+ ASSERT_EQ(ITE, ite.getKind());
+ ASSERT_EQ(3, ite.getNumChildren());
+
+ ASSERT_EQ(*(ite.begin()), cnd);
+ ASSERT_EQ(*(++ite.begin()), thenBranch);
+ ASSERT_EQ(*(++(++ite.begin())), elseBranch);
+}
+
+TEST_F(TestNodeBlackNode, iffNode)
+{
+ Node left = d_nodeManager->mkConst(true);
+ Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+ Node eq = left.eqNode(right);
+
+ ASSERT_EQ(EQUAL, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(*(eq.begin()), left);
+ ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, impNode)
+{
+ Node left = d_nodeManager->mkConst(true);
+ Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+ Node eq = left.impNode(right);
+
+ ASSERT_EQ(IMPLIES, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(*(eq.begin()), left);
+ ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, xorNode)
+{
+ Node left = d_nodeManager->mkConst(true);
+ Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkConst(false)));
+ Node eq = left.xorNode(right);
+
+ ASSERT_EQ(XOR, eq.getKind());
+ ASSERT_EQ(2, eq.getNumChildren());
+
+ ASSERT_EQ(*(eq.begin()), left);
+ ASSERT_EQ(*(++eq.begin()), right);
+}
+
+TEST_F(TestNodeBlackNode, getKind)
+{
+ Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+ Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
+
+ Node n = d_nodeManager->mkNode(NOT, a);
+ ASSERT_EQ(NOT, n.getKind());
+
+ n = d_nodeManager->mkNode(EQUAL, a, b);
+ ASSERT_EQ(EQUAL, n.getKind());
+
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
+
+ n = d_nodeManager->mkNode(PLUS, x, y);
+ ASSERT_EQ(PLUS, n.getKind());
+
+ n = d_nodeManager->mkNode(UMINUS, x);
+ ASSERT_EQ(UMINUS, n.getKind());
+}
+
+TEST_F(TestNodeBlackNode, getOperator)
+{
+ TypeNode sort = d_nodeManager->mkSort("T");
+ TypeNode booleanType = d_nodeManager->booleanType();
+ TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
+
+ Node f = d_nodeManager->mkSkolem("f", predType);
+ Node a = d_nodeManager->mkSkolem("a", sort);
+ Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
+
+ ASSERT_TRUE(fa.hasOperator());
+ ASSERT_FALSE(f.hasOperator());
+ ASSERT_FALSE(a.hasOperator());
+
+ ASSERT_EQ(fa.getNumChildren(), 1);
+ ASSERT_EQ(f.getNumChildren(), 0);
+ ASSERT_EQ(a.getNumChildren(), 0);
+
+ ASSERT_EQ(f, fa.getOperator());
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
+ ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
+#endif
+}
+
+TEST_F(TestNodeBlackNode, getNumChildren)
+{
+ Node trueNode = d_nodeManager->mkConst(true);
+
+ ASSERT_EQ(0, (Node::null()).getNumChildren());
+ ASSERT_EQ(1, trueNode.notNode().getNumChildren());
+ ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
+
+ srand(0);
+ for (uint32_t i = 0; i < 500; ++i)
+ {
+ uint32_t n = rand() % 1000 + 2;
+ testNaryExpForSize(AND, n);
+ }
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(testNaryExpForSize(AND, 0),
+ "getNumChildren\\(\\) >= "
+ "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+ ASSERT_DEATH(testNaryExpForSize(AND, 1),
+ "getNumChildren\\(\\) >= "
+ "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+ ASSERT_DEATH(testNaryExpForSize(NOT, 0),
+ "getNumChildren\\(\\) >= "
+ "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
+ ASSERT_DEATH(testNaryExpForSize(NOT, 2),
+ "getNumChildren\\(\\) <= "
+ "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestNodeBlackNode, iterator)
+{
+ NodeBuilder<> b;
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+ Node n = b << x << y << z << kind::AND;
+
+ { // iterator
+ Node::iterator i = n.begin();
+ ASSERT_EQ(*i++, x);
+ ASSERT_EQ(*i++, y);
+ ASSERT_EQ(*i++, z);
+ ASSERT_EQ(i, n.end());
+ }
+
+ { // same for const iterator
+ const Node& c = n;
+ Node::const_iterator i = c.begin();
+ ASSERT_EQ(*i++, x);
+ ASSERT_EQ(*i++, y);
+ ASSERT_EQ(*i++, z);
+ ASSERT_EQ(i, n.end());
+ }
+}
+
+TEST_F(TestNodeBlackNode, kinded_iterator)
+{
+ TypeNode integerType = d_nodeManager->integerType();
+
+ Node x = d_nodeManager->mkSkolem("x", integerType);
+ Node y = d_nodeManager->mkSkolem("y", integerType);
+ Node z = d_nodeManager->mkSkolem("z", integerType);
+ Node plus_x_y_z = d_nodeManager->mkNode(kind::PLUS, x, y, z);
+ Node x_minus_y = d_nodeManager->mkNode(kind::MINUS, x, y);
+
+ { // iterator
+ Node::kinded_iterator i = plus_x_y_z.begin(PLUS);
+ ASSERT_EQ(*i++, x);
+ ASSERT_EQ(*i++, y);
+ ASSERT_EQ(*i++, z);
+ ASSERT_TRUE(i == plus_x_y_z.end(PLUS));
+
+ i = x.begin(PLUS);
+ ASSERT_EQ(*i++, x);
+ ASSERT_TRUE(i == x.end(PLUS));
+ }
+}
+
+TEST_F(TestNodeBlackNode, toString)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+
+ Node w = d_nodeManager->mkSkolem(
+ "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node x = d_nodeManager->mkSkolem(
+ "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node y = d_nodeManager->mkSkolem(
+ "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node z = d_nodeManager->mkSkolem(
+ "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node m = NodeBuilder<>() << w << x << kind::OR;
+ Node n = NodeBuilder<>() << m << y << z << kind::AND;
+
+ ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
+}
+
+TEST_F(TestNodeBlackNode, toStream)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+
+ Node w = d_nodeManager->mkSkolem(
+ "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node x = d_nodeManager->mkSkolem(
+ "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node y = d_nodeManager->mkSkolem(
+ "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node z = d_nodeManager->mkSkolem(
+ "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node m = NodeBuilder<>() << x << y << kind::OR;
+ Node n = NodeBuilder<>() << w << m << z << kind::AND;
+ Node o = NodeBuilder<>() << n << n << kind::XOR;
+
+ std::stringstream sstr;
+ sstr << Node::dag(false);
+ n.toStream(sstr);
+ ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+ sstr.str(std::string());
+ o.toStream(sstr, -1, 0);
+ ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(std::string());
+ sstr << n;
+ ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+ sstr.str(std::string());
+ sstr << o;
+ ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(0) << n;
+ ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(0) << o;
+ ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(1) << n;
+ ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(1) << o;
+ ASSERT_EQ(sstr.str(),
+ "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(2) << n;
+ ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(2) << o;
+ ASSERT_EQ(sstr.str(),
+ "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(3) << n;
+ ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
+
+ sstr.str(std::string());
+ sstr << Node::setdepth(3) << o;
+ ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+}
+
+TEST_F(TestNodeBlackNode, dagifier)
+{
+ TypeNode intType = d_nodeManager->integerType();
+ TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
+
+ Node x =
+ d_nodeManager->mkSkolem("x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node y =
+ d_nodeManager->mkSkolem("y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node f =
+ d_nodeManager->mkSkolem("f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node g =
+ d_nodeManager->mkSkolem("g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+ Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
+ Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
+ Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
+ Node gy = d_nodeManager->mkNode(APPLY_UF, g, y);
+ Node fgx = d_nodeManager->mkNode(APPLY_UF, f, gx);
+ Node ffx = d_nodeManager->mkNode(APPLY_UF, f, fx);
+ Node fffx = d_nodeManager->mkNode(APPLY_UF, f, ffx);
+ Node fffx_eq_x = d_nodeManager->mkNode(EQUAL, fffx, x);
+ Node fffx_eq_y = d_nodeManager->mkNode(EQUAL, fffx, y);
+ Node fx_eq_gx = d_nodeManager->mkNode(EQUAL, fx, gx);
+ Node x_eq_y = d_nodeManager->mkNode(EQUAL, x, y);
+ Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
+
+ Node n = d_nodeManager->mkNode(
+ OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
+
+ std::stringstream sstr;
+ sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
+ sstr << Node::dag(false) << n; // never dagify
+ ASSERT_EQ(sstr.str(),
+ "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
+ "y) OR (f(g(x)) = g(y))");
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
+{
+ const std::vector<Node> skolems =
+ makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+ Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+ std::vector<Node> children;
+ for (Node child : add)
+ {
+ children.push_back(child);
+ }
+ ASSERT_TRUE(children.size() == skolems.size()
+ && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
+{
+ const std::vector<Node> skolems =
+ makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+ Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
+ std::vector<TNode> children;
+ for (TNode child : add)
+ {
+ children.push_back(child);
+ }
+ ASSERT_TRUE(children.size() == skolems.size()
+ && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
+{
+ const std::vector<Node> skolems =
+ makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+ Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+ TNode add_tnode = add_node;
+ std::vector<Node> children;
+ for (Node child : add_tnode)
+ {
+ children.push_back(child);
+ }
+ ASSERT_TRUE(children.size() == skolems.size()
+ && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
+{
+ const std::vector<Node> skolems =
+ makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+ Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
+ TNode add_tnode = add_node;
+ std::vector<TNode> children;
+ for (TNode child : add_tnode)
+ {
+ children.push_back(child);
+ }
+ ASSERT_TRUE(children.size() == skolems.size()
+ && std::equal(children.begin(), children.end(), skolems.begin()));
+}
+
+TEST_F(TestNodeBlackNode, isConst)
+{
+ // more complicated "constants" exist in datatypes and arrays theories
+ DType list("list");
+ std::shared_ptr<DTypeConstructor> consC =
+ std::make_shared<DTypeConstructor>("cons");
+ consC->addArg("car", d_nodeManager->integerType());
+ consC->addArgSelf("cdr");
+ list.addConstructor(consC);
+ list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+ TypeNode listType = d_nodeManager->mkDatatypeType(list);
+ const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
+ listType.getDType().getConstructors();
+ Node cons = lcons[0]->getConstructor();
+ Node nil = lcons[1]->getConstructor();
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+ Node cons_x_nil =
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+ cons,
+ x,
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+ Node cons_1_nil =
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+ cons,
+ d_nodeManager->mkConst(Rational(1)),
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+ Node cons_1_cons_2_nil = d_nodeManager->mkNode(
+ APPLY_CONSTRUCTOR,
+ cons,
+ d_nodeManager->mkConst(Rational(1)),
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+ cons,
+ d_nodeManager->mkConst(Rational(2)),
+ d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
+ ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
+ ASSERT_FALSE(cons_x_nil.isConst());
+ ASSERT_TRUE(cons_1_nil.isConst());
+ ASSERT_TRUE(cons_1_cons_2_nil.isConst());
+
+ TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+ d_nodeManager->integerType());
+ Node zero = d_nodeManager->mkConst(Rational(0));
+ Node one = d_nodeManager->mkConst(Rational(1));
+ Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+ ASSERT_TRUE(storeAll.isConst());
+
+ Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+ ASSERT_FALSE(arr.isConst());
+ arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+ ASSERT_TRUE(arr.isConst());
+ Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+ ASSERT_FALSE(arr2.isConst());
+ arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+ ASSERT_FALSE(arr2.isConst());
+
+ arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
+ d_nodeManager->mkBitVectorType(1));
+ zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
+ one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
+ storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+ ASSERT_TRUE(storeAll.isConst());
+
+ arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+ ASSERT_FALSE(arr.isConst());
+ arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+ ASSERT_TRUE(arr.isConst());
+ arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+ ASSERT_FALSE(arr2.isConst());
+ arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+ ASSERT_FALSE(arr2.isConst());
+ arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+ ASSERT_FALSE(arr2.isConst());
+}
+
+namespace {
+Node level0(NodeManager* nm)
+{
+ NodeBuilder<> nb(kind::AND);
+ Node x = nm->mkSkolem("x", nm->booleanType());
+ nb << x;
+ nb << x;
+ return Node(nb.constructNode());
+}
+TNode level1(NodeManager* nm) { return level0(nm); }
+} // namespace
+
+/**
+ * This is for demonstrating what a certain type of user error looks like.
+ */
+TEST_F(TestNodeBlackNode, node_tnode_usage)
+{
+ Node n;
+ ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
+ ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
+}
+
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_builder_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Tim King, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::NodeBuilder.
+ **
+ ** Black box testing of CVC4::NodeBuilder.
+ **/
+
+#include <limits.h>
+
+#include <sstream>
+#include <vector>
+
+#include "base/check.h"
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/rational.h"
+
+#define K 30u
+#define LARGE_K UINT_MAX / 40
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeBuilder : public TestNode
+{
+ protected:
+ template <unsigned N>
+ void push_back(NodeBuilder<N>& nb, uint32_t n)
+ {
+ for (uint32_t i = 0; i < n; ++i)
+ {
+ nb << d_nodeManager->mkConst(true);
+ }
+ }
+ Kind d_specKind = AND;
+};
+
+/** Tests just constructors. No modification is done to the node. */
+TEST_F(TestNodeBlackNodeBuilder, ctors)
+{
+ /* Default size tests. */
+ NodeBuilder<> def;
+ ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<> spec(d_specKind);
+ ASSERT_EQ(spec.getKind(), d_specKind);
+ ASSERT_EQ(spec.getNumChildren(), 0u);
+ ASSERT_EQ(spec.begin(), spec.end());
+
+ NodeBuilder<> from_nm(d_nodeManager.get());
+ ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(from_nm.getNumChildren(),
+ "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind);
+ ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
+ ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
+ ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end());
+
+ /* Non-default size tests */
+ NodeBuilder<K> ws;
+ ASSERT_EQ(ws.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<K> ws_kind(d_specKind);
+ ASSERT_EQ(ws_kind.getKind(), d_specKind);
+ ASSERT_EQ(ws_kind.getNumChildren(), 0u);
+ ASSERT_EQ(ws_kind.begin(), ws_kind.end());
+
+ NodeBuilder<K> ws_from_nm(d_nodeManager.get());
+ ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(ws_from_nm.getNumChildren(),
+ "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind);
+ ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind);
+ ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u);
+ ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
+
+ /* Extreme size tests */
+ NodeBuilder<0> ws_size_0;
+
+ /* Allocating on the heap instead of the stack. */
+ NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>;
+ delete ws_size_large;
+
+ /* Copy constructors */
+ NodeBuilder<> copy(def);
+ ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<K> cp_ws(ws);
+ ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<K - 10> cp_from_larger(ws);
+ ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(cp_from_larger.getNumChildren(),
+ "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ NodeBuilder<K + 10> cp_from_smaller(ws);
+ ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(cp_from_smaller.getNumChildren(),
+ "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_from_smaller.begin(),
+ "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, dtor)
+{
+ NodeBuilder<K>* nb = new NodeBuilder<K>();
+ delete nb;
+}
+
+TEST_F(TestNodeBlackNodeBuilder, begin_end)
+{
+ /* Test begin() and end() without resizing. */
+ NodeBuilder<K> ws(d_specKind);
+ ASSERT_EQ(ws.begin(), ws.end());
+
+ push_back(ws, K);
+ ASSERT_NE(ws.begin(), ws.end());
+
+ NodeBuilder<K>::iterator iter = ws.begin();
+ for (uint32_t i = 0; i < K; ++i)
+ {
+ ASSERT_NE(iter, ws.end());
+ ++iter;
+ }
+ ASSERT_EQ(iter, ws.end());
+
+ NodeBuilder<K>::const_iterator citer = ws.begin();
+ for (uint32_t i = 0; i < K; ++i)
+ {
+ ASSERT_NE(citer, ws.end());
+ ++citer;
+ }
+ ASSERT_EQ(citer, ws.end());
+
+ /* Repeat same tests and make sure that resizing occurs. */
+ NodeBuilder<> smaller(d_specKind);
+ ASSERT_EQ(smaller.begin(), smaller.end());
+
+ push_back(smaller, K);
+ ASSERT_NE(smaller.begin(), smaller.end());
+
+ NodeBuilder<>::iterator smaller_iter = smaller.begin();
+ for (uint32_t i = 0; i < K; ++i)
+ {
+ ASSERT_NE(smaller_iter, smaller.end());
+ ++smaller_iter;
+ }
+ ASSERT_EQ(iter, ws.end());
+
+ NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
+ for (uint32_t i = 0; i < K; ++i)
+ {
+ ASSERT_NE(smaller_citer, smaller.end());
+ ++smaller_citer;
+ }
+ ASSERT_EQ(smaller_citer, smaller.end());
+}
+
+TEST_F(TestNodeBlackNodeBuilder, iterator)
+{
+ NodeBuilder<> b;
+ Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
+ Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+ Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+ b << x << y << z << AND;
+
+ {
+ NodeBuilder<>::iterator i = b.begin();
+ ASSERT_EQ(*i++, x);
+ ASSERT_EQ(*i++, y);
+ ASSERT_EQ(*i++, z);
+ ASSERT_EQ(i, b.end());
+ }
+
+ {
+ const NodeBuilder<>& c = b;
+ NodeBuilder<>::const_iterator i = c.begin();
+ ASSERT_EQ(*i++, x);
+ ASSERT_EQ(*i++, y);
+ ASSERT_EQ(*i++, z);
+ ASSERT_EQ(i, b.end());
+ }
+}
+
+TEST_F(TestNodeBlackNodeBuilder, getKind)
+{
+ NodeBuilder<> noKind;
+ ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
+
+ Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+ noKind << x << x;
+ ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND);
+
+ noKind << PLUS;
+
+ ASSERT_EQ(noKind.getKind(), PLUS);
+
+ Node n = noKind;
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
+#endif
+
+ NodeBuilder<> spec(PLUS);
+ ASSERT_EQ(spec.getKind(), PLUS);
+ spec << x << x;
+ ASSERT_EQ(spec.getKind(), PLUS);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
+{
+ Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode));
+
+ NodeBuilder<> nb;
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+ nb << PLUS << x << x;
+
+ ASSERT_EQ(nb.getNumChildren(), 2u);
+
+ nb << x << x;
+ ASSERT_EQ(nb.getNumChildren(), 4u);
+
+ nb.clear();
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+ nb.clear(PLUS);
+ ASSERT_EQ(nb.getNumChildren(), 0u);
+ nb << x << x << x;
+
+ ASSERT_EQ(nb.getNumChildren(), 3u);
+
+ nb << x << x << x;
+ ASSERT_EQ(nb.getNumChildren(), 6u);
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
+ Node n = nb;
+ ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_square)
+{
+ NodeBuilder<> arr(d_specKind);
+
+ Node i_0 = d_nodeManager->mkConst(false);
+ Node i_2 = d_nodeManager->mkConst(true);
+ Node i_K = d_nodeManager->mkNode(NOT, i_0);
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(arr[-1], "index out of range");
+ ASSERT_DEATH(arr[0], "index out of range");
+#endif
+
+ arr << i_0;
+
+ ASSERT_EQ(arr[0], i_0);
+
+ push_back(arr, 1);
+
+ arr << i_2;
+
+ ASSERT_EQ(arr[0], i_0);
+ ASSERT_EQ(arr[2], i_2);
+
+ push_back(arr, K - 3);
+
+ ASSERT_EQ(arr[0], i_0);
+ ASSERT_EQ(arr[2], i_2);
+ for (unsigned i = 3; i < K; ++i)
+ {
+ ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
+ }
+
+ arr << i_K;
+
+ ASSERT_EQ(arr[0], i_0);
+ ASSERT_EQ(arr[2], i_2);
+ for (unsigned i = 3; i < K; ++i)
+ {
+ ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
+ }
+ ASSERT_EQ(arr[K], i_K);
+
+#ifdef CVC4_ASSERTIONS
+ Node n = arr;
+ ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, clear)
+{
+ NodeBuilder<> nb;
+
+ ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ nb << d_specKind;
+ push_back(nb, K);
+
+ ASSERT_EQ(nb.getKind(), d_specKind);
+ ASSERT_EQ(nb.getNumChildren(), K);
+ ASSERT_NE(nb.begin(), nb.end());
+
+ nb.clear();
+
+ ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+
+ nb << d_specKind;
+ push_back(nb, K);
+
+ ASSERT_EQ(nb.getKind(), d_specKind);
+ ASSERT_EQ(nb.getNumChildren(), K);
+ ASSERT_NE(nb.begin(), nb.end());
+
+ nb.clear(d_specKind);
+
+ ASSERT_EQ(nb.getKind(), d_specKind);
+ ASSERT_EQ(nb.getNumChildren(), 0u);
+ ASSERT_EQ(nb.begin(), nb.end());
+
+ push_back(nb, K);
+ nb.clear();
+
+ ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+ ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
+{
+#ifdef CVC4_ASSERTIONS
+ NodeBuilder<> spec(d_specKind);
+ ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
+#endif
+
+ NodeBuilder<> noSpec;
+ noSpec << d_specKind;
+ ASSERT_EQ(noSpec.getKind(), d_specKind);
+
+ NodeBuilder<> modified;
+ push_back(modified, K);
+ modified << d_specKind;
+ ASSERT_EQ(modified.getKind(), d_specKind);
+
+ NodeBuilder<> nb(d_specKind);
+ nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
+ nb.clear(PLUS);
+
+#ifdef CVC4_ASSERTIONS
+ Node n;
+ ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
+ nb.clear(PLUS);
+#endif
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
+#endif
+
+ NodeBuilder<> testRef;
+ ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
+
+#ifdef CVC4_ASSERTIONS
+ NodeBuilder<> testTwo;
+ ASSERT_DEATH(testTwo << d_specKind << PLUS,
+ "can't redefine the Kind of a NodeBuilder");
+#endif
+
+ NodeBuilder<> testMixOrder1;
+ ASSERT_EQ(
+ (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
+ d_specKind);
+ NodeBuilder<> testMixOrder2;
+ ASSERT_EQ(
+ (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
+ d_specKind);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
+{
+ NodeBuilder<K> nb(d_specKind);
+ ASSERT_EQ(nb.getKind(), d_specKind);
+ ASSERT_EQ(nb.getNumChildren(), 0u);
+ ASSERT_EQ(nb.begin(), nb.end());
+ push_back(nb, K);
+ ASSERT_EQ(nb.getKind(), d_specKind);
+ ASSERT_EQ(nb.getNumChildren(), K);
+ ASSERT_NE(nb.begin(), nb.end());
+
+#ifdef CVC4_ASSERTIONS
+ Node n = nb;
+ ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
+#endif
+
+ NodeBuilder<> overflow(d_specKind);
+ ASSERT_EQ(overflow.getKind(), d_specKind);
+ ASSERT_EQ(overflow.getNumChildren(), 0u);
+ ASSERT_EQ(overflow.begin(), overflow.end());
+
+ push_back(overflow, 5 * K + 1);
+
+ ASSERT_EQ(overflow.getKind(), d_specKind);
+ ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
+ ASSERT_NE(overflow.begin(), overflow.end());
+}
+
+TEST_F(TestNodeBlackNodeBuilder, append)
+{
+ Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode);
+ Node y = d_nodeManager->mkSkolem("y", *d_boolTypeNode);
+ Node z = d_nodeManager->mkSkolem("z", *d_boolTypeNode);
+ Node m = d_nodeManager->mkNode(AND, y, z, x);
+ Node n = d_nodeManager->mkNode(OR, d_nodeManager->mkNode(NOT, x), y, z);
+ Node o = d_nodeManager->mkNode(XOR, y, x);
+
+ Node r = d_nodeManager->mkSkolem("r", *d_realTypeNode);
+ Node s = d_nodeManager->mkSkolem("s", *d_realTypeNode);
+ Node t = d_nodeManager->mkSkolem("t", *d_realTypeNode);
+
+ Node p = d_nodeManager->mkNode(
+ EQUAL,
+ d_nodeManager->mkConst<Rational>(0),
+ d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
+ Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
+ "Nodes with kind XOR must have at most 2 children");
+#endif
+
+ NodeBuilder<> b(d_specKind);
+
+ /* test append(TNode) */
+ b.append(n).append(o).append(q);
+
+ ASSERT_EQ(b.getNumChildren(), 3);
+ ASSERT_EQ(b[0], n);
+ ASSERT_EQ(b[1], o);
+ ASSERT_EQ(b[2], q);
+
+ std::vector<Node> v;
+ v.push_back(m);
+ v.push_back(p);
+ v.push_back(q);
+
+ /* test append(vector<Node>) */
+ b.append(v);
+
+ ASSERT_EQ(b.getNumChildren(), 6);
+ ASSERT_EQ(b[0], n);
+ ASSERT_EQ(b[1], o);
+ ASSERT_EQ(b[2], q);
+ ASSERT_EQ(b[3], m);
+ ASSERT_EQ(b[4], p);
+ ASSERT_EQ(b[5], q);
+
+ /* test append(iterator, iterator) */
+ b.append(v.rbegin(), v.rend());
+
+ ASSERT_EQ(b.getNumChildren(), 9);
+ ASSERT_EQ(b[0], n);
+ ASSERT_EQ(b[1], o);
+ ASSERT_EQ(b[2], q);
+ ASSERT_EQ(b[3], m);
+ ASSERT_EQ(b[4], p);
+ ASSERT_EQ(b[5], q);
+ ASSERT_EQ(b[6], q);
+ ASSERT_EQ(b[7], p);
+ ASSERT_EQ(b[8], m);
+}
+
+TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
+{
+ NodeBuilder<K> implicit(d_specKind);
+ NodeBuilder<K> explic(d_specKind);
+
+ push_back(implicit, K);
+ push_back(explic, K);
+
+ Node nimpl = implicit;
+ Node nexplicit = (Node)explic;
+
+ ASSERT_EQ(nimpl.getKind(), d_specKind);
+ ASSERT_EQ(nimpl.getNumChildren(), K);
+
+ ASSERT_EQ(nexplicit.getKind(), d_specKind);
+ ASSERT_EQ(nexplicit.getNumChildren(), K);
+
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
+#endif
+}
+
+TEST_F(TestNodeBlackNodeBuilder, leftist_building)
+{
+ NodeBuilder<> nb;
+
+ Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
+
+ Node b = d_nodeManager->mkSkolem("b", *d_boolTypeNode);
+ Node c = d_nodeManager->mkSkolem("c", *d_boolTypeNode);
+
+ Node d = d_nodeManager->mkSkolem("d", *d_realTypeNode);
+ Node e = d_nodeManager->mkSkolem("e", *d_realTypeNode);
+
+ nb << a << NOT << b << c << OR << c << a << AND << d << e << ITE;
+
+ Node n = nb;
+ ASSERT_EQ(n.getNumChildren(), 3u);
+ ASSERT_EQ(n.getType(), *d_realTypeNode);
+ ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
+ ASSERT_EQ(n[1].getType(), *d_realTypeNode);
+ ASSERT_EQ(n[2].getType(), *d_realTypeNode);
+
+ Node nota = d_nodeManager->mkNode(NOT, a);
+ Node nota_or_b_or_c = d_nodeManager->mkNode(OR, nota, b, c);
+ Node n0 = d_nodeManager->mkNode(AND, nota_or_b_or_c, c, a);
+ Node nexpected = d_nodeManager->mkNode(ITE, n0, d, e);
+
+ ASSERT_EQ(nexpected, n);
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_manager_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Christopher L. Conway, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::NodeManager.
+ **
+ ** Black box testing of CVC4::NodeManager.
+ **/
+
+#include <string>
+#include <vector>
+
+#include "base/output.h"
+#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "test_node.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeBlackNodeManager : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeManager, mkNode_not)
+{
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(NOT, x);
+ ASSERT_EQ(n.getNumChildren(), 1u);
+ ASSERT_EQ(n.getKind(), NOT);
+ ASSERT_EQ(n[0], x);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_binary)
+{
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(IMPLIES, x, y);
+ ASSERT_EQ(n.getNumChildren(), 2u);
+ ASSERT_EQ(n.getKind(), IMPLIES);
+ ASSERT_EQ(n[0], x);
+ ASSERT_EQ(n[1], y);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
+{
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+ Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(AND, x, y, z);
+ ASSERT_EQ(n.getNumChildren(), 3u);
+ ASSERT_EQ(n.getKind(), AND);
+ ASSERT_EQ(n[0], x);
+ ASSERT_EQ(n[1], y);
+ ASSERT_EQ(n[2], z);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
+{
+ Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
+ ASSERT_EQ(n.getNumChildren(), 4u);
+ ASSERT_EQ(n.getKind(), AND);
+ ASSERT_EQ(n[0], x1);
+ ASSERT_EQ(n[1], x2);
+ ASSERT_EQ(n[2], x3);
+ ASSERT_EQ(n[3], x4);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
+{
+ Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ Node x4 = d_nodeManager->mkSkolem("x4", d_nodeManager->booleanType());
+ Node x5 = d_nodeManager->mkSkolem("x5", d_nodeManager->booleanType());
+ Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
+ ASSERT_EQ(n.getNumChildren(), 5u);
+ ASSERT_EQ(n.getKind(), AND);
+ ASSERT_EQ(n[0], x1);
+ ASSERT_EQ(n[1], x2);
+ ASSERT_EQ(n[2], x3);
+ ASSERT_EQ(n[3], x4);
+ ASSERT_EQ(n[4], x5);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
+{
+ Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ std::vector<Node> args;
+ args.push_back(x1);
+ args.push_back(x2);
+ args.push_back(x3);
+ Node n = d_nodeManager->mkNode(AND, args);
+ ASSERT_EQ(n.getNumChildren(), args.size());
+ ASSERT_EQ(n.getKind(), AND);
+ for (unsigned i = 0; i < args.size(); ++i)
+ {
+ ASSERT_EQ(n[i], args[i]);
+ }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
+{
+ Node x1 = d_nodeManager->mkSkolem("x1", d_nodeManager->booleanType());
+ Node x2 = d_nodeManager->mkSkolem("x2", d_nodeManager->booleanType());
+ Node x3 = d_nodeManager->mkSkolem("x3", d_nodeManager->booleanType());
+ std::vector<TNode> args;
+ args.push_back(x1);
+ args.push_back(x2);
+ args.push_back(x3);
+ Node n = d_nodeManager->mkNode(AND, args);
+ ASSERT_EQ(n.getNumChildren(), args.size());
+ ASSERT_EQ(n.getKind(), AND);
+ for (unsigned i = 0; i < args.size(); ++i)
+ {
+ ASSERT_EQ(n[i], args[i]);
+ }
+}
+
+TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
+{
+ Node x = d_nodeManager->mkSkolem(
+ "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
+ ASSERT_EQ(x.getKind(), SKOLEM);
+ ASSERT_EQ(x.getNumChildren(), 0u);
+ ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
+ ASSERT_EQ(x.getType(), *d_boolTypeNode);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_bool)
+{
+ Node tt = d_nodeManager->mkConst(true);
+ ASSERT_EQ(tt.getConst<bool>(), true);
+ Node ff = d_nodeManager->mkConst(false);
+ ASSERT_EQ(ff.getConst<bool>(), false);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkConst_rational)
+{
+ Rational r("3/2");
+ Node n = d_nodeManager->mkConst(r);
+ ASSERT_EQ(n.getConst<Rational>(), r);
+}
+
+TEST_F(TestNodeBlackNodeManager, hasOperator)
+{
+ ASSERT_TRUE(NodeManager::hasOperator(AND));
+ ASSERT_TRUE(NodeManager::hasOperator(OR));
+ ASSERT_TRUE(NodeManager::hasOperator(NOT));
+ ASSERT_TRUE(NodeManager::hasOperator(APPLY_UF));
+ ASSERT_TRUE(!NodeManager::hasOperator(VARIABLE));
+}
+
+TEST_F(TestNodeBlackNodeManager, booleanType)
+{
+ TypeNode t = d_nodeManager->booleanType();
+ TypeNode t2 = d_nodeManager->booleanType();
+ TypeNode t3 = d_nodeManager->mkSort("T");
+ ASSERT_TRUE(t.isBoolean());
+ ASSERT_FALSE(t.isFunction());
+ ASSERT_FALSE(t.isNull());
+ ASSERT_FALSE(t.isPredicate());
+ ASSERT_FALSE(t.isSort());
+ ASSERT_EQ(t, t2);
+ ASSERT_NE(t, t3);
+
+ TypeNode bt = t;
+ ASSERT_EQ(bt, t);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
+{
+ TypeNode booleanType = d_nodeManager->booleanType();
+ TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
+ TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
+
+ ASSERT_FALSE(t.isBoolean());
+ ASSERT_TRUE(t.isFunction());
+ ASSERT_FALSE(t.isNull());
+ ASSERT_TRUE(t.isPredicate());
+ ASSERT_FALSE(t.isSort());
+
+ ASSERT_EQ(t, t2);
+
+ TypeNode ft = t;
+ ASSERT_EQ(ft, t);
+ ASSERT_EQ(ft.getArgTypes().size(), 1u);
+ ASSERT_EQ(ft.getArgTypes()[0], booleanType);
+ ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
+{
+ TypeNode a = d_nodeManager->mkSort();
+ TypeNode b = d_nodeManager->mkSort();
+ TypeNode c = d_nodeManager->mkSort();
+
+ std::vector<TypeNode> argTypes;
+ argTypes.push_back(a);
+ argTypes.push_back(b);
+
+ TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
+ TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
+
+ ASSERT_FALSE(t.isBoolean());
+ ASSERT_TRUE(t.isFunction());
+ ASSERT_FALSE(t.isNull());
+ ASSERT_FALSE(t.isPredicate());
+ ASSERT_FALSE(t.isSort());
+
+ ASSERT_EQ(t, t2);
+
+ TypeNode ft = t;
+ ASSERT_EQ(ft, t);
+ ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+ ASSERT_EQ(ft.getArgTypes()[0], a);
+ ASSERT_EQ(ft.getArgTypes()[1], b);
+ ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
+{
+ TypeNode a = d_nodeManager->mkSort();
+ TypeNode b = d_nodeManager->mkSort();
+ TypeNode c = d_nodeManager->mkSort();
+
+ std::vector<TypeNode> types;
+ types.push_back(a);
+ types.push_back(b);
+ types.push_back(c);
+
+ TypeNode t = d_nodeManager->mkFunctionType(types);
+ TypeNode t2 = d_nodeManager->mkFunctionType(types);
+
+ ASSERT_FALSE(t.isBoolean());
+ ASSERT_TRUE(t.isFunction());
+ ASSERT_FALSE(t.isNull());
+ ASSERT_FALSE(t.isPredicate());
+ ASSERT_FALSE(t.isSort());
+
+ ASSERT_EQ(t, t2);
+
+ TypeNode ft = t;
+ ASSERT_EQ(ft, t);
+ ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
+ ASSERT_EQ(ft.getArgTypes()[0], a);
+ ASSERT_EQ(ft.getArgTypes()[1], b);
+ ASSERT_EQ(ft.getRangeType(), c);
+}
+
+TEST_F(TestNodeBlackNodeManager, mkPredicateType)
+{
+ TypeNode a = d_nodeManager->mkSort("a");
+ TypeNode b = d_nodeManager->mkSort("b");
+ TypeNode c = d_nodeManager->mkSort("c");
+ TypeNode booleanType = d_nodeManager->booleanType();
+
+ std::vector<TypeNode> argTypes;
+ argTypes.push_back(a);
+ argTypes.push_back(b);
+ argTypes.push_back(c);
+
+ TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+ TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
+
+ ASSERT_FALSE(t.isBoolean());
+ ASSERT_TRUE(t.isFunction());
+ ASSERT_FALSE(t.isNull());
+ ASSERT_TRUE(t.isPredicate());
+ ASSERT_FALSE(t.isSort());
+
+ ASSERT_EQ(t, t2);
+
+ TypeNode ft = t;
+ ASSERT_EQ(ft, t);
+ ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
+ ASSERT_EQ(ft.getArgTypes()[0], a);
+ ASSERT_EQ(ft.getArgTypes()[1], b);
+ ASSERT_EQ(ft.getArgTypes()[2], c);
+ ASSERT_EQ(ft.getRangeType(), booleanType);
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
+{
+#ifdef CVC4_ASSERTIONS
+ Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+ ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
+ "Nodes with kind AND must have at least 2 children");
+#endif
+}
+
+/* This test is only valid if assertions are enabled. */
+TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
+{
+#ifdef CVC4_ASSERTIONS
+ std::vector<Node> vars;
+ const uint32_t max = metakind::getMaxArityForKind(AND);
+ TypeNode boolType = d_nodeManager->booleanType();
+ Node skolem_i = d_nodeManager->mkSkolem("i", boolType);
+ Node skolem_j = d_nodeManager->mkSkolem("j", boolType);
+ Node andNode = skolem_i.andNode(skolem_j);
+ Node orNode = skolem_i.orNode(skolem_j);
+ while (vars.size() <= max)
+ {
+ vars.push_back(andNode);
+ vars.push_back(skolem_j);
+ vars.push_back(orNode);
+ }
+ ASSERT_DEATH(d_nodeManager->mkNode(AND, vars), "toSize > d_nvMaxChildren");
+#endif
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_manager_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::NodeManager.
+ **
+ ** White box testing of CVC4::NodeManager.
+ **/
+
+#include <string>
+
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/integer.h"
+#include "util/rational.h"
+
+namespace CVC4 {
+
+using namespace CVC4::expr;
+
+namespace test {
+
+class TestNodeWhiteNodeManager : public TestNode
+{
+};
+
+TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
+{
+ Rational i("3");
+ Node n = d_nodeManager->mkConst(i);
+ Node m = d_nodeManager->mkConst(i);
+ ASSERT_EQ(n.getId(), m.getId());
+}
+
+TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
+{
+ NodeBuilder<> nb;
+
+ ASSERT_NO_THROW(nb.realloc(15));
+ ASSERT_NO_THROW(nb.realloc(25));
+ ASSERT_NO_THROW(nb.realloc(256));
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren");
+#endif /* CVC4_ASSERTIONS */
+ ASSERT_NO_THROW(nb.realloc(257));
+ ASSERT_NO_THROW(nb.realloc(4000));
+ ASSERT_NO_THROW(nb.realloc(20000));
+ ASSERT_NO_THROW(nb.realloc(60000));
+ ASSERT_NO_THROW(nb.realloc(65535));
+ ASSERT_NO_THROW(nb.realloc(65536));
+ ASSERT_NO_THROW(nb.realloc(67108863));
+#ifdef CVC4_ASSERTIONS
+ ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren");
+#endif /* CVC4_ASSERTIONS */
+}
+
+TEST_F(TestNodeWhiteNodeManager, topological_sort)
+{
+ TypeNode boolType = d_nodeManager->booleanType();
+ Node i = d_nodeManager->mkSkolem("i", boolType);
+ Node j = d_nodeManager->mkSkolem("j", boolType);
+ Node n1 = d_nodeManager->mkNode(kind::AND, j, j);
+ Node n2 = d_nodeManager->mkNode(kind::AND, i, n1);
+
+ {
+ std::vector<NodeValue*> roots = {n1.d_nv};
+ ASSERT_EQ(NodeManager::TopologicalSort(roots), roots);
+ }
+
+ {
+ std::vector<NodeValue*> roots = {n2.d_nv, n1.d_nv};
+ std::vector<NodeValue*> result = {n1.d_nv, n2.d_nv};
+ ASSERT_EQ(NodeManager::TopologicalSort(roots), result);
+ }
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \file node_traversal_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Alex Ozdemir, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of node traversal iterators.
+ **/
+
+#include <algorithm>
+#include <cstddef>
+#include <iterator>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/node_traversal.h"
+#include "expr/node_value.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackNodeTraversalPostorder : public TestNode
+{
+};
+
+class TestNodeBlackNodeTraversalPreorder : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, preincrement_iteration)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+ NodeDfsIterator i = traversal.begin();
+ NodeDfsIterator end = traversal.end();
+ ASSERT_EQ(*i, tb);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_EQ(*i, eb);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_EQ(*i, cnd);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postincrement_iteration)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ auto traversal = NodeDfsIterable(cnd, VisitOrder::POSTORDER);
+ NodeDfsIterator i = traversal.begin();
+ NodeDfsIterator end = traversal.end();
+ ASSERT_EQ(*(i++), tb);
+ ASSERT_EQ(*(i++), eb);
+ ASSERT_EQ(*(i++), cnd);
+ ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, postorder_is_default)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ auto traversal = NodeDfsIterable(cnd);
+ NodeDfsIterator i = traversal.begin();
+ NodeDfsIterator end = traversal.end();
+ ASSERT_EQ(*i, tb);
+ ASSERT_FALSE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, range_for_loop)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ size_t count = 0;
+ for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+ {
+ ++count;
+ }
+ ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, count_if_with_loop)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ size_t count = 0;
+ for (auto i : NodeDfsIterable(cnd, VisitOrder::POSTORDER))
+ {
+ if (i.isConst())
+ {
+ ++count;
+ }
+ }
+ ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_count_if)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+ auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+ size_t count = std::count_if(
+ traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+ ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, stl_copy)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+ std::vector<TNode> expected = {tb, eb, cnd, top};
+
+ auto traversal = NodeDfsIterable(top, VisitOrder::POSTORDER);
+
+ std::vector<TNode> actual;
+ std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+ ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_if)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+ std::vector<TNode> expected = {top};
+
+ auto traversal = NodeDfsIterable(
+ top, VisitOrder::POSTORDER, [&cnd](TNode n) { return n == cnd; });
+
+ std::vector<TNode> actual;
+ std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+ ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPostorder, skip_all)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+ std::vector<TNode> expected = {};
+
+ auto traversal =
+ NodeDfsIterable(top, VisitOrder::POSTORDER, [](TNode n) { return true; });
+
+ std::vector<TNode> actual;
+ std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+ ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, preincrement_iteration)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+ NodeDfsIterator i = traversal.begin();
+ NodeDfsIterator end = traversal.end();
+ ASSERT_EQ(*i, cnd);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_EQ(*i, tb);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_EQ(*i, eb);
+ ASSERT_FALSE(i == end);
+ ++i;
+ ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, postincrement_iteration)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ auto traversal = NodeDfsIterable(cnd, VisitOrder::PREORDER);
+ NodeDfsIterator i = traversal.begin();
+ NodeDfsIterator end = traversal.end();
+ ASSERT_EQ(*(i++), cnd);
+ ASSERT_EQ(*(i++), tb);
+ ASSERT_EQ(*(i++), eb);
+ ASSERT_TRUE(i == end);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, range_for_loop)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ size_t count = 0;
+ for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+ {
+ ++count;
+ }
+ ASSERT_EQ(count, 3);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, count_if_with_loop)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+
+ size_t count = 0;
+ for (auto i : NodeDfsIterable(cnd, VisitOrder::PREORDER))
+ {
+ if (i.isConst())
+ {
+ ++count;
+ }
+ }
+ ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_count_if)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+
+ auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+ size_t count = std::count_if(
+ traversal.begin(), traversal.end(), [](TNode n) { return n.isConst(); });
+ ASSERT_EQ(count, 2);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, stl_copy)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+ std::vector<TNode> expected = {top, cnd, tb, eb};
+
+ auto traversal = NodeDfsIterable(top, VisitOrder::PREORDER);
+
+ std::vector<TNode> actual;
+ std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+ ASSERT_EQ(actual, expected);
+}
+
+TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
+{
+ const Node tb = d_nodeManager->mkConst(true);
+ const Node eb = d_nodeManager->mkConst(false);
+ const Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
+ const Node top = d_nodeManager->mkNode(XOR, cnd, cnd);
+ std::vector<TNode> expected = {top, cnd, eb};
+
+ auto traversal = NodeDfsIterable(
+ top, VisitOrder::PREORDER, [&tb](TNode n) { return n == tb; });
+
+ std::vector<TNode> actual;
+ std::copy(traversal.begin(), traversal.end(), std::back_inserter(actual));
+ ASSERT_EQ(actual, expected);
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file node_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::Node.
+ **
+ ** White box testing of CVC4::Node.
+ **/
+
+#include <string>
+
+#include "base/check.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace expr;
+
+namespace test {
+
+class TestNodeWhiteNode : public TestNode
+{
+};
+
+TEST_F(TestNodeWhiteNode, null) { ASSERT_EQ(Node::null(), Node::s_null); }
+
+TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); }
+
+TEST_F(TestNodeWhiteNode, builder)
+{
+ NodeBuilder<> b;
+ ASSERT_TRUE(b.d_nv->getId() == 0);
+ ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND);
+ ASSERT_EQ(b.d_nv->d_nchildren, 0u);
+ /* etc. */
+}
+
+TEST_F(TestNodeWhiteNode, iterators)
+{
+ Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
+ Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
+ Node x_plus_y = d_nodeManager->mkNode(PLUS, x, y);
+ Node two = d_nodeManager->mkConst(Rational(2));
+ Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
+
+ Node n = d_nodeManager->mkNode(PLUS, x_times_2, x_plus_y, y);
+
+ Node::iterator i;
+
+ i = std::find(n.begin(), n.end(), x_plus_y);
+ ASSERT_TRUE(i != n.end());
+ ASSERT_TRUE(*i == x_plus_y);
+
+ i = std::find(n.begin(), n.end(), x);
+ ASSERT_TRUE(i == n.end());
+
+ i = std::find(x_times_2.begin(), x_times_2.end(), two);
+ ASSERT_TRUE(i != x_times_2.end());
+ ASSERT_TRUE(*i == two);
+
+ i = std::find(n.begin(), n.end(), y);
+ ASSERT_TRUE(i != n.end());
+ ASSERT_TRUE(*i == y);
+
+ std::vector<Node> v;
+ copy(n.begin(), n.end(), back_inserter(v));
+ ASSERT_EQ(n.getNumChildren(), v.size());
+ ASSERT_EQ(3, v.size());
+ ASSERT_EQ(v[0], x_times_2);
+ ASSERT_EQ(v[1], x_plus_y);
+ ASSERT_EQ(v[2], y);
+}
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file symbol_table_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters, Christopher L. Conway
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::SymbolTable
+ **
+ ** Black box testing of CVC4::SymbolTable.
+ **/
+
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "base/exception.h"
+#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/symbol_table.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeBlackSymbolTable : public TestApi
+{
+};
+
+TEST_F(TestNodeBlackSymbolTable, bind1)
+{
+ SymbolTable symtab;
+ api::Sort booleanType = d_solver.getBooleanSort();
+ api::Term x = d_solver.mkConst(booleanType);
+ symtab.bind("x", x);
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind2)
+{
+ SymbolTable symtab;
+ api::Sort booleanType = d_solver.getBooleanSort();
+ // var name attribute shouldn't matter
+ api::Term y = d_solver.mkConst(booleanType, "y");
+ symtab.bind("x", y);
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind3)
+{
+ SymbolTable symtab;
+ api::Sort booleanType = d_solver.getBooleanSort();
+ api::Term x = d_solver.mkConst(booleanType);
+ symtab.bind("x", x);
+ api::Term y = d_solver.mkConst(booleanType);
+ // new binding covers old
+ symtab.bind("x", y);
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), y);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind4)
+{
+ SymbolTable symtab;
+ api::Sort booleanType = d_solver.getBooleanSort();
+ api::Term x = d_solver.mkConst(booleanType);
+ symtab.bind("x", x);
+
+ api::Sort t = d_solver.mkUninterpretedSort("T");
+ // duplicate binding for type is OK
+ symtab.bindType("x", t);
+
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), x);
+ ASSERT_TRUE(symtab.isBoundType("x"));
+ ASSERT_EQ(symtab.lookupType("x"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type1)
+{
+ SymbolTable symtab;
+ api::Sort s = d_solver.mkUninterpretedSort("S");
+ symtab.bindType("S", s);
+ ASSERT_TRUE(symtab.isBoundType("S"));
+ ASSERT_EQ(symtab.lookupType("S"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type2)
+{
+ SymbolTable symtab;
+ // type name attribute shouldn't matter
+ api::Sort s = d_solver.mkUninterpretedSort("S");
+ symtab.bindType("T", s);
+ ASSERT_TRUE(symtab.isBoundType("T"));
+ ASSERT_EQ(symtab.lookupType("T"), s);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bind_type3)
+{
+ SymbolTable symtab;
+ api::Sort s = d_solver.mkUninterpretedSort("S");
+ symtab.bindType("S", s);
+ api::Sort t = d_solver.mkUninterpretedSort("T");
+ // new binding covers old
+ symtab.bindType("S", t);
+ ASSERT_TRUE(symtab.isBoundType("S"));
+ ASSERT_EQ(symtab.lookupType("S"), t);
+}
+
+TEST_F(TestNodeBlackSymbolTable, push_scope)
+{
+ SymbolTable symtab;
+ api::Sort booleanType = d_solver.getBooleanSort();
+ api::Term x = d_solver.mkConst(booleanType);
+ symtab.bind("x", x);
+ symtab.pushScope();
+
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), x);
+
+ api::Term y = d_solver.mkConst(booleanType);
+ symtab.bind("x", y);
+
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), y);
+
+ symtab.popScope();
+ ASSERT_TRUE(symtab.isBound("x"));
+ ASSERT_EQ(symtab.lookup("x"), x);
+}
+
+TEST_F(TestNodeBlackSymbolTable, bad_pop)
+{
+ SymbolTable symtab;
+ ASSERT_THROW(symtab.popScope(), ScopeException);
+}
+
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file type_cardinality_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Public box testing of Type::getCardinality() for various Types
+ **
+ ** Public box testing of Type::getCardinality() for various Types.
+ **/
+
+#include <string>
+
+#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "test_node.h"
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestNodeBlackTypeCardinality : public TestNode
+{
+};
+
+TEST_F(TestNodeBlackTypeCardinality, basics)
+{
+ ASSERT_EQ(d_nodeManager->booleanType().getCardinality().compare(2),
+ Cardinality::EQUAL);
+ ASSERT_EQ(d_nodeManager->integerType().getCardinality().compare(
+ Cardinality::INTEGERS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(
+ d_nodeManager->realType().getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, arrays)
+{
+ TypeNode intToInt = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+ d_nodeManager->integerType());
+ TypeNode realToReal = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+ d_nodeManager->realType());
+ TypeNode realToInt = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+ d_nodeManager->integerType());
+ TypeNode intToReal = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+ d_nodeManager->realType());
+ TypeNode intToBool = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+ d_nodeManager->booleanType());
+ TypeNode realToBool = d_nodeManager->mkArrayType(
+ d_nodeManager->realType(), d_nodeManager->booleanType());
+ TypeNode boolToReal = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+ d_nodeManager->realType());
+ TypeNode boolToInt = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+ d_nodeManager->integerType());
+ TypeNode boolToBool = d_nodeManager->mkArrayType(
+ d_nodeManager->booleanType(), d_nodeManager->booleanType());
+
+ ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, unary_functions)
+{
+ TypeNode intToInt = d_nodeManager->mkFunctionType(
+ d_nodeManager->integerType(), d_nodeManager->integerType());
+ TypeNode realToReal = d_nodeManager->mkFunctionType(
+ d_nodeManager->realType(), d_nodeManager->realType());
+ TypeNode realToInt = d_nodeManager->mkFunctionType(
+ d_nodeManager->realType(), d_nodeManager->integerType());
+ TypeNode intToReal = d_nodeManager->mkFunctionType(
+ d_nodeManager->integerType(), d_nodeManager->realType());
+ TypeNode intToBool = d_nodeManager->mkFunctionType(
+ d_nodeManager->integerType(), d_nodeManager->booleanType());
+ TypeNode realToBool = d_nodeManager->mkFunctionType(
+ d_nodeManager->realType(), d_nodeManager->booleanType());
+ TypeNode boolToReal = d_nodeManager->mkFunctionType(
+ d_nodeManager->booleanType(), d_nodeManager->realType());
+ TypeNode boolToInt = d_nodeManager->mkFunctionType(
+ d_nodeManager->booleanType(), d_nodeManager->integerType());
+ TypeNode boolToBool = d_nodeManager->mkFunctionType(
+ d_nodeManager->booleanType(), d_nodeManager->booleanType());
+
+ ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, binary_functions)
+{
+ std::vector<TypeNode> boolbool;
+ boolbool.push_back(d_nodeManager->booleanType());
+ boolbool.push_back(d_nodeManager->booleanType());
+ std::vector<TypeNode> boolint;
+ boolint.push_back(d_nodeManager->booleanType());
+ boolint.push_back(d_nodeManager->integerType());
+ std::vector<TypeNode> intbool;
+ intbool.push_back(d_nodeManager->integerType());
+ intbool.push_back(d_nodeManager->booleanType());
+ std::vector<TypeNode> intint;
+ intint.push_back(d_nodeManager->integerType());
+ intint.push_back(d_nodeManager->integerType());
+ std::vector<TypeNode> intreal;
+ intreal.push_back(d_nodeManager->integerType());
+ intreal.push_back(d_nodeManager->realType());
+ std::vector<TypeNode> realint;
+ realint.push_back(d_nodeManager->realType());
+ realint.push_back(d_nodeManager->integerType());
+ std::vector<TypeNode> realreal;
+ realreal.push_back(d_nodeManager->realType());
+ realreal.push_back(d_nodeManager->realType());
+ std::vector<TypeNode> realbool;
+ realbool.push_back(d_nodeManager->realType());
+ realbool.push_back(d_nodeManager->booleanType());
+ std::vector<TypeNode> boolreal;
+ boolreal.push_back(d_nodeManager->booleanType());
+ boolreal.push_back(d_nodeManager->realType());
+
+ TypeNode boolboolToBool =
+ d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType());
+ TypeNode boolboolToInt =
+ d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType());
+ TypeNode boolboolToReal =
+ d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType());
+
+ TypeNode boolintToBool =
+ d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType());
+ TypeNode boolintToInt =
+ d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType());
+ TypeNode boolintToReal =
+ d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType());
+
+ TypeNode intboolToBool =
+ d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType());
+ TypeNode intboolToInt =
+ d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType());
+ TypeNode intboolToReal =
+ d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType());
+
+ TypeNode intintToBool =
+ d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType());
+ TypeNode intintToInt =
+ d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType());
+ TypeNode intintToReal =
+ d_nodeManager->mkFunctionType(intint, d_nodeManager->realType());
+
+ TypeNode intrealToBool =
+ d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType());
+ TypeNode intrealToInt =
+ d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType());
+ TypeNode intrealToReal =
+ d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType());
+
+ TypeNode realintToBool =
+ d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType());
+ TypeNode realintToInt =
+ d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType());
+ TypeNode realintToReal =
+ d_nodeManager->mkFunctionType(realint, d_nodeManager->realType());
+
+ TypeNode realrealToBool =
+ d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType());
+ TypeNode realrealToInt =
+ d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType());
+ TypeNode realrealToReal =
+ d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType());
+
+ TypeNode realboolToBool =
+ d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType());
+ TypeNode realboolToInt =
+ d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType());
+ TypeNode realboolToReal =
+ d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType());
+
+ TypeNode boolrealToBool =
+ d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType());
+ TypeNode boolrealToInt =
+ d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType());
+ TypeNode boolrealToReal =
+ d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType());
+
+ ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL);
+ ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+
+ ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+
+ ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+
+ ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+ ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::EQUAL);
+
+ ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+
+ ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+
+ ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+
+ ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+
+ ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+ ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS),
+ Cardinality::GREATER);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, ternary_functions)
+{
+ std::vector<TypeNode> boolbool;
+ boolbool.push_back(d_nodeManager->booleanType());
+ boolbool.push_back(d_nodeManager->booleanType());
+ std::vector<TypeNode> boolboolbool = boolbool;
+ boolboolbool.push_back(d_nodeManager->booleanType());
+
+ TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool);
+ TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool);
+
+ TypeNode boolboolboolToBool =
+ d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType());
+ TypeNode boolboolToBoolbool =
+ d_nodeManager->mkFunctionType(boolbool, boolboolTuple);
+ TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType(
+ d_nodeManager->booleanType(), boolboolboolTuple);
+
+ ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8),
+ Cardinality::EQUAL);
+ ASSERT_EQ(
+ boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4),
+ Cardinality::EQUAL);
+ ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8),
+ Cardinality::EQUAL);
+}
+
+TEST_F(TestNodeBlackTypeCardinality, undefined_sorts)
+{
+ TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE);
+ // We've currently assigned them a specific Beth number, which
+ // isn't really correct, but...
+ ASSERT_FALSE(foo.getCardinality().isFinite());
+}
+
+TEST_F(TestNodeBlackTypeCardinality, bitvectors)
+{
+ ASSERT_EQ(d_nodeManager->mkBitVectorType(0).getCardinality().compare(0),
+ Cardinality::EQUAL);
+ Cardinality lastCard = 0;
+ for (unsigned i = 1; i <= 65; ++i)
+ {
+ Cardinality card = Cardinality(2) ^ i;
+ Cardinality typeCard = d_nodeManager->mkBitVectorType(i).getCardinality();
+ ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER
+ || (typeCard.isLargeFinite() && lastCard.isLargeFinite()));
+ ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL
+ || typeCard.isLargeFinite());
+ lastCard = typeCard;
+ }
+}
+
+} // namespace test
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file type_node_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief White box testing of TypeNode
+ **
+ ** White box testing of TypeNode.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+#include "smt/smt_engine.h"
+#include "test_node.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace test {
+
+class TestNodeWhiteTypeNode : public TestNode
+{
+ protected:
+ void SetUp() override
+ {
+ TestNode::SetUp();
+ d_smt.reset(new SmtEngine(d_nodeManager.get()));
+ }
+ std::unique_ptr<SmtEngine> d_smt;
+};
+
+TEST_F(TestNodeWhiteTypeNode, sub_types)
+{
+ TypeNode realType = d_nodeManager->realType();
+ TypeNode integerType = d_nodeManager->realType();
+ TypeNode booleanType = d_nodeManager->booleanType();
+ TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType);
+ TypeNode bvType = d_nodeManager->mkBitVectorType(32);
+
+ Node x = d_nodeManager->mkBoundVar("x", realType);
+ Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
+ TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
+ Node lambda = d_nodeManager->mkVar("lambda", funtype);
+ std::vector<Node> formals;
+ formals.push_back(x);
+ d_smt->defineFunction(lambda, formals, xPos);
+
+ ASSERT_FALSE(realType.isComparableTo(booleanType));
+ ASSERT_TRUE(realType.isComparableTo(integerType));
+ ASSERT_TRUE(realType.isComparableTo(realType));
+ ASSERT_FALSE(realType.isComparableTo(arrayType));
+ ASSERT_FALSE(realType.isComparableTo(bvType));
+
+ ASSERT_FALSE(booleanType.isComparableTo(integerType));
+ ASSERT_FALSE(booleanType.isComparableTo(realType));
+ ASSERT_TRUE(booleanType.isComparableTo(booleanType));
+ ASSERT_FALSE(booleanType.isComparableTo(arrayType));
+ ASSERT_FALSE(booleanType.isComparableTo(bvType));
+
+ ASSERT_TRUE(integerType.isComparableTo(realType));
+ ASSERT_TRUE(integerType.isComparableTo(integerType));
+ ASSERT_FALSE(integerType.isComparableTo(booleanType));
+ ASSERT_FALSE(integerType.isComparableTo(arrayType));
+ ASSERT_FALSE(integerType.isComparableTo(bvType));
+
+ ASSERT_FALSE(arrayType.isComparableTo(booleanType));
+ ASSERT_FALSE(arrayType.isComparableTo(integerType));
+ ASSERT_FALSE(arrayType.isComparableTo(realType));
+ ASSERT_TRUE(arrayType.isComparableTo(arrayType));
+ ASSERT_FALSE(arrayType.isComparableTo(bvType));
+
+ ASSERT_FALSE(bvType.isComparableTo(booleanType));
+ ASSERT_FALSE(bvType.isComparableTo(integerType));
+ ASSERT_FALSE(bvType.isComparableTo(realType));
+ ASSERT_FALSE(bvType.isComparableTo(arrayType));
+ ASSERT_TRUE(bvType.isComparableTo(bvType));
+
+ ASSERT_TRUE(realType.getBaseType() == realType);
+ ASSERT_TRUE(integerType.getBaseType() == realType);
+ ASSERT_TRUE(booleanType.getBaseType() == booleanType);
+ ASSERT_TRUE(arrayType.getBaseType() == arrayType);
+ ASSERT_TRUE(bvType.getBaseType() == bvType);
+}
+} // namespace test
+} // namespace CVC4
projects / cvc5.git / commitdiff