about summary refs log tree commit diff homepage
path: root/lib/Solver/PCLoggingSolver.cpp
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/PCLoggingSolver.cpp
parent094a21832d94bfaa5da8ea667e646328ca0e5432 (diff)
downloadklee-f27cf86466d75c71a302abe5e0a3ffcad1670373.tar.gz
Renamed .pc to .kquery (kleaver query)
Diffstat (limited to 'lib/Solver/PCLoggingSolver.cpp')
-rw-r--r--lib/Solver/PCLoggingSolver.cpp68
1 files changed, 0 insertions, 68 deletions
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));
-}