mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Modernize more files to use std::format: bv_decl_plugin, dl_decl_plugin, datatype_decl_plugin, seq_decl_plugin

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:34:47 +00:00
parent 99a40e79d4
commit 64957e2b0e
4 changed files with 34 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/bv_decl_plugin.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include<sstream>
#include<format>
#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;
}
}

9
src/ast/datatype_decl_plugin.cpp
View file

@ -17,6 +17,8 @@ Revision History:
--*/
#include<sstream>
#include<format>
#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];

5
src/ast/dl_decl_plugin.cpp
View file

@ -17,6 +17,7 @@ Revision History:
--*/
#include<sstream>
#include<format>
#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;
}

48
src/ast/seq_decl_plugin.cpp
View file

@ -21,6 +21,7 @@ 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),
@ -82,10 +83,8 @@ 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) {
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);