Updated the SMT test driver. Other small changes to parser_temp.h and

smtlib.y.



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

3 files changed, 12 insertions, 17 deletions

diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 4643d50a..4d2b8e0a 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -1,23 +1,16 @@
-#include "parser_temp.h"
-#include "parser.h"
+#include "SMTParser.h"
 
 #include <iostream>
 
 using namespace std;
-using namespace klee;
-using namespace klee::expr;
-
 
 int main(int argc, char** argv) {
   if (argc != 2) {
     cout << "Usage: " << argv[0] << " <smt-filename>\n";
     return 1;
   }
+  
+  klee::expr::SMTParser smtParser(argv[1]);
 
-  CVC3::Parser* parser = new CVC3::Parser(false, argv[1]);
-  while (!parser->done()) {
-    ExprHandle e = parser->next();
-    if (!e.isNull())
-      cout << "e: " << e << "\n";
-  }
+  smtParser.Init();
 }
diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h
index 704157d9..ce0eecc8 100644
--- a/lib/SMT/parser_temp.h
+++ b/lib/SMT/parser_temp.h
@@ -27,6 +27,7 @@
 
 #include <sstream>
 #include <vector>
+#include <iostream>
 
 namespace CVC3 {
 
@@ -64,7 +65,12 @@ namespace CVC3 {
     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);
+    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;
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 72185a93..40413345 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -24,6 +24,7 @@
 */
 
 #include "parser_temp.h"
+#include "SMTParser.h"
 #include "klee/Expr.h"
 
 using namespace klee;
@@ -40,7 +41,6 @@ namespace CVC3 {
 #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
@@ -159,10 +159,6 @@ int smtliberror(const char *s)
 cmd:
     benchmark
     {
-      /*
-      EXPR = *$1;
-      delete $1;
-      */
       EXPR = $1;
       YYACCEPT;
     }