From f27cf86466d75c71a302abe5e0a3ffcad1670373 Mon Sep 17 00:00:00 2001
From: Eric Rizzi <eric.rizzi@gmail.com>
Date: Mon, 14 Sep 2015 14:32:37 -0400
Subject: Renamed .pc to .kquery (kleaver query)

---
 lib/Solver/CMakeLists.txt          |  2 +-
 lib/Solver/KQueryLoggingSolver.cpp | 69 ++++++++++++++++++++++++++++++++++++++
 lib/Solver/PCLoggingSolver.cpp     | 68 -------------------------------------
 3 files changed, 70 insertions(+), 69 deletions(-)
 create mode 100644 lib/Solver/KQueryLoggingSolver.cpp
 delete mode 100644 lib/Solver/PCLoggingSolver.cpp

(limited to 'lib/Solver')

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/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
new file mode 100644
index 00000000..a0ac950c
--- /dev/null
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -0,0 +1,69 @@
+//===-- KQueryLoggingSolver.cpp -----------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "QueryLoggingSolver.h"
+
+#include "klee/Expr.h"
+#include "klee/util/ExprPPrinter.h"
+#include "klee/Internal/Support/QueryLog.h"
+
+using namespace klee;
+
+///
+
+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();
+        }
+
+        const Query* q = (0 == falseQuery) ? &query : falseQuery;
+
+        printer->printQuery(logBuffer, q->constraints, q->expr,
+                            evalExprsBegin, evalExprsEnd,
+                            evalArraysBegin, evalArraysEnd);
+    }
+
+public:
+    KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
+    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),
+    printer(ExprPPrinter::create(logBuffer)) {
+    }
+
+    virtual ~KQueryLoggingSolver() {
+        delete printer;
+    }
+};
+
+///
+
+Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path,
+                                    int minQueryTimeToLog) {
+  return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog));
+}
+
diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp
deleted file mode 100644
index 67e9be45..00000000
--- a/lib/Solver/PCLoggingSolver.cpp
+++ /dev/null
@@ -1,68 +0,0 @@
-//===-- PCLoggingSolver.cpp -----------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "QueryLoggingSolver.h"
-
-#include "klee/Expr.h"
-#include "klee/util/ExprPPrinter.h"
-#include "klee/Internal/Support/QueryLog.h"
-
-using namespace klee;
-
-///
-
-class PCLoggingSolver : 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();            
-        }
-        
-        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),    
-    printer(ExprPPrinter::create(logBuffer)) {
-    }                                                      
-    
-    virtual ~PCLoggingSolver() {    
-        delete printer;
-    }    
-};
-
-///
-
-Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path,
-                                    int minQueryTimeToLog) {
-  return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog));
-}
-- 
cgit 1.4.1