From d30cb55bae24113468b3ae6f07d39536402b4891 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 3 Jan 2023 09:35:17 +0000 Subject: [PATCH] don't flush stream when printing param vals --- src/params/bit_blaster_params.h | 4 ++-- src/params/pattern_inference_params.cpp | 2 +- src/smt/params/dyn_ack_params.cpp | 2 +- src/smt/params/preprocessor_params.cpp | 2 +- src/smt/params/qi_params.cpp | 2 +- src/smt/params/smt_params.cpp | 2 +- src/smt/params/theory_arith_params.cpp | 2 +- src/smt/params/theory_array_params.cpp | 2 +- src/smt/params/theory_bv_params.cpp | 2 +- src/smt/params/theory_datatype_params.h | 2 +- src/smt/params/theory_pb_params.cpp | 2 +- src/smt/params/theory_str_params.cpp | 2 +- src/tactic/smtlogics/smt_tactic.cpp | 2 +- 13 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/params/bit_blaster_params.h b/src/params/bit_blaster_params.h index 527835d2abf..9e405f187b4 100644 --- a/src/params/bit_blaster_params.h +++ b/src/params/bit_blaster_params.h @@ -33,8 +33,8 @@ struct bit_blaster_params { #endif void display(std::ostream & out) const { - out << "m_bb_ext_gates=" << m_bb_ext_gates << std::endl; - out << "m_bb_quantifiers=" << m_bb_quantifiers << std::endl; + out << "m_bb_ext_gates=" << m_bb_ext_gates << '\n'; + out << "m_bb_quantifiers=" << m_bb_quantifiers << '\n'; } }; diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index bb9b481ca23..26f606b635e 100644 --- a/src/params/pattern_inference_params.cpp +++ b/src/params/pattern_inference_params.cpp @@ -31,7 +31,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) { m_pi_warnings = p.warnings(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void pattern_inference_params::display(std::ostream & out) const { DISPLAY_PARAM(m_pi_max_multi_patterns); diff --git a/src/smt/params/dyn_ack_params.cpp b/src/smt/params/dyn_ack_params.cpp index b1e99cf21d7..57645903d80 100644 --- a/src/smt/params/dyn_ack_params.cpp +++ b/src/smt/params/dyn_ack_params.cpp @@ -29,7 +29,7 @@ void dyn_ack_params::updt_params(params_ref const & _p) { m_dack_gc_inv_decay = p.dack_gc_inv_decay(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void dyn_ack_params::display(std::ostream & out) const { DISPLAY_PARAM((unsigned)m_dack); diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 9fcb09843b9..f3c46f95c98 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -34,7 +34,7 @@ void preprocessor_params::updt_params(params_ref const & p) { updt_local_params(p); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void preprocessor_params::display(std::ostream & out) const { pattern_inference_params::display(out); diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index 387df4dd599..d6b22d9f1fd 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -39,7 +39,7 @@ void qi_params::updt_params(params_ref const & _p) { m_qi_quick_checker = static_cast(p.qi_quick_checker()); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void qi_params::display(std::ostream & out) const { DISPLAY_PARAM(m_qi_cost); diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 37249fdaca2..3c63e2fffee 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -85,7 +85,7 @@ void smt_params::updt_params(context_params const & p) { m_model = p.m_model; } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void smt_params::display(std::ostream & out) const { preprocessor_params::display(out); diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 565000ebe91..7f3f1ca23ce 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -42,7 +42,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_arith_eq2ineq); diff --git a/src/smt/params/theory_array_params.cpp b/src/smt/params/theory_array_params.cpp index 892edb4ad15..2283be256af 100644 --- a/src/smt/params/theory_array_params.cpp +++ b/src/smt/params/theory_array_params.cpp @@ -25,7 +25,7 @@ void theory_array_params::updt_params(params_ref const & _p) { m_array_extensional = p.array_extensional(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void theory_array_params::display(std::ostream & out) const { DISPLAY_PARAM(m_array_mode); diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 35a62e7fc94..09fa4513fe2 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -31,7 +31,7 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_size_reduce = p.bv_size_reduce(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_bv_mode); diff --git a/src/smt/params/theory_datatype_params.h b/src/smt/params/theory_datatype_params.h index 05957bfe9b3..b16f4254aef 100644 --- a/src/smt/params/theory_datatype_params.h +++ b/src/smt/params/theory_datatype_params.h @@ -32,7 +32,7 @@ struct theory_datatype_params { m_dt_lazy_splits = p.dt_lazy_splits(); } - void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; } + void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << '\n'; } }; diff --git a/src/smt/params/theory_pb_params.cpp b/src/smt/params/theory_pb_params.cpp index 45a6ede1086..2df8d6fee98 100644 --- a/src/smt/params/theory_pb_params.cpp +++ b/src/smt/params/theory_pb_params.cpp @@ -25,7 +25,7 @@ void theory_pb_params::updt_params(params_ref const & _p) { m_pb_learn_complements = p.pb_learn_complements(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void theory_pb_params::display(std::ostream & out) const { DISPLAY_PARAM(m_pb_conflict_frequency); diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index e0802b5d77f..7f84a6cbeed 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -37,7 +37,7 @@ void theory_str_params::updt_params(params_ref const & _p) { m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex(); } -#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl; +#define DISPLAY_PARAM(X) out << #X"=" << X << '\n'; void theory_str_params::display(std::ostream & out) const { DISPLAY_PARAM(m_StrongArrangements); diff --git a/src/tactic/smtlogics/smt_tactic.cpp b/src/tactic/smtlogics/smt_tactic.cpp index d47650c3460..aefe7ccadee 100644 --- a/src/tactic/smtlogics/smt_tactic.cpp +++ b/src/tactic/smtlogics/smt_tactic.cpp @@ -23,7 +23,7 @@ Module Name: tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) { sat_params sp(p); - if (sp.smt()) + if (sp.smt()) return mk_solver2tactic(mk_smt2_solver(m, p)); if (sp.euf()) return mk_sat_tactic(m, p);