about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorMartin Nowack <martin.nowack@gmail.com>2015-08-09 23:53:13 +0200
committerDan Liew <daniel.liew@imperial.ac.uk>2015-12-17 19:30:14 +0000
commit512b9f16e1c7ef23c8adc25cb435517de6bf3e81 (patch)
tree920fe1c1df002df538b2d995545852e5255b7a0b /lib/Solver
parent771cdf39d9c1e142269e2cafc4365d0d68e05f9a (diff)
downloadklee-512b9f16e1c7ef23c8adc25cb435517de6bf3e81.tar.gz
[Solver]Add simple option to dump queries
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Solver.cpp12
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3903ab0d..07331fa4 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -1267,4 +1267,16 @@ template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
 template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
 
 #endif /* SUPPORT_METASMT */
+///
 
+void Query::dump() const {
+  llvm::errs() << "Constraints [\n";
+  for (ConstraintManager::const_iterator i = constraints.begin();
+      i != constraints.end(); i++) {
+    (*i)->dump();
+  }
+  llvm::errs() << "]\n";
+  llvm::errs() << "Query [\n";
+  expr->dump();
+  llvm::errs() << "]\n";
+}