update-copyright.pl now retrieves and incorporates author information from repository history; re-ran update-copyright.pl; cleaned up some things with make

69 files changed, 461 insertions, 78 deletions

diff --git a/Makefile.subdir b/Makefile.subdir
index 590b3ea4e..6470510d9 100644
--- a/Makefile.subdir
+++ b/Makefile.subdir
@@ -4,7 +4,7 @@ builddir = $(topdir)/builds/$(CURRENT_BUILD)/$(srcdir)
 
 .PHONY: _default_build_ all
 _default_build_: all
-%:
+all %:
 	@if test -e $(builddir); then \
 		echo cd $(builddir); \
 		cd $(builddir); \
diff --git a/contrib/get-authors b/contrib/get-authors
new file mode 100755
index 000000000..a42f8a25b
--- /dev/null
+++ b/contrib/get-authors
@@ -0,0 +1,33 @@
+#!/bin/sh
+#
+# get-authors
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# usage: get-authors [ files... ]
+#
+# This script uses svn to get the original author
+#
+
+while [ $# -gt 0 ]; do
+  f=$1
+  shift
+  original_author=
+  major_contributors=
+  minor_contributors=
+  total_lines=`wc -l "$f" | awk '{print$1}'`
+  original_author=`svn log -q --incremental "$f" | tail -1 | awk '{print$3}'`
+  svn blame "$f" | awk '{print$2}' | sort | uniq -c | sort -n |
+    ( while read lines author; do
+        pct=$((100*$lines/$total_lines))
+        if [ "$author" != "$original_author" ]; then
+          if [ $pct -gt 10 ]; then
+            major_contributors="${major_contributors:+$major_contributors, }$author"
+          else
+            minor_contributors="${minor_contributors:+$minor_contributors, }$author"
+          fi
+        fi
+      done; \
+      echo "$original_author"
+      echo "${major_contributors:-none}"
+      echo "${minor_contributors:-none}" )
+done
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 72bc006d7..1548e3fa6 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -1,5 +1,10 @@
 #!/usr/bin/perl -w
 #
+# update-copyright.pl
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# usage: update-copyright [ files/directories... ]
+#
 # This script goes through a source directory rewriting the top bits of
 # source files to match a template (inline, below).  For files with no
 # top comment, it adds a fresh one.
@@ -50,12 +55,12 @@ EOF
 use strict;
 use Fcntl ':mode';
 
+my $dir = $0;
+$dir =~ s,/[^/]+/*$,,;
+
 my @searchdirs = ();
 if($#ARGV == -1) {
-  my $dir = $0;
-  $dir =~ s,/[^/]+/*$,,;
-
-  (chdir($dir."/..") && -f "src/include/cvc4_expr.h") || die "can't find top-level source directory for CVC4";
+  (chdir($dir."/..") && -f "src/include/cvc4_config.h") || die "can't find top-level source directory for CVC4";
   my $pwd = `pwd`; chomp $pwd;
 
   print <<EOF;
@@ -103,6 +108,11 @@ sub recurse {
       my $outfile = $srcdir.'/#'.$file.'.tmp';
       open(my $IN, $infile) || die "error opening $infile for reading";
       open(my $OUT, '>', $outfile) || die "error opening $outfile for writing";
+      open(my $AUTHOR, "$dir/get-authors " . $infile . '|');
+      my $author = <$AUTHOR>; chomp $author;
+      my $major_contributors = <$AUTHOR>; chomp $major_contributors;
+      my $minor_contributors = <$AUTHOR>; chomp $minor_contributors;
+      close $AUTHOR;
       $_ = <$IN>;
       if(m,^(%{)?/\*\*\*\*\*,) {
         print "updating\n";
@@ -112,6 +122,9 @@ sub recurse {
           print $OUT "/*********************                                           -*- C++ -*-  */\n";
         }
         print $OUT "/** $file\n";
