diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/TimingSolver.h | 6 | ||||
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 10 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 10 | ||||
-rw-r--r-- | lib/Solver/IncompleteSolver.cpp | 9 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 10 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 7 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 3 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 28 |
8 files changed, 76 insertions, 7 deletions
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); } /***/ |