From 4a426569a38760b9ecf34af46b4eeca76e21e8e6 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 18:25:16 +0100 Subject: TimingSolver and constructSolverChain() no longer coupled with pointers to STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver. --- tools/kleaver/main.cpp | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) (limited to 'tools/kleaver/main.cpp') diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 6c2a29e5..accc48e4 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -211,25 +211,19 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *S = 0; - Solver *STP = 0; + Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + if (!UseDummySolver) { - STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver); if (0 != MaxCoreSolverTime) { - stpSolver->setCoreSolverTimeout(MaxCoreSolverTime); + coreSolver->setCoreSolverTimeout(MaxCoreSolverTime); } - STP = S = stpSolver; - } - else { - STP = S = createDummySolver(); } - S= constructSolverChain((STPSolver*) STP, - getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); - + Solver *S = constructSolverChain(coreSolver, + getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); unsigned Index = 0; for (std::vector::iterator it = Decls.begin(), -- cgit 1.4.1