+        print $OUT " ** Original author: $author\n";
+        print $OUT " ** Major contributors: $major_contributors\n";
+        print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
         print $OUT $standard_template;
         print $OUT " **\n";
         while(my $line = <$IN>) {
@@ -126,6 +139,9 @@ sub recurse {
           print $OUT "/*********************                                           -*- C++ -*-  */\n";
         }
         print $OUT "/** $file\n";
+        print $OUT " ** Original author: $author\n";
+        print $OUT " ** Major contributors: $major_contributors\n";
+        print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
         print $OUT $standard_template;
         print $OUT " **\n";
         print $OUT " ** [[ Add file-specific comments here ]]\n";
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 005c3bd6a..3635d0c07 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** context.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/context/context.h b/src/context/context.h
index 6cc36ae9b..68667c223 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** context.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Context class and context manager.
  **/
 
 #ifndef __CVC4__CONTEXT__CONTEXT_H
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 3b4089b25..d772b886f 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** context_mm.cpp
+ ** Original author: barrett
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index d48cbedc0..eeaa0a2c8 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** context_mm.h
+ ** Original author: barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 597be0fe7..7fa828237 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** attr_type.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Node attribute describing the type of a node.
  **/
 
 #ifndef __CVC4__EXPR__ATTR_TYPE_H
diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h
index 13a2ec36f..a17a3ba18 100644
--- a/src/expr/attr_var_name.h
+++ b/src/expr/attr_var_name.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
-/** attr_type.h
+/** attr_var_name.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** The node attribute describing variable names.
  **/
 
 #ifndef __CVC4__EXPR__ATTR_VAR_NAME_H
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index eacd1cb24..ee9334f3c 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -1,9 +1,17 @@
-/*
- * expr.cpp
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
 
 #include "expr/expr.h"
 #include "expr/node.h"
diff --git a/src/expr/expr.h b/src/expr/expr.h
index a0a646900..447c35f77 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -1,9 +1,17 @@
-/*
- * expr.h
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Public-facing expression interface.
+ **/
 
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index ea1649e12..ea1ade477 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -1,3 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 /*
  * expr_manager.cpp
  *
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 645193ecf..ace8b2d1c 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -1,9 +1,17 @@
-/*
- * expr_manager.h
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Public-facing expression manager interface.
+ **/
 
 #ifndef __CVC4__EXPR_MANAGER_H
 #define __CVC4__EXPR_MANAGER_H
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 624ab7337..ea9dbd662 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** kind.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Kinds of Nodes.
  **/
 
 #ifndef __CVC4__KIND_H
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 334cf1b0e..9c73b982c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node.h b/src/expr/node.h
index aad0689bb..9bb138b21 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Reference-counted encapsulation of a pointer to an expression.
+ ** Reference-counted encapsulation of a pointer to node information.
  **/
 
 #include "expr/node_value.h"
diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h
index 0b759efb4..021e64649 100644
--- a/src/expr/node_attribute.h
+++ b/src/expr/node_attribute.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_attribute.h
+/** node_attribute.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Node attributes.
  **/
 
 #ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 0a36421f2..9e24fa280 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_builder.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 63048c1ac..b974ecc67 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_builder.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A builder interface for nodes.
  **/
 
 #ifndef __CVC4__NODE_BUILDER_H
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7e871d9c3..d752db88f 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_manager.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 643f09f11..827c6c1b7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_manager.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A manager for Nodes.
  **/
 
 #ifndef __CVC4__NODE_MANAGER_H
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 42b7b05e4..6724b0771 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_value.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 75c694ec9..352be7d27 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** node_value.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
index f1877781f..9cf9a182b 100644
--- a/src/include/cvc4_config.h
+++ b/src/include/cvc4_config.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** cvc4_config.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Macros that should be defined everywhere during the building of
+ ** the libraries and driver binary.
  **/
 
 #ifndef __CVC4_CONFIG_H
diff --git a/src/main/about.h b/src/main/about.h
index 592c09551..ec6f3dced 100644
--- a/src/main/about.h
+++ b/src/main/about.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** about.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 24c96f69a..c191b2a15 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** getopt.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): barrett, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 187a0f316..ba71b043f 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** main.cpp
+ ** Original author: mdeters
+ ** Major contributors: barrett, dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/main.h b/src/main/main.h
index 0141e2848..c44cd9d67 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** main.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, barrett
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/usage.h b/src/main/usage.h
index d48c1c96d..e9d8aa983 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** usage.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 94a295d54..9bb96d853 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** util.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 1baaf2139..c42415c54 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -1,3 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** antlr_parser.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): cconway, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 /*
  * antlr_parser.cpp
  *
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index b2ef3f181..8a9dea5ad 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -1,9 +1,17 @@
-/*
- * antlr_parser.h
- *
- *  Created on: Nov 30, 2009
- *      Author: dejan
- */
+/*********************                                           -*- C++ -*-  */
+/** antlr_parser.h
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Base for ANTLR parser classes.
+ **/
 
 #ifndef CVC4_PARSER_H_
 #define CVC4_PARSER_H_
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
index adeb5761d..57d5e6c96 100644
--- a/src/parser/cvc/cvc_parser.cpp
+++ b/src/parser/cvc/cvc_parser.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** cvc_parser.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
index 9cb6b7594..82d659566 100644
--- a/src/parser/cvc/cvc_parser.h
+++ b/src/parser/cvc/cvc_parser.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** cvc_parser.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8d4af5ba1..2ff409686 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** parser.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7755d65f0..b448cd2a6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** parser.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index b2cf8bc55..3504eeba2 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** parser_exception.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Exception class.
+ ** Exception class for parse errors.
  **/
 
 #ifndef __CVC4__PARSER__PARSER_EXCEPTION_H
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
index 65d36690c..8c5773e32 100644
--- a/src/parser/smt/smt_parser.cpp
+++ b/src/parser/smt/smt_parser.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** smt_parser.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
index 6927888cf..21c278a37 100644
--- a/src/parser/smt/smt_parser.h
+++ b/src/parser/smt/smt_parser.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** smt_parser.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): cconway, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 2c4f0e8b7..66d5727d6 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** symbol_table.h
+ ** Original author: cconway
+ ** Major contributors: dejan, mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A symbol table for the parsers' use.
  **/
 
 #ifndef __CVC4__PARSER__SYMBOL_TABLE_H
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index caf87428b..ffd335453 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
-/** prop_engine.h
+/** prop_engine.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 21a6669d7..6cb818d10 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** prop_engine.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** The PropEngine (proposiitonal engine); main interface point
+ ** between CVC4's SMT infrastructure and the SAT solver.
  **/
 
 #ifndef __CVC4__PROP_ENGINE_H
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 32ca9e983..9e216b126 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** sat.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** SAT Solver.
  **/
 
 #ifndef __CVC4__PROP__SAT_H
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 23dc1153a..4c7f6a156 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** smt_engine.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index edcbdcca3..98cffb6de 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** smt_engine.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** SmtEngine: the main public entry point of libcvc4.
  **/
 
 #ifndef __CVC4__SMT_ENGINE_H
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 024d192e6..c4b2b8d83 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** theory.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Base for theory interface.
  **/
 
 #include "theory/theory.h"
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 21124375a..b695ca03d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** theory.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Base of the theory interface.
  **/
 
 #ifndef __CVC4__THEORY__THEORY_H
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 6d0b9d91d..2289f2fea 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** theory_engine.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** The theory engine.
  **/
 
 #include "theory/theory_engine.h"
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index d6d8691b2..65a317433 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** theory_engine.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** The theory engine.
  **/
 
 #ifndef __CVC4__THEORY_ENGINE_H
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index a86e2021a..337649039 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** Assert.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 26a1ee7d4..49c97e9b6 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** Assert.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 3911897f5..5a5b766cb 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -1,3 +1,18 @@
+/*********************                                           -*- C++ -*-  */
+/** command.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 /*
  * command.cpp
  *
diff --git a/src/util/command.h b/src/util/command.h
index 221c513f0..9cc009d01 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** command.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Implementation of the command pattern on SmtEngines.  Generated by
+ ** the parser.
  **/
 
 #ifndef __CVC4__COMMAND_H
