diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index e2e6a9fab..ce1eed52c 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -251,7 +251,7 @@ namespace api { save_ast_trail(exprs[0]); return exprs[0]; default: { - expr * a = m().mk_and(num_exprs, exprs); + expr * a = m().mk_and(std::span(exprs, num_exprs)); save_ast_trail(a); return a; } } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ebeba94be..188146d6a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1913,6 +1913,10 @@ app * ast_manager::mk_app(family_id fid, decl_kind k, unsigned num_args, expr * return mk_app(fid, k, 0, nullptr, num_args, args); } +app * ast_manager::mk_app(family_id fid, decl_kind k, std::span args) { + return mk_app(fid, k, 0, nullptr, args.size(), args.data()); +} + app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg) { return mk_app(fid, k, 0, nullptr, 1, &arg); } diff --git a/src/ast/ast.h b/src/ast/ast.h index dfdad9e0f..63f3407c4 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1791,6 +1791,8 @@ public: [[nodiscard]] 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, std::span args); + [[nodiscard]] app * mk_app(family_id fid, decl_kind k, expr * arg); [[nodiscard]] app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2); @@ -1806,6 +1808,8 @@ private: app * mk_app_core(func_decl * decl, unsigned num_args, expr * const * args); + app * mk_and(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_AND, num_args, args); } + public: [[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(nullptr)); @@ -2201,17 +2205,17 @@ public: app * mk_xor(ptr_vector const& args) { return mk_xor(args.size(), args.data()); } app * mk_xor(ref_buffer const& args) { return mk_xor(args.size(), args.data()); } app * mk_or(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_OR, num_args, args); } - app * mk_and(unsigned num_args, expr * const * args) { return mk_app(basic_family_id, OP_AND, num_args, args); } + app * mk_and(std::span args) { return mk_app(basic_family_id, OP_AND, args); } app * mk_or(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_OR, arg1, arg2); } app * mk_and(expr * arg1, expr * arg2) { return mk_app(basic_family_id, OP_AND, arg1, arg2); } app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_OR, arg1, arg2, arg3); } app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(basic_family_id, OP_OR, 4, args); } app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(basic_family_id, OP_AND, arg1, arg2, arg3); } - app * mk_and(ref_vector const& args) { return mk_and(args.size(), args.data()); } - app * mk_and(ptr_vector const& args) { return mk_and(args.size(), args.data()); } - app * mk_and(ref_buffer const& args) { return mk_and(args.size(), args.data()); } - app * mk_and(ptr_buffer const& args) { return mk_and(args.size(), args.data()); } + app * mk_and(ref_vector const& args) { return mk_and(std::span(args.data(), args.size())); } + app * mk_and(ptr_vector const& args) { return mk_and(std::span(args.data(), args.size())); } + app * mk_and(ref_buffer const& args) { return mk_and(std::span(args.data(), args.size())); } + app * mk_and(ptr_buffer const& args) { return mk_and(std::span(args.data(), args.size())); } app * mk_or(ref_vector const& args) { return mk_or(args.size(), args.data()); } app * mk_or(ptr_vector const& args) { return mk_or(args.size(), args.data()); } app * mk_or(ref_buffer const& args) { return mk_or(args.size(), args.data()); } diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 3f8080490..5d71ffda9 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -164,7 +164,7 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) { else if (num_args == 1) return args[0]; else - return m.mk_and(num_args, args); + return m.mk_and(std::span(args, num_args)); } app* mk_and(ast_manager & m, unsigned num_args, app * const * args) { diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 3aa1a919b..efd5784cf 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -470,7 +470,7 @@ struct nnf::imp { } app * r; if (m.is_and(t) == fr.m_pol) - r = m.mk_and(t->get_num_args(), m_result_stack.data() + fr.m_spos); + r = m.mk_and(std::span(m_result_stack.data() + fr.m_spos, t->get_num_args())); else r = m.mk_or(t->get_num_args(), m_result_stack.data() + fr.m_spos); @@ -524,7 +524,7 @@ struct nnf::imp { if (fr.m_pol) r = m.mk_or(2, m_result_stack.data() + fr.m_spos); else - r = m.mk_and(2, m_result_stack.data() + fr.m_spos); + r = m.mk_and(std::span(m_result_stack.data() + fr.m_spos, 2)); m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 849f4f369..2b52404e5 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -159,7 +159,7 @@ public: void mk_and(unsigned num_args, expr * const * args, expr_ref & result) { if (mk_and_core(num_args, args, result) == BR_FAILED) { SASSERT(!m_elim_and); - result = m().mk_and(num_args, args); + result = m().mk_and(std::span(args, num_args)); } } void mk_or(unsigned num_args, expr * const * args, expr_ref & result) { diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp index dcdc25517..3bf9f4bf1 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -170,6 +170,6 @@ br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & resul for (unsigned i = 0; i < num; ++i) { eqs.push_back(m().mk_eq(to_app(lhs)->get_arg(i), to_app(rhs)->get_arg(i))); } - result = m().mk_and(eqs.size(), eqs.data()); + result = m().mk_and(std::span(eqs.data(), eqs.size())); return BR_REWRITE2; } diff --git a/src/ast/rewriter/dom_simplifier.cpp b/src/ast/rewriter/dom_simplifier.cpp index 13d87290d..68582fe1f 100644 --- a/src/ast/rewriter/dom_simplifier.cpp +++ b/src/ast/rewriter/dom_simplifier.cpp @@ -140,7 +140,7 @@ bool expr_dominators::compile(expr * e) { } bool expr_dominators::compile(unsigned sz, expr * const* es) { - expr_ref e(m.mk_and(sz, es), m); + expr_ref e(m.mk_and(std::span(es, sz)), m); return compile(e); } diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp index 2220d8613..89354b236 100644 --- a/src/ast/rewriter/factor_rewriter.cpp +++ b/src/ast/rewriter/factor_rewriter.cpp @@ -115,7 +115,7 @@ br_status factor_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { eqs[i] = m().mk_not(eqs[i].get()); } eqs.push_back(neg); - result = m().mk_and(eqs.size(), eqs.data()); + result = m().mk_and(std::span(eqs.data(), eqs.size())); TRACE(factor_rewriter, tout << mk_pp(result.get(), m()) << "\n";); return BR_DONE; } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 62bb53611..c1a1a3d94 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -945,7 +945,7 @@ struct pb2bv_rewriter::imp { pliteral mk_false() { return m.mk_false(); } pliteral mk_true() { return m.mk_true(); } pliteral mk_max(unsigned n, pliteral const* lits) { return trail(m.mk_or(n, lits)); } - pliteral mk_min(unsigned n, pliteral const* lits) { return trail(m.mk_and(n, lits)); } + pliteral mk_min(unsigned n, pliteral const* lits) { return trail(m.mk_and(std::span(lits, n))); } pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_ismt2_pp(lit, m); } diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index d649737f5..7b1c25cf1 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -217,7 +217,7 @@ private: if (rewrite_ok) m_rewriter.mk_and(args.size(), args.data(), result); else - result = m.mk_and (args.size (), args.data ()); + result = m.mk_and(std::span(args.data(), args.size())); } else if (m.is_or(fml)) { num_args = to_app(fml)->get_num_args(); diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 8c21c3a2e..12051d0d9 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -274,7 +274,7 @@ private: if (premise) { expr_ref f1 = bind_variables(mk_implies(m_body, head)); - expr* f2 = m.mk_and(sz, m_todo.data()+m_todo.size()-sz); + expr* f2 = m.mk_and(std::span(m_todo.data()+m_todo.size()-sz, sz)); proof_ref p2(m), p3(m); p2 = m.mk_def_axiom(m.mk_iff(f1, f2)); p3 = mk_quant_intro(fml, f1, p); diff --git a/src/muz/spacer/spacer_cluster_util.cpp b/src/muz/spacer/spacer_cluster_util.cpp index eecf90176..615f850bd 100644 --- a/src/muz/spacer/spacer_cluster_util.cpp +++ b/src/muz/spacer/spacer_cluster_util.cpp @@ -178,7 +178,7 @@ struct term_ordered_rpp : public default_rewriter_cfg { kids.append(num, args); std::stable_sort(kids.data(), kids.data() + kids.size(), m_and_less); - result = m.mk_and(num, kids.data()); + result = m.mk_and(std::span(kids.data(), num)); return BR_DONE; } return st; diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 6c5c1e9fe..b70c86377 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -112,7 +112,7 @@ namespace opt { pliteral mk_false() { return m.mk_false(); } pliteral mk_true() { return m.mk_true(); } pliteral mk_max(unsigned n, pliteral const* as) { return trail(m.mk_or(n, as)); } - pliteral mk_min(unsigned n, pliteral const* as) { return trail(m.mk_and(n, as)); } + pliteral mk_min(unsigned n, pliteral const* as) { return trail(m.mk_and(std::span(as, n))); } pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } std::ostream& pp(std::ostream& out, pliteral lit) { return out << mk_pp(lit, m); } diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index a28ac36cd..cd20e6ae6 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -342,7 +342,7 @@ namespace array { else if (a.is_union(map)) result = m.mk_or(n, args); else if (a.is_intersect(map)) - result = m.mk_and(n, args); + result = m.mk_and(std::span(args, n)); else if (a.is_difference(map)) { SASSERT(n > 0); result = args[0]; diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index fda2f8688..6d4963c0d 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -1628,7 +1628,7 @@ namespace smtfd { unsigned sz = m_assertions.size() - m_assertions_qhead; if (sz > 0) { m_assertions.push_back(m_toggles.back()); - expr_ref fml(m.mk_and(sz + 1, m_assertions.data() + m_assertions_qhead), m); + expr_ref fml(m.mk_and(std::span(m_assertions.data() + m_assertions_qhead, sz + 1)), m); m_assertions.pop_back(); expr* toggle = add_toggle(m.mk_fresh_const("toggle", m.mk_bool_sort())); m_assertions_qhead = m_assertions.size(); diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index c8a6c18d3..63d5e2ddc 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -441,7 +441,7 @@ void goal::display_as_and(std::ostream & out) const { for (unsigned i = 0; i < sz; ++i) args.push_back(form(i)); expr_ref tmp(m()); - tmp = m().mk_and(args.size(), args.data()); + tmp = m().mk_and(std::span(args.data(), args.size())); out << mk_ismt2_pp(tmp, m()) << "\n"; } diff --git a/src/test/ho_matcher.cpp b/src/test/ho_matcher.cpp index a7f275812..dccd8af08 100644 --- a/src/test/ho_matcher.cpp +++ b/src/test/ho_matcher.cpp @@ -111,12 +111,12 @@ namespace euf { s = m_arith.mk_add(s, m.mk_app(f.get(), zero)); - pat = m_arith.mk_add(m.mk_app(sum, 3, args), m_array.mk_select(F, L1)); + pat = m_arith.mk_add(m.mk_app(sum, (unsigned)3, args), m_array.mk_select(F, L1)); IF_VERBOSE(0, verbose_stream() << "test5a: " << pat << " =?= " << s << "\n";); m_matcher.add_pattern(pat.get()); m_matcher(pat, s, 4); - pat = m_arith.mk_add(m_array.mk_select(F, L1), m.mk_app(sum, 3, args)); + pat = m_arith.mk_add(m_array.mk_select(F, L1), m.mk_app(sum, (unsigned)3, args)); IF_VERBOSE(0, verbose_stream() << "test5b: " << pat << " =?= " << s << "\n";); m_matcher.add_pattern(pat.get()); m_matcher(pat, s, 4); diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 8c57f2c28..af32b2c47 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -193,7 +193,7 @@ static app_ref generate_ineqs(ast_manager& m, sort* s, vector& static void test_c(app* x, expr_ref_vector const& c) { ast_manager& m = c.get_manager(); expr_ref fml(m); - fml = m.mk_and(c.size(), c.data()); + fml = m.mk_and(std::span(c.data(), c.size())); test(x, fml); } diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 5c171bb78..bf78d890b 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -163,7 +163,7 @@ struct ast_ext2 { return trail(m.mk_or(n, lits)); } pliteral mk_min(unsigned n, pliteral const* lits) { - return trail(m.mk_and(n, lits)); + return trail(m.mk_and(std::span(lits, n))); } pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a));