diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /test/unit | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* 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).
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/expr/kind_black.h | 1 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 17 | ||||
-rw-r--r-- | test/unit/expr/node_builder_black.h | 1 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 60 |
4 files changed, 42 insertions, 37 deletions
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<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; + +struct ecdata; +struct cleanupfcn { + static void cleanup(ecdata* ec) { /* clean up */ } +}; + +// ManagedAttribute<> has a cleanup function deleting the value +typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr; + 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; +struct FooBar {}; +struct Test6; +typedef Attribute<Test6, FooBar> 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<bool>::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 |