fixes and additions

6 files changed, 208 insertions, 228 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 0ebcad8c7..8cf9f4a6d 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -10,9 +10,26 @@ libparser_a_SOURCES = \
 	parser.cpp
 
 BUILT_SOURCES = \
-	pl_scanner.lpp \
-	pl.ypp \
-	smtlib_scanner.lpp \
-	smtlib.ypp
+	pl_scanner.cpp \
+	pl.cpp \
+	pl.h \
+	smtlib_scanner.cpp \
+	smtlib.cpp \
+	smtlib.h
+
+# produce headers too
+AM_YFLAGS = -d
+
+pl_scanner.cpp: pl_scanner.lpp
+	$(LEX) $(AM_LFLAGS) $(LFLAGS) -P PL -o $@ $<
+smtlib_scanner.cpp: smtlib_scanner.lpp
+	$(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $<
+
+pl_scanner.o: pl.h
+pl.cpp: pl.ypp
+	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $<
 
 
+smtlib_scanner.o: smtlib.h
+smtlib.cpp: smtlib.ypp
+	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $<
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
new file mode 100644
index 000000000..4444925e2
--- /dev/null
+++ b/src/parser/parser_state.h
@@ -0,0 +1,89 @@
+/*********************                                           -*- C++ -*-  */
+/** parser_state.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Extra state of the parser shared by the lexer and parser.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PARSER_STATE_H
+#define __CVC4_PARSER_STATE_H
+
+#include <iostream>
+#include <sstream>
+#include "expr.h"
+#include "exception.h"
+
+namespace CVC4 {
+
+class ValidityChecker;
+
+class ParserState {
+private:
+  // Counter for uniqueID of bound variables
+  int d_uid;
+  // The main prompt when running interactive
+  std::string prompt1;
+  // The interactive prompt in the middle of a multi-line command
+  std::string prompt2;
+  // The currently used prompt
+  std::string prompt;
+public:
+  ValidityChecker* vc;
+  std::istream* is;
+  // The current input line
+  int lineNum;
+  // File name
+  std::string fileName;
+  // The last parsed Expr
+  Expr expr;
+  // Whether we are done or not
+  bool done;
+  // Whether we are running interactive
+  bool interactive;
+  // Whether arrays are enabled for smt-lib format
+  bool arrFlag;
+  // Whether bit-vectors are enabled for smt-lib format
+  bool bvFlag;
+  // Size of bit-vectors for smt-lib format
+  int bvSize;
+  // Did we encounter a formula query (smtlib)
+  bool queryParsed;
+  // Default constructor
+  ParserState() : d_uid(0),
+                  prompt1("CVC> "),
+                  prompt2("- "),
+                  prompt("CVC> "),
+                  vc(0),
+                  is(0),
+                  lineNum(1),
+                  fileName(),
+                  expr(Expr::null()),
+                  done(false),
+                  interactive(false),
+                  arrFlag(false),
+                  bvFlag(false),
+                  bvSize(0),
+                  queryParsed(false) { }
+  // Parser error handling (implemented in parser.cpp)
+  int error(const std::string& s);
+  // Get the next uniqueID as a string
+  std::string uniqueID() {
+    std::ostringstream ss;
+    ss << d_uid++;
+    return ss.str();
+  }
+  // Get the current prompt
+  std::string getPrompt() { return prompt; }
+  // Set the prompt to the main one
+  void setPrompt1() { prompt = prompt1; }
+  // Set the prompt to the secondary one
+  void setPrompt2() { prompt = prompt2; }
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_STATE_H */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index dfed55dbb..e9aeab78e 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -1,43 +1,32 @@
+/*********************                                           -*- 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 the presentation language (hence "PL").
+ **/
+
 %{
-/*****************************************************************************/
-/*!
- * \file PL.y
- * 
- * Author: Sergey Berezin
- * 
- * Created: Feb 06 03:00:43 GMT 2003
- *
- * <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>
- * 
- */
-/*****************************************************************************/
-/* PL.y
-   Aaron Stump, 4/14/01
-
-   This file contains the bison code for the parser that reads in CVC
-   commands in the presentation language (hence "PL").
-*/
 
 #include "vc.h"
 #include "parser_exception.h"
-#include "parser_temp.h"
-#include "rational.h"
+#include "parser_state.h"
+//#include "rational.h"
 
 // Exported shared data
 namespace CVC4 {
-  extern ParserTemp* parserTemp;
+  extern ParserState* parserState;
 }
 // Define shortcuts for various things
-#define TMP CVC4::parserTemp
-#define EXPR CVC4::parserTemp->expr
-#define VC (CVC4::parserTemp->vc)
+#define TMP CVC4::parserState
+#define EXPR CVC4::parserState->expr
+#define VC (CVC4::parserState->vc)
 #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -50,9 +39,9 @@ extern int PLlex(void);
 int PLerror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
      << ": " << s;
-  return CVC4::parserTemp->error(ss.str());
+  return CVC4::parserState->error(ss.str());
 }
 
 
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index d203a1e9a..d70937e34 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -1,76 +1,34 @@
+/*********************                                           -*- 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+%option prefix="PL"
+
 %{
-/*****************************************************************************/
-/*!
- * \file PL.lex
- * 
- * Author: Sergey Berezin
- * 
- * Created: Feb 06 03:00:43 GMT 2003
- *
- * <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>
- * 
- */
-/*****************************************************************************/
 
 #include <iostream>
-#include "parser_temp.h"
 #include "expr_manager.h" /* for the benefit of parsePL_defs.h */
-#include "parsePL_defs.h"
+#include "parser_state.h"
+#include "pl.h"
 #include "debug.h"
 
 namespace CVC4 {
-  extern ParserTemp* parserTemp;
+  extern ParserState* parserState;
 }
 
-/* prefixing hack from gdb (via automake docs) */
-#define	yymaxdepth PL_maxdepth
-#define	yyparse	PL_parse
-#define	yylex	PL_lex
-#define	yyerror	PL_error
-#define	yylval	PL_lval
-#define	yychar	PL_char
-#define	yydebug	PL_debug
-#define	yypact	PL_pact	
-#define	yyr1	PL_r1			
-#define	yyr2	PL_r2			
-#define	yydef	PL_def		
-#define	yychk	PL_chk		
-#define	yypgo	PL_pgo		
-#define	yyact	PL_act		
-#define	yyexca	PL_exca
-#define yyerrflag PL_errflag
-#define yynerrs	PL_nerrs
-#define	yyps	PL_ps
-#define	yypv	PL_pv
-#define	yys	PL_s
-#define	yy_yys	PL_yys
-#define	yystate	PL_state
-#define	yytmp	PL_tmp
-#define	yyv	PL_v
-#define	yy_yyv	PL_yyv
-#define	yyval	PL_val
-#define	yylloc	PL_lloc
-#define yyreds	PL_reds
-#define yytoks	PL_toks
-#define yylhs	PL_yylhs
-#define yylen	PL_yylen
-#define yydefred PL_yydefred
-#define yydgoto	PL_yydgoto
-#define yysindex PL_yysindex
-#define yyrindex PL_yyrindex
-#define yygindex PL_yygindex
-#define yytable	 PL_yytable
-#define yycheck	 PL_yycheck
-#define yyname   PL_yyname
-#define yyrule   PL_yyrule
-
 extern int PL_inputLine;
 extern char *PLtext;
 
@@ -81,11 +39,11 @@ static int PLinput(std::istream& is, char* buf, int size) {
   if(is) {
     // If interactive, read line by line; otherwise read as much as we
     // can gobble
-    if(CVC4::parserTemp->interactive) {
+    if(CVC4::parserState->interactive) {
       // Print the current prompt
-      std::cout << CVC4::parserTemp->getPrompt() << std::flush;
+      std::cout << CVC4::parserState->getPrompt() << std::flush;
       // Set the prompt to "middle of the command" one
-      CVC4::parserTemp->setPrompt2();
+      CVC4::parserState->setPrompt2();
       // Read the line
       is.getline(buf, size-1);
     } else // Set the terminator char to 0
@@ -110,7 +68,7 @@ static int PLinput(std::istream& is, char* buf, int size) {
 
 // Redefine the input buffer function to read from an istream
 #define YY_INPUT(buf,result,max_size) \
-  result = PLinput(*CVC4::parserTemp->is, buf, max_size);
+  result = PLinput(*CVC4::parserState->is, buf, max_size);
 
 int PL_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
@@ -152,13 +110,6 @@ static std::string _string_lit;
 
 %}
 
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
 %x	COMMENT
 %x	STRING_LITERAL
 
@@ -171,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 
-[\n]            { CVC4::parserTemp->lineNum++; }
+[\n]            { CVC4::parserState->lineNum++; }
 
 [ \t\r\f]	{ /* skip whitespace */ }
 
@@ -184,7 +135,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 "%"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parserTemp->lineNum++; }
+                  CVC4::parserState->lineNum++; }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
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:
     }
 ;
 
-
-
 %%
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index d5bdaaf26..b78b27a0d 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -1,76 +1,31 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.lex
- * 
- * Author: Clark Barrett
- * 
- * Created: 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>
- * 
- */
-/*****************************************************************************/
+/*********************                                           -*- 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
 
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+%option prefix="smtlib"
+
+%{
 #include <iostream>
-#include "parser_temp.h"
-#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
-#include "parsesmtlib_defs.h"
+#include "smtlib.h"
 #include "debug.h"
 
 namespace CVC4 {
   extern ParserTemp* parserTemp;
 }
 
-/* prefixing hack from gdb (via automake docs) */
-#define	yymaxdepth smtlib_maxdepth
-#define	yyparse	smtlib_parse
-#define	yylex	smtlib_lex
-#define	yyerror	smtlib_error
-#define	yylval	smtlib_lval
-#define	yychar	smtlib_char
-#define	yydebug	smtlib_debug
-#define	yypact	smtlib_pact	
-#define	yyr1	smtlib_r1			
-#define	yyr2	smtlib_r2			
-#define	yydef	smtlib_def		
-#define	yychk	smtlib_chk		
-#define	yypgo	smtlib_pgo		
-#define	yyact	smtlib_act		
-#define	yyexca	smtlib_exca
-#define yyerrflag smtlib_errflag
-#define yynerrs	smtlib_nerrs
-#define	yyps	smtlib_ps
-#define	yypv	smtlib_pv
-#define	yys	smtlib_s
-#define	yy_yys	smtlib_yys
-#define	yystate	smtlib_state
-#define	yytmp	smtlib_tmp
-#define	yyv	smtlib_v
-#define	yy_yyv	smtlib_yyv
-#define	yyval	smtlib_val
-#define	yylloc	smtlib_lloc
-#define yyreds	smtlib_reds
-#define yytoks	smtlib_toks
-#define yylhs	smtlib_yylhs
-#define yylen	smtlib_yylen
-#define yydefred smtlib_yydefred
-#define yydgoto	smtlib_yydgoto
-#define yysindex smtlib_yysindex
-#define yyrindex smtlib_yyrindex
-#define yygindex smtlib_yygindex
-#define yytable	 smtlib_yytable
-#define yycheck	 smtlib_yycheck
-#define yyname   smtlib_yyname
-#define yyrule   smtlib_yyrule
-
 extern int smtlib_inputLine;
 extern char *smtlibtext;
 
@@ -152,13 +107,6 @@ static std::string _string_lit;
 
 %}
 
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
 %x	COMMENT
 %x	STRING_LITERAL
 %x      USER_VALUE
@@ -257,4 +205,3 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 
 . { smtliberror("Illegal input character."); }
 %%
-