diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/Makefile.am | 1 | ||||
| -rw-r--r-- | test/unit/expr/attribute_black.h | 2 | ||||
| -rw-r--r-- | test/unit/expr/attribute_white.h | 565 | ||||
| -rw-r--r-- | test/unit/expr/node_black.h | 131 | ||||
| -rw-r--r-- | test/unit/expr/node_white.h | 513 | ||||
| -rw-r--r-- | test/unit/parser/parser_black.h | 7 |
6 files changed, 640 insertions, 579 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 305731f5b..f78171dac 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/attribute_white \ expr/attribute_black \ parser/parser_black \ context/context_black \ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index b5e897e89..12ecd347a 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -62,7 +62,7 @@ public: struct MyDataAttributeId {}; struct MyDataCleanupFunction { - static void cleanup(MyData*& myData){ + static void cleanup(MyData* myData){ delete myData; } }; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h new file mode 100644 index 000000000..7a0e538f6 --- /dev/null +++ b/test/unit/expr/attribute_white.h @@ -0,0 +1,565 @@ +/********************* */ +/** attribute_white.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** White box testing of Node attributes. + **/ + +#include <cxxtest/TestSuite.h> + +#include <string> + +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node.h" +#include "expr/attribute.h" +#include "context/context.h" +#include "util/Assert.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +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; + +// it would be nice to have CDAttribute<> for context-dependence +typedef CDAttribute<Test1, bool> TestCDFlag; + +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; + +typedef CDAttribute<Test1, bool> TestFlag1cd; +typedef CDAttribute<Test2, bool> TestFlag2cd; + +class AttributeWhite : public CxxTest::TestSuite { + + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_scope; + delete d_nm; + delete d_ctxt; + } + + void testAttributeIds() { + TS_ASSERT(VarNameAttr::s_id == 0); + TS_ASSERT(TestStringAttr1::s_id == 1); + TS_ASSERT(TestStringAttr2::s_id == 2); + TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3)); + + TS_ASSERT(TypeAttr::s_id == 0); + TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1)); + + TS_ASSERT(TestFlag1::s_id == 0); + TS_ASSERT(TestFlag2::s_id == 1); + TS_ASSERT(TestFlag3::s_id == 2); + TS_ASSERT(TestFlag4::s_id == 3); + TS_ASSERT(TestFlag5::s_id == 4); + TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5)); + + TS_ASSERT(TestFlag1cd::s_id == 0); + TS_ASSERT(TestFlag2cd::s_id == 1); + TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2)); + } + + void testCDAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 1 + + // test that all boolean flags are FALSE to start + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + // test that they all HAVE the boolean attributes + TS_ASSERT(a.hasAttribute(TestFlag1cd())); + TS_ASSERT(b.hasAttribute(TestFlag1cd())); + TS_ASSERT(c.hasAttribute(TestFlag1cd())); + + // test two-arg version of hasAttribute() + bool bb; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + + // setting boolean flags + Debug("boolattr", "set flag 1 on a to T\n"); + a.setAttribute(TestFlag1cd(), true); + Debug("boolattr", "set flag 1 on b to F\n"); + b.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on c to F\n"); + c.setAttribute(TestFlag1cd(), false); + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on a to F\n"); + a.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on b to T\n"); + b.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 3 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on c to T\n"); + c.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 1 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 0 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ + } + + void testAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node unnamed = d_nm->mkVar(); + + 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; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 2 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 3 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 4 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 5 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(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/expr/node_black.h b/test/unit/expr/node_black.h index c1ece1145..21c19a8f9 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -72,7 +72,7 @@ public: TS_ASSERT(b.isNull()); Node c = b; - + TS_ASSERT(c.isNull()); } @@ -93,7 +93,7 @@ public: /*tests: bool operator==(const Node& e) const */ void testOperatorEquals() { Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -113,7 +113,7 @@ public: TS_ASSERT(c==a); TS_ASSERT(c==b); - TS_ASSERT(c==c); + TS_ASSERT(c==c); TS_ASSERT(d==d); @@ -133,7 +133,7 @@ public: Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -142,19 +142,19 @@ public: Node d = d_nodeManager->mkVar(); /*structed assuming operator == works */ - TS_ASSERT(iff(a!=a,!(a==a))); - TS_ASSERT(iff(a!=b,!(a==b))); - TS_ASSERT(iff(a!=c,!(a==c))); + TS_ASSERT(iff(a!=a, !(a==a))); + TS_ASSERT(iff(a!=b, !(a==b))); + TS_ASSERT(iff(a!=c, !(a==c))); - TS_ASSERT(iff(b!=a,!(b==a))); - TS_ASSERT(iff(b!=b,!(b==b))); - TS_ASSERT(iff(b!=c,!(b==c))); + TS_ASSERT(iff(b!=a, !(b==a))); + TS_ASSERT(iff(b!=b, !(b==b))); + TS_ASSERT(iff(b!=c, !(b==c))); - TS_ASSERT(iff(c!=a,!(c==a))); - TS_ASSERT(iff(c!=b,!(c==b))); - TS_ASSERT(iff(c!=c,!(c==c))); + TS_ASSERT(iff(c!=a, !(c==a))); + TS_ASSERT(iff(c!=b, !(c==b))); + TS_ASSERT(iff(c!=c, !(c==c))); TS_ASSERT(!(d!=d)); @@ -164,7 +164,7 @@ public: } - void testOperatorSquare() { + void testOperatorSquare() { /*Node operator[](int i) const */ #ifdef CVC4_ASSERTIONS @@ -177,7 +177,7 @@ public: Node tb = d_nodeManager->mkNode(TRUE); Node eb = d_nodeManager->mkNode(FALSE); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - Node ite = cnd.iteNode(tb,eb); + Node ite = cnd.iteNode(tb, eb); TS_ASSERT(tb == cnd[0]); TS_ASSERT(eb == cnd[1]); @@ -188,8 +188,8 @@ public: #ifdef CVC4_ASSERTIONS //Bounds check on a node with children - TS_ASSERT_THROWS(ite == ite[-1],AssertionException); - TS_ASSERT_THROWS(ite == ite[4],AssertionException); + TS_ASSERT_THROWS(ite == ite[-1], AssertionException); + TS_ASSERT_THROWS(ite == ite[4], AssertionException); #endif /* CVC4_ASSERTIONS */ } @@ -197,23 +197,23 @@ public: void testOperatorAssign() { Node a, b; Node c = d_nodeManager->mkNode(NOT); - + b = c; TS_ASSERT(b==c); - + a = b = c; TS_ASSERT(a==b); TS_ASSERT(a==c); } - + void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation - * in the black box tests. + * in the black box tests. */ - + Node a = d_nodeManager->mkVar(); Node b = d_nodeManager->mkVar(); @@ -225,14 +225,14 @@ public: TS_ASSERT(!(c<d)); TS_ASSERT(!(d<c)); - + /* TODO: * Less than has the rather difficult to test property that subexpressions * are less than enclosing expressions. * * But what would be a convincing test of this property? */ - + //Simple test of descending descendant property Node child = d_nodeManager->mkNode(TRUE); Node parent = d_nodeManager->mkNode(NOT, child); @@ -245,9 +245,9 @@ public: Node curr = d_nodeManager->mkNode(NULL_EXPR); for(int i=0;i<N;i++) { chain.push_back(curr); - curr = d_nodeManager->mkNode(AND,curr); + curr = d_nodeManager->mkNode(AND, curr); } - + for(int i=0;i<N;i++) { for(int j=i+1;j<N;j++) { Node chain_i = chain[i]; @@ -255,16 +255,16 @@ public: TS_ASSERT(chain_i<chain_j); } } - + } void testEqNode() { /*Node eqNode(const Node& right) const;*/ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.eqNode(right); - + TS_ASSERT(EQUAL == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -283,31 +283,31 @@ public: TS_ASSERT(1 == parent.getNumChildren()); TS_ASSERT(parent[0] == child); - + } void testAndNode() { /*Node andNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.andNode(right); - + TS_ASSERT(AND == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); - + } void testOrNode() { /*Node orNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.orNode(right); - + TS_ASSERT(OR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -322,9 +322,9 @@ public: Node cnd = d_nodeManager->mkNode(PLUS); Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); - Node ite = cnd.iteNode(thenBranch,elseBranch); - + Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node ite = cnd.iteNode(thenBranch, elseBranch); + TS_ASSERT(ITE == ite.getKind()); TS_ASSERT(3 == ite.getNumChildren()); @@ -336,11 +336,11 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.iffNode(right); - + TS_ASSERT(IFF == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -349,13 +349,13 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - + void testImpNode() { /* Node impNode(const Node& right) const; */ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.impNode(right); - + TS_ASSERT(IMPLIES == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -367,9 +367,9 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.xorNode(right); - + TS_ASSERT(XOR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -394,13 +394,13 @@ public: void testGetOperator() { - const Type* sort = d_nodeManager->mkSort("T"); - const Type* booleanType = d_nodeManager->booleanType(); - const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType); + Type* sort = d_nodeManager->mkSort("T"); + Type* booleanType = d_nodeManager->booleanType(); + Type* predType = d_nodeManager->mkFunctionType(sort, booleanType); Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); - Node fa = d_nodeManager->mkNode(kind::APPLY,f,a); + Node fa = d_nodeManager->mkNode(kind::APPLY, f, a); TS_ASSERT( fa.hasOperator() ); TS_ASSERT( !f.hasOperator() ); @@ -410,7 +410,7 @@ public: TS_ASSERT_THROWS( f.getOperator(), AssertionException ); TS_ASSERT_THROWS( a.getOperator(), AssertionException ); } - + void testNaryExpForSize(Kind k, int N){ NodeBuilder<> nbz(k); for(int i=0;i<N;i++){ @@ -434,13 +434,13 @@ public: //Bigger tests - srand(0); + srand(0); int trials = 500; for(int i=0;i<trials; i++){ int N = rand() % 1000; testNaryExpForSize(NOT, N); } - + } void testIterator(){ @@ -469,10 +469,12 @@ public: } void testToString(){ - Node w = d_nodeManager->mkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -480,11 +482,12 @@ public: } void testToStream(){ - NodeBuilder<> b; - Node w = d_nodeManager->mkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 5b63557ba..28dbde933 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -21,7 +21,6 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node.h" -#include "expr/attribute.h" #include "context/context.h" #include "util/Assert.h" @@ -29,30 +28,8 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; 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; - -// it would be nice to have CDAttribute<> for context-dependence -typedef CDAttribute<Test1, bool> TestCDFlag; - -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; - -typedef CDAttribute<Test1, bool> TestFlag1cd; -typedef CDAttribute<Test2, bool> TestFlag2cd; - class NodeWhite : public CxxTest::TestSuite { Context* d_ctxt; @@ -88,494 +65,4 @@ public: TS_ASSERT(b.d_nv->getNumChildren() == 0); /* etc. */ } - - void testAttributeIds() { - TS_ASSERT(VarNameAttr::s_id == 0); - TS_ASSERT(TestStringAttr1::s_id == 1); - TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3)); - - TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1)); - - TS_ASSERT(TestFlag1::s_id == 0); - TS_ASSERT(TestFlag2::s_id == 1); - TS_ASSERT(TestFlag3::s_id == 2); - TS_ASSERT(TestFlag4::s_id == 3); - TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5)); - - TS_ASSERT(TestFlag1cd::s_id == 0); - TS_ASSERT(TestFlag2cd::s_id == 1); - TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2)); - } - - void testCDAttributes() { - AttributeManager& am = d_nm->d_attrManager; - - //Debug.on("boolattr"); - - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 1 - - // test that all boolean flags are FALSE to start - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - // test that they all HAVE the boolean attributes - TS_ASSERT(a.hasAttribute(TestFlag1cd())); - TS_ASSERT(b.hasAttribute(TestFlag1cd())); - TS_ASSERT(c.hasAttribute(TestFlag1cd())); - - // test two-arg version of hasAttribute() - bool bb; - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - - // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); - a.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "set flag 1 on b to F\n"); - b.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on c to F\n"); - c.setAttribute(TestFlag1cd(), false); - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 2 - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("boolattr", "set flag 1 on a to F\n"); - a.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on b to T\n"); - b.setAttribute(TestFlag1cd(), true); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 3 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("boolattr", "set flag 1 on c to T\n"); - c.setAttribute(TestFlag1cd(), true); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be T)\n"); - TS_ASSERT(c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 2 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 1 - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 0 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); -#endif /* CVC4_ASSERTIONS */ - } - - void testAttributes() { - AttributeManager& am = d_nm->d_attrManager; - - //Debug.on("boolattr"); - - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node unnamed = d_nm->mkVar(); - - 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; - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 2 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 3 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 4 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 5 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(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/parser/parser_black.h b/test/unit/parser/parser_black.h index 1b05f490e..f7d4eff24 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -170,7 +170,7 @@ class ParserBlack : public CxxTest::TestSuite { } catch (Exception& e) { cout << "\nGood input failed:\n" << goodInputs[i] << endl << e << endl; - throw e; + throw; } } @@ -226,6 +226,7 @@ class ParserBlack : public CxxTest::TestSuite { ( smtParser->parseNextExpression(); cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, ParserException ); + delete smtParser; } //Debug.off("parser"); } @@ -235,6 +236,10 @@ public: d_exprManager = new ExprManager(); } + void tearDown() { + delete d_exprManager; + } + void testGoodCvc4Inputs() { tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); } |