mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
add statistics to verbose output of asserted formulas
This commit is contained in:
parent
9a656772b4
commit
8da13ae24a
|
@ -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";);
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue