aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorEric Rizzi <eric.rizzi@gmail.com>2015-09-14 14:32:37 -0400
committerDan Liew <delcypher@gmail.com>2016-11-23 20:36:44 +0000
commitf27cf86466d75c71a302abe5e0a3ffcad1670373 (patch)
treedd598d703d01fc8292afa6cc56816ec822715923 /lib/Solver
parent094a21832d94bfaa5da8ea667e646328ca0e5432 (diff)
downloadklee-f27cf86466d75c71a302abe5e0a3ffcad1670373.tar.gz
Renamed .pc to .kquery (kleaver query)
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CMakeLists.txt2
-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));
}
+