aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver/QueryLoggingSolver.cpp
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/QueryLoggingSolver.cpp
parent082e9d7bab796eda37624c026d8d006608625b90 (diff)
downloadklee-20eb0485850073fafdac07a630cededf8b99c536.tar.gz
Refactoring of conditional flush into own function.
@delcypher: Thanks a lot Dan!
Diffstat (limited to 'lib/Solver/QueryLoggingSolver.cpp')
-rw-r--r--lib/Solver/QueryLoggingSolver.cpp24
1 files changed, 14 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) {