Renamed .pc to .kquery (kleaver query)

6 files changed, 42 insertions, 38 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 399c27a2..e55c4550 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -73,9 +73,9 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
     "use-query-log",
     llvm::cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."),
     llvm::cl::values(
-        clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
+        clEnumValN(ALL_KQUERY,"all:kquery","All queries in .kquery (KQuery) format"),
         clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
-        clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
+        clEnumValN(SOLVER_KQUERY,"solver:kquery","All queries reaching the solver in .kquery (KQuery) format"),
         clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"),
         clEnumValEnd
 	),
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index debb1e9e..68e1b08b 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -16,17 +16,18 @@
 #include "llvm/Support/raw_ostream.h"
 
 namespace klee {
-Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
+Solver *constructSolverChain(Solver *coreSolver,
+                             std::string querySMT2LogPath,
                              std::string baseSolverQuerySMT2LogPath,
-                             std::string queryPCLogPath,
-                             std::string baseSolverQueryPCLogPath) {
+                             std::string queryKQueryLogPath,
+                             std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
 
-  if (optionIsSet(queryLoggingOptions, SOLVER_PC)) {
-    solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath,
+  if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) {
+    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
                                    MinQueryTimeToLog);
-    klee_message("Logging queries that reach solver in .pc format to %s\n",
-                 baseSolverQueryPCLogPath.c_str());
+    klee_message("Logging queries that reach solver in .kquery format to %s\n",
+                 baseSolverQueryKQueryLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) {
@@ -51,10 +52,11 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath,
   if (DebugValidateSolver)
     solver = createValidatingSolver(solver, coreSolver);
 
-  if (optionIsSet(queryLoggingOptions, ALL_PC)) {
-    solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog);
-    klee_message("Logging all queries in .pc format to %s\n",
-                 queryPCLogPath.c_str());
+  if (optionIsSet(queryLoggingOptions, ALL_KQUERY)) {
+    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
+                                       MinQueryTimeToLog);
+    klee_message("Logging all queries in .kquery format to %s\n",
+                 queryKQueryLogPath.c_str());
   }
 
   if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) {
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 0981b8f4..1f3c1939 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -353,12 +353,13 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih)
   if (!coreSolver) {
     klee_error("Failed to create core solver\n");
   }
+
   Solver *solver = 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));
+      interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
+      interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
   this->solver = new TimingSolver(solver, EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index eefe443a..19ce5af7 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -67,11 +67,11 @@ Decl* SMTParser::ParseTopLevelDecl() {
 
 bool SMTParser::Solve() {
   // FIXME: Support choice of solver.
-  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true;
+  bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true;
   Solver *S, *STP = S = 
     UseDummySolver ? createDummySolver() : new STPSolver(true);
-  if (UseSTPQueryPCLog)
-    S = createPCLoggingSolver(S, "stp-queries.pc");
+  if (UseSTPQueryKQueryLog)
+    S = createKQueryLoggingSolver(S, "stp-queries.kquery");
   if (UseFastCexSolver)
     S = createFastCexSolver(S);
   S = createCexCachingSolver(S);
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));
 }
+