diff options
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/CMakeLists.txt | 2 | ||||
-rw-r--r-- | lib/Solver/KQueryLoggingSolver.cpp (renamed from lib/Solver/PCLoggingSolver.cpp) | 39 |
2 files changed, 21 insertions, 20 deletions
diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 20da74da..1302db38 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -16,7 +16,7 @@ klee_add_component(kleaverSolver IncompleteSolver.cpp IndependentSolver.cpp MetaSMTSolver.cpp - PCLoggingSolver.cpp + KQueryLoggingSolver.cpp QueryLoggingSolver.cpp SMTLIBLoggingSolver.cpp Solver.cpp diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index 67e9be45..a0ac950c 100644 --- a/lib/Solver/PCLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -1,4 +1,4 @@ -//===-- PCLoggingSolver.cpp -----------------------------------------------===// +//===-- KQueryLoggingSolver.cpp -----------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -17,52 +17,53 @@ using namespace klee; /// -class PCLoggingSolver : public QueryLoggingSolver { +class KQueryLoggingSolver : public QueryLoggingSolver { private : ExprPPrinter *printer; - + virtual void printQuery(const Query& query, const Query* falseQuery = 0, const std::vector<const Array*>* objects = 0) { - + const ref<Expr>* evalExprsBegin = 0; const ref<Expr>* evalExprsEnd = 0; - + if (0 != falseQuery) { evalExprsBegin = &query.expr; evalExprsEnd = &query.expr + 1; } - + const Array* const *evalArraysBegin = 0; const Array* const *evalArraysEnd = 0; - + if ((0 != objects) && (false == objects->empty())) { evalArraysBegin = &((*objects)[0]); - evalArraysEnd = &((*objects)[0]) + objects->size(); + evalArraysEnd = &((*objects)[0]) + objects->size(); } - + const Query* q = (0 == falseQuery) ? &query : falseQuery; - + printer->printQuery(logBuffer, q->constraints, q->expr, evalExprsBegin, evalExprsEnd, evalArraysBegin, evalArraysEnd); } - + public: - PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) - : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), + KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) + : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), printer(ExprPPrinter::create(logBuffer)) { - } - - virtual ~PCLoggingSolver() { + } + + virtual ~KQueryLoggingSolver() { delete printer; - } + } }; /// -Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path, +Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path, int minQueryTimeToLog) { - return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog)); + return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog)); } + |