another pass

diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 73adba7e83e903c7356102f450f11d3c876eb806..96728a1d890406c6b151d309065f9cd1e7e0ebbb 100755 (executable)
--- 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 1af197f27e331eff627862851167dbf774ea3aaa..cdc7e6775e5391b4f7feea676ebf8448c94d6a50 100644 (file)
--- 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 93903c3aafb4b2091be1432ab8ee0c0b49e3581e..c18fd9652b18e453229d21703468b1856c3006db 100644 (file)
--- 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 b7c65023e47fb701d3564e6f94c7e48da07b61a6..b42773482a80301859fd4f2ebe094fe66dc3d484 100644 (file)
--- 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 473cd21f14e696206b0252ef323647358e4b5820..a66503641d48bc9a06a02fa6b5edcb8c884f6161 100644 (file)
--- 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 e5eb222fe8c9ade97ac0dded500512995ad39c6e..d24385f8eb58cd955ffbf3277fe96864f5c182bc 100644 (file)
--- 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 45b59a95ba529dc1975e0154444848a2f5f53234..944b9c62142f9b6f01ca34645e5b49023e4e26e4 100644 (file)
--- 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 1997e63d6d534753aa3f26d693ad8118ce3a5458..fce2f0b8d446ed27c412c7bebeefc40eed32d05b 100644 (file)
--- 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 95e705bcb3b648522b866033e4bfbb2c986df38e..36942d1aebbe2395eedb88097d798919613e14e9 100644 (file)
--- 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 8745adad5ec36c4505cc458d1d771b7861f2df2f..ec017253595822f9228069a87ccc652488cd76aa 100644 (file)
--- 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 ce19b0d6853a743288f49379da1780c1351b084d..792a98701dface2c1464e9f5d61363d06e9cbc91 100644 (file)
--- 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 9ca449ce77d5bd9abc78b48f7ecfa79c26654007..e92ece93dc098a7205dbd25d72e4c20f79aa5398 100644 (file)
--- 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 1c10a6663b768810b95525e6d3a3b6a8246c6084..77700096edc417e493a4a15879a804a1c8fbe841 100644 (file)
--- 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 342834e37695b336d88d1429dc0f69e8c2aeb022..a95ecb2e3539ceae92ec5a687c48084dc1989c16 100644 (file)
--- 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 5dae5b8542d9fb0521613391cc1ada2697e14808..59a3eb7a354f863866b611216dfe966ce6dbe595 100644 (file)
--- 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 c15241ebf69f2b0eb184dc3578d7d4b21816ac8f..ea14c3fa7731de5b0b235f07de4effa36f430395 100644 (file)
--- 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 a015a6b7191779690b050b07e3456f7a2cdfddf7..5d99330cae91ee7b7e97a732e435c79cd0afabd9 100644 (file)
--- 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 93855edb8b1b5f83262f5c40823cd218832eb682..8b147c6404e48c6a4b9f36bee2ba7336965e02f8 100644 (file)
--- 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 205dcf18fefa413d85bd194c86367a7a0a9ff8ba..c07b75dfad9e65e455e16270a166aced2c22a7a3 100644 (file)
--- 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 63a448b282f846a3a71733c0ee72dc19b10c49f6..e30b31b1c06dfe94ac9e036411066dba19f59dde 100644 (file)
--- 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 8bad801f47d209ca7b21cb8393be8ff32f3fbd46..debb75e7004a754ee4d7c08b725e33b8a7c8775c 100644 (file)
--- 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 90d07a47bb42d05b17cb671face96ae9447c9469..de25c55949dcc681a9693da4ab50edf227241db9 100644 (file)
--- 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 e48d6336c7970a78a354fa9ad3af12014f562a6b..de29f48c056503a7c7d73ec0588ba68f28723470 100644 (file)
--- 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 cfabd3be2e4f82d8bda5f3c229824206c18b7bbb..50f488682790ab16bb8344551b8dd6f23e3c0708 100644 (file)
--- 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 13578ec8d53816df5b9b42b085666e1954379642..00a94c1425ddcf0eca95550895956d30bcce31c2 100644 (file)
--- 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 5c50c7a3730f11ec0dca2f6fbd356fed11ce205e..935c23b08516946e1738a29236ac387f060f8135 100644 (file)
--- 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 f4e36f604dd165df25e8f68148513e4982256748..2a0841d8d795adb1ba7e315aeb29d47cabebd1fc 100644 (file)
--- 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 55fa24e5161f75f5c41ac6e1b9226231d711f0cb..1a6f3427a39638effe4b83237a234eecf5475b37 100644 (file)
--- 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 57d8a957e11649441a74df4bb538349a64c8facb..845d1eb6d0d8663abc189dd29f6875de13dbe7c1 100644 (file)
--- 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 8cf9f4a6d51c103416338475884332f8c73de287..a9560ab93f26d425869ac646900815238cb7ba9a 100644 (file)
--- 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 35ca74ecd34e2ac14edd00a84e3dc769d478ea28..89170beeb5db65c6e94d85ca2855f8a735bb60cc 100644 (file)
--- 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 4444925e2b9e1926e6b3556431ec40ee5c16e67f..6ab0ada498ce1285f64a8ea467665666186b9fd7 100644 (file)
--- 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 e9aeab78e812aa408769b4ad6128990c66bc3bc3..d8fd57c8ccc590d06d9be251af8dec2400f83c6c 100644 (file)
--- 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 d70937e3444a2e9a2df2dddba82c2b8a36eba72e..ba8a8e85d6f5fae6bbddf6102ff6d215ceaaa2b2 100644 (file)
--- 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 97f61e7159260b9c38e10d7be7e7369cdf0e2a14..0f3aa8cf4f456b28f929e7e0acc2848ac71ff1b9 100644 (file)
--- 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 b78b27a0d2ca0a773eb9e2984919c4b404e88ca3..bb5802aed46f77be571011f455b7d8dc97ae9e2f 100644 (file)
--- 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 {