diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/IncompleteSolver.h | 2 | ||||
-rw-r--r-- | include/klee/Solver.h | 13 | ||||
-rw-r--r-- | include/klee/SolverImpl.h | 9 |
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) {}; }; } |