mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-03 07:37:54 +00:00
Code Activity

Modernize ostringstream to std::format in ast.cpp and array_decl_plugin.cpp

Browse source 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-13 21:29:51 +00:00
parent d274181c1f
commit 99a40e79d4
3 changed files with 53 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/ast/array_decl_plugin.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/ --*/
#include<sstream> #include<sstream>
#include<format>
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
#include "util/warning.h" #include "util/warning.h"
#include "ast/ast_pp.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) { func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* domain) {
if (arity != f->get_arity()) { if (arity != f->get_arity()) {
std::ostringstream buffer; m_manager->raise_exception(std::format("map expects to take as many arguments as the function being mapped, it was given {} but expects {}",
buffer << "map expects to take as many arguments as the function being mapped, " arity, f->get_arity()));
<< "it was given " << arity << " but expects " << f->get_arity();
m_manager->raise_exception(buffer.str());
return nullptr; return nullptr;
} }
if (arity == 0) { 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]); unsigned dom_arity = get_array_arity(domain[0]);
for (unsigned i = 0; i < arity; ++i) { for (unsigned i = 0; i < arity; ++i) {
if (!is_array_sort(domain[i])) { if (!is_array_sort(domain[i])) {
std::ostringstream buffer; m_manager->raise_exception(std::format("map expects an array sort as argument at position {}", i));
buffer << "map expects an array sort as argument at position " << i;
m_manager->raise_exception(buffer.str());
return nullptr; return nullptr;
} }
if (get_array_arity(domain[i]) != dom_arity) { if (get_array_arity(domain[i]) != dom_arity) {
std::ostringstream buffer; m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i));
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());
return nullptr; return nullptr;
} }
for (unsigned j = 0; j < dom_arity; ++j) { for (unsigned j = 0; j < dom_arity; ++j) {
if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) { if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) {
std::ostringstream buffer; m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i));
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());
return nullptr; return nullptr;
} }
} }
if (get_array_range(domain[i]) != f->get_domain(i)) { if (get_array_range(domain[i]) != f->get_domain(i)) {
std::ostringstream buffer; m_manager->raise_exception(std::format("map expects the argument at position {} to have the array range the same as the function", i));
buffer << "map expects the argument at position " << i
<< " to have the array range the same as the function";
m_manager->raise_exception(buffer.str());
return nullptr; return nullptr;
} }
} }
@ -243,9 +231,8 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
parameter const* parameters = s->get_parameters(); parameter const* parameters = s->get_parameters();
if (num_parameters != arity) { if (num_parameters != arity) {
std::stringstream strm; m_manager->raise_exception(std::format("select requires {} arguments, but was provided with {} arguments",
strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments"; num_parameters, arity));
m_manager->raise_exception(strm.str());
return nullptr; return nullptr;
} }
ptr_buffer<sort> new_domain; // we need this because of coercions. ptr_buffer<sort> 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() || if (!parameters[i].is_ast() ||
!is_sort(parameters[i].get_ast()) || !is_sort(parameters[i].get_ast()) ||
!m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) { !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
std::stringstream strm; m_manager->raise_exception(std::format("domain sort {} and parameter {} do not match",
strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter "; to_string(sort_ref(domain[i+1], *m_manager)),
strm << parameter_pp(parameters[i], *m_manager) << " do not match"; to_string(parameter_pp(parameters[i], *m_manager))));
m_manager->raise_exception(strm.str());
return nullptr; return nullptr;
} }
new_domain.push_back(to_sort(parameters[i].get_ast())); 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; return nullptr;
} }
if (arity != num_parameters+1) { if (arity != num_parameters+1) {
std::ostringstream buffer; m_manager->raise_exception(std::format("store expects the first argument to be an array taking {}, instead it was passed {}arguments",
buffer << "store expects the first argument to be an array taking " << num_parameters+1 num_parameters+1, arity - 1));
<< ", instead it was passed " << (arity - 1) << "arguments";
m_manager->raise_exception(buffer.str());
UNREACHABLE(); UNREACHABLE();
return nullptr; 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* srt1 = to_sort(parameters[i].get_ast());
sort* srt2 = domain[i+1]; sort* srt2 = domain[i+1];
if (!m_manager->compatible_sorts(srt1, srt2)) { if (!m_manager->compatible_sorts(srt1, srt2)) {
std::stringstream strm; m_manager->raise_exception(std::format("domain sort {} and parameter sort {} do not match",
strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match"; to_string(sort_ref(srt2, *m_manager)),
m_manager->raise_exception(strm.str()); to_string(sort_ref(srt1, *m_manager))));
UNREACHABLE(); UNREACHABLE();
return nullptr; 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) { bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domain) {
for (unsigned i = 0; i < arity; ++i) { for (unsigned i = 0; i < arity; ++i) {
if (domain[i] != domain[0]) { if (domain[i] != domain[0]) {
std::ostringstream buffer; m_manager->raise_exception(std::format("arguments {} and {} have different sorts", 1, i+1));
buffer << "arguments " << 1 << " and " << (i+1) << " have different sorts";
m_manager->raise_exception(buffer.str());
return false; return false;
} }
if (domain[i]->get_family_id() != m_family_id) { if (domain[i]->get_family_id() != m_family_id) {
std::ostringstream buffer; m_manager->raise_exception(std::format("argument {} is not of array sort", i+1));
buffer << "argument " << (i+1) << " is not of array sort";
m_manager->raise_exception(buffer.str());
return false; return false;
} }
} }

54
src/ast/ast.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/ --*/
#include <sstream> #include <sstream>
#include <format>
#include <cstring> #include <cstring>
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
@ -1021,9 +1022,9 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
return s2; return s2;
if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id) if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id)
return s1; return s1;
std::ostringstream buffer; throw ast_exception(std::format("Sorts {} and {} are incompatible",
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; to_string(mk_pp(s1, *m_manager)),
throw ast_exception(buffer.str()); to_string(mk_pp(s2, *m_manager))));
} }
@ -1700,10 +1701,8 @@ ast * ast_manager::register_node_core(ast * n) {
SASSERT(contains); SASSERT(contains);
SASSERT(m_ast_table.contains(n)); SASSERT(m_ast_table.contains(n));
if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) { if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {
std::ostringstream buffer; throw ast_exception(std::format("Recycling of declaration for the same name '{}' and domain, but different range type is not permitted",
buffer << "Recycling of declaration for the same name '" << to_func_decl(r)->get_name().str() to_func_decl(r)->get_name().str()));
<< "' and domain, but different range type is not permitted";
throw ast_exception(buffer.str());
} }
deallocate_node(n, ::get_node_size(n)); deallocate_node(n, ::get_node_size(n));
return r; 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++) { for (unsigned i = 0; i < num_args; i++) {
sort * given = args[i]->get_sort(); sort * given = args[i]->get_sort();
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
std::ostringstream buff; throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
buff << "invalid function application for " << decl->get_name() << ", "; to_string(decl->get_name()),
buff << "sort mismatch on argument at position " << (i+1) << ", "; i + 1,
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); to_string(mk_pp(expected, m)),
throw ast_exception(buff.str()); 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 * expected = decl->get_domain(i);
sort * given = args[i]->get_sort(); sort * given = args[i]->get_sort();
if (!compatible_sorts(expected, given)) { if (!compatible_sorts(expected, given)) {
std::ostringstream buff; throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
buff << "invalid function application for " << decl->get_name() << ", "; to_string(decl->get_name()),
buff << "sort mismatch on argument at position " << (i+1) << ", "; i + 1,
buff << "expected " << mk_pp(expected, m) << " but given " << mk_pp(given, m); to_string(mk_pp(expected, m)),
throw ast_exception(buff.str()); 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 * actual_sort = es[i]->get_sort();
sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i); sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i);
if (expected_sort != actual_sort) { if (expected_sort != actual_sort) {
std::ostringstream buffer; throw ast_exception(std::format("Sort mismatch at argument #{} for function {} supplied sort is {}",
buffer << "Sort mismatch at argument #" << (i+1) i + 1,
<< " for function " << mk_pp(f,*this) to_string(mk_pp(f, *this)),
<< " supplied sort is " to_string(mk_pp(actual_sort, *this))));
<< mk_pp(actual_sort, *this);
throw ast_exception(buffer.str());
} }
} }
} }
@ -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()); decl->get_family_id() == basic_family_id && !decl->is_associative());
if (type_error) { if (type_error) {
std::ostringstream buffer; std::string arg_list;
buffer << "Wrong number of arguments (" << num_args
<< ") passed to function " << mk_pp(decl, *this) << " ";
for (unsigned i = 0; i < num_args; ++i) for (unsigned i = 0; i < num_args; ++i)
buffer << "\narg: " << mk_pp(args[i], *this) << "\n"; arg_list += std::format("\narg: {}\n", to_string(mk_pp(args[i], *this)));
throw ast_exception(std::move(buffer).str()); 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; app * r = nullptr;
if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {

8
src/ast/ast_pp.h
View file

@ -71,3 +71,11 @@ inline std::string& operator+=(std::string& s, mk_pp const& pp) {
return s = s + pp; return s = s + pp;
} }
// Helper function to convert streamable objects (like mk_pp) to strings for use with std::format
template<typename T>
inline std::string to_string(T const& obj) {
std::ostringstream strm;
strm << obj;
return std::move(strm).str();
}