From 2cad881ef123605664f367c64afc69df4bf55450 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 1 Mar 2022 13:23:21 +0000 Subject: [PATCH] Do pretty printing for debug logging only when vebosity is high This avoids wasting execution time in `irept::pretty` in the case where verbosity is set to the default level. Before this performance fix, the pretty printed output was generated and then discarded when the verbosity was set to the default level. Comparing this change against the `develop` branch, using a benchmark has been shown to reduce the runtime from approximately 12 seconds to approximately 3 seconds for that particular example. --- .../smt2_incremental_decision_procedure.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index d326ee87143..0692522363a 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -159,7 +159,9 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined( exprt smt2_incremental_decision_proceduret::handle(const exprt &expr) { - log.debug() << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom; + log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { + debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom; + }); ensure_handle_for_expr_defined(expr); return expr; } @@ -182,7 +184,9 @@ static optionalt get_identifier( exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const { - log.debug() << "`get` - \n " + expr.pretty(2, 0) << messaget::eom; + log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { + debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom; + }); optionalt descriptor = get_identifier(expr, expression_handle_identifiers, expression_identifiers); if(!descriptor) @@ -251,8 +255,10 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value) { PRECONDITION(can_cast_type(expr.type())); - log.debug() << "`set_to` (" << std::string{value ? "true" : "false"} - << ") -\n " << expr.pretty(2, 0) << messaget::eom; + log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) { + debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n " + << expr.pretty(2, 0) << messaget::eom; + }); define_dependent_functions(expr); auto converted_term = [&]() -> smt_termt {