Skip to content

Commit 2cad881

Browse files
committed
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.
1 parent c1336e4 commit 2cad881

File tree

1 file changed

+10
-4
lines changed

1 file changed

+10
-4
lines changed

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

+10-4
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,9 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
159159

160160
exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
161161
{
162-
log.debug() << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
162+
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
163+
debug << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
164+
});
163165
ensure_handle_for_expr_defined(expr);
164166
return expr;
165167
}
@@ -182,7 +184,9 @@ static optionalt<smt_termt> get_identifier(
182184

183185
exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
184186
{
185-
log.debug() << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
187+
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
188+
debug << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
189+
});
186190
optionalt<smt_termt> descriptor =
187191
get_identifier(expr, expression_handle_identifiers, expression_identifiers);
188192
if(!descriptor)
@@ -251,8 +255,10 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
251255
void smt2_incremental_decision_proceduret::set_to(const exprt &expr, bool value)
252256
{
253257
PRECONDITION(can_cast_type<bool_typet>(expr.type()));
254-
log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
255-
<< ") -\n " << expr.pretty(2, 0) << messaget::eom;
258+
log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
259+
debug << "`set_to` (" << std::string{value ? "true" : "false"} << ") -\n "
260+
<< expr.pretty(2, 0) << messaget::eom;
261+
});
256262

257263
define_dependent_functions(expr);
258264
auto converted_term = [&]() -> smt_termt {

0 commit comments

Comments
 (0)