From 83ee21cd22eb527515448aafe4f241cb838de03b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2025 14:42:35 -0800 Subject: [PATCH] streamline tracing --- src/muz/spacer/spacer_qe_project.cpp | 29 ++++++++++------------------ 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index ff707dd4d..124563057 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -2206,16 +2206,10 @@ void array_project(model &mdl, app_ref_vector &arr_vars, expr_ref &fml, app_ref_vector &aux_vars, bool reduce_all_selects) { // 1. project array equalities array_project_eqs(mdl, arr_vars, fml, aux_vars); - TRACE( - "qe", ast_manager &m = fml.get_manager(); - tout << "Projected array eqs:\n" - << mk_pp(fml, m) << "\n"; - tout << "Remaining array vars:\n"; for (unsigned i = 0; - i < arr_vars.size(); i++) { - tout << mk_pp(arr_vars.get(i), m) << "\n"; - } tout << "Aux vars:\n"; - for (unsigned i = 0; i < aux_vars.size(); - i++) { tout << mk_pp(aux_vars.get(i), m) << "\n"; }); + TRACE("qe", + tout << "Projected array eqs:\n" << fml << "\n"; + tout << "Remaining array vars:\n" << arr_vars; + tout << "Aux vars:\n" << aux_vars;); // 2. reduce selects if (reduce_all_selects) { @@ -2223,19 +2217,16 @@ void array_project(model &mdl, app_ref_vector &arr_vars, expr_ref &fml, } else { reduce_array_selects(mdl, arr_vars, fml); } - TRACE("qe", ast_manager &m = fml.get_manager(); tout << "Reduced selects:\n" - << mk_pp(fml, m) - << "\n";); + TRACE("qe", tout << "Reduced selects:\n" << fml << "\n";); // 3. project selects using model based ackermannization array_project_selects(mdl, arr_vars, fml, aux_vars); TRACE( - "qe", ast_manager &m = fml.get_manager(); - tout << "Projected array selects:\n" - << mk_pp(fml, m) << "\n"; - tout << "All aux vars:\n"; - for (unsigned i = 0; i < aux_vars.size(); - i++) { tout << mk_pp(aux_vars.get(i), m) << "\n"; }); + "qe", + tout << "Projected array selects:\n"; + tout << fml << "\n"; + tout << "All aux vars:\n" << aux_vars;); + } } // namespace spacer_qe