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().

12 files changed, 94 insertions, 15 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) {};
 };
 
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index b13879df..2684e071 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -42,7 +42,11 @@ namespace klee {
     }
 
     void setTimeout(double t) {
-      stpSolver->setTimeout(t);
+      stpSolver->setCoreSolverTimeout(t);
+    }
+    
+    char *getConstraintLog(const Query& query) {
+      return solver->getConstraintLog(query);
     }
 
     bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5911bbf3..674d4627 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -85,6 +85,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -244,6 +246,14 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index b38df672..df7fffc5 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -83,6 +83,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query& query);
+  void setCoreSolverTimeout(double timeout);
 };
 
 ///
@@ -350,6 +352,14 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();
 }
 
+char *CexCachingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void CexCachingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 ///
 
 Solver *klee::createCexCachingSolver(Solver *_solver) {
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index 7bc8058d..dc2c9fd4 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -138,3 +138,12 @@ StagedSolverImpl::computeInitialValues(const Query& query,
 SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() {
   return secondary->impl->getOperationStatusCode();
 }
+
+char *StagedSolverImpl::getConstraintLog(const Query& query) {
+  return secondary->impl->getConstraintLog(query);
+}
+
+void StagedSolverImpl::setCoreSolverTimeout(double timeout) {
+  secondary->impl->setCoreSolverTimeout(timeout);
+}
+
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index b3ef1e57..d9fc77dc 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -285,6 +285,8 @@ public:
                                               hasSolution);
   }
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -318,6 +320,14 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() {
   return solver->impl->getOperationStatusCode();      
 }
 
+char *IndependentSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void IndependentSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createIndependentSolver(Solver *s) {
   return new Solver(new IndependentSolver(s));
 }
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 245ad3bf..e7187fc3 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -183,4 +183,11 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *QueryLoggingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
 
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 527d075b..2c7d80e8 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -70,7 +70,8 @@ public:
                               std::vector< std::vector<unsigned char> > &values,
                               bool &hasSolution);
     SolverRunStatus getOperationStatusCode();
-
+    char *getConstraintLog(const Query&);
+    void setCoreSolverTimeout(double timeout);
 };
 
 #endif	/* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index b3d1613d..3414cda2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -101,6 +101,14 @@ Solver::~Solver() {
   delete impl; 
 }
 
+char *Solver::getConstraintLog(const Query& query) {
+    return impl->getConstraintLog(query);
+}
+
+void Solver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
+}
+
 bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
@@ -307,6 +315,8 @@ public:
                             std::vector< std::vector<unsigned char> > &values,
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
+  char *getConstraintLog(const Query&);
+  void setCoreSolverTimeout(double timeout);
 };
 
 bool ValidatingSolver::computeTruth(const Query& query,
@@ -408,6 +418,14 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() {
     return solver->impl->getOperationStatusCode();
 }
 
+char *ValidatingSolver::getConstraintLog(const Query& query) {
+  return solver->impl->getConstraintLog(query);
+}
+
+void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+  solver->impl->setCoreSolverTimeout(timeout);
+}
+
 Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
   return new Solver(new ValidatingSolver(s, oracle));
 }
@@ -466,9 +484,9 @@ private:
 public:
   STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
-
+  
   char *getConstraintLog(const Query&);
-  void setTimeout(double _timeout) { timeout = _timeout; }
+  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
 
   bool computeTruth(const Query&, bool &isValid);
   bool computeValue(const Query&, ref<Expr> &result);
@@ -532,11 +550,11 @@ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
 }
 
 char *STPSolver::getConstraintLog(const Query &query) {
-  return static_cast<STPSolverImpl*>(impl)->getConstraintLog(query);  
+  return impl->getConstraintLog(query);  
 }
 
-void STPSolver::setTimeout(double timeout) {
-  static_cast<STPSolverImpl*>(impl)->setTimeout(timeout);
+void STPSolver::setCoreSolverTimeout(double timeout) {
+    impl->setCoreSolverTimeout(timeout);
 }
 
 /***/
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 47c4f07f..6c2a29e5 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -216,7 +216,7 @@ static bool EvaluateInputAST(const char *Filename,
   if (!UseDummySolver) {
     STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver);
     if (0 != MaxCoreSolverTime) {
-      stpSolver->setTimeout(MaxCoreSolverTime);    
+      stpSolver->setCoreSolverTimeout(MaxCoreSolverTime);    
     }
     STP = S = stpSolver;
   }