** Don't fear the files-changed list, almost all changes are in the **

** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.

1 files changed, 6 insertions, 14 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bf0e2f96e..3eb2a8109 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** expr_manager_template.cpp
+/*! \file expr_manager_template.cpp
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression manager interface, implementation.
  **
  ** Public-facing expression manager interface, implementation.
  **/
@@ -71,17 +74,6 @@ BitVectorType ExprManager::bitVectorType(unsigned size) const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size)));
 }
 
-Expr ExprManager::mkExpr(Kind kind) {
-  const unsigned n = 0;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind));
-}
-
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   const unsigned n = 1;
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
@@ -252,7 +244,7 @@ Expr ExprManager::mkVar(const Type& type) {
 
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
-  CheckArgument( metakind::isAssociative(kind), kind,
+  CheckArgument( kind::isAssociative(kind), kind,
                  "Illegal kind in mkAssociative: %s",
                  kind::kindToString(kind).c_str());