* 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, 104 insertions, 17 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1c46743e9..bcb5f6d47 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -40,6 +40,19 @@ namespace CVC4 {
 
 class Type;
 
+namespace expr {
+namespace attr {
+
+struct VarName {};
+struct Type {};
+
+}/* CVC4::expr::attr namespace */
+
+typedef Attribute<attr::VarName, std::string> VarNameAttr;
+typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+
+}/* CVC4::expr namespace */
+
 class NodeManager {
   static __thread NodeManager* s_current;
 
@@ -48,7 +61,7 @@ class NodeManager {
   typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
-  expr::AttributeManager d_attrManager;
+  expr::attr::AttributeManager d_attrManager;
 
   NodeValue* poolLookup(NodeValue* nv) const;
   void poolInsert(NodeValue* nv);
@@ -57,7 +70,7 @@ class NodeManager {
 
 public:
 
-  NodeManager() : d_attrManager(this) {
+  NodeManager() {
     poolInsert( &NodeValue::s_null );
   }
 
@@ -65,11 +78,11 @@ public:
 
   // general expression-builders
   Node mkNode(Kind kind);
-  Node mkNode(Kind kind, const Node& child1);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+  Node mkNode(Kind kind, TNode child1);
+  Node mkNode(Kind kind, TNode child1, TNode child2);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
   // N-ary version
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
@@ -79,20 +92,29 @@ public:
   Node mkVar();
 
   template <class AttrKind>
-  inline typename AttrKind::value_type getAttribute(const Node& n,
+  inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) const;
 
+  // Note that there are two, distinct hasAttribute() declarations for
+  // a reason (rather than using a pointer-valued argument with a
+  // default value): they permit more optimized code in the underlying
+  // hasAttribute() implementations.
+
+  template <class AttrKind>
+  inline bool hasAttribute(TNode n,
+                           const AttrKind&) const;
+
   template <class AttrKind>
-  inline bool hasAttribute(const Node& n,
+  inline bool hasAttribute(TNode n,
                            const AttrKind&,
-                           typename AttrKind::value_type* = NULL) const;
+                           typename AttrKind::value_type&) const;
 
   template <class AttrKind>
-  inline void setAttribute(const Node& n,
+  inline void setAttribute(TNode n,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  inline const Type* getType(const Node& n);
+  inline const Type* getType(TNode n);
 };
 
 class NodeManagerScope {
@@ -112,29 +134,94 @@ public:
 };
 
 template <class AttrKind>
-inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
+inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
                                                                const AttrKind&) const {
   return d_attrManager.getAttribute(n, AttrKind());
 }
 
 template <class AttrKind>
-inline bool NodeManager::hasAttribute(const Node& n,
+inline bool NodeManager::hasAttribute(TNode n,
+                                      const AttrKind&) const {
+  return d_attrManager.hasAttribute(n, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(TNode n,
                                       const AttrKind&,
-                                      typename AttrKind::value_type* ret) const {
+                                      typename AttrKind::value_type& ret) const {
   return d_attrManager.hasAttribute(n, AttrKind(), ret);
 }
 
 template <class AttrKind>
-inline void NodeManager::setAttribute(const Node& n,
+inline void NodeManager::setAttribute(TNode n,
                                       const AttrKind&,
                                       const typename AttrKind::value_type& value) {
   d_attrManager.setAttribute(n, AttrKind(), value);
 }
 
-inline const Type* NodeManager::getType(const Node& n) {
+inline const Type* NodeManager::getType(TNode n) {
   return getAttribute(n,CVC4::expr::TypeAttr());
 }
 
+inline void NodeManager::poolInsert(NodeValue* nv) {
+  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
+         "the pool!");
+  d_nodeValueSet.insert(nv);
+}
+
+}/* CVC4 namespace */
+
+#include "expr/node_builder.h"
+
+namespace CVC4 {
+
+// general expression-builders
+
+inline Node NodeManager::mkNode(Kind kind) {
+  return NodeBuilder<>(this, kind);
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1) {
+  return NodeBuilder<>(this, kind) << child1;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
+  return NodeBuilder<>(this, kind) << child1 << child2;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+  return NodeBuilder<>(this, kind).append(children);
+}
+
+inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
+  Node n = mkVar(type);
+  n.setAttribute(expr::VarNameAttr(), name);
+  return n;
+}
+
+inline Node NodeManager::mkVar(const Type* type) {
+  Node n = NodeBuilder<>(this, kind::VARIABLE);
+  n.setAttribute(expr::TypeAttr(), type);
+  return n;
+}
+
+inline Node NodeManager::mkVar() {
+  return NodeBuilder<>(this, kind::VARIABLE);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_H */