diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index f38894d06..bd9d954c7 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -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); diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index f3be7d2c6..e1e3efe99 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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(&m_val)) { m_val = alloc(rational, **p); } if (auto p = std::get_if(&m_val)) { m_val = alloc(zstring, **p); } - return *this; } void parameter::init_eh(ast_manager & m) { diff --git a/src/ast/ast.h b/src/ast/ast.h index 9618c7e12..053390022 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -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(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; } }; diff --git a/src/ast/ast_lt.cpp b/src/ast/ast_lt.cpp index 3537dc71e..869c7bff8 100644 --- a/src/ast/ast_lt.cpp +++ b/src/ast/ast_lt.cpp @@ -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(); diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 30cfe4cdb..6b2106f3f 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -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)); } diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index cc2abf01c..a3008851b 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -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 ¶m = f->get_parameter(0); func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, ¶m, 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); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 78d300ca7..76e44278d 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -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)); diff --git a/src/ast/polymorphism_util.cpp b/src/ast/polymorphism_util.cpp index 1c961d21f..3431dd034 100644 --- a/src/ast/polymorphism_util.cpp +++ b/src/ast/polymorphism_util.cpp @@ -40,7 +40,7 @@ namespace polymorphism { unsigned n = s->get_num_parameters(); vector 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 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())); diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 800a63291..9fbd4e01c 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -209,10 +209,6 @@ namespace spacer { static proof_ref mk_th_lemma(ast_manager &m, ptr_buffer const &parents, unsigned num_params, parameter const *params) { - buffer 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; }