From 8da13ae24a2b8ab9948fb413f2d8510691ee7354 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Nov 2022 18:37:30 -0800 Subject: [PATCH] add statistics to verbose output of asserted formulas --- src/solver/assertions/asserted_formulas.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 90c84e7ee..2b20ebd80 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -306,7 +306,7 @@ void asserted_formulas::reduce() { if (!invoke(m_flatten_clauses)) return; // if (!invoke(m_propagate_values)) return; - IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";); + IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done :num-exprs " << get_total_size() << ")\n";); TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); TRACE("macros", m_macro_manager.display(tout);); @@ -327,8 +327,8 @@ unsigned asserted_formulas::get_formulas_last_level() const { bool asserted_formulas::invoke(simplify_fmls& s) { if (!s.should_apply()) return true; - IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";); s(); + IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << " :num-exprs " << get_total_size() << ")\n";); IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); CASSERT("well_sorted",check_well_sorted()); @@ -514,9 +514,9 @@ void asserted_formulas::simplify_fmls::operator()() { void asserted_formulas::reduce_and_solve() { - IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";); flush_cache(); // collect garbage m_reduce_asserted_formulas(); + IF_VERBOSE(10, verbose_stream() << "(smt.reduced " << get_total_size() << ")\n";); }