diff --git a/src/util/debug.h b/src/util/debug.h
index 14dc0fbd1..800106764 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** debug.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,20 +10,27 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Debugging things.
+ **
+ ** These are low-level assertions!  Generally you should use
+ ** CVC4::Assert() instead (they throw an exception!).  See
+ ** util/Assert.h.
  **/
 
 #ifndef __CVC4__DEBUG_H
 #define __CVC4__DEBUG_H
 
+#include "cvc4_config.h"
+
 #include <cassert>
 
-#ifdef DEBUG
+#ifdef CVC4_ASSERTIONS
 // the __builtin_expect() helps us if assert is built-in or a macro
-# define cvc4assert(x) assert(__builtin_expect((x), 1))
+#  define cvc4assert(x) assert(EXPECT_TRUE( x ))
 #else
 // TODO: use a compiler annotation when assertions are off ?
 // (to improve optimization)
-# define cvc4assert(x)
-#endif /* DEBUG */
+#  define cvc4assert(x) /*EXPECT_TRUE( x )*/
+#endif /* CVC4_ASSERTIONS */
 
 #endif /* __CVC4__DEBUG_H */
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index ae79f920d..36f99f4ac 100644
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index 3a093211c..58f9400b5 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A decision engine for CVC4.
  **/
 
 #ifndef __CVC4__DECISION_ENGINE_H
