another pass

35 files changed, 174 insertions, 114 deletions

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 {