From 826f583ee14b922f39666dc827a5624fff753724 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 25 Feb 2010 07:48:03 +0000 Subject: * src/expr/node.h: add a copy constructor. Apparently GCC doesn't recognize an instantiation of the join conversion/copy ctor with ref_count = ref_count_1 as a copy constructor. Problems with reference counts ensue. * src/theory/theory.h, src/theory/theory.cpp: Theory base implementation work. Changed from continuation-style theory calls to having an data member for the output channel. registerTerm() and preRegisterTerm() work. * src/theory/output_channel.h, src/theory/theory.h, src/theory/theory.cpp, src/theory/uf/theory_uf.h, src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into OutputChannel. * test/unit/expr/node_black.h: remove testPlusNode(), testUMinusNode(), testMultNode(). * src/expr/attribute.h: new facilities ManagedAttribute<> and CDAttribute<>, and add new template parameters to Attribute<>. Make CDAttribute<>s work with context manager. * src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and TypeAttr are now "owned" (defined) by the NodeManager. The AttributeManager knows nothing of specific attributes, it just as all the code for dealing generically with attributes. * test/unit/expr/node_white.h: test new attribute facilities. * src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes away. * src/theory/Makefile.am: fixed improper linking of theories * src/theory/theory_engine.h: some implementation work (mainly stubs for now, just to make sure TheoryUF can be instantiated properly, etc.) * src/expr/node_value.cpp, src/expr/node_value.h: move a number of function implementations to the header and make them inline * src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of function implementations to the header and make them inline * src/theory/theoryof_table_prologue.h, src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof, src/theory/Makefile.am: make the theoryOf() table from kinds and implement TheoryEngine::theoryOf(). * src/theory/arith/Makefile, src/theory/bool/Makefile: generated these stub Makefiles (with contrib/addsourcedir) as per policy * src/theory/arith, src/theory/bool [directory properties]: add .deps to svn:ignore. * contrib/configure-in-place: permit configuring "in-place" in the source directory. * contrib/get-authors, contrib/dimacs_to_smt.pl, contrib/update-copyright.pl, contrib/get-authors, contrib/addsourcedir, src/expr/mkkind: copyright notice * src/expr/node_manager.h, src/expr/node_builder.h, src/prop/prop_engine.h, src/prop/prop_engine.cpp, src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp, src/theory/output_channel.h: turn "const Node&"-typed formal parameters into "TNode" * src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans" to avoid keyword clash on containing namespace * src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h, src/theory/arith/theory_def.h: "define" a theory simply (for automatic theoryOf() generator). * src/Makefile.am: build theory subdirectory before prop, smt, etc. so that src/theory/theoryof_table.h header gets generated before it's needed * src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a separate CVC4::kind namespace to avoid its contents from cluttering the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace but not the enum values. * src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h, src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp, src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g, src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp, test/unit/expr/node_white.h, test/unit/expr/node_black.h, test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h: update for having moved Kind into CVC4::kind. * src/parser/parser.cpp: added file-does-not-exist check (was failing silently). --- test/unit/expr/kind_black.h | 1 + test/unit/expr/node_black.h | 17 ++--------- test/unit/expr/node_builder_black.h | 1 + test/unit/expr/node_white.h | 60 +++++++++++++++++++++++-------------- 4 files changed, 42 insertions(+), 37 deletions(-) (limited to 'test/unit') diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 35c5fde16..a9db0262e 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -22,6 +22,7 @@ #include "expr/kind.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class KindBlack : public CxxTest::TestSuite { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 75ab25f4c..4731810ea 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -24,6 +24,7 @@ #include "expr/node.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class NodeBlack : public CxxTest::TestSuite { @@ -40,8 +41,8 @@ public: } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; } bool imp(bool a, bool b) const { @@ -381,20 +382,6 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testPlusNode() { - /*Node plusNode(const Node& right) const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - - void testUMinusNode() { - /*Node uMinusNode() const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - void testMultNode() { - /* Node multNode(const Node& right) const;*/ - TS_WARN( "TODO: No implementation to test." ); - } - void testKindSingleton(Kind k) { Node n = d_nm->mkNode(k); TS_ASSERT(k == n.getKind()); diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 10d761166..5dc327a67 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -26,6 +26,7 @@ #include "expr/kind.h" using namespace CVC4; +using namespace CVC4::kind; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 1b57d01df..871abe232 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -24,7 +24,9 @@ #include "expr/attribute.h" using namespace CVC4; +using namespace CVC4::kind; using namespace CVC4::expr; +using namespace CVC4::expr::attr; using namespace std; struct Test1; @@ -36,12 +38,27 @@ struct Test5; typedef Attribute TestStringAttr1; typedef Attribute TestStringAttr2; +// it would be nice to have CDAttribute<> for context-dependence +typedef CDAttribute TestCDFlag; + +struct ecdata; +struct cleanupfcn { + static void cleanup(ecdata* ec) { /* clean up */ } +}; + +// ManagedAttribute<> has a cleanup function deleting the value +typedef ManagedAttribute TestECDataAttr; + typedef Attribute TestFlag1; typedef Attribute TestFlag2; typedef Attribute TestFlag3; typedef Attribute TestFlag4; typedef Attribute TestFlag5; +struct FooBar {}; +struct Test6; +typedef Attribute TestFlag6; + class NodeWhite : public CxxTest::TestSuite { NodeManagerScope *d_scope; @@ -55,8 +72,8 @@ public: } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; } void testNull() { @@ -89,7 +106,6 @@ public: TS_ASSERT(TestFlag3::s_id == 2); TS_ASSERT(TestFlag4::s_id == 3); TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT(attr::LastAttributeId::s_id == 5); } void testAttributes() { @@ -201,68 +217,68 @@ public: // 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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(unnamed.hasAttribute(TestFlag5(), bb)); TS_ASSERT(! bb); // setting boolean flags -- cgit v1.2.3