Merge branch 'master' of https://github.com/hpalikareva/klee into hpalikareva-master

5 files changed, 23 insertions, 9 deletions

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index f303ae6c..38b22c6f 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -22,7 +22,11 @@ extern llvm::cl::opt<bool> DebugValidateSolver;
   
 extern llvm::cl::opt<int> MinQueryTimeToLog;
 
-extern llvm::cl::opt<double> MaxSTPTime;
+extern llvm::cl::opt<double> MaxCoreSolverTime;
+
+extern llvm::cl::opt<bool> UseForkedCoreSolver;
+
+extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 1418f1b6..7149708a 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -22,7 +22,7 @@ namespace klee {
     const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
     const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
 
-    Solver *constructSolverChain(STPSolver *stpSolver,
+    Solver *constructSolverChain(Solver *coreSolver,
                                  std::string querySMT2LogPath,
                                  std::string baseSolverQuerySMT2LogPath,
                                  std::string queryPCLogPath,
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index 9a122c74..f589e3b3 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -102,6 +102,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 }
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 1af30870..8fe33c7c 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -194,6 +194,9 @@ namespace klee {
     //
     // FIXME: This should go into a helper class, and should handle failure.
     virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
+    
+    virtual char *getConstraintLog(const Query& query);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /// STPSolver - A complete solver based on STP.
@@ -207,15 +210,13 @@ namespace klee {
     /// be optimized into add/shift/multiply operations.
     STPSolver(bool useForkedSTP, bool optimizeDivides = true);
 
-    
-    
     /// getConstraintLog - Return the constraint log for the given state in CVC
     /// format.
-    char *getConstraintLog(const Query&);
-    
-    /// setTimeout - Set constraint solver timeout delay to the given value; 0
+    virtual char *getConstraintLog(const Query&);
+
+    /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0
     /// is off.
-    void setTimeout(double timeout);
+    virtual void setCoreSolverTimeout(double timeout);
   };
 
   /* *** */
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index e200205b..c17082a8 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -93,10 +93,17 @@ namespace klee {
     
     /// getOperationStatusCode - get the status of the last solver operation
     virtual SolverRunStatus getOperationStatusCode() = 0;
-    
+
     /// getOperationStatusString - get string representation of the operation
     /// status code
     static const char* getOperationStatusString(SolverRunStatus statusCode);
+
+    virtual char *getConstraintLog(const Query& query)  {
+        // dummy
+        return(NULL);
+    }
+
+    virtual void setCoreSolverTimeout(double timeout) {};
 };
 
 }