Code to answer satisfiability queries.

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

1 files changed, 7 insertions, 6 deletions

diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index 798e70b3..fd1ec044 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -38,16 +38,17 @@ class SMTParser : public klee::expr::Parser {
   bool arraysEnabled;
   
   std::vector<ExprHandle> assumptions;
-  klee::expr::ExprHandle query;
+  klee::expr::ExprHandle satQuery;
 
   int bvSize;
   bool queryParsed;
-
+  
   klee::ExprBuilder *builder;
     
   SMTParser(const std::string filename, ExprBuilder *builder);
   
   virtual klee::expr::Decl *ParseTopLevelDecl();
+  bool Solve();
   
   virtual void SetMaxErrors(unsigned N) { }
   
@@ -55,15 +56,15 @@ class SMTParser : public klee::expr::Parser {
   
   virtual ~SMTParser() {}
   
-  void Init(void);
-
+  void Parse(void);
+  
   int Error(const std::string& s);
   
   int StringToInt(const std::string& s);
   ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
-
+  
   void DeclareExpr(std::string name, Expr::Width w);
-
+  
   ExprHandle CreateAnd(std::vector<ExprHandle>);
   ExprHandle CreateOr(std::vector<ExprHandle>);
   ExprHandle CreateXor(std::vector<ExprHandle>);