* 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).

1 files changed, 38 insertions, 22 deletions

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