From 7293554b109742697d4d928ed7b58acadc6de947 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 17 Nov 2009 08:39:27 +0000 Subject: [PATCH] another pass --- contrib/update-copyright.pl | 168 ++++++++++++++++++++++++--------- src/core/expr.cpp | 9 +- src/core/expr_manager.cpp | 7 +- src/core/expr_value.cpp | 11 ++- src/include/assert.h | 6 +- src/include/attr_type.h | 6 +- src/include/command.h | 6 +- src/include/context.h | 6 +- src/include/debug.h | 6 +- src/include/decision_engine.h | 10 +- src/include/exception.h | 9 +- src/include/expr.h | 9 +- src/include/expr_attribute.h | 6 +- src/include/expr_builder.h | 6 +- src/include/expr_manager.h | 6 +- src/include/expr_value.h | 11 ++- src/include/kind.h | 6 +- src/include/literal.h | 6 +- src/include/model.h | 6 +- src/include/parser.h | 9 +- src/include/parser_exception.h | 11 ++- src/include/prop_engine.h | 6 +- src/include/prover.h | 6 +- src/include/result.h | 6 +- src/include/sat.h | 6 +- src/include/theory.h | 6 +- src/include/theory_engine.h | 6 +- src/include/unique_id.h | 6 +- src/include/vc.h | 6 +- src/parser/Makefile.am | 8 +- src/parser/parser.cpp | 5 + src/parser/parser_state.h | 5 + src/parser/pl.ypp | 9 +- src/parser/pl_scanner.lpp | 11 ++- src/parser/smtlib.ypp | 39 ++++---- src/parser/smtlib_scanner.lpp | 11 ++- 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 <) { - next if !m,^ \*\* ,; +$_ = ; 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 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 #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 *strvec; - CVC3::Expr *node; - std::vector *vec; - std::pair, std::vector > *pat_ann; + CVC4::Expr *node; + std::vector *vec; + std::pair, std::vector > *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 -#include "smtlib.h" +#include "smtlib.hpp" #include "debug.h" namespace CVC4 { -- 2.30.2