Methods getConstraintLog() and setTimeout() made virtual and moved from STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().

3 files changed, 17 insertions, 7 deletions

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) {};
 };
 
 }