diff --git a/src/util/exception.h b/src/util/exception.h
index d239f48de..8481a8504 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** exception.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,9 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Exception class.
- **
- ** As many paragraphs as you like.
+ ** CVC4's exception base class and some associated utilities.
  **/
 
 #ifndef __CVC4__EXCEPTION_H
diff --git a/src/util/literal.h b/src/util/literal.h
index 3ec216a6a..921a9ef0d 100644
--- a/src/util/literal.h
+++ b/src/util/literal.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** literal.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A literal.
  **/
 
 #ifndef __CVC4__LITERAL_H
diff --git a/src/util/model.h b/src/util/model.h
index cf006b3e1..b79032221 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** model.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A model.
  **/
 
 #ifndef __CVC4__MODEL_H
diff --git a/src/util/options.h b/src/util/options.h
index 8d2d113a2..2bfbf675f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** options.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Global (command-line or equivalent) tuning parameters.
  **/
 
 #include <iostream>
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 103a3d61a..05c74918c 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** output.cpp
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/output.h b/src/util/output.h
index 43dfe8a40..57ce5f3ca 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** output.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/result.h b/src/util/result.h
index 8d9b93a1e..87686d59c 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** result.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** Encapsulation of the result of a query.
  **/
 
 #ifndef __CVC4__RESULT_H
diff --git a/src/util/unique_id.h b/src/util/unique_id.h
index 4ac80f772..633a544f0 100644
--- a/src/util/unique_id.h
+++ b/src/util/unique_id.h
@@ -1,5 +1,8 @@
 /*********************                                           -*- C++ -*-  */
 /** unique_id.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -7,6 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
+ ** A mechanism for getting a compile-time unique ID.
  **/
 
 #ifndef __CVC4__UNIQUE_ID_H
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index d8f321f10..61eef32d5 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,23 +1,39 @@
+# all unit tests
+UNIT_TESTS = \
+	expr/node_white \
+	expr/node_black \
+	parser/cvc/cvc_parser_black \
+	parser/smt/smt_parser_black
+
+# things that aren't tests but that tests rely on and need to
+# go into the distribution
+TEST_DEPENDENCIES =
+
 if HAVE_CXXTESTGEN
 
 AM_CPPFLAGS = \
-	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
+	$(TEST_CPPFLAGS)
+AM_CXXFLAGS = $(TEST_CXXFLAGS)
+AM_LDFLAGS = $(TEST_LDFLAGS)
+
 AM_CXXFLAGS_WHITE = -fno-access-control
 AM_CXXFLAGS_BLACK =
 AM_CXXFLAGS_PUBLIC =
 AM_LDFLAGS_WHITE = \
-	    @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
-	    @abs_top_builddir@/src/libcvc4_noinst.la
+	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
+	@abs_top_builddir@/src/libcvc4_noinst.la
 AM_LDFLAGS_BLACK = \
-		$(AM_LDFLAGS_WHITE)
+	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
+	@abs_top_builddir@/src/libcvc4_noinst.la
 AM_LDFLAGS_PUBLIC = \
-		@abs_top_builddir@/src/libcvc4.la
+	@abs_top_builddir@/src/libcvc4.la
 
-TESTS = \
-	expr/node_white \
-	expr/node_black \
-	parser/cvc/cvc_parser_black \
-	parser/smt/smt_parser_black
+TESTS = $(UNIT_TESTS)
+
+EXTRA_DIST = \
+	no_cxxtest \
+	$(TEST_DEPENDENCIES)
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
 noinst_LTLIBRARIES = libdummy.la
