mirror of
https://github.com/Z3Prover/z3
synced 2026-01-15 15:16:15 +00:00
Add [[nodiscard]] to AST factory functions and modernize iterator loops (#8143)
* Initial plan * Add [[nodiscard]] to AST factory functions and modernize iterator loops - Added [[nodiscard]] attribute to key factory functions in ast.h: - All mk_app() variants for creating application nodes - All mk_func_decl() variants for creating function declarations - All mk_const() variants for creating constants - All mk_sort() variants for creating sorts - mk_var() for creating variables - mk_quantifier(), mk_forall(), mk_exists(), mk_lambda() for quantifiers - mk_label(), mk_pattern() and related functions - Converted iterator loops to range-based for loops in: - src/util/region.cpp: pop_scope() - src/util/dec_ref_util.h: dec_ref_key_values(), dec_ref_keys(), dec_ref_values() - src/util/mpf.h: dispose() - src/util/numeral_buffer.h: reset() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Modernize additional iterator loops to range-based for loops - Converted iterator loops to range-based for loops in: - src/api/api_ast_map.cpp: Z3_ast_map_keys() and Z3_ast_map_to_string() - src/api/c++/z3++.h: optimize copy constructor and add() method - src/opt/wmax.cpp: mk_assumptions() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert changes to z3++.h for C++ version compatibility Revert the range-based for loop changes in src/api/c++/z3++.h to maintain compatibility with older C++ versions that users may rely on. The C++ API wrapper must support down-level C++ standards for backward compatibility. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Trigger CI build [skip ci] is not used to ensure CI runs --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
d29fc3eef3
commit
6c90b7ec3f
7 changed files with 89 additions and 104 deletions
|
|
@ -138,10 +138,8 @@ extern "C" {
|
|||
RESET_ERROR_CODE();
|
||||
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), to_ast_map(m)->m);
|
||||
mk_c(c)->save_object(v);
|
||||
obj_map<ast, ast*>::iterator it = to_ast_map_ref(m).begin();
|
||||
obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();
|
||||
for (; it != end; ++it) {
|
||||
v->m_ast_vector.push_back(it->m_key);
|
||||
for (auto const& kv : to_ast_map_ref(m)) {
|
||||
v->m_ast_vector.push_back(kv.m_key);
|
||||
}
|
||||
Z3_ast_vector r = of_ast_vector(v);
|
||||
RETURN_Z3(r);
|
||||
|
|
@ -155,10 +153,8 @@ extern "C" {
|
|||
std::ostringstream buffer;
|
||||
ast_manager & mng = to_ast_map(m)->m;
|
||||
buffer << "(ast-map";
|
||||
obj_map<ast, ast*>::iterator it = to_ast_map_ref(m).begin();
|
||||
obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();
|
||||
for (; it != end; ++it) {
|
||||
buffer << "\n (" << mk_ismt2_pp(it->m_key, mng, 3) << "\n " << mk_ismt2_pp(it->m_value, mng, 3) << ")";
|
||||
for (auto const& kv : to_ast_map_ref(m)) {
|
||||
buffer << "\n (" << mk_ismt2_pp(kv.m_key, mng, 3) << "\n " << mk_ismt2_pp(kv.m_value, mng, 3) << ")";
|
||||
}
|
||||
buffer << ')';
|
||||
return mk_c(c)->mk_external_string(std::move(buffer).str());
|
||||
|
|
|
|||
140
src/ast/ast.h
140
src/ast/ast.h
|
|
@ -1719,13 +1719,13 @@ private:
|
|||
sort * mk_sort(symbol const & name, sort_info * info);
|
||||
|
||||
public:
|
||||
sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
|
||||
[[nodiscard]] sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
|
||||
|
||||
sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, nullptr); }
|
||||
[[nodiscard]] sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, nullptr); }
|
||||
|
||||
sort * mk_type_var(symbol const& name);
|
||||
[[nodiscard]] sort * mk_type_var(symbol const& name);
|
||||
|
||||
sort * mk_sort(symbol const & name, sort_info const & info) {
|
||||
[[nodiscard]] sort * mk_sort(symbol const & name, sort_info const & info) {
|
||||
if (info.get_family_id() == null_family_id) {
|
||||
return mk_uninterpreted_sort(name);
|
||||
}
|
||||
|
|
@ -1734,15 +1734,15 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr);
|
||||
[[nodiscard]] sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr);
|
||||
|
||||
sort * substitute(sort* s, unsigned n, sort * const * src, sort * const * dst);
|
||||
[[nodiscard]] sort * substitute(sort* s, unsigned n, sort * const * src, sort * const * dst);
|
||||
|
||||
sort * mk_bool_sort() const { return m_bool_sort; }
|
||||
[[nodiscard]] sort * mk_bool_sort() const { return m_bool_sort; }
|
||||
|
||||
sort * mk_proof_sort() const { return m_proof_sort; }
|
||||
[[nodiscard]] sort * mk_proof_sort() const { return m_proof_sort; }
|
||||
|
||||
sort * mk_fresh_sort(char const * prefix = "");
|
||||
[[nodiscard]] sort * mk_fresh_sort(char const * prefix = "");
|
||||
|
||||
bool is_uninterp(sort const * s) const { return s->get_family_id() == null_family_id || s->get_family_id() == user_sort_family_id; }
|
||||
|
||||
|
|
@ -1767,24 +1767,24 @@ public:
|
|||
|
||||
bool has_type_var(unsigned n, sort* const* domain, sort* range) const;
|
||||
|
||||
func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
[[nodiscard]] func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned arity, sort * const * domain, sort * range = nullptr);
|
||||
|
||||
func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
[[nodiscard]] func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
|
||||
unsigned num_args, expr * const * args, sort * range = nullptr);
|
||||
|
||||
app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr,
|
||||
[[nodiscard]] app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr,
|
||||
unsigned num_args = 0, expr * const * args = nullptr, sort * range = nullptr);
|
||||
|
||||
app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args);
|
||||
[[nodiscard]] app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args);
|
||||
|
||||
app * mk_app(family_id fid, decl_kind k, expr * arg);
|
||||
[[nodiscard]] app * mk_app(family_id fid, decl_kind k, expr * arg);
|
||||
|
||||
app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2);
|
||||
[[nodiscard]] app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2);
|
||||
|
||||
app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
|
||||
[[nodiscard]] app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
|
||||
|
||||
app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast<expr * const *>(nullptr)); }
|
||||
[[nodiscard]] app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast<expr * const *>(nullptr)); }
|
||||
private:
|
||||
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
|
||||
func_decl_info * info);
|
||||
|
|
@ -1794,11 +1794,11 @@ private:
|
|||
app * mk_app_core(func_decl * decl, unsigned num_args, expr * const * args);
|
||||
|
||||
public:
|
||||
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
|
||||
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
|
||||
func_decl_info const & info) {
|
||||
if (info.is_null()) {
|
||||
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
|
||||
|
|
@ -1808,55 +1808,55 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(unsigned arity, sort * const * domain, func_decl_info const & info) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(unsigned arity, sort * const * domain, func_decl_info const & info) {
|
||||
return mk_func_decl(info.get_family_id(), info.get_decl_kind(), info.get_num_parameters(), info.get_parameters(),
|
||||
arity, domain);
|
||||
}
|
||||
|
||||
func_decl * mk_skolem_const_decl(symbol const& name, sort* s) {
|
||||
[[nodiscard]] func_decl * mk_skolem_const_decl(symbol const& name, sort* s) {
|
||||
func_decl_info info;
|
||||
info.set_skolem(true);
|
||||
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
|
||||
}
|
||||
|
||||
func_decl * mk_const_decl(const char* name, sort * s) {
|
||||
[[nodiscard]] func_decl * mk_const_decl(const char* name, sort * s) {
|
||||
return mk_func_decl(symbol(name), static_cast<unsigned>(0), nullptr, s);
|
||||
}
|
||||
|
||||
func_decl * mk_const_decl(std::string const& name, sort * s) {
|
||||
[[nodiscard]] func_decl * mk_const_decl(std::string const& name, sort * s) {
|
||||
return mk_func_decl(symbol(name.c_str()), static_cast<unsigned>(0), nullptr, s);
|
||||
}
|
||||
|
||||
func_decl * mk_const_decl(symbol const & name, sort * s) {
|
||||
[[nodiscard]] func_decl * mk_const_decl(symbol const & name, sort * s) {
|
||||
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s);
|
||||
}
|
||||
|
||||
func_decl * mk_const_decl(symbol const & name, sort * s, func_decl_info const & info) {
|
||||
[[nodiscard]] func_decl * mk_const_decl(symbol const & name, sort * s, func_decl_info const & info) {
|
||||
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range, func_decl_info const & info) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range, func_decl_info const & info) {
|
||||
return mk_func_decl(name, 1, &domain, range, info);
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range) {
|
||||
return mk_func_decl(name, 1, &domain, range);
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, func_decl_info const & info) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, func_decl_info const & info) {
|
||||
sort * d[2] = { domain1, domain2 };
|
||||
return mk_func_decl(name, 2, d, range, info);
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range) {
|
||||
sort * d[2] = { domain1, domain2 };
|
||||
return mk_func_decl(name, 2, d, range);
|
||||
}
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
|
||||
bool assoc, bool comm = false, bool inj = false);
|
||||
|
||||
func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, bool assoc, bool comm = false) {
|
||||
[[nodiscard]] func_decl * mk_func_decl(symbol const & name, sort * domain1, sort * domain2, sort * range, bool assoc, bool comm = false) {
|
||||
sort * d[2] = { domain1, domain2 };
|
||||
return mk_func_decl(name, 2, d, range, assoc, comm, false);
|
||||
}
|
||||
|
|
@ -1869,113 +1869,113 @@ public:
|
|||
return !p || p->is_considered_uninterpreted(f);
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, unsigned num_args, expr * const * args);
|
||||
|
||||
app* mk_app(func_decl* decl, ref_vector<expr, ast_manager> const& args) {
|
||||
[[nodiscard]] app* mk_app(func_decl* decl, ref_vector<expr, ast_manager> const& args) {
|
||||
return mk_app(decl, args.size(), args.data());
|
||||
}
|
||||
|
||||
app* mk_app(func_decl* decl, ref_buffer<expr, ast_manager> const& args) {
|
||||
[[nodiscard]] app* mk_app(func_decl* decl, ref_buffer<expr, ast_manager> const& args) {
|
||||
return mk_app(decl, args.size(), args.data());
|
||||
}
|
||||
|
||||
app* mk_app(func_decl* decl, ref_vector<app, ast_manager> const& args) {
|
||||
[[nodiscard]] app* mk_app(func_decl* decl, ref_vector<app, ast_manager> const& args) {
|
||||
return mk_app(decl, args.size(), (expr*const*)args.data());
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, ptr_vector<expr> const& args) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, ptr_vector<expr> const& args) {
|
||||
return mk_app(decl, args.size(), args.data());
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, ptr_buffer<expr> const& args) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, ptr_buffer<expr> const& args) {
|
||||
return mk_app(decl, args.size(), args.data());
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, ptr_vector<app> const& args) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, ptr_vector<app> const& args) {
|
||||
return mk_app(decl, args.size(), (expr*const*)args.data());
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, expr * const * args) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, expr * const * args) {
|
||||
return mk_app(decl, decl->get_arity(), args);
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, expr * arg) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, expr * arg) {
|
||||
SASSERT(decl->get_arity() == 1);
|
||||
return mk_app(decl, 1, &arg);
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, expr * arg1, expr * arg2) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, expr * arg1, expr * arg2) {
|
||||
SASSERT(decl->get_arity() == 2);
|
||||
expr * args[2] = { arg1, arg2 };
|
||||
return mk_app(decl, 2, args);
|
||||
}
|
||||
|
||||
app * mk_app(func_decl * decl, expr * arg1, expr * arg2, expr * arg3) {
|
||||
[[nodiscard]] app * mk_app(func_decl * decl, expr * arg1, expr * arg2, expr * arg3) {
|
||||
SASSERT(decl->get_arity() == 3);
|
||||
expr * args[3] = { arg1, arg2, arg3 };
|
||||
return mk_app(decl, 3, args);
|
||||
}
|
||||
|
||||
app * mk_app(symbol const& name, unsigned n, expr* const* args, sort* range);
|
||||
[[nodiscard]] app * mk_app(symbol const& name, unsigned n, expr* const* args, sort* range);
|
||||
|
||||
app * mk_const(func_decl * decl) {
|
||||
[[nodiscard]] app * mk_const(func_decl * decl) {
|
||||
SASSERT(decl->get_arity() == 0);
|
||||
return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));
|
||||
}
|
||||
|
||||
app * mk_skolem_const(symbol const & name, sort * s) {
|
||||
[[nodiscard]] app * mk_skolem_const(symbol const & name, sort * s) {
|
||||
return mk_const(mk_skolem_const_decl(name, s));
|
||||
}
|
||||
|
||||
app * mk_const(symbol const & name, sort * s) {
|
||||
[[nodiscard]] app * mk_const(symbol const & name, sort * s) {
|
||||
return mk_const(mk_const_decl(name, s));
|
||||
}
|
||||
|
||||
app * mk_const(std::string const & name, sort * s) {
|
||||
[[nodiscard]] app * mk_const(std::string const & name, sort * s) {
|
||||
return mk_const(mk_const_decl(name, s));
|
||||
}
|
||||
|
||||
app * mk_const(char const* name, sort * s) {
|
||||
[[nodiscard]] app * mk_const(char const* name, sort * s) {
|
||||
return mk_const(mk_const_decl(name, s));
|
||||
}
|
||||
|
||||
func_decl * mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity,
|
||||
[[nodiscard]] func_decl * mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity,
|
||||
sort * const * domain, sort * range, bool skolem = true);
|
||||
|
||||
func_decl * mk_fresh_func_decl(unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
|
||||
[[nodiscard]] func_decl * mk_fresh_func_decl(unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
|
||||
return mk_fresh_func_decl(symbol::null, symbol::null, arity, domain, range, skolem);
|
||||
}
|
||||
|
||||
func_decl * mk_fresh_func_decl(char const * prefix, char const * suffix, unsigned arity,
|
||||
[[nodiscard]] func_decl * mk_fresh_func_decl(char const * prefix, char const * suffix, unsigned arity,
|
||||
sort * const * domain, sort * range, bool skolem = true) {
|
||||
return mk_fresh_func_decl(symbol(prefix), symbol(suffix), arity, domain, range, skolem);
|
||||
}
|
||||
|
||||
func_decl * mk_fresh_func_decl(char const * prefix, unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
|
||||
[[nodiscard]] func_decl * mk_fresh_func_decl(char const * prefix, unsigned arity, sort * const * domain, sort * range, bool skolem = true) {
|
||||
return mk_fresh_func_decl(symbol(prefix), symbol::null, arity, domain, range, skolem);
|
||||
}
|
||||
|
||||
bool is_parametric_function(func_decl* f, func_decl *& g) const;
|
||||
|
||||
app * mk_fresh_const(char const * prefix, sort * s, bool skolem = true) {
|
||||
[[nodiscard]] app * mk_fresh_const(char const * prefix, sort * s, bool skolem = true) {
|
||||
return mk_const(mk_fresh_func_decl(prefix, 0, nullptr, s, skolem));
|
||||
}
|
||||
|
||||
app * mk_fresh_const(std::string const& prefix, sort * s, bool skolem = true) {
|
||||
[[nodiscard]] app * mk_fresh_const(std::string const& prefix, sort * s, bool skolem = true) {
|
||||
return mk_fresh_const(prefix.c_str(), s, skolem);
|
||||
}
|
||||
|
||||
app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) {
|
||||
[[nodiscard]] app * mk_fresh_const(symbol const& prefix, sort * s, bool skolem = true) {
|
||||
return mk_const(mk_fresh_func_decl(prefix, symbol::null, 0, nullptr, s, skolem));
|
||||
}
|
||||
|
||||
symbol mk_fresh_var_name(char const * prefix = nullptr);
|
||||
[[nodiscard]] symbol mk_fresh_var_name(char const * prefix = nullptr);
|
||||
|
||||
var * mk_var(unsigned idx, sort * ty);
|
||||
[[nodiscard]] var * mk_var(unsigned idx, sort * ty);
|
||||
|
||||
app * mk_label(bool pos, unsigned num_names, symbol const * names, expr * n);
|
||||
[[nodiscard]] app * mk_label(bool pos, unsigned num_names, symbol const * names, expr * n);
|
||||
|
||||
app * mk_label(bool pos, symbol const & name, expr * n);
|
||||
[[nodiscard]] app * mk_label(bool pos, symbol const & name, expr * n);
|
||||
|
||||
bool is_label(expr const * n, bool & pos, buffer<symbol> & names) const;
|
||||
|
||||
|
|
@ -1999,9 +1999,9 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
app * mk_label_lit(unsigned num_names, symbol const * names);
|
||||
[[nodiscard]] app * mk_label_lit(unsigned num_names, symbol const * names);
|
||||
|
||||
app * mk_label_lit(symbol const & name);
|
||||
[[nodiscard]] app * mk_label_lit(symbol const & name);
|
||||
|
||||
bool is_label_lit(expr const * n, buffer<symbol> & names) const;
|
||||
|
||||
|
|
@ -2009,9 +2009,9 @@ public:
|
|||
|
||||
family_id get_label_family_id() const { return label_family_id; }
|
||||
|
||||
app * mk_pattern(unsigned num_exprs, app * const * exprs);
|
||||
[[nodiscard]] app * mk_pattern(unsigned num_exprs, app * const * exprs);
|
||||
|
||||
app * mk_pattern(app * expr) { return mk_pattern(1, &expr); }
|
||||
[[nodiscard]] app * mk_pattern(app * expr) { return mk_pattern(1, &expr); }
|
||||
|
||||
bool is_pattern(expr const * n) const;
|
||||
|
||||
|
|
@ -2019,12 +2019,12 @@ public:
|
|||
|
||||
public:
|
||||
|
||||
quantifier * mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
[[nodiscard]] quantifier * mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
|
||||
unsigned num_patterns = 0, expr * const * patterns = nullptr,
|
||||
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr);
|
||||
|
||||
quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
[[nodiscard]] quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
|
||||
unsigned num_patterns = 0, expr * const * patterns = nullptr,
|
||||
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
|
||||
|
|
@ -2032,7 +2032,7 @@ public:
|
|||
num_no_patterns, no_patterns);
|
||||
}
|
||||
|
||||
quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
[[nodiscard]] quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
|
||||
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
|
||||
unsigned num_patterns = 0, expr * const * patterns = nullptr,
|
||||
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
|
||||
|
|
@ -2040,13 +2040,13 @@ public:
|
|||
num_no_patterns, no_patterns);
|
||||
}
|
||||
|
||||
quantifier * mk_lambda(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body);
|
||||
[[nodiscard]] quantifier * mk_lambda(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body);
|
||||
|
||||
quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body);
|
||||
[[nodiscard]] quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body);
|
||||
|
||||
quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, unsigned new_num_no_patterns, expr * const * new_no_patterns, expr * new_body);
|
||||
[[nodiscard]] quantifier * update_quantifier(quantifier * q, unsigned new_num_patterns, expr * const * new_patterns, unsigned new_num_no_patterns, expr * const * new_no_patterns, expr * new_body);
|
||||
|
||||
quantifier * update_quantifier(quantifier * q, expr * new_body);
|
||||
[[nodiscard]] quantifier * update_quantifier(quantifier * q, expr * new_body);
|
||||
|
||||
quantifier * update_quantifier_weight(quantifier * q, int new_weight);
|
||||
|
||||
|
|
|
|||
|
|
@ -129,9 +129,8 @@ namespace opt {
|
|||
|
||||
void mk_assumptions(expr_ref_vector& asms) {
|
||||
ptr_vector<expr> _asms;
|
||||
obj_map<expr, rational>::iterator it = m_weights.begin(), end = m_weights.end();
|
||||
for (; it != end; ++it) {
|
||||
_asms.push_back(it->m_key);
|
||||
for (auto const& kv : m_weights) {
|
||||
_asms.push_back(kv.m_key);
|
||||
}
|
||||
compare_asm comp(*this);
|
||||
std::sort(_asms.begin(),_asms.end(), comp);
|
||||
|
|
|
|||
|
|
@ -25,11 +25,9 @@ Notes:
|
|||
*/
|
||||
template<typename Mng, typename Map>
|
||||
void dec_ref_key_values(Mng & m, Map & map) {
|
||||
typename Map::iterator it = map.begin();
|
||||
typename Map::iterator end = map.end();
|
||||
for (; it != end; ++it) {
|
||||
m.dec_ref(it->m_key);
|
||||
m.dec_ref(it->m_value);
|
||||
for (auto& kv : map) {
|
||||
m.dec_ref(kv.m_key);
|
||||
m.dec_ref(kv.m_value);
|
||||
}
|
||||
map.reset();
|
||||
}
|
||||
|
|
@ -40,10 +38,8 @@ void dec_ref_key_values(Mng & m, Map & map) {
|
|||
*/
|
||||
template<typename Mng, typename Map>
|
||||
void dec_ref_keys(Mng & m, Map & map) {
|
||||
typename Map::iterator it = map.begin();
|
||||
typename Map::iterator end = map.end();
|
||||
for (; it != end; ++it) {
|
||||
m.dec_ref(it->m_key);
|
||||
for (auto& kv : map) {
|
||||
m.dec_ref(kv.m_key);
|
||||
}
|
||||
map.reset();
|
||||
}
|
||||
|
|
@ -55,10 +51,8 @@ void dec_ref_keys(Mng & m, Map & map) {
|
|||
*/
|
||||
template<typename Mng, typename Map>
|
||||
void dec_ref_values(Mng & m, Map & map) {
|
||||
typename Map::iterator it = map.begin();
|
||||
typename Map::iterator end = map.end();
|
||||
for (; it != end; ++it) {
|
||||
m.dec_ref(it->m_value);
|
||||
for (auto& kv : map) {
|
||||
m.dec_ref(kv.m_value);
|
||||
}
|
||||
map.reset();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -247,9 +247,9 @@ protected:
|
|||
}
|
||||
|
||||
void dispose(u_map<mpz*> & map) {
|
||||
for (u_map<mpz*>::iterator it = map.begin(); it != map.end(); it++) {
|
||||
m.del(*it->m_value);
|
||||
dealloc(it->m_value);
|
||||
for (auto& kv : map) {
|
||||
m.del(*kv.m_value);
|
||||
dealloc(kv.m_value);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -68,10 +68,8 @@ public:
|
|||
}
|
||||
|
||||
void reset() {
|
||||
typename vector<Numeral>::iterator it = m_buffer.begin();
|
||||
typename vector<Numeral>::iterator end = m_buffer.end();
|
||||
for (; it != end; ++it)
|
||||
m().del(*it);
|
||||
for (auto& numeral : m_buffer)
|
||||
m().del(numeral);
|
||||
m_buffer.reset();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -40,9 +40,7 @@ void region::reset() {
|
|||
void region::pop_scope() {
|
||||
unsigned old_size = m_scopes.back();
|
||||
m_scopes.pop_back();
|
||||
ptr_vector<char>::iterator it = m_chunks.begin() + old_size;
|
||||
ptr_vector<char>::iterator end = m_chunks.end();
|
||||
for (; it != end; ++it)
|
||||
for (auto it = m_chunks.begin() + old_size; it != m_chunks.end(); ++it)
|
||||
dealloc_svect(*it);
|
||||
m_chunks.shrink(old_size);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue