Renamed .pc to .kquery (kleaver query)

6 files changed, 12 insertions, 12 deletions

diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h
index 6cce8031..9319b487 100644
--- a/include/expr/Lexer.h
+++ b/include/expr/Lexer.h
@@ -72,7 +72,7 @@ namespace expr {
     void dump();
   };
 
-  /// Lexer - Interface for lexing tokens from a .pc language file.
+  /// Lexer - Interface for lexing tokens from a .kquery language file.
   class Lexer {
     const char *BufferPos;      /// The current lexer position.
     const char *BufferEnd;      /// The buffer end position.
diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index a9133e9d..fa07bae2 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -202,7 +202,7 @@ namespace expr {
     static bool classof(const QueryCommand *) { return true; }
   };
   
-  /// Parser - Public interface for parsing a .pc language file.
+  /// Parser - Public interface for parsing a .kquery language file.
   class Parser {
   protected:
     Parser();
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index dc69de6e..95aa51e0 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -32,9 +32,9 @@ extern llvm::cl::opt<bool> CoreSolverOptimizeDivides;
 ///The different query logging solvers that can switched on/off
 enum QueryLoggingSolverType
 {
-    ALL_PC,       ///< Log all queries (un-optimised) in .pc (KQuery) format
+    ALL_KQUERY,   ///< Log all queries (un-optimised) in .kquery (KQuery) format
     ALL_SMTLIB,   ///< Log all queries (un-optimised)  .smt2 (SMT-LIBv2) format
-    SOLVER_PC,    ///< Log queries passed to solver (optimised) in .pc (KQuery) format
+    SOLVER_KQUERY,///< Log queries passed to solver (optimised) in .kquery (KQuery) format
     SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
 };
 
diff --git a/include/klee/Common.h b/include/klee/Common.h
index 7149708a..5f0f0e1d 100644
--- a/include/klee/Common.h
+++ b/include/klee/Common.h
@@ -19,14 +19,14 @@
 namespace klee {
     const char ALL_QUERIES_SMT2_FILE_NAME[]="all-queries.smt2";
     const char SOLVER_QUERIES_SMT2_FILE_NAME[]="solver-queries.smt2";
-    const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc";
-    const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc";
+    const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery";
+    const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery";
 
     Solver *constructSolverChain(Solver *coreSolver,
                                  std::string querySMT2LogPath,
                                  std::string baseSolverQuerySMT2LogPath,
-                                 std::string queryPCLogPath,
-                                 std::string baseSolverQueryPCLogPath);
+                                 std::string queryKQueryLogPath,
+                                 std::string baseSolverQueryKQueryLogPath);
 }
 
 
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 3a4d40b4..ece84b2c 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -66,7 +66,7 @@ public:
   enum LogType
   {
 	  STP, //.CVC (STP's native language)
-	  KQUERY, //.PC files (kQuery native language)
+	  KQUERY, //.KQUERY files (kQuery native language)
 	  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
   };
 
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index c82ab135..2f613992 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -296,9 +296,9 @@ namespace klee {
   /// \param s - The underlying solver to use.
   Solver *createIndependentSolver(Solver *s);
   
-  /// createPCLoggingSolver - Create a solver which will forward all queries
-  /// after writing them to the given path in .pc format.
-  Solver *createPCLoggingSolver(Solver *s, std::string path,
+  /// createKQueryLoggingSolver - Create a solver which will forward all queries
+  /// after writing them to the given path in .kquery format.
+  Solver *createKQueryLoggingSolver(Solver *s, std::string path,
                                 int minQueryTimeToLog);
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries