fixes and additions

1 files changed, 28 insertions, 41 deletions

diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 1bc22675a..97f61e715 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -1,45 +1,34 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.y
- * 
- * Author: Clark Barrett
- * 
- * Created: Apr 30 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* 
-   This file contains the bison code for the parser that reads in CVC
-   commands in SMT-LIB language.
-*/
+%{/*******************                                           -*- 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **
+ ** This file contains the bison code for the parser that reads in CVC
+ ** commands in SMT-LIB language.
+ **/
 
 #include "vc.h"
 #include "parser_exception.h"
-#include "parser_temp.h"
+#include "parser_state.h"
 
 // Exported shared data
-namespace CVC4 {
+namespace CVC3 {
   extern ParserTemp* parserTemp;
 }
 // Define shortcuts for various things
-#define TMP CVC4::parserTemp
-#define EXPR CVC4::parserTemp->expr
-#define VC (CVC4::parserTemp->vc)
-#define ARRAYSENABLED (CVC4::parserTemp->arrFlag)
-#define BVENABLED (CVC4::parserTemp->bvFlag)
-#define BVSIZE (CVC4::parserTemp->bvSize)
-#define RAT(args) CVC4::newRational args
-#define QUERYPARSED CVC4::parserTemp->queryParsed
+#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
 
 // Suppress the bogus warning suppression in bison (it generates
 // compile error)
@@ -51,9 +40,9 @@ extern int smtliblex(void);
 int smtliberror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
      << ": " << s;
-  return CVC4::parserTemp->error(ss.str());
+  return CVC3::parserTemp->error(ss.str());
 }
 
 
@@ -66,9 +55,9 @@ int smtliberror(const char *s)
 %union {
   std::string *str;
   std::vector<std::string> *strvec;
-  CVC4::Expr *node;
-  std::vector<CVC4::Expr> *vec;
-  std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann;
+  CVC3::Expr *node;
+  std::vector<CVC3::Expr> *vec;
+  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
 };
 
 
@@ -1548,6 +1537,4 @@ fun_pred_symb:
     }
 ;
 
-
-
 %%