[Solver]Add simple option to dump queries

klee · Dec 17, 2015 · 512b9f1 · 512b9f1
1 parent 771cdf3
commit 512b9f1
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
@@ -42,6 +42,9 @@ namespace klee {
     Query negateExpr() const {
       return withExpr(Expr::createIsZero(expr));
     }
+
+    /// Dump query
+    void dump() const ;
   };
 
   class Solver {

diff --git 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";
+}