mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00
Code Activity

Add std::initializer_list overloads for update_quantifier and update call sites

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 01:28:31 +00:00
parent 66c8b0c874
commit fb043ac9ee
3 changed files with 20 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/ast.cpp
View file

@ -2588,6 +2588,15 @@ quantifier * ast_manager::update_quantifier(quantifier * q, quantifier_kind k, u
num_patterns == 0 ? q->get_no_patterns() : nullptr);
}
quantifier * ast_manager::update_quantifier(quantifier * q, std::initializer_list<expr*> patterns, expr * body) {
return update_quantifier(q, static_cast<unsigned>(patterns.size()), patterns.begin(), body);
}
quantifier * ast_manager::update_quantifier(quantifier * q, std::initializer_list<expr*> patterns, std::initializer_list<expr*> no_patterns, expr * body) {
return update_quantifier(q, static_cast<unsigned>(patterns.size()), patterns.begin(),
static_cast<unsigned>(no_patterns.size()), no_patterns.begin(), body);
}
app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) {
return mk_app(basic_family_id, OP_DISTINCT, num_args, args);
}

7
src/ast/ast.h
View file

@ -49,6 +49,7 @@ Revision History:
#include "util/rlimit.h"
#include <variant>
#include <span>
#include <initializer_list>
#define RECYCLE_FREE_AST_INDICES
@ -2071,6 +2072,12 @@ public:
quantifier * update_quantifier(quantifier * q, quantifier_kind new_kind, unsigned new_num_patterns, expr * const * new_patterns, expr * new_body);
// Convenience overloads with std::initializer_list
[[nodiscard]] quantifier * update_quantifier(quantifier * q, std::initializer_list<expr*> new_patterns, expr * new_body);
[[nodiscard]] quantifier * update_quantifier(quantifier * q, std::initializer_list<expr*> new_patterns, std::initializer_list<expr*> new_no_patterns, expr * new_body);
// -----------------------------------
//
// expr_array

12
src/ast/macros/macro_finder.cpp
View file

@ -97,8 +97,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, bool deps_valid, expr_de
expr * body1 = m.mk_eq(head, new_rhs2);
expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
quantifier * q1 = m.update_quantifier(new_q, body1);
expr * patterns[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
quantifier * q2 = m.update_quantifier(new_q, { m.mk_pattern(k_app) }, body2);
new_exprs.push_back(q1);
new_exprs.push_back(q2);
if (m.proofs_enabled()) {
@ -169,8 +168,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
expr * body1 = m.mk_eq(head, new_rhs2);
expr * body2 = m.mk_app(new_body->get_decl(), k_app, m_autil.mk_int(0));
quantifier * q1 = m.update_quantifier(new_q, body1);
expr * patterns[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
quantifier * q2 = m.update_quantifier(new_q, { m.mk_pattern(k_app) }, body2);
proof* pr1 = nullptr, *pr2 = nullptr;
if (m.proofs_enabled()) {
// new_pr : new_q
@ -210,8 +208,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
app * body_1 = m.mk_eq(head, ite);
app * body_2 = m.mk_not(m.mk_eq(k_app, t));
quantifier * q1 = m.update_quantifier(q, body_1);
expr * pats[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
quantifier * q2 = m.update_quantifier(q, { m.mk_pattern(k_app) }, body_2); // erase patterns
new_exprs.push_back(q1);
new_exprs.push_back(q2);
if (m.proofs_enabled()) {
@ -244,8 +241,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
app * body_2 = m.mk_not(m.mk_eq(k_app, t));
quantifier * q1 = m.update_quantifier(q, body_1);
proof * pr1 = nullptr, *pr2 = nullptr;
expr * pats[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
quantifier * q2 = m.update_quantifier(q, { m.mk_pattern(k_app) }, body_2); // erase patterns
if (m.proofs_enabled()) {
// r : [rewrite] q ~ q1 & q2
// pr : q