@@ -28,18 +44,12 @@ $(TESTS:%=%.cpp): %.cpp: %.h
 	mkdir -p `dirname "$@"`
 	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
 $(filter %_white,$(TESTS)): %_white: %_white.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
 $(filter %_black,$(TESTS)): %_black: %_black.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
 $(filter %_public,$(TESTS)): %_public: %_public.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
 	$(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
@@ -50,4 +60,8 @@ else
 # force a user-visible failure for "make check"
 TESTS = no_cxxtest
 
+EXTRA_DIST = \
+	$(UNIT_TESTS) \
+	$(TEST_DEPENDENCIES)
+
 endif
diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 251ef2dfe..6e518d527 100644
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -213,30 +213,49 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
+
+# all unit tests
+UNIT_TESTS = \
+	expr/node_white \
+	expr/node_black \
+	parser/cvc/cvc_parser_black \
+	parser/smt/smt_parser_black
+
+
+# things that aren't tests but that tests rely on and need to
+# go into the distribution
+TEST_DEPENDENCIES = 
 @HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
-@HAVE_CXXTESTGEN_TRUE@	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
+@HAVE_CXXTESTGEN_TRUE@	-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
+@HAVE_CXXTESTGEN_TRUE@	$(TEST_CPPFLAGS)
 
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS = $(TEST_CXXFLAGS)
+@HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS = $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_WHITE = -fno-access-control
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK = 
 @HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC = 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \
-@HAVE_CXXTESTGEN_TRUE@	    @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
-@HAVE_CXXTESTGEN_TRUE@	    @abs_top_builddir@/src/libcvc4_noinst.la
+@HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
+@HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/libcvc4_noinst.la
 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \
-@HAVE_CXXTESTGEN_TRUE@		$(AM_LDFLAGS_WHITE)
+@HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
+@HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/libcvc4_noinst.la
 
 @HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_PUBLIC = \
-@HAVE_CXXTESTGEN_TRUE@		@abs_top_builddir@/src/libcvc4.la
+@HAVE_CXXTESTGEN_TRUE@	@abs_top_builddir@/src/libcvc4.la
 
 
 # force a user-visible failure for "make check"
 @HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
-@HAVE_CXXTESTGEN_TRUE@TESTS = \
-@HAVE_CXXTESTGEN_TRUE@	expr/node_white \
-@HAVE_CXXTESTGEN_TRUE@	expr/node_black \
-@HAVE_CXXTESTGEN_TRUE@	parser/cvc/cvc_parser_black \
-@HAVE_CXXTESTGEN_TRUE@	parser/smt/smt_parser_black
+@HAVE_CXXTESTGEN_TRUE@TESTS = $(UNIT_TESTS)
+@HAVE_CXXTESTGEN_FALSE@EXTRA_DIST = \
+@HAVE_CXXTESTGEN_FALSE@	$(UNIT_TESTS) \
+@HAVE_CXXTESTGEN_FALSE@	$(TEST_DEPENDENCIES)
+
+@HAVE_CXXTESTGEN_TRUE@EXTRA_DIST = \
+@HAVE_CXXTESTGEN_TRUE@	no_cxxtest \
+@HAVE_CXXTESTGEN_TRUE@	$(TEST_DEPENDENCIES)
 
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
@@ -629,18 +648,12 @@ uninstall-am:
 @HAVE_CXXTESTGEN_TRUE@	mkdir -p `dirname "$@"`
 @HAVE_CXXTESTGEN_TRUE@	@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
 @HAVE_CXXTESTGEN_TRUE@$(filter %_white,$(TESTS)): %_white: %_white.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@	$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
 @HAVE_CXXTESTGEN_TRUE@$(filter %_black,$(TESTS)): %_black: %_black.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@	$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
 @HAVE_CXXTESTGEN_TRUE@$(filter %_public,$(TESTS)): %_public: %_public.cpp
-#	get these in here somehow
-#	$(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
 @HAVE_CXXTESTGEN_TRUE@	$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
 @HAVE_CXXTESTGEN_TRUE@	$(CXXLINK) $(AM_LDFLAGS_PUBLIC) $@.lo
 
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index c95900383..aa99c70c4 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -1,4 +1,17 @@
-/* Black box testing of CVC4::Node. */
+/*********************                                           -*- C++ -*-  */
+/** node_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Black box testing of CVC4::Node.
+ **/
 
 #include <cxxtest/TestSuite.h>
 
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index dd462fdd8..96a30e582 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -1,4 +1,17 @@
-/* White box testing of CVC4::Node. */
+/*********************                                           -*- C++ -*-  */
+/** node_white.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** White box testing of CVC4::Node.
+ **/
 
 #include <cxxtest/TestSuite.h>
 
diff --git a/test/unit/parser/cvc/cvc_parser_black.h b/test/unit/parser/cvc/cvc_parser_black.h
index e99cce44d..4679d358c 100644
--- a/test/unit/parser/cvc/cvc_parser_black.h
+++ b/test/unit/parser/cvc/cvc_parser_black.h
@@ -1,4 +1,17 @@
-/* Black box testing of CVC4::parser::CvcParser. */
+/*********************                                           -*- C++ -*-  */
+/** cvc_parser_black.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 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.
+ **
+ ** Black box testing of CVC4::parser::CvcParser.
+ **/
 
 #include <cxxtest/TestSuite.h>
 //#include <string>