From: Aina Niemetz Date: Wed, 9 Dec 2020 19:14:01 +0000 (-0800) Subject: google test: expr: Migrate attribute_white. (#5632) X-Git-Tag: cvc5-1.0.0~2466 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24ad9f014107b792fae8239174dc476971a6e334;p=cvc5.git google test: expr: Migrate attribute_white. (#5632) --- diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index 35710379b..1b619b2f2 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -12,7 +12,7 @@ # Add unit tests cvc4_add_unit_test_black(attribute_black expr) -cvc4_add_cxx_unit_test_white(attribute_white expr) +cvc4_add_unit_test_white(attribute_white expr) cvc4_add_cxx_unit_test_black(kind_black expr) cvc4_add_cxx_unit_test_black(kind_map_black expr) cvc4_add_cxx_unit_test_black(node_black expr) diff --git a/test/unit/expr/attribute_black.cpp b/test/unit/expr/attribute_black.cpp index 0d0fee4ea..cd2745a07 100644 --- a/test/unit/expr/attribute_black.cpp +++ b/test/unit/expr/attribute_black.cpp @@ -30,7 +30,7 @@ using namespace smt; namespace test { -class TextExprBlackAttributeBlack : public TestExprBlack +class TestExprBlackAttribute : public TestExprBlack { protected: struct PrimitiveIntAttributeId @@ -52,7 +52,7 @@ class TextExprBlackAttributeBlack : public TestExprBlack using BoolAttribute = expr::Attribute; }; -TEST_F(TextExprBlackAttributeBlack, ints) +TEST_F(TestExprBlackAttribute, ints) { TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -69,7 +69,7 @@ TEST_F(TextExprBlackAttributeBlack, ints) delete node; } -TEST_F(TextExprBlackAttributeBlack, tnodes) +TEST_F(TestExprBlackAttribute, tnodes) { TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -87,7 +87,7 @@ TEST_F(TextExprBlackAttributeBlack, tnodes) delete node; } -TEST_F(TextExprBlackAttributeBlack, strings) +TEST_F(TestExprBlackAttribute, strings) { TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); @@ -105,7 +105,7 @@ TEST_F(TextExprBlackAttributeBlack, strings) delete node; } -TEST_F(TextExprBlackAttributeBlack, bools) +TEST_F(TestExprBlackAttribute, bools) { TypeNode booleanType = d_nodeManager->booleanType(); Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); diff --git a/test/unit/expr/attribute_white.cpp b/test/unit/expr/attribute_white.cpp new file mode 100644 index 000000000..1403fbe21 --- /dev/null +++ b/test/unit/expr/attribute_white.cpp @@ -0,0 +1,448 @@ +/********************* */ +/*! \file attribute_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief White box testing of Node attributes. + ** + ** White box testing of Node attributes. + **/ + +#include + +#include "base/check.h" +#include "expr/attribute.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node_manager_attributes.h" +#include "expr/node_value.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "test_expr.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" + +namespace CVC4 { + +using namespace kind; +using namespace smt; +using namespace expr; +using namespace expr::attr; + +namespace test { + +struct Test1; +struct Test2; +struct Test3; +struct Test4; +struct Test5; + +typedef Attribute TestStringAttr1; +typedef Attribute TestStringAttr2; + +using TestFlag1 = Attribute; +using TestFlag2 = Attribute; +using TestFlag3 = Attribute; +using TestFlag4 = Attribute; +using TestFlag5 = Attribute; + +class TestExprWhiteAttribute : public TestExprWhite +{ + protected: + void SetUp() override + { + TestExprWhite::SetUp(); + d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); + } + std::unique_ptr d_booleanType; +}; + +TEST_F(TestExprWhiteAttribute, attribute_ids) +{ + // Test that IDs for (a subset of) attributes in the system are + // unique and that the LastAttributeId (which would be the next ID + // to assign) is greater than all attribute IDs. + + // We used to check ID assignments explicitly. However, between + // compilation modules, you don't get a strong guarantee + // (initialization order is somewhat implementation-specific, and + // anyway you'd have to change the tests anytime you add an + // attribute). So we back off, and just test that they're unique + // and that the next ID to be assigned is strictly greater than + // those that have already been assigned. + + unsigned lastId = attr::LastAttributeId::getId(); + EXPECT_LT(VarNameAttr::s_id, lastId); + EXPECT_LT(TestStringAttr1::s_id, lastId); + EXPECT_LT(TestStringAttr2::s_id, lastId); + + EXPECT_NE(VarNameAttr::s_id, TestStringAttr1::s_id); + EXPECT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); + EXPECT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); + + lastId = attr::LastAttributeId::getId(); + EXPECT_LT(TestFlag1::s_id, lastId); + EXPECT_LT(TestFlag2::s_id, lastId); + EXPECT_LT(TestFlag3::s_id, lastId); + EXPECT_LT(TestFlag4::s_id, lastId); + EXPECT_LT(TestFlag5::s_id, lastId); + EXPECT_NE(TestFlag1::s_id, TestFlag2::s_id); + EXPECT_NE(TestFlag1::s_id, TestFlag3::s_id); + EXPECT_NE(TestFlag1::s_id, TestFlag4::s_id); + EXPECT_NE(TestFlag1::s_id, TestFlag5::s_id); + EXPECT_NE(TestFlag2::s_id, TestFlag3::s_id); + EXPECT_NE(TestFlag2::s_id, TestFlag4::s_id); + EXPECT_NE(TestFlag2::s_id, TestFlag5::s_id); + EXPECT_NE(TestFlag3::s_id, TestFlag4::s_id); + EXPECT_NE(TestFlag3::s_id, TestFlag5::s_id); + EXPECT_NE(TestFlag4::s_id, TestFlag5::s_id); + + lastId = attr::LastAttributeId::getId(); + EXPECT_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); + + EXPECT_EQ(a.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(a.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(a.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); + EXPECT_EQ(b.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(b.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(b.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(c.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); + EXPECT_EQ(c.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(c.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + EXPECT_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"); + + EXPECT_EQ(a.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(a.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(a.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); + EXPECT_EQ(b.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(b.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(b.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(c.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); + EXPECT_EQ(c.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(c.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + EXPECT_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"); + + EXPECT_EQ(c.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(c.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(c.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(c.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(a.getAttribute(VarNameAttr()), "a"); + EXPECT_EQ(a.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(a.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(a.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(b.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(b.getAttribute(VarNameAttr()), "b"); + EXPECT_EQ(b.getAttribute(VarNameAttr()), "c"); + EXPECT_NE(b.getAttribute(VarNameAttr()), ""); + + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b"); + EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c"); + EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), ""); + + ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h deleted file mode 100644 index de1795264..000000000 --- a/test/unit/expr/attribute_white.h +++ /dev/null @@ -1,478 +0,0 @@ -/********************* */ -/*! \file attribute_white.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief White box testing of Node attributes. - ** - ** White box testing of Node attributes. - **/ - -#include - -#include - -#include "base/check.h" -#include "expr/attribute.h" -#include "expr/node.h" -#include "expr/node_builder.h" -#include "expr/node_manager.h" -#include "expr/node_manager_attributes.h" -#include "expr/node_value.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::smt; -using namespace CVC4::expr; -using namespace CVC4::expr::attr; -using namespace std; - -struct Test1; -struct Test2; -struct Test3; -struct Test4; -struct Test5; - -typedef Attribute TestStringAttr1; -typedef Attribute TestStringAttr2; - -typedef Attribute TestFlag1; -typedef Attribute TestFlag2; -typedef Attribute TestFlag3; -typedef Attribute TestFlag4; -typedef Attribute TestFlag5; - -class AttributeWhite : public CxxTest::TestSuite { - - ExprManager* d_em; - NodeManager* d_nm; - SmtScope* d_scope; - TypeNode* d_booleanType; - SmtEngine* d_smtEngine; - - public: - void setUp() override - { - d_em = new ExprManager(); - d_nm = NodeManager::fromExprManager(d_em); - d_smtEngine = new SmtEngine(d_nm); - d_scope = new SmtScope(d_smtEngine); - d_booleanType = new TypeNode(d_nm->booleanType()); - } - - void tearDown() override - { - delete d_booleanType; - delete d_scope; - delete d_smtEngine; - delete d_em; - } - - void testAttributeIds() { - // Test that IDs for (a subset of) attributes in the system are - // unique and that the LastAttributeId (which would be the next ID - // to assign) is greater than all attribute IDs. - - // We used to check ID assignments explicitly. However, between - // compilation modules, you don't get a strong guarantee - // (initialization order is somewhat implementation-specific, and - // anyway you'd have to change the tests anytime you add an - // attribute). So we back off, and just test that they're unique - // and that the next ID to be assigned is strictly greater than - // those that have already been assigned. - - unsigned lastId = attr::LastAttributeId::getId(); - TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId); - TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId); - TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId); - - TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr1::s_id); - TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); - TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); - - //lastId = attr::LastAttributeId::getId(); - //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); - - lastId = attr::LastAttributeId::getId(); - TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); - TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); - TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); - TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId); - TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId); - TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id); - TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id); - TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id); - TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag5::s_id); - TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag3::s_id); - TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag4::s_id); - TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag5::s_id); - TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag4::s_id); - TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id); - TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); - - lastId = attr::LastAttributeId::getId(); - - lastId = attr::LastAttributeId::getId(); -// TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId); -// TS_ASSERT_LESS_THAN(theory::PostRewriteCache::s_id, lastId); -// TS_ASSERT_LESS_THAN(theory::PreRewriteCacheTop::s_id, lastId); -// TS_ASSERT_LESS_THAN(theory::PostRewriteCacheTop::s_id, lastId); -// TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCache::s_id); -// TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PreRewriteCacheTop::s_id); -// TS_ASSERT_DIFFERS(theory::PreRewriteCache::s_id, theory::PostRewriteCacheTop::s_id); -// TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PreRewriteCacheTop::s_id); -// TS_ASSERT_DIFFERS(theory::PostRewriteCache::s_id, theory::PostRewriteCacheTop::s_id); -// TS_ASSERT_DIFFERS(theory::PreRewriteCacheTop::s_id, theory::PostRewriteCacheTop::s_id); - - lastId = attr::LastAttributeId::getId(); - TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId); - } - - void testAttributes() { - //Debug.on("boolattr"); - - Node a = d_nm->mkVar(*d_booleanType); - Node b = d_nm->mkVar(*d_booleanType); - Node c = d_nm->mkVar(*d_booleanType); - Node unnamed = d_nm->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"; - TS_ASSERT(! a.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag1())); - - Debug("boolattr") << "get flag 2 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - - Debug("boolattr") << "get flag 3 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag3())); - - Debug("boolattr") << "get flag 4 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag4())); - - Debug("boolattr") << "get flag 5 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag5())); - - // test that they all HAVE the boolean attributes - TS_ASSERT(a.hasAttribute(TestFlag1())); - TS_ASSERT(b.hasAttribute(TestFlag1())); - TS_ASSERT(c.hasAttribute(TestFlag1())); - TS_ASSERT(unnamed.hasAttribute(TestFlag1())); - - TS_ASSERT(a.hasAttribute(TestFlag2())); - TS_ASSERT(b.hasAttribute(TestFlag2())); - TS_ASSERT(c.hasAttribute(TestFlag2())); - TS_ASSERT(unnamed.hasAttribute(TestFlag2())); - - TS_ASSERT(a.hasAttribute(TestFlag3())); - TS_ASSERT(b.hasAttribute(TestFlag3())); - TS_ASSERT(c.hasAttribute(TestFlag3())); - TS_ASSERT(unnamed.hasAttribute(TestFlag3())); - - TS_ASSERT(a.hasAttribute(TestFlag4())); - TS_ASSERT(b.hasAttribute(TestFlag4())); - TS_ASSERT(c.hasAttribute(TestFlag4())); - TS_ASSERT(unnamed.hasAttribute(TestFlag4())); - - TS_ASSERT(a.hasAttribute(TestFlag5())); - TS_ASSERT(b.hasAttribute(TestFlag5())); - TS_ASSERT(c.hasAttribute(TestFlag5())); - TS_ASSERT(unnamed.hasAttribute(TestFlag5())); - - // test two-arg version of hasAttribute() - bool bb = false; - Debug("boolattr") << "get flag 1 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr") << "get flag 2 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 2 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 2 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr") << "get flag 3 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 3 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 3 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr") << "get flag 4 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 4 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 4 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr") << "get flag 5 on a (should be F)\n"; - TS_ASSERT(a.getAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 5 on b (should be F)\n"; - TS_ASSERT(b.getAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 5 on c (should be F)\n"; - TS_ASSERT(c.getAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag5(), bb)); - TS_ASSERT(! 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); - - TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr1())); - TS_ASSERT(! b.hasAttribute(TestStringAttr1())); - TS_ASSERT(! c.hasAttribute(TestStringAttr1())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr2())); - TS_ASSERT(! b.hasAttribute(TestStringAttr2())); - TS_ASSERT(! c.hasAttribute(TestStringAttr2())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); - - Debug("boolattr") << "get flag 1 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on b (should be F)\n"; - TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr") << "get flag 1 on unnamed (should be T)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag1())); - - Debug("boolattr") << "get flag 2 on a (should be F)\n"; - TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on c (should be T)\n"; - TS_ASSERT(c.getAttribute(TestFlag2())); - Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; - TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - - Debug("boolattr") << "get flag 3 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on c (should be T)\n"; - TS_ASSERT(c.getAttribute(TestFlag3())); - Debug("boolattr") << "get flag 3 on unnamed (should be T)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag3())); - - Debug("boolattr") << "get flag 4 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on c (should be T)\n"; - TS_ASSERT(c.getAttribute(TestFlag4())); - Debug("boolattr") << "get flag 4 on unnamed (should be T)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag4())); - - Debug("boolattr") << "get flag 5 on a (should be T)\n"; - TS_ASSERT(a.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on b (should be T)\n"; - TS_ASSERT(b.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on c (should be F)\n"; - TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr") << "get flag 5 on unnamed (should be T)\n"; - TS_ASSERT(unnamed.getAttribute(TestFlag5())); - - a.setAttribute(TestStringAttr1(), "foo"); - b.setAttribute(TestStringAttr1(), "bar"); - c.setAttribute(TestStringAttr1(), "baz"); - - TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - - TS_ASSERT(a.hasAttribute(TestStringAttr1())); - TS_ASSERT(b.hasAttribute(TestStringAttr1())); - TS_ASSERT(c.hasAttribute(TestStringAttr1())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr2())); - TS_ASSERT(! b.hasAttribute(TestStringAttr2())); - TS_ASSERT(! c.hasAttribute(TestStringAttr2())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); - - a.setAttribute(VarNameAttr(), "b"); - b.setAttribute(VarNameAttr(), "c"); - c.setAttribute(VarNameAttr(), "a"); - - TS_ASSERT(c.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(a.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - } -}; diff --git a/test/unit/test_expr.h b/test/unit/test_expr.h index 7bcef5e0a..a6757a506 100644 --- a/test/unit/test_expr.h +++ b/test/unit/test_expr.h @@ -41,6 +41,18 @@ class TestExprBlack : public TestApi SmtEngine* d_smtEngine; }; +class TestExprWhite : public TestApi +{ + protected: + void SetUp() override + { + d_nodeManager.reset(new NodeManager(nullptr)); + d_scope.reset(new NodeManagerScope(d_nodeManager.get())); + } + std::unique_ptr d_nodeManager; + std::unique_ptr d_scope; +}; + } // namespace test } // namespace CVC4 #endif