[PATCH] D48221: [analyzer] Add method to the generic SMT API to dump the SMT formula

[Phabricator via Phabricator via llvm-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rL334891: [analyzer] Add method to the generic SMT API to dump the SMT formula (authored by mramalho, committed by ).
Herald added a subscriber: llvm-commits.

Changed prior to commit:
  https://reviews.llvm.org/D48221?vs=151531&id=151618#toc

Repository:
  rL LLVM

https://reviews.llvm.org/D48221

Files:
  cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
  cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp


Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -35,6 +35,8 @@
   /// Checks if the added constraints are satisfiable
   virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
 
+  /// Dumps SMT formula
+  LLVM_DUMP_METHOD virtual void dump() const = 0;
 }; // end class SMTConstraintManager
 
 } // namespace ento
Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -911,6 +911,8 @@
 
   ConditionTruthVal isModelFeasible() override;
 
+  LLVM_DUMP_METHOD void dump() const override;
+
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
@@ -1299,6 +1301,11 @@
   return ConditionTruthVal();
 }
 
+LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const
+{
+  Solver.dump();
+}
+
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D48221.151618.patch
Type: text/x-patch
Size: 1529 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20180616/a82414bd/attachment.bin>