diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 14 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 9 | ||||
| -rw-r--r-- | lib/Core/TimingSolver.h | 11 |
3 files changed, 16 insertions, 18 deletions
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 70c728df..c0d0ef61 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -16,13 +16,13 @@ namespace klee { - Solver *constructSolverChain(STPSolver *stpSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryPCLogPath, - std::string baseSolverQueryPCLogPath) + Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryPCLogPath, + std::string baseSolverQueryPCLogPath) { - Solver *solver = stpSolver; + Solver *solver = coreSolver; if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { @@ -55,7 +55,7 @@ namespace klee solver = createIndependentSolver(solver); if (DebugValidateSolver) - solver = createValidatingSolver(solver, stpSolver); + solver = createValidatingSolver(solver, coreSolver); if (optionIsSet(queryLoggingOptions, ALL_PC)) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 309c5fd5..b57b1956 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -251,16 +251,17 @@ Executor::Executor(const InterpreterOptions &opts, coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 ? std::min(MaxCoreSolverTime,MaxInstructionTime) : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; - STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = - constructSolverChain(stpSolver, + constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver, stpSolver); + this->solver = new TimingSolver(solver); memory = new MemoryManager(); } @@ -3280,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state, case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); + char *log = solver->getConstraintLog(query); res = std::string(log); free(log); } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 2684e071..c98dd881 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -17,15 +17,13 @@ namespace klee { class ExecutionState; - class Solver; - class STPSolver; + class Solver; /// TimingSolver - A simple class which wraps a solver and handles /// tracking the statistics that we care about. class TimingSolver { public: Solver *solver; - STPSolver *stpSolver; bool simplifyExprs; public: @@ -34,15 +32,14 @@ namespace klee { /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, STPSolver *_stpSolver, - bool _simplifyExprs = true) - : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {} + TimingSolver(Solver *_solver, bool _simplifyExprs = true) + : solver(_solver), simplifyExprs(_simplifyExprs) {} ~TimingSolver() { delete solver; } void setTimeout(double t) { - stpSolver->setCoreSolverTimeout(t); + solver->setCoreSolverTimeout(t); } char *getConstraintLog(const Query& query) { |