Changed SMTParser to return the parsed QueryCommand.

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

2 files changed, 13 insertions, 5 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index a66c2bf4..88d0a6c9 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -13,6 +13,7 @@
 #include <iostream>
 #include <fstream>
 #include <cstring>
+#include <cassert>
 
 using namespace std;
 using namespace klee;
@@ -28,26 +29,29 @@ extern void smtlib_setInteractive(bool);
 SMTParser* SMTParser::parserTemp = NULL;
 
 SMTParser::SMTParser(const std::string filename) : fileName(filename), 
-						   lineNum(0),
+						   lineNum(1),
 						   done(false),
-						   expr(NULL),
+						   query(NULL),
 						   bvSize(0),
 						   queryParsed(false) {
   is = new ifstream(filename.c_str());
 }
 
 void SMTParser::Init() {
-  cout << "Initializing parser\n";
   SMTParser::parserTemp = this;
 
   void *buf = smtlib_createBuffer(smtlib_bufSize());
   smtlib_switchToBuffer(buf);
   smtlib_setInteractive(false);
   smtlibparse();
+  cout << "Parsed successfully.\n";
 }
 
 Decl* SMTParser::ParseTopLevelDecl() {
-  return NULL;
+  assert(done);
+  return new QueryCommand(assumptions, query, 
+			  std::vector<ExprHandle>(), 
+			  std::vector<const Array*>());
 }
 
 // XXX: give more info
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index 35a0b00e..edc1258f 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -32,7 +32,11 @@ class SMTParser : public klee::expr::Parser {
   std::istream* is;
   int lineNum;
   bool done;
-  klee::expr::ExprHandle expr;
+  bool arraysEnabled;
+  
+  std::vector<ExprHandle> assumptions;
+  klee::expr::ExprHandle query;
+
   int bvSize;
   bool queryParsed;