mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity

Revert "Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage"

Browse source 
This reverts commit d9bdb6b83c, reversing
changes made to 8b188621a5.
This commit is contained in:
Lev Nachmanson 2026-01-13 18:18:07 -10:00
parent 3bf271bb42
commit d5e0216070
7 changed files with 104 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/ast/seq_decl_plugin.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "ast/array_decl_plugin.h"
#include "ast/ast_pp.h"
#include <sstream>
#include <format>
seq_decl_plugin::seq_decl_plugin(): m_init(false),
@ -83,8 +82,10 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor
ptr_vector<sort> binding;
ast_manager& m = *m_manager;
if (dsz == 0) {
m.raise_exception(std::format("Unexpected number of arguments to '{}' at least one argument expected {} given",
sig.m_name.str(), dsz));
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());
}
bool is_match = true;
for (unsigned i = 0; is_match && i < dsz; ++i) {
@ -95,16 +96,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::string domain_str;
std::ostringstream strm;
strm << "Sort of function '" << sig.m_name << "' ";
strm << "does not match the declared type. Given domain: ";
for (unsigned i = 0; i < dsz; ++i) {
domain_str += to_string(mk_pp(dom[i], m)) + " ";
strm << mk_pp(dom[i], m) << " ";
}
std::string range_str;
if (range) {
range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
strm << " and range: " << mk_pp(range, m);
}
m.raise_exception(std::format("Sort of function '{}' does not match the declared type. Given domain: {}{}",
sig.m_name.str(), domain_str, range_str));
m.raise_exception(strm.str());
}
range_out = apply_binding(binding, sig.m_range);
SASSERT(range_out);
@ -114,8 +115,10 @@ 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) {
m.raise_exception(std::format("Unexpected number of arguments to '{}' {} arguments expected {} given",
sig.m_name.str(), 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());
}
bool is_match = true;
for (unsigned i = 0; is_match && i < dsz; ++i) {
@ -125,25 +128,28 @@ 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::string given_domain;
std::ostringstream strm;
strm << "Sort of polymorphic function '" << sig.m_name << "' ";
strm << "does not match the declared type. ";
strm << "\nGiven domain: ";
for (unsigned i = 0; i < dsz; ++i) {
given_domain += to_string(mk_pp(dom[i], m)) + " ";
strm << mk_pp(dom[i], m) << " ";
}
std::string range_str;
if (range) {
range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
strm << " and range: " << mk_pp(range, m);
}
std::string expected_domain;
strm << "\nExpected domain: ";
for (unsigned i = 0; i < dsz; ++i) {
expected_domain += to_string(mk_pp(sig.m_dom[i].get(), m)) + " ";
strm << mk_pp(sig.m_dom[i].get(), m) << " ";
}
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));
m.raise_exception(strm.str());
}
if (!range && dsz == 0) {
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()));
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());
}
range_out = apply_binding(m_binding, sig.m_range);
SASSERT(range_out);