From 6e68911cbb32f26429f7ab70361a02ec47c0742a Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 15 Jan 2026 21:30:29 -0800 Subject: [PATCH] Reapply PR #8190: Replace std::ostringstream with C++20 std::format (#8204) * Initial plan * Reapply PR #8190: Replace std::ostringstream with C++20 std::format Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/array_decl_plugin.cpp | 58 +++++++++++--------------------- src/ast/ast.cpp | 54 ++++++++++++++--------------- src/ast/ast_pp.h | 8 +++++ src/ast/bv_decl_plugin.cpp | 9 +++-- src/ast/datatype_decl_plugin.cpp | 9 ++--- src/ast/dl_decl_plugin.cpp | 5 ++- src/ast/seq_decl_plugin.cpp | 48 ++++++++++++-------------- 7 files changed, 87 insertions(+), 104 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 5d79bb97d..7da470221 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "ast/array_decl_plugin.h" #include "util/warning.h" #include "ast/ast_pp.h" @@ -139,10 +140,8 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* domain) { if (arity != f->get_arity()) { - std::ostringstream buffer; - buffer << "map expects to take as many arguments as the function being mapped, " - << "it was given " << arity << " but expects " << f->get_arity(); - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("map expects to take as many arguments as the function being mapped, it was given {} but expects {}", + arity, f->get_arity())); return nullptr; } if (arity == 0) { @@ -157,32 +156,21 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* unsigned dom_arity = get_array_arity(domain[0]); for (unsigned i = 0; i < arity; ++i) { if (!is_array_sort(domain[i])) { - std::ostringstream buffer; - buffer << "map expects an array sort as argument at position " << i; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("map expects an array sort as argument at position {}", i)); return nullptr; } if (get_array_arity(domain[i]) != dom_arity) { - std::ostringstream buffer; - buffer << "map expects all arguments to have the same array domain, " - << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i)); return nullptr; } for (unsigned j = 0; j < dom_arity; ++j) { if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) { - std::ostringstream buffer; - buffer << "map expects all arguments to have the same array domain, " - << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i)); return nullptr; } } if (get_array_range(domain[i]) != f->get_domain(i)) { - std::ostringstream buffer; - buffer << "map expects the argument at position " << i - << " to have the array range the same as the function"; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("map expects the argument at position {} to have the array range the same as the function", i)); return nullptr; } } @@ -243,9 +231,8 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { parameter const* parameters = s->get_parameters(); if (num_parameters != arity) { - std::stringstream strm; - strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments"; - m_manager->raise_exception(strm.str()); + m_manager->raise_exception(std::format("select requires {} arguments, but was provided with {} arguments", + num_parameters, arity)); return nullptr; } ptr_buffer new_domain; // we need this because of coercions. @@ -254,10 +241,9 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast()) || !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) { - std::stringstream strm; - strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter "; - strm << parameter_pp(parameters[i], *m_manager) << " do not match"; - m_manager->raise_exception(strm.str()); + m_manager->raise_exception(std::format("domain sort {} and parameter {} do not match", + to_string(sort_ref(domain[i+1], *m_manager)), + to_string(parameter_pp(parameters[i], *m_manager)))); return nullptr; } new_domain.push_back(to_sort(parameters[i].get_ast())); @@ -281,10 +267,8 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { return nullptr; } if (arity != num_parameters+1) { - std::ostringstream buffer; - buffer << "store expects the first argument to be an array taking " << num_parameters+1 - << ", instead it was passed " << (arity - 1) << "arguments"; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("store expects the first argument to be an array taking {}, instead it was passed {} arguments", + num_parameters+1, arity - 1)); UNREACHABLE(); return nullptr; } @@ -298,9 +282,9 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { sort* srt1 = to_sort(parameters[i].get_ast()); sort* srt2 = domain[i+1]; if (!m_manager->compatible_sorts(srt1, srt2)) { - std::stringstream strm; - strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match"; - m_manager->raise_exception(strm.str()); + m_manager->raise_exception(std::format("domain sort {} and parameter sort {} do not match", + to_string(sort_ref(srt2, *m_manager)), + to_string(sort_ref(srt1, *m_manager)))); UNREACHABLE(); return nullptr; } @@ -333,15 +317,11 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domain) { for (unsigned i = 0; i < arity; ++i) { if (domain[i] != domain[0]) { - std::ostringstream buffer; - buffer << "arguments " << 1 << " and " << (i+1) << " have different sorts"; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("arguments {} and {} have different sorts", 1, i+1)); return false; } if (domain[i]->get_family_id() != m_family_id) { - std::ostringstream buffer; - buffer << "argument " << (i+1) << " is not of array sort"; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("argument {} is not of array sort", i+1)); return false; } } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index be5ac7a58..ebeba94be 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include #include "ast/ast.h" #include "ast/ast_pp.h" @@ -1021,9 +1022,9 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) { return s2; if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id) return s1; - std::ostringstream buffer; - buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; - throw ast_exception(buffer.str()); + throw ast_exception(std::format("Sorts {} and {} are incompatible", + to_string(mk_pp(s1, *m_manager)), + to_string(mk_pp(s2, *m_manager)))); } @@ -1700,10 +1701,8 @@ ast * ast_manager::register_node_core(ast * n) { SASSERT(contains); SASSERT(m_ast_table.contains(n)); if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) { - std::ostringstream buffer; - buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str() - << "' and domain, but different range type is not permitted"; - throw ast_exception(buffer.str()); + throw ast_exception(std::format("Recycling of declaration for the same name '{}' and domain, but different range type is not permitted", + to_func_decl(r)->get_name().str())); } deallocate_node(n, ::get_node_size(n)); return r; @@ -2022,11 +2021,11 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c for (unsigned i = 0; i < num_args; ++i) { sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { - std::ostringstream buff; - buff << "invalid function application for " << decl->get_name() << ", "; - buff << "sort mismatch on argument at position " << (i+1) << ", "; - buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); - throw ast_exception(buff.str()); + throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}", + to_string(decl->get_name()), + i + 1, + to_string(mk_pp(expected, m)), + to_string(mk_pp(given, m)))); } } } @@ -2038,11 +2037,11 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c sort * expected = decl->get_domain(i); sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { - std::ostringstream buff; - buff << "invalid function application for " << decl->get_name() << ", "; - buff << "sort mismatch on argument at position " << (i+1) << ", "; - buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); - throw ast_exception(buff.str()); + throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}", + to_string(decl->get_name()), + i + 1, + to_string(mk_pp(expected, m)), + to_string(mk_pp(given, m)))); } } } @@ -2197,12 +2196,10 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) { sort * actual_sort = es[i]->get_sort(); sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i); if (expected_sort != actual_sort) { - std::ostringstream buffer; - buffer << "Sort mismatch at argument #" << (i+1) - << " for function " << mk_pp(f,*this) - << " supplied sort is " - << mk_pp(actual_sort, *this); - throw ast_exception(buffer.str()); + throw ast_exception(std::format("Sort mismatch at argument #{} for function {} supplied sort is {}", + i + 1, + to_string(mk_pp(f, *this)), + to_string(mk_pp(actual_sort, *this)))); } } } @@ -2223,12 +2220,13 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar decl->get_family_id() == basic_family_id && !decl->is_associative()); if (type_error) { - std::ostringstream buffer; - buffer << "Wrong number of arguments (" << num_args - << ") passed to function " << mk_pp(decl, *this) << " "; + std::string arg_list; for (unsigned i = 0; i < num_args; ++i) - buffer << "\narg: " << mk_pp(args[i], *this) << "\n"; - throw ast_exception(std::move(buffer).str()); + arg_list += std::format("\narg: {}\n", to_string(mk_pp(args[i], *this))); + throw ast_exception(std::format("Wrong number of arguments ({}) passed to function {} {}", + num_args, + to_string(mk_pp(decl, *this)), + arg_list)); } app * r = nullptr; if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h index 1f20ce300..4fb0daef0 100644 --- a/src/ast/ast_pp.h +++ b/src/ast/ast_pp.h @@ -71,3 +71,11 @@ inline std::string& operator+=(std::string& s, mk_pp const& pp) { return s = s + pp; } +// Helper function to convert streamable objects (like mk_pp) to strings for use with std::format +template +inline std::string to_string(T const& obj) { + std::ostringstream strm; + strm << obj; + return std::move(strm).str(); +} + diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 8ec2bfb90..28fbb9fbb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" @@ -672,9 +673,11 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p } for (unsigned i = 0; i < num_args; ++i) { if (args[i]->get_sort() != r->get_domain(i)) { - std::ostringstream buffer; - buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " has sort " << mk_pp(args[i]->get_sort(), m) << " it does not match declaration " << mk_pp(r, m); - m.raise_exception(buffer.str()); + m.raise_exception(std::format("Argument {} at position {} has sort {} it does not match declaration {}", + to_string(mk_pp(args[i], m)), + i, + to_string(mk_pp(args[i]->get_sort(), m)), + to_string(mk_pp(r, m)))); return nullptr; } } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 48dfc1fbe..a8db335b2 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -17,6 +17,8 @@ Revision History: --*/ +#include +#include #include "util/warning.h" #include "ast/array_decl_plugin.h" #include "ast/seq_decl_plugin.h" @@ -377,10 +379,9 @@ namespace datatype { return nullptr; } if (rng != domain[1]) { - std::ostringstream buffer; - buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) - << " instead of " << mk_ismt2_pp(domain[1], m); - m.raise_exception(buffer.str()); + m.raise_exception(std::format("second argument to field update should be {} instead of {}", + to_string(mk_ismt2_pp(rng, m)), + to_string(mk_ismt2_pp(domain[1], m)))); return nullptr; } range = domain[0]; diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index a63d13f59..19ae67fd5 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "ast/ast_pp.h" #include "ast/array_decl_plugin.h" @@ -52,9 +53,7 @@ namespace datalog { if (low <= val && val <= up) { return true; } - std::ostringstream buffer; - buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up; - m_manager->raise_exception(buffer.str()); + m_manager->raise_exception(std::format("{}, value is not within bound {} <= {} <= {}", msg, low, val, up)); return false; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 72eefeab0..634ced5c9 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -21,6 +21,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/ast_pp.h" #include +#include seq_decl_plugin::seq_decl_plugin(): m_init(false), @@ -82,10 +83,8 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor ptr_vector binding; ast_manager& m = *m_manager; if (dsz == 0) { - std::ostringstream strm; - strm << "Unexpected number of arguments to '" << sig.m_name << "' "; - strm << "at least one argument expected " << dsz << " given"; - m.raise_exception(strm.str()); + m.raise_exception(std::format("Unexpected number of arguments to '{}' at least one argument expected {} given", + sig.m_name.str(), dsz)); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -96,16 +95,16 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor is_match = match(binding, range, sig.m_range); } if (!is_match) { - std::ostringstream strm; - strm << "Sort of function '" << sig.m_name << "' "; - strm << "does not match the declared type. Given domain: "; + std::string domain_str; for (unsigned i = 0; i < dsz; ++i) { - strm << mk_pp(dom[i], m) << " "; + domain_str += to_string(mk_pp(dom[i], m)) + " "; } + std::string range_str; if (range) { - strm << " and range: " << mk_pp(range, m); + range_str = std::format(" and range: {}", to_string(mk_pp(range, m))); } - m.raise_exception(strm.str()); + m.raise_exception(std::format("Sort of function '{}' does not match the declared type. Given domain: {}{}", + sig.m_name.str(), domain_str, range_str)); } range_out = apply_binding(binding, sig.m_range); SASSERT(range_out); @@ -115,10 +114,8 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran m_binding.reset(); ast_manager& m = *m_manager; if (sig.m_dom.size() != dsz) { - std::ostringstream strm; - strm << "Unexpected number of arguments to '" << sig.m_name << "' "; - strm << sig.m_dom.size() << " arguments expected " << dsz << " given"; - m.raise_exception(strm.str()); + m.raise_exception(std::format("Unexpected number of arguments to '{}' {} arguments expected {} given", + sig.m_name.str(), sig.m_dom.size(), dsz)); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -128,28 +125,25 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran is_match = match(m_binding, range, sig.m_range); } if (!is_match) { - std::ostringstream strm; - strm << "Sort of polymorphic function '" << sig.m_name << "' "; - strm << "does not match the declared type. "; - strm << "\nGiven domain: "; + std::string given_domain; for (unsigned i = 0; i < dsz; ++i) { - strm << mk_pp(dom[i], m) << " "; + given_domain += to_string(mk_pp(dom[i], m)) + " "; } + std::string range_str; if (range) { - strm << " and range: " << mk_pp(range, m); + range_str = std::format(" and range: {}", to_string(mk_pp(range, m))); } - strm << "\nExpected domain: "; + std::string expected_domain; for (unsigned i = 0; i < dsz; ++i) { - strm << mk_pp(sig.m_dom[i].get(), m) << " "; + expected_domain += to_string(mk_pp(sig.m_dom[i].get(), m)) + " "; } - m.raise_exception(strm.str()); + m.raise_exception(std::format("Sort of polymorphic function '{}' does not match the declared type. \nGiven domain: {}{}\nExpected domain: {}", + sig.m_name.str(), given_domain, range_str, expected_domain)); } if (!range && dsz == 0) { - std::ostringstream strm; - strm << "Sort of polymorphic function '" << sig.m_name << "' "; - strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained"; - m.raise_exception(strm.str()); + m.raise_exception(std::format("Sort of polymorphic function '{}' is ambiguous. Function takes no arguments and sort of range has not been constrained", + sig.m_name.str())); } range_out = apply_binding(m_binding, sig.m_range); SASSERT(range_out);