Code to answer satisfiability queries.

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

4 files changed, 50 insertions, 15 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index b6ac5480..22578f46 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -10,6 +10,8 @@
 #include "SMTParser.h"
 
 #include "klee/ExprBuilder.h"
+#include "klee/Solver.h"
+#include "klee/Constraints.h"
 #include "expr/Parser.h"
 
 #include <iostream>
@@ -38,7 +40,7 @@ SMTParser::SMTParser(const std::string _filename,
 		     ExprBuilder* _builder) : fileName(_filename),
 					      lineNum(1),
 					      done(false),
-					      query(NULL),
+					      satQuery(NULL),
 					      bvSize(0),
 					      queryParsed(false),
 					      builder(_builder) {
@@ -49,7 +51,7 @@ SMTParser::SMTParser(const std::string _filename,
   fvarEnvs.push(FVarEnv());
 }
 
-void SMTParser::Init() {
+void SMTParser::Parse() {
   SMTParser::parserTemp = this;
 
   void *buf = smtlib_createBuffer(smtlib_bufSize());
@@ -60,12 +62,45 @@ void SMTParser::Init() {
 }
 
 Decl* SMTParser::ParseTopLevelDecl() {
-  assert(done);
-  return new QueryCommand(assumptions, query, 
+  return new QueryCommand(assumptions, builder->Not(satQuery),
 			  std::vector<ExprHandle>(), 
 			  std::vector<const Array*>());
 }
 
+bool SMTParser::Solve() {
+  // FIXME: Support choice of solver.
+  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true;
+  Solver *S, *STP = S = 
+    UseDummySolver ? createDummySolver() : new STPSolver(true);
+  if (UseSTPQueryPCLog)
+    S = createPCLoggingSolver(S, "stp-queries.pc");
+  if (UseFastCexSolver)
+    S = createFastCexSolver(S);
+  S = createCexCachingSolver(S);
+  S = createCachingSolver(S);
+  S = createIndependentSolver(S);
+  if (0)
+    S = createValidatingSolver(S, STP);
+
+  Decl *D = this->ParseTopLevelDecl();
+  if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
+    //llvm::cout << "Query " << ":\t";
+
+    assert("FIXME: Support counterexample query commands!");
+    if (QC->Values.empty() && QC->Objects.empty()) {
+      bool result;
+      if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
+			result)) {
+	//std::cout << (result ? "VALID" : "INVALID") << "\n";
+	return result;	
+      }
+    }
+  }
+  llvm::cout << "FAIL";
+  exit(1);
+}
+
+
 // XXX: give more info
 int SMTParser::Error(const string& msg) {
   std::cerr << SMTParser::parserTemp->fileName << ":" 
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>);
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 934f0702..034c4ce4 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -36,8 +36,8 @@ int main(int argc, char** argv) {
   }
   
   klee::expr::SMTParser smtParser(argv[1], Builder);
-
-  smtParser.Init();
+  smtParser.Parse();
+  int result = smtParser.Solve();
   
-  cout << smtParser.query << "\n"; 
+  cout << (result ? "UNSAT":"SAT") << "\n"; 
 }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 28a434c9..01d3539d 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -36,9 +36,8 @@ using namespace klee::expr;
 #define PARSER SMTParser::parserTemp
 #define BUILDER SMTParser::parserTemp->builder
 #define DONE SMTParser::parserTemp->done
-#define EXPR SMTParser::parserTemp->query
 #define ASSUMPTIONS SMTParser::parserTemp->assumptions
-#define QUERY SMTParser::parserTemp->query
+#define QUERY SMTParser::parserTemp->satQuery
 
 #define ARRAYSENABLED (SMTParser::parserTemp->arraysEnabled)
 #define BVSIZE (SMTParser::parserTemp->bvSize)