diff options
Diffstat (limited to 'lib/Solver/Z3Builder.h')
-rw-r--r-- | lib/Solver/Z3Builder.h | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index f3b2732b..a3473f82 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -81,19 +81,13 @@ template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() { // instead to simplify our implementation but this seems cleaner. return ::Z3_sort_to_ast(context, node); } -template <> inline void Z3NodeHandle<Z3_sort>::dump() { - llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) - << "\n"; -} typedef Z3NodeHandle<Z3_sort> Z3SortHandle; +template <> void Z3NodeHandle<Z3_sort>::dump() __attribute__((used)); // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; } -template <> inline void Z3NodeHandle<Z3_ast>::dump() { - llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) - << "\n"; -} typedef Z3NodeHandle<Z3_ast> Z3ASTHandle; +template <> void Z3NodeHandle<Z3_ast>::dump() __attribute__((used)); class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> { @@ -171,11 +165,11 @@ private: Z3SortHandle getBvSort(unsigned width); Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort); bool autoClearConstructCache; + std::string z3LogInteractionFile; public: Z3_context ctx; - - Z3Builder(bool autoClearConstructCache = true); + Z3Builder(bool autoClearConstructCache, const char *z3LogInteractionFile); ~Z3Builder(); Z3ASTHandle getTrue(); |