Removed parser_temp.h. Adapted the code to use SMTParser directly.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73215 91177308-0d34-0410-b5e6-96231b3b80d8

5 files changed, 53 insertions, 138 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index b87bbdbc..a66c2bf4 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -7,7 +7,6 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "parser_temp.h"
 #include "SMTParser.h"
 #include "expr/Parser.h"
 
@@ -26,19 +25,22 @@ extern void smtlib_switchToBuffer(void *);
 extern int smtlib_bufSize(void);
 extern void smtlib_setInteractive(bool);
 
-namespace CVC3 {
-  ParserTemp* parserTemp;
+SMTParser* SMTParser::parserTemp = NULL;
+
+SMTParser::SMTParser(const std::string filename) : fileName(filename), 
+						   lineNum(0),
+						   done(false),
+						   expr(NULL),
+						   bvSize(0),
+						   queryParsed(false) {
+  is = new ifstream(filename.c_str());
 }
 
 void SMTParser::Init() {
   cout << "Initializing parser\n";
-  void *buf = smtlib_createBuffer(smtlib_bufSize());
+  SMTParser::parserTemp = this;
 
-  CVC3::parserTemp = new CVC3::ParserTemp();
-  CVC3::parserTemp->fileName = fname;
-  CVC3::parserTemp->is = new ifstream(fname.c_str());
-  CVC3::parserTemp->interactive = false;
-  
+  void *buf = smtlib_createBuffer(smtlib_bufSize());
   smtlib_switchToBuffer(buf);
   smtlib_setInteractive(false);
   smtlibparse();
@@ -47,3 +49,10 @@ void SMTParser::Init() {
 Decl* SMTParser::ParseTopLevelDecl() {
   return NULL;
 }
+
+// XXX: give more info
+int SMTParser::Error(const string& s) {
+  std::cerr << "error: " << s << "\n";
+  exit(1);
+  return 0;
+}
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index 5abbee7b..35a0b00e 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -11,7 +11,6 @@
 #ifndef SMT_PARSER_H
 #define SMT_PARSER_H
 
-#include "parser_temp.h"
 #include "expr/Parser.h"
 
 #include <cassert>
@@ -23,12 +22,21 @@ namespace klee {
 namespace expr {
 
 class SMTParser : public klee::expr::Parser {
- private:
-  std::string fname;
-  void *buf;
+  private:
+    void *buf;
 
  public:
-  SMTParser(const std::string filename) : fname(filename) {}
+  /* For interacting w/ the actual parser, should make this nicer */
+  static SMTParser* parserTemp;
+  std::string fileName;
+  std::istream* is;
+  int lineNum;
+  bool done;
+  klee::expr::ExprHandle expr;
+  int bvSize;
+  bool queryParsed;
+    
+  SMTParser(const std::string filename);
   
   virtual klee::expr::Decl *ParseTopLevelDecl();
   
@@ -39,6 +47,8 @@ class SMTParser : public klee::expr::Parser {
   virtual ~SMTParser() {}
   
   void Init(void);
+
+  int Error(const std::string& s);
 };
 
 }
diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h
deleted file mode 100644
index ce0eecc8..00000000
--- a/lib/SMT/parser_temp.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/*****************************************************************************/
-/*!
- * \file parser_temp.h
- *
- * Author: Sergey Berezin
- *
- * Created: Wed Feb  5 17:53:02 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>
- *
- * A class used to communicate with the actual parser.  No one else
- * should use it.
- */
-/*****************************************************************************/
-
-#ifndef _cvc3__parser_temp_h_
-#define _cvc3__parser_temp_h_
-
-#include "expr/Parser.h"
-
-#include <sstream>
-#include <vector>
-#include <iostream>
-
-namespace CVC3 {
-
-  class ParserTemp {
-  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:
-    std::istream* is;
-    // The current input line
-    int lineNum;
-    // File name
-    std::string fileName;
-    // The last parsed Expr
-    klee::expr::ExprHandle 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
-    ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "),
-      prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { }
-    // Parser error handling (implemented in parser.cpp)
-    int error(const std::string& s) {
-      // FIXME: Fail better?
-      std::cerr << "error: " << s << "\n";
-      exit(1);
-      return 0;
-    }
-    // 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; }
-  };
-
-} // end of namespace CVC3
-
-#endif
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index 9f01c437..24acf56c 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -20,12 +20,11 @@
 /*****************************************************************************/
 
 #include <iostream>
-#include "parser_temp.h"
+#include "SMTParser.h"
 #include "smtlib_parser.h"
 
-namespace CVC3 {
-  extern ParserTemp* parserTemp;
-}
+using namespace klee;
+using namespace klee::expr;
 
 extern int smtlib_inputLine;
 extern char *smtlibtext;
@@ -35,17 +34,8 @@ extern int smtliberror (const char *msg);
 static int smtlibinput(std::istream& is, char* buf, int size) {
   int res;
   if(is) {
-    // If interactive, read line by line; otherwise read as much as we
-    // can gobble
-    if(CVC3::parserTemp->interactive) {
-      // Print the current prompt
-      std::cout << CVC3::parserTemp->getPrompt() << std::flush;
-      // Set the prompt to "middle of the command" one
-      CVC3::parserTemp->setPrompt2();
-      // Read the line
-      is.getline(buf, size-1);
-    } else // Set the terminator char to 0
-      is.getline(buf, size-1, 0);
+    // Set the terminator char to 0
+    is.getline(buf, size-1, 0);
     // If failbit is set, but eof is not, it means the line simply
     // didn't fit; so we clear the state and keep on reading.
     bool partialStr = is.fail() && !is.eof();
@@ -66,13 +56,13 @@ static int smtlibinput(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 = smtlibinput(*CVC3::parserTemp->is, buf, max_size);
+  result = smtlibinput(*SMTParser::parserTemp->is, buf, max_size);
 
 int smtlib_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
 
 /* some wrappers for methods that need to refer to a struct.
-   These are used by CVC3::Parser. */
+   These are used by SMTParser. */
 void *smtlib_createBuffer(int sz) {
   return (void *)smtlib_create_buffer(NULL, sz);
 }
@@ -125,7 +115,7 @@ OPCHAR	(['\.\_])
 IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 %%
 
-[\n]            { CVC3::parserTemp->lineNum++; }
+[\n]            { SMTParser::parserTemp->lineNum++; }
 [ \t\r\f]	{ /* skip whitespace */ }
 
 {DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
@@ -134,7 +124,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 
 ";"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC3::parserTemp->lineNum++; }
+                  SMTParser::parserTemp->lineNum++; }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
@@ -163,7 +153,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
                           return USER_VAL_TOK; }
 
 <USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
-                          CVC3::parserTemp->lineNum++; }
+                          SMTParser::parserTemp->lineNum++; }
 <USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }
 
 "true"          { return TRUE_TOK; }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 40413345..422c28ad 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -23,25 +23,21 @@
    commands in SMT-LIB language.
 */
 
-#include "parser_temp.h"
 #include "SMTParser.h"
 #include "klee/Expr.h"
 
+#include <sstream>
+
 using namespace klee;
 using namespace klee::expr;
 
-// Exported shared data
-namespace CVC3 {
-  extern ParserTemp* parserTemp;
-}
 // 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 QUERYPARSED CVC3::parserTemp->queryParsed
+#define TMP SMTParser::parserTemp
+#define EXPR SMTParser::parserTemp->expr
+#define ARRAYSENABLED (SMTParser::parserTemp->arrFlag)
+#define BVENABLED (SMTParser::parserTemp->bvFlag)
+#define BVSIZE (SMTParser::parserTemp->bvSize)
+#define QUERYPARSED SMTParser::parserTemp->queryParsed
 
 // Suppress the bogus warning suppression in bison (it generates
 // compile error)
@@ -53,9 +49,9 @@ extern int smtliblex(void);
 int smtliberror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
+  ss << SMTParser::parserTemp->fileName << ":" << SMTParser::parserTemp->lineNum
      << ": " << s;
-  return CVC3::parserTemp->error(ss.str());
+  return SMTParser::parserTemp->Error(ss.str());
 }