another pass

36 files changed, 296 insertions, 160 deletions

diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 73adba7e8..96728a1d8 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -1,61 +1,137 @@
-#!/bin/bash
+#!/usr/bin/perl -w
+#
+# 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.
+#
+# It ignores any file/directory not starting with [a-zA-Z]
+# (so, this includes . and .., vi swaps, .svn meta-info,
+# .deps, etc.)
+#
+# It ignores any file not ending with one of:
+#   .c .cc .cpp .C .h .hh .hpp .H .y .yy .ypp .Y .l .ll .lpp .L
+# (so, this includes emacs ~-backups, CVS detritus, etc.)
+#
+# It ignores any directory matching $excluded_directories
+# (so, you should add here any sources imported but not covered under
+# the license.)
 
-cd `dirname "$0"`/../src
+my $excluded_directories = '^(minisat|CVS)$';
 
-cat <<EOF
+# Years of copyright for the template.  E.g., the string
+# "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
+my $years = '2009';
+
+## end config ##
+
+use strict;
+use Fcntl ':mode';
+
+my $dir = $0;
+$dir =~ s,/[^/]+/*$,,;
+
+(chdir($dir."/..") && -f "src/include/expr.h") || die "can't find top-level source directory for CVC4";
+my $pwd = `pwd`; chomp $pwd;
+
+print <<EOF;
 Warning: this script is dangerous.  It will overwrite the header comments in your
 source files to match the template in the script, attempting to retain file-specific
 comments, but this isn't guaranteed.  You should run this in an svn working directory
 and run "svn diff" after to ensure everything was correctly rewritten.
 
 The directory to search for and change sources is:
-  $(pwd)
+  $pwd/src
 
 Continue? y or n:
 EOF
 
-read x
-if [ "$x" != 'y' -a "$x" != 'Y' -a "$x" != 'YES' -a "$x" != 'yes' ]; then
-  echo Aborting operation.
-  exit
-fi
-
-echo Updating sources...
-
-for FILE in $(find . -name '*.cpp' -o -name '*.h' -o -name '*.c' -o -name '*.cc' -o -name '*.hh' -o -name '*.hpp'); do
-echo $FILE
-
-perl -i -e '\
-if(m,^/\*\*\*\*\*,) {
-  print "/*********************                                           -*- C++ -*-  */\n";
-  print "/** (basename FILE)\n";
-  print " ** This file is part of the CVC4 prototype.\n";
-  print " ** Copyright (c) (date +%Y) The Analysis of Computer Systems Group (ACSys)\n";
-  print " ** Courant Institute of Mathematical Sciences\n";
-  print " ** New York University\n";
-  print " ** See the file COPYING in the top-level source directory for licensing\n";
-  print " ** information.\n";
-  print " **\n";
-  print " ** [[ Add file-specific comments here ]]\n";
-  print " **/\n\n";
-} else {
-  m,^/\*\* , || exit;
-  print "/*********************                                           -*- C++ -*-  */\n";
-  print "/** (basename FILE)\n";
-  print " ** This file is part of the CVC4 prototype.\n";
-  print " ** Copyright (c) $(date +%Y) The Analysis of Computer Systems Group (ACSys)\n";
-  print " ** Courant Institute of Mathematical Sciences\n";
-  print " ** New York University\n";
-  print " ** See the file COPYING in the top-level source directory for licensing\n";
-  print " ** information.\n";
-  print " **\n";
-  while(<>) {
-    next if !m,^ \*\* ,;
+$_ = <STDIN>; chomp;
+die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' );
+
+print "Updating sources...\n";
+
+recurse('src');
+
+sub recurse {
+  my ($srcdir) = @_;
+  opendir(my $DIR, $srcdir);
+  while(my $file = readdir $DIR) {
+    next if !($file =~ /^[a-zA-Z]/);
+
+    my $mode = (stat($srcdir.'/'.$file))[2];
+    my $is_directory = S_ISDIR($mode);
+    if($is_directory) {
+      next if $file =~ /$excluded_directories/;
+      recurse($srcdir.'/'.$file);
+    } else {
+      next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L)$/);
+      print "$srcdir/$file...";
+      my $infile = $srcdir.'/'.$file;
+      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";
+      $_ = <$IN>;
+      if(m,^(%{)?/\*\*\*\*\*,) {
+        print "updating\n";
+        if($file =~ /\.(y|yy|ypp|Y)$/) {
+          print $OUT "%{/*******************                                           -*- C++ -*-  */\n";
+        } else {
+          print $OUT "/*********************                                           -*- C++ -*-  */\n";
+        }
+        print $OUT "/** $file\n";
+        print $OUT " ** This file is part of the CVC4 prototype.\n";
+        print $OUT " ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)\n";
+        print $OUT " ** Courant Institute of Mathematical Sciences\n";
+        print $OUT " ** New York University\n";
+        print $OUT " ** See the file COPYING in the top-level source directory for licensing\n";
+        print $OUT " ** information.\n";
+        print $OUT " **\n";
+        while(my $line = <$IN>) {
+          last if $line =~ /^ \*\*\s*$/;
+        }
+      } else {
+        print "adding\n";
+        if($file =~ /\.(y|yy|ypp|Y)$/) {
+          print $OUT "%{/*******************                                           -*- C++ -*-  */\n";
+        } else {
+          print $OUT "/*********************                                           -*- C++ -*-  */\n";
+        }
+        print $OUT "/** $file\n";
+        print $OUT " ** This file is part of the CVC4 prototype.\n";
+        print $OUT " ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)\n";
+        print $OUT " ** Courant Institute of Mathematical Sciences\n";
+        print $OUT " ** New York University\n";
+        print $OUT " ** See the file COPYING in the top-level source directory for licensing\n";
+        print $OUT " ** information.\n";
+        print $OUT " **\n";
+        print $OUT " ** [[ Add file-specific comments here ]]\n";
+        print $OUT " **/\n\n";
+        if($file =~ /\.(y|yy|ypp|Y)$/) {
+          while(my $line = <$IN>) {
+            chomp $line;
+            if($line =~ '\s*%{(.*)') {
+              print $OUT "$1\n";
+              last;
+            }
+            # just in case something's weird with the file ?
+            if(!($line =~ '\s*')) {
+              print $OUT "$line\n";
+              last;
+            }
+          }
+        }
+      }
+      while(my $line = <$IN>) {
+        print $OUT $line;
+      }
+      close $IN;
+      close $OUT;
+      rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'";
+    }
   }
+  closedir $DIR;
 }
-while(<>) {
-  print;
-}' "$FILE"
-
-done
 
+### Local Variables:
+### perl-indent-level: 2
+### End:
diff --git a/src/core/expr.cpp b/src/core/expr.cpp
index 1af197f27..cdc7e6775 100644
--- a/src/core/expr.cpp
+++ b/src/core/expr.cpp
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** expr.cpp
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
 #include "expr.h"
diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp
index 93903c3aa..c18fd9652 100644
--- a/src/core/expr_manager.cpp
+++ b/src/core/expr_manager.cpp
@@ -1,10 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_manager.cpp
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Expression manager implementation.
  **/
 
 #include <vector>
diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp
index b7c65023e..b42773482 100644
--- a/src/core/expr_value.cpp
+++ b/src/core/expr_value.cpp
@@ -1,16 +1,17 @@
-/*********************
+/*********************                                           -*- C++ -*-  */
 /** expr_value.cpp
  ** 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.
  **
  ** An expression node.
  **
  ** Instances of this class are generally referenced through
  ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
  ** reference count on ExprValue instances and
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
  **/
 
 #include "expr_value.h"
diff --git a/src/include/assert.h b/src/include/assert.h
index 473cd21f1..a66503641 100644
--- a/src/include/assert.h
+++ b/src/include/assert.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** assert.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_ASSERT_H
diff --git a/src/include/attr_type.h b/src/include/attr_type.h
index e5eb222fe..d24385f8e 100644
--- a/src/include/attr_type.h
+++ b/src/include/attr_type.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** attr_type.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_ATTR_TYPE_H
diff --git a/src/include/command.h b/src/include/command.h
index 45b59a95b..944b9c621 100644
--- a/src/include/command.h
+++ b/src/include/command.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** command.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_COMMAND_H
diff --git a/src/include/context.h b/src/include/context.h
index 1997e63d6..fce2f0b8d 100644
--- a/src/include/context.h
+++ b/src/include/context.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** context.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_CONTEXT_H
diff --git a/src/include/debug.h b/src/include/debug.h
index 95e705bcb..36942d1ae 100644
--- a/src/include/debug.h
+++ b/src/include/debug.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** debug.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_DEBUG_H
diff --git a/src/include/decision_engine.h b/src/include/decision_engine.h
index 8745adad5..ec0172535 100644
--- a/src/include/decision_engine.h
+++ b/src/include/decision_engine.h
@@ -1,17 +1,19 @@
 /*********************                                           -*- C++ -*-  */
 /** decision_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
-#include "literal.h"
-
 #ifndef __CVC4_DECISION_ENGINE_H
 #define __CVC4_DECISION_ENGINE_H
 
+#include "literal.h"
+
 namespace CVC4 {
 
 // In terms of abstraction, this is below (and provides services to)
diff --git a/src/include/exception.h b/src/include/exception.h
index ce19b0d68..792a98701 100644
--- a/src/include/exception.h
+++ b/src/include/exception.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** exception.h
  ** This file is part of the CVC4 prototype.
- **
- ** Exception class.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Exception class.
  **/
 
 #ifndef __CVC4_EXCEPTION_H
diff --git a/src/include/expr.h b/src/include/expr.h
index 9ca449ce7..e92ece93d 100644
--- a/src/include/expr.h
+++ b/src/include/expr.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** expr.h
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
 #ifndef __CVC4_EXPR_H
diff --git a/src/include/expr_attribute.h b/src/include/expr_attribute.h
index 1c10a6663..77700096e 100644
--- a/src/include/expr_attribute.h
+++ b/src/include/expr_attribute.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_attribute.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_ATTRIBUTE_H
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
index 342834e37..a95ecb2e3 100644
--- a/src/include/expr_builder.h
+++ b/src/include/expr_builder.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_builder.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_BUILDER_H
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
index 5dae5b854..59a3eb7a3 100644
--- a/src/include/expr_manager.h
+++ b/src/include/expr_manager.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** expr_manager.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_EXPR_MANAGER_H
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
index c15241ebf..ea14c3fa7 100644
--- a/src/include/expr_value.h
+++ b/src/include/expr_value.h
@@ -1,16 +1,17 @@
-/*********************
+/*********************                                           -*- C++ -*-  */
 /** expr_value.h
  ** 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.
  **
  ** An expression node.
  **
  ** Instances of this class are generally referenced through
  ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
  ** reference count on ExprValue instances and
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
  **/
 
 #ifndef __CVC4_EXPR_VALUE_H
diff --git a/src/include/kind.h b/src/include/kind.h
index a015a6b71..5d99330ca 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** kind.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_KIND_H
diff --git a/src/include/literal.h b/src/include/literal.h
index 93855edb8..8b147c640 100644
--- a/src/include/literal.h
+++ b/src/include/literal.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** literal.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_LITERAL_H
diff --git a/src/include/model.h b/src/include/model.h
index 205dcf18f..c07b75dfa 100644
--- a/src/include/model.h
+++ b/src/include/model.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** model.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_MODEL_H
diff --git a/src/include/parser.h b/src/include/parser.h
index 63a448b28..e30b31b1c 100644
--- a/src/include/parser.h
+++ b/src/include/parser.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** parser.h
  ** This file is part of the CVC4 prototype.
- **
- ** Parser abstraction.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Parser abstraction.
  **/
 
 #ifndef __CVC4_PARSER_H
diff --git a/src/include/parser_exception.h b/src/include/parser_exception.h
index 8bad801f4..debb75e70 100644
--- a/src/include/parser_exception.h
+++ b/src/include/parser_exception.h
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
-/** exception.h
+/** parser_exception.h
  ** This file is part of the CVC4 prototype.
- **
- ** Exception class.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Exception class.
  **/
 
 #ifndef __CVC4_PARSER_EXCEPTION_H
diff --git a/src/include/prop_engine.h b/src/include/prop_engine.h
index 90d07a47b..de25c5594 100644
--- a/src/include/prop_engine.h
+++ b/src/include/prop_engine.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** prop_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_PROP_ENGINE_H
diff --git a/src/include/prover.h b/src/include/prover.h
index e48d6336c..de29f48c0 100644
--- a/src/include/prover.h
+++ b/src/include/prover.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** prover.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_PROVER_H
diff --git a/src/include/result.h b/src/include/result.h
index cfabd3be2..50f488682 100644
--- a/src/include/result.h
+++ b/src/include/result.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** result.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_RESULT_H
diff --git a/src/include/sat.h b/src/include/sat.h
index 13578ec8d..00a94c142 100644
--- a/src/include/sat.h
+++ b/src/include/sat.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** sat.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_SAT_H
diff --git a/src/include/theory.h b/src/include/theory.h
index 5c50c7a37..935c23b08 100644
--- a/src/include/theory.h
+++ b/src/include/theory.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** theory.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_THEORY_H
diff --git a/src/include/theory_engine.h b/src/include/theory_engine.h
index f4e36f604..2a0841d8d 100644
--- a/src/include/theory_engine.h
+++ b/src/include/theory_engine.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** theory_engine.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_THEORY_ENGINE_H
diff --git a/src/include/unique_id.h b/src/include/unique_id.h
index 55fa24e51..1a6f3427a 100644
--- a/src/include/unique_id.h
+++ b/src/include/unique_id.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** unique_id.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_UNIQUE_ID_H
diff --git a/src/include/vc.h b/src/include/vc.h
index 57d8a957e..845d1eb6d 100644
--- a/src/include/vc.h
+++ b/src/include/vc.h
@@ -1,10 +1,12 @@
 /*********************                                           -*- C++ -*-  */
 /** vc.h
  ** This file is part of the CVC4 prototype.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
  **/
 
 #ifndef __CVC4_VC_H
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 8cf9f4a6d..a9560ab93 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -12,10 +12,10 @@ libparser_a_SOURCES = \
 BUILT_SOURCES = \
 	pl_scanner.cpp \
 	pl.cpp \
-	pl.h \
+	pl.hpp \
 	smtlib_scanner.cpp \
 	smtlib.cpp \
-	smtlib.h
+	smtlib.hpp
 
 # produce headers too
 AM_YFLAGS = -d
@@ -25,11 +25,11 @@ pl_scanner.cpp: pl_scanner.lpp
 smtlib_scanner.cpp: smtlib_scanner.lpp
 	$(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $<
 
-pl_scanner.o: pl.h
+pl_scanner.o: pl.hpp
 pl.cpp: pl.ypp
 	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $<
 
 
-smtlib_scanner.o: smtlib.h
+smtlib_scanner.o: smtlib.hpp
 smtlib.cpp: smtlib.ypp
 	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $<
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 35ca74ecd..89170beeb 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -1,6 +1,11 @@
 /*********************                                           -*- C++ -*-  */
 /** parser.cpp
  ** 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.
  **
  ** Parser implementation.
  **
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 4444925e2..6ab0ada49 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -1,6 +1,11 @@
 /*********************                                           -*- C++ -*-  */
 /** parser_state.h
  ** 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.
  **
  ** Extra state of the parser shared by the lexer and parser.
  **
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index e9aeab78e..d8fd57c8c 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -1,12 +1,11 @@
 /*********************                                           -*- C++ -*-  */
-/** smtlib.ypp
+/** pl.ypp
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
  **
  ** This file contains the bison code for the parser that reads in CVC
  ** commands in the presentation language (hence "PL").
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index d70937e34..ba8a8e85d 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** pl_scanner.lpp
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** CVC4 presentation language lexer.
  **/
 
 %option interactive
@@ -22,7 +23,7 @@
 #include <iostream>
 #include "expr_manager.h" /* for the benefit of parsePL_defs.h */
 #include "parser_state.h"
-#include "pl.h"
+#include "pl.hpp"
 #include "debug.h"
 
 namespace CVC4 {
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 97f61e715..0f3aa8cf4 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -1,12 +1,11 @@
-%{/*******************                                           -*- C++ -*-  */
+%{/*********************                                         -*- C++ -*-  */
 /** smtlib.ypp
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
  **
  ** This file contains the bison code for the parser that reads in CVC
  ** commands in SMT-LIB language.
@@ -17,18 +16,18 @@
 #include "parser_state.h"
 
 // Exported shared data
-namespace CVC3 {
-  extern ParserTemp* parserTemp;
+namespace CVC4 {
+  extern ParserState* parserState;
 }
 // Define shortcuts for various things
-#define TMP CVC3::parserTemp
-#define EXPR CVC3::parserTemp->expr
-#define VC (CVC3::parserTemp->vc)
-#define ARRAYSENABLED (CVC3::parserTemp->arrFlag)
-#define BVENABLED (CVC3::parserTemp->bvFlag)
-#define BVSIZE (CVC3::parserTemp->bvSize)
-#define RAT(args) CVC3::newRational args
-#define QUERYPARSED CVC3::parserTemp->queryParsed
+#define TMP CVC4::parserState
+#define EXPR CVC4::parserState->expr
+#define VC (CVC4::parserState->vc)
+#define ARRAYSENABLED (CVC4::parserState->arrFlag)
+#define BVENABLED (CVC4::parserState->bvFlag)
+#define BVSIZE (CVC4::parserState->bvSize)
+#define RAT(args) CVC4::newRational args
+#define QUERYPARSED CVC4::parserState->queryParsed
 
 // Suppress the bogus warning suppression in bison (it generates
 // compile error)
@@ -40,9 +39,9 @@ extern int smtliblex(void);
 int smtliberror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
+  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
      << ": " << s;
-  return CVC3::parserTemp->error(ss.str());
+  return CVC4::parserState->error(ss.str());
 }
 
 
@@ -55,9 +54,9 @@ int smtliberror(const char *s)
 %union {
   std::string *str;
   std::vector<std::string> *strvec;
-  CVC3::Expr *node;
-  std::vector<CVC3::Expr> *vec;
-  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
+  CVC4::Expr *node;
+  std::vector<CVC4::Expr> *vec;
+  std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann;
 };
 
 
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index b78b27a0d..bb5802aed 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -1,12 +1,13 @@
 /*********************                                           -*- C++ -*-  */
 /** smtlib_scanner.lpp
  ** This file is part of the CVC4 prototype.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **
- ** The Analysis of Computer Systems Group (ACSys)
+ ** 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.
+ **
+ ** Lexer for smtlib format.
  **/
 
 %option interactive
@@ -19,7 +20,7 @@
 
 %{
 #include <iostream>
-#include "smtlib.h"
+#include "smtlib.hpp"
 #include "debug.h"
 
 namespace CVC4 {