mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

bv_decl_plugin: remove some mem allocs of parameters

Browse source
This commit is contained in:
Nuno Lopes 2018-07-12 18:36:09 +01:00
parent 5314ae60cc
commit b7ea90c12b
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/bv_decl_plugin.cpp
View file

@ -401,7 +401,7 @@ bool bv_decl_plugin::get_int2bv_size(unsigned num_parameters, parameter const *
m_manager->raise_exception("int2bv expects one parameter");
return false;
}
parameter p(parameters[0]);
const parameter &p = parameters[0];
if (p.is_int()) {
result = p.get_int();
return true;
@ -428,7 +428,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
// After SMT-COMP, I should find all offending modules.
// For now, I will just simplify the numeral here.
parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
parameter ps[2] = { p0, parameters[1] };
parameter ps[2] = { std::move(p0), 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));
}
@ -746,7 +746,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
expr * bv_decl_plugin::get_some_value(sort * s) {
SASSERT(s->is_sort_of(m_family_id, BV_SORT));
unsigned bv_size = s->get_parameter(0).get_int();
parameter p[2] = { parameter(rational(0)), parameter(static_cast<int>(bv_size)) };
parameter p[2] = { parameter(rational::zero()), parameter(static_cast<int>(bv_size)) };
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, nullptr);
}