about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-23 21:48:12 +0100
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-03-23 21:48:12 +0100
commit20eb0485850073fafdac07a630cededf8b99c536 (patch)
tree445080c0a8bfef0fcb473a5ad4a4eab93f94baca /lib/Solver
parent082e9d7bab796eda37624c026d8d006608625b90 (diff)
downloadklee-20eb0485850073fafdac07a630cededf8b99c536.tar.gz
Refactoring of conditional flush into own function.
@delcypher: Thanks a lot Dan!
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp24
-rw-r--r--lib/Solver/QueryLoggingSolver.h1
2 files changed, 15 insertions, 10 deletions
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 6084e2e1..f93bec3c 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -39,6 +39,16 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
 
 QueryLoggingSolver::~QueryLoggingSolver() { delete solver; }
 
+void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
+  logBuffer.flush();
+  if (writeToFile) {
+    os << logBuffer.str();
+    os.flush();
+  }
+  // prepare the buffer for reuse
+  BufferString = "";
+}
+
 void QueryLoggingSolver::startQuery(const Query &query, const char *typeName,
                                     const Query *falseQuery,
                                     const std::vector<const Array *> *objects) {
@@ -52,11 +62,7 @@ void QueryLoggingSolver::startQuery(const Query &query, const char *typeName,
   printQuery(query, falseQuery, objects);
 
   if (DumpPartialQueryiesEarly) {
-    logBuffer.flush();
-    os << logBuffer.str();
-    os.flush();
-    // prepare the buffer for reuse
-    BufferString = "";
+    flushBufferConditionally(true);
   }
   startTime = getWallTime();
 }
@@ -74,7 +80,7 @@ void QueryLoggingSolver::finishQuery(bool success) {
 }
 
 void QueryLoggingSolver::flushBuffer() {
-  logBuffer.flush();
+  bool writeToFile = false;
 
   if ((0 == minQueryTimeToLog) ||
       (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
@@ -86,13 +92,11 @@ void QueryLoggingSolver::flushBuffer() {
          (solver->impl->getOperationStatusCode()))) {
       // we do additional check here to log only timeouts in case
       // user specified negative value for minQueryTimeToLog param
-      os << logBuffer.str();
-      os.flush();
+      writeToFile = true;
     }
   }
 
-  // prepare the buffer for reuse
-  BufferString = "";
+  flushBufferConditionally(writeToFile);
 }
 
 bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 3068f2ab..bb266c67 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -55,6 +55,7 @@ protected:
 
   virtual void printQuery(const Query &query, const Query *falseQuery = 0,
                           const std::vector<const Array *> *objects = 0) = 0;
+  void flushBufferConditionally(bool writeToFile);
 
 public:
   QueryLoggingSolver(Solver *_solver, std::string path,