mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

remove unnecessary parameter copies

Browse source
This commit is contained in:
Nuno Lopes 2023-12-22 16:11:06 +00:00
parent ab22e763d7
commit cab3c45863
9 changed files with 23 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/array_decl_plugin.cpp
View file

@ -49,7 +49,7 @@ sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
return nullptr;
}
parameter params[2] = { parameters[0], parameter(m_manager->mk_bool_sort()) };
parameter params[2] = { parameter(parameters[0]), parameter(m_manager->mk_bool_sort()) };
return mk_sort(ARRAY_SORT, 2, params);
}
SASSERT(k == ARRAY_SORT);

10
src/ast/ast.cpp
View file

@ -48,21 +48,13 @@ parameter::~parameter() {
}
}
parameter& parameter::operator=(parameter const& other) {
if (this == &other) {
return *this;
}
this->~parameter();
m_val = other.m_val;
parameter::parameter(parameter const& other) : m_val(other.m_val) {
if (auto p = std::get_if<rational*>(&m_val)) {
m_val = alloc(rational, **p);
}
if (auto p = std::get_if<zstring*>(&m_val)) {
m_val = alloc(zstring, **p);
}
return *this;
}
void parameter::init_eh(ast_manager & m) {

9
src/ast/ast.h
View file

@ -142,7 +142,7 @@ public:
explicit parameter(const char *s): m_val(symbol(s)) {}
explicit parameter(const std::string &s): m_val(symbol(s)) {}
explicit parameter(unsigned ext_id, bool): m_val(ext_id) {}
parameter(parameter const& other) { *this = other; }
explicit parameter(parameter const& other);
parameter(parameter && other) noexcept : m_val(std::move(other.m_val)) {
other.m_val = 0;
@ -150,7 +150,10 @@ public:
~parameter();
parameter& operator=(parameter const& other);
parameter& operator=(parameter && other) {
std::swap(other.m_val, m_val);
return *this;
}
kind_t get_kind() const { return static_cast<kind_t>(m_val.index()); }
bool is_int() const { return get_kind() == PARAM_INT; }
@ -1099,7 +1102,7 @@ public:
// Event handlers for deleting/translating PARAM_EXTERNAL
virtual void del(parameter const & p) {}
virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return p; }
virtual parameter translate(parameter const & p, decl_plugin & target) { UNREACHABLE(); return {}; }
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
};

8
src/ast/ast_lt.cpp
View file

@ -68,8 +68,8 @@ bool lt(ast * n1, ast * n2) {
num = to_sort(n1)->get_num_parameters();
SASSERT(num > 0);
for (unsigned i = 0; i < num; i++) {
parameter p1 = to_sort(n1)->get_parameter(i);
parameter p2 = to_sort(n2)->get_parameter(i);
const parameter &p1 = to_sort(n1)->get_parameter(i);
const parameter &p2 = to_sort(n2)->get_parameter(i);
check_parameter(p1, p2);
}
UNREACHABLE();
@ -80,8 +80,8 @@ bool lt(ast * n1, ast * n2) {
check_value(to_func_decl(n1)->get_num_parameters(), to_func_decl(n2)->get_num_parameters());
num = to_func_decl(n1)->get_num_parameters();
for (unsigned i = 0; i < num; i++) {
parameter p1 = to_func_decl(n1)->get_parameter(i);
parameter p2 = to_func_decl(n2)->get_parameter(i);
const parameter &p1 = to_func_decl(n1)->get_parameter(i);
const parameter &p2 = to_func_decl(n2)->get_parameter(i);
check_parameter(p1, p2);
}
num = to_func_decl(n1)->get_arity();

5
src/ast/bv_decl_plugin.cpp
View file

@ -454,9 +454,8 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
// This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
// After SMT-COMP, I should find all offending modules.
// For now, I will just simplify the numeral here.
rational v = parameters[0].get_rational();
parameter p0(mod2k(v, bv_size));
parameter ps[2] = { std::move(p0), parameters[1] };
const rational &v = parameters[0].get_rational();
parameter ps[2] = { parameter(mod2k(v, bv_size)), parameter(parameters[1]) };
sort * bv = get_bv_sort(bv_size);
return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
}

2
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -319,7 +319,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
if (m_fpa_util.is_to_sbv(f) || m_fpa_util.is_to_ubv(f)) {
auto k = m_fpa_util.is_to_sbv(f) ? OP_FPA_TO_SBV_I : OP_FPA_TO_UBV_I;
parameter param = f->get_parameter(0);
const parameter &param = f->get_parameter(0);
func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, &param, dom.size(), dom.data()), m);
expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m);
result->set_else(else_value);

3
src/ast/fpa_decl_plugin.cpp
View file

@ -208,8 +208,7 @@ sort * fpa_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
if (ebits > 63)
m_manager->raise_exception("maximum number of exponent bits is 63");
parameter p1(ebits), p2(sbits);
parameter ps[2] = { p1, p2 };
parameter ps[2] = { parameter(ebits), parameter(sbits) };
sort_size sz;
sz = sort_size::mk_very_big(); // TODO: refine
return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOATING_POINT_SORT, sz, 2, ps));

12
src/ast/polymorphism_util.cpp
View file

@ -40,7 +40,7 @@ namespace polymorphism {
unsigned n = s->get_num_parameters();
vector<parameter> ps;
for (unsigned i = 0; i < n; ++i) {
auto p = s->get_parameter(i);
auto &p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
sort_ref s = (*this)(to_sort(p.get_ast()));
ps.push_back(parameter(s.get()));
@ -167,8 +167,8 @@ namespace polymorphism {
if (s1->get_num_parameters() != s2->get_num_parameters())
return false;
for (unsigned i = s1->get_num_parameters(); i-- > 0;) {
auto p1 = s1->get_parameter(i);
auto p2 = s2->get_parameter(i);
auto &p1 = s1->get_parameter(i);
auto &p2 = s2->get_parameter(i);
if (p1.is_ast() && is_sort(p1.get_ast())) {
if (!p2.is_ast())
return false;
@ -204,8 +204,8 @@ namespace polymorphism {
if (s1->get_num_parameters() != s2->get_num_parameters())
return false;
for (unsigned i = s1->get_num_parameters(); i-- > 0;) {
auto p1 = s1->get_parameter(i);
auto p2 = s2->get_parameter(i);
auto &p1 = s1->get_parameter(i);
auto &p2 = s2->get_parameter(i);
if (p1.is_ast() && is_sort(p1.get_ast())) {
if (!p2.is_ast())
return false;
@ -282,7 +282,7 @@ namespace polymorphism {
}
vector<parameter> params;
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter p = s->get_parameter(i);
const parameter &p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
sort_ref fs = fresh(to_sort(p.get_ast()));
params.push_back(parameter(fs.get()));

6
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -209,10 +209,6 @@ namespace spacer {
static proof_ref mk_th_lemma(ast_manager &m, ptr_buffer<proof> const &parents,
unsigned num_params, parameter const *params) {
buffer<parameter> v;
for (unsigned i = 1; i < num_params; ++i)
v.push_back(params[i]);
SASSERT(params[0].is_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
@ -220,7 +216,7 @@ namespace spacer {
proof_ref pf(m);
pf = m.mk_th_lemma(tid, m.mk_false(),
parents.size(), parents.data(),
v.size(), v.data());
num_params - 1, params + 1);
return pf;
}