mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

Refactor mk_or and mk_and helpers to use std::initializer_list

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-07 13:12:21 +00:00
parent ffbadabc15
commit af9841122b
3 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
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
@ -2210,7 +2211,7 @@ public:
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_or(std::initializer_list<expr*> args) { return mk_app(basic_family_id, OP_OR, static_cast<unsigned>(args.size()), args.begin()); }
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<expr, ast_manager> const& args) { return mk_and(std::span<expr* const>(args.data(), args.size())); }

2
src/ast/ast_util.cpp
View file

@ -177,7 +177,7 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
else if (num_args == 1)
return args[0];
else
return m.mk_or(num_args, args);
return m.mk_or(std::span<expr* const>(args, num_args));
}
app* mk_or(ast_manager & m, unsigned num_args, app * const * args) {

4
src/ast/ast_util.h
View file

@ -103,7 +103,7 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
app * mk_and(ast_manager & m, unsigned num_args, app * const * args);
inline expr * mk_and(ast_manager & m, ptr_vector<expr> const& args) { return mk_and(m, args.size(), args.data()); }
inline expr * mk_and(ast_manager & m, ptr_buffer<expr> const& args) { return mk_and(m, args.size(), args.data()); }
inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); }
inline expr * mk_and(ast_manager & m, std::initializer_list<expr*> args) { return mk_and(m, static_cast<unsigned>(args.size()), args.begin()); }
inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }
inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.data()), args.get_manager()); }
@ -125,7 +125,7 @@ app_ref operator+(expr_ref& a, expr_ref& b);
*/
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
app * mk_or(ast_manager & m, unsigned num_args, app * const * args);
inline expr * mk_or(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_or(m, 2, args); }
inline expr * mk_or(ast_manager & m, std::initializer_list<expr*> args) { return mk_or(m, static_cast<unsigned>(args.size()), args.begin()); }
inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); }
inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.data()), args.get_manager()); }