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

24 files changed, 181 insertions, 71 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 1611f28d3..dbf292108 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** Assert.cpp
+/*! \file Assert.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 Assertion utility classes, functions, and exceptions.
  **
  ** Assertion utility classes, functions, and exceptions.  Implementation.
  **/
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 744782ba2..5333817aa 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** Assert.h
+/*! \file Assert.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 Assertion utility classes, functions, exceptions, and macros.
  **
  ** Assertion utility classes, functions, exceptions, and macros.
  **/
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 125065118..f789313b8 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -1,9 +1,21 @@
-/*
- * bitvector.cpp
- *
- *  Created on: Apr 5, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file bitvector.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #include "bitvector.h"
 
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 4f6038a81..e3ba969ec 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -1,9 +1,21 @@
-/*
- * bitvector.h
- *
- *  Created on: Mar 31, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file bitvector.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #ifndef __CVC4__BITVECTOR_H_
 #define __CVC4__BITVECTOR_H_
diff --git a/src/util/bool.h b/src/util/bool.h
index edd45b8a0..d2a29c8d5 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** bool.h
+/*! \file bool.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 A multiprecision rational constant.
  **
  ** A multiprecision rational constant.
  ** This stores the rational as a pair of multiprecision integers,
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 5ed13a139..2a7563f82 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** configuration.cpp
+/*! \file configuration.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,10 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of Configuration class, which provides compile-time
+ ** configuration information about the CVC4 library.
  **
  ** Implementation of Configuration class, which provides compile-time
  ** configuration information about the CVC4 library.
diff --git a/src/util/configuration.h b/src/util/configuration.h
index f939d8981..00651202d 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** configuration.h
+/*! \file configuration.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,10 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Interface to a public class that provides compile-time information
+ ** about the CVC4 library.
  **
  ** Interface to a public class that provides compile-time information
  ** about the CVC4 library.
diff --git a/src/util/debug.h b/src/util/debug.h
index a99652661..4fc5d5caa 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** debug.h
+/*! \file debug.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 Debugging things.
  **
  ** Debugging things.
  **
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index 06ea283a8..1ef2440c9 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** decision_engine.cpp
+/*! \file decision_engine.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 .
  **
  **/
 
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 84ace55b2..e1d9e21b7 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** decision_engine.h
+/*! \file decision_engine.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 A decision engine for CVC4.
  **
  ** A decision engine for CVC4.
  **/
diff --git a/src/util/exception.h b/src/util/exception.h
index 48dcf1244..4893bd3c2 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** exception.h
+/*! \file exception.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief CVC4's exception base class and some associated utilities.
  **
  ** CVC4's exception base class and some associated utilities.
  **/
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index 1849974cd..de237b793 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -1,9 +1,21 @@
-/*
- * gmp.h
- *
- *  Created on: Apr 5, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file gmp_util.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #ifndef __CVC4__GMP_H_
 #define __CVC4__GMP_H_
diff --git a/src/util/hash.h b/src/util/hash.h
index c72fe47e8..708628c24 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -1,9 +1,21 @@
-/*
- * hash.h
- *
- *  Created on: May 8, 2010
- *      Author: chris
- */
+/*********************                                                        */
+/*! \file hash.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #ifndef __CVC4__HASH_H_
 #define __CVC4__HASH_H_
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index a26f2108f..85075fd39 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** integer.cpp
+/*! \file integer.cpp
+ ** \verbatim
  ** Original author: taking
  ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision rational constant.
  **
  ** A multiprecision rational constant.
  ** This stores the rational as a pair of multiprecision integers,
diff --git a/src/util/integer.h b/src/util/integer.h
index 41582d8db..d1921f597 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** integer.h
+/*! \file integer.h
+ ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): dejan, cconway, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision integer constant.
  **
  ** A multiprecision integer constant.
  **/
diff --git a/src/util/model.h b/src/util/model.h
index f807ff963..31fed1f31 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** model.h
+/*! \file model.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 A model.
  **
  ** A model.
  **/
diff --git a/src/util/options.h b/src/util/options.h
index c7a730b14..7fcf35f00 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** options.h
+/*! \file options.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
  ** Minor contributors (to current version): dejan
@@ -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 Global (command-line or equivalent) tuning parameters.
  **
  ** Global (command-line or equivalent) tuning parameters.
  **/
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 5d09e1d93..501ef52fd 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** output.cpp
+/*! \file output.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 Output utility classes and functions.
  **
  ** Output utility classes and functions.
  **/
diff --git a/src/util/output.h b/src/util/output.h
index ea96606cb..f27ec24da 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** output.h
+/*! \file output.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Output utility classes and functions.
  **
  ** Output utility classes and functions.
  **/
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index 5e9141758..beaa184bb 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** rational.cpp
+/*! \file rational.cpp
+ ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A multi-precision rational constant.
  **
  ** A multi-precision rational constant.
  **/
diff --git a/src/util/rational.h b/src/util/rational.h
index 8218984a7..5e187de7f 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** rational.h
+/*! \file rational.h
+ ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Multi-precision rational constants.
  **
  ** Multi-precision rational constants.
  **/
diff --git a/src/util/result.h b/src/util/result.h
index 679e68763..e76e5605b 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** result.h
+/*! \file result.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 Encapsulation of the result of a query.
  **
  ** Encapsulation of the result of a query.
  **/
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index cf9298c4e..f00343729 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** sexpr.cpp
+/*! \file sexpr.h
+ ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
  ** 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 Simple representation of SMT S-expressions.
  **
  ** Simple representation of SMT S-expressions.
  **/
diff --git a/src/util/unique_id.h b/src/util/unique_id.h
index 54e56da96..67a6c5cff 100644
--- a/src/util/unique_id.h
+++ b/src/util/unique_id.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** unique_id.h
+/*! \file unique_id.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** 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 A mechanism for getting a compile-time unique ID.
  **
  ** A mechanism for getting a compile-time unique ID.
  **/