# 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)
namespace test {
-class TextExprBlackAttributeBlack : public TestExprBlack
+class TestExprBlackAttribute : public TestExprBlack
{
protected:
struct PrimitiveIntAttributeId
using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
};
-TEST_F(TextExprBlackAttributeBlack, ints)
+TEST_F(TestExprBlackAttribute, ints)
{
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
delete node;
}
-TEST_F(TextExprBlackAttributeBlack, tnodes)
+TEST_F(TestExprBlackAttribute, tnodes)
{
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
delete node;
}
-TEST_F(TextExprBlackAttributeBlack, strings)
+TEST_F(TestExprBlackAttribute, strings)
{
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
delete node;
}
-TEST_F(TextExprBlackAttributeBlack, bools)
+TEST_F(TestExprBlackAttribute, bools)
{
TypeNode booleanType = d_nodeManager->booleanType();
Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
--- /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-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 <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_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<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 TestExprWhite
+{
+ protected:
+ void SetUp() override
+ {
+ TestExprWhite::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();
+ 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<bool, false>::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<TypeNode, false>::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
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#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 "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<Test1, std::string> TestStringAttr1;
-typedef Attribute<Test2, std::string> TestStringAttr2;
-
-typedef Attribute<Test1, bool> TestFlag1;
-typedef Attribute<Test2, bool> TestFlag2;
-typedef Attribute<Test3, bool> TestFlag3;
-typedef Attribute<Test4, bool> TestFlag4;
-typedef Attribute<Test5, bool> 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<string, false>::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<void*, false>::getId();
- //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
-
- lastId = attr::LastAttributeId<bool, false>::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<bool, true>::getId();
-
- lastId = attr::LastAttributeId<Node, false>::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<TypeNode, false>::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()));
- }
-};
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<NodeManager> d_nodeManager;
+ std::unique_ptr<NodeManagerScope> d_scope;
+};
+
} // namespace test
} // namespace CVC4
#endif
projects / cvc5.git / commitdiff