update-copyright.pl now retrieves and incorporates author information from repository...

diff --git a/Makefile.subdir b/Makefile.subdir
index 590b3ea4ed2d6cd07437aefd554f0ce2da6b6d76..6470510d9826fd5ed2626e0178195d8e0327da3d 100644 (file)
--- 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 (executable)
index 0000000..a42f8a2
--- /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 72bc006d70fc70497e6d14bf75ad43d03ba79e45..1548e3fa6bd85e47e237b740d386cc2a4219a8f8 100755 (executable)
--- 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 005c3bd6a6345b3381d97b559611c989aca250f6..3635d0c071fc1d7620fc02836cb74ed6838ca456 100644 (file)
--- 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 6cc36ae9b1870ce2100e245a93efb7bceca73769..68667c223d46ffae9e3b56cb927e9dab9366e2bc 100644 (file)
--- 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 3b4089b250b8d4af5a0bdede54ecf88d815bb90d..d772b886f350af65da63621231ec527cbb3af244 100644 (file)
--- 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 d48cbedc07a35e40ff3a63cf4d0abeebd0d744e7..eeaa0a2c89fc97070d0a145b9b0842778af02236 100644 (file)
--- 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 597be0fe71bd52d27aae91327829cf7b76693fdb..7fa828237c1eb371f55430fc4048336731a904fd 100644 (file)
--- 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 13a2ec36f13b5b2551db123f101ca4272f0f1d6c..a17a3ba18a14f4ec1ad1c1ea8748b0a5f2527d5f 100644 (file)
--- 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 eacd1cb2409f5935f4c34cfe969177ab064b0e9c..ee9334f3c7b7b943207fc3659d274d296120f885 100644 (file)
--- 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 a0a64690015dc1c29ea9ced8287d26a3d038fcdd..447c35f77aca71472413715b75282e1e42b5c071 100644 (file)
--- 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 ea1649e12ac1cffef2ed983d077d4e3385e32f2d..ea1ade47706ae6274014c3bc868ac2059e8605f0 100644 (file)
--- 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 645193ecfe9133cf6d31107e663c5e03d38209f1..ace8b2d1cb9ecf91413f23ac273a78bfc29277f3 100644 (file)
--- 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 624ab73374b23019dff4fd358f85bfdb61e3ff2d..ea9dbd66205d83d532c6f8105b9e644885dd052a 100644 (file)
--- 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 334cf1b0eec1631c3cdf8ac40f3345a436a11204..9c73b982c36aded7063824a7c8a43c8e6ce891bd 100644 (file)
--- 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 aad0689bbe7bb300f0cdac2a325c048570c14672..9bb138b21d8334f7dba05234c2811f7cabe8a29b 100644 (file)
--- 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 0b759efb40052fd75d2a39d3d76b491aa81792e3..021e64649c2927427fdd0245092c5abf053aa4fd 100644 (file)
--- 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 0a36421f23e59a860769c6e64c357cba7192d1ff..9e24fa2802bcd0b9ad6a811e7190c5793e40e2fc 100644 (file)
--- 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 63048c1ac7c9675557b3cfabf8334e57bc053654..b974ecc671081880f49fd69aba8e0f1641b676de 100644 (file)
--- 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 7e871d9c34ffed633fbf9e2c41e01a473327f93b..d752db88f11cd9b652e5ac0badec467f1537e6bf 100644 (file)
--- 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 643f09f11224419b45f3d78237274990a01210c6..827c6c1b70628a1d5e41ee325a29bcf80b82ff92 100644 (file)
--- 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 42b7b05e4894070eda221c3bc3dab6c5fc472837..6724b07719015d8899d0be34361146c33690763c 100644 (file)
--- 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 75c694ec9e5a1c60767a1ea7536becc1de060a4b..352be7d277bfed60e26f2859b95a437b8857afc3 100644 (file)
--- 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 f1877781fd16bc52937fb440f95dc1c32f1d07fa..9cf9a182ba25dd784b029bc8ce3694ca300f3f45 100644 (file)
--- 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 592c09551e9a6d0f41c58c0ae707794559363dad..ec6f3dced41a98957194dddd53a9f7e43c4ff3d3 100644 (file)
--- 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 24c96f69ad5f60c5e7dbece5037e4308538b9a67..c191b2a155f97c9f6ba30f8a159a0b5dd900d99f 100644 (file)
--- 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 187a0f316b14336a64989e1b56ecaad53bb63bfe..ba71b043f348278a470ec3832bb543a34aff0291 100644 (file)
--- 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 0141e28487ad2ebad9b928e5e6c3ba8571d9eb52..c44cd9d674b203cc22d30c57df4ae437e3f64858 100644 (file)
--- 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 d48c1c96d1063c84bcef1a241a9a6047b25302f4..e9d8aa983de6cccab853fa9ee15a88ac09d32c91 100644 (file)
--- 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 94a295d5418fa3e465144ba4cc93f64b0afb883b..9bb96d85381c12c37eff06bf91327ab74ff3412e 100644 (file)
--- 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 1baaf21399a90e90d6d234e8f934182f0785dec0..c42415c54f8c519f2a4ba22a831f08f9a32edb06 100644 (file)
--- 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 b2ef3f1818d26a81cb661240f83abf65760fcb49..8a9dea5adcc32113e2b98326a8b26cbbea0aa3d6 100644 (file)
--- 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 adeb5761dbcafc9893c8694708435ecd351d6018..57d5e6c96aedb46f02fb69a2711f545f4cc6ad4b 100644 (file)
--- 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 9cb6b759450035496c1a40a25f0c7d45c70a7e16..82d6595663f5c676e80a4fd55e8969944bb78969 100644 (file)
--- 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 8d4af5ba17c957ccfd286b1b9e0a09d09abba35b..2ff409686cb6669aa920c03f48a2503a982647cb 100644 (file)
--- 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 7755d65f064548f750e2ba6498db1cd60bd394b0..b448cd2a614ceab0292ae6abdee75576504e1382 100644 (file)
--- 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 b2cf8bc55dd1e48c70fb0e73338ec3f385ccf9c1..3504eeba29c9edd7036a06e0e571eae0a976dffc 100644 (file)
--- 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 65d36690cce1abc0c23e5b88bf429dcd51c6c189..8c5773e32de8c467d60b0e4f55af9efa23b14d4c 100644 (file)
--- 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 6927888cfab7ce3cde4df72df7d58536338b7127..21c278a376b45aa855c31e16a6a65af8c7ec8d35 100644 (file)
--- 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 2c4f0e8b77b3ddc2f1c176db8164e3057cac3561..66d5727d659b234354a5b5fce65d4fa097f401b9 100644 (file)
--- 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 caf87428b917208ec7b55bf7cb7ff0f58e0cbc20..ffd3354532b586d9a68dae2957bc80486bac4264 100644 (file)
--- 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 21a6669d797b361646e80d668702311eacba044d..6cb818d100353dc949d628e3e141b725132dd4da 100644 (file)
--- 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 32ca9e9835deee233df674b64bdfcb724d6b1f1b..9e216b1261f106614857055c6f92ee64a1358ff2 100644 (file)
--- 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 23dc1153abb4f818ad4f83388e619c0dc62a6535..4c7f6a156af80f7f1f574bee0b64ef5ab1737abd 100644 (file)
--- 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 edcbdcca3fc443e72da73d645f3dfba917083e26..98cffb6dec5191224b6f1d1110acaec32d20f079 100644 (file)
--- 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 024d192e6d9d88421a7bd3a005e3c88a23998e7b..c4b2b8d836c882e75a3db94c911f4b2e346b1e40 100644 (file)
--- 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 21124375af5fbd7ec46d8bae3c786a57f62189b3..b695ca03d47ed3c8dd4d0541a0b8c1e8ecc2c1a4 100644 (file)
--- 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 6d0b9d91d2c09199df2242323ae607d1dad18b97..2289f2fea9d0d179205da9bb8eb171a144d2f2e5 100644 (file)
--- 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 d6d8691b2c85aa5ee6b5ca4f376ce0fed307538a..65a31743306a3e0c849bb5caed4496620426782c 100644 (file)
--- 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 a86e2021a332c6735ccae2f23667158ba74377f6..3376490391a111929db6b4965a68804b1e97fbe3 100644 (file)
--- 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 26a1ee7d4d5afe738a0ad9b246c447901b61f965..49c97e9b65b1447dcdca31cdd12b8e4dee3d6ad8 100644 (file)
--- 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 3911897f5f9e4e269e8959f5d442478797b789ae..5a5b766cb9a6aee5b8e321de30b707271739adfe 100644 (file)
--- 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 221c513f05603c2b3d3825d343be316db6c82d2c..9cc009d0176fe8aae6b556191dd0516d0ec9b557 100644 (file)
--- 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 14dc0fbd11e905eeb2c102cc5b314d2e98ccf146..800106764c6468c425c502e8f66d640adb1fe33c 100644 (file)
--- 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 ae79f920d73718c8474deb541784c4f3cbcb9ac7..36f99f4aca70174d19819b52fbfca702f89fb8a6 100644 (file)
--- 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 3a093211c76fa267d68af11ee118043240119fcf..58f9400b5e717c4a9f1f76e59d6135d9c66b30bc 100644 (file)
--- 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 d239f48ded9085b7e825d12bc87fc6262ba2f6ff..8481a8504a76c1bb406d1a952f6fed520b4ffa4b 100644 (file)
--- 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 3ec216a6a8748db1bbe4d41cee7b5a3518b0a3d4..921a9ef0d84c1c5955a4fbac92b119e565a9cdd6 100644 (file)
--- 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 cf006b3e1779c9772861f5dac5e63e1920c1a428..b79032221e9c2d0b33a32b0f2c441c70ab957f9d 100644 (file)
--- 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 8d2d113a2fcafe61f8dd0d613d39b940d90178ab..2bfbf675f2ff19d0db404ee2e33fa0b266554acc 100644 (file)
--- 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 103a3d61a8d22f8fef443bc1b7925d0c7153b247..05c74918caae80c7ff234b34b7ba24912b9267d4 100644 (file)
--- 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 43dfe8a409c5fc74dd71bdcb329dbe100d9c8aff..57ce5f3ca7a1dd617cc537a849961d0f53b63a08 100644 (file)
--- 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 8d9b93a1ecc19c78d2c5df1f544a2b046c9d9776..87686d59c363528c8788e1b2897a53700a81584f 100644 (file)
--- 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 4ac80f7726f5937d6c4ae455a0ece6b3c69197d7..633a544f03d688ee1ffc0dbda6396f4aee3e07ae 100644 (file)
--- 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 d8f321f1074f890c5a837c68875237ec781e3705..61eef32d56223907c0395dd673687bdc340f2cc9 100644 (file)
--- 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 251ef2dfe945d736569f041d9b4219caf2265d7f..6e518d52759e59c169cb8ee7ac1e9b4a35970550 100644 (file)
--- 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 c95900383a58938b0ae5364b69a311eeaa559a60..aa99c70c42f091101de0d94deda2ce0baab27fe0 100644 (file)
--- 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 dd462fdd81348db57b2410d1de7ec56dce26d648..96a30e58286c264632d5f79ae49275b902444f5f 100644 (file)
--- 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 e99cce44ddb18be0d7059e9bd0917a9aee4d43c8..4679d358c299d45f4509a10831ba8b05b13c364b 100644 (file)
--- 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>