about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
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));
 }
+