mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add C++ bindings for sequence operations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-05-09 20:20:05 -07:00
parent c7529d0b25
commit b120745078
1 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/api/c++/z3++.h
View file

@ -2497,6 +2497,34 @@ namespace z3 {
return expr(ctx, r); return expr(ctx, r);
} }
inline expr map(expr const& f, expr const& list) {
context& ctx = f.ctx();
Z3_ast r = Z3_mk_seq_map(ctx, f, list);
ctx.check_error();
return expr(ctx, r);
}
inline expr mapi(expr const& f, expr const& i, expr const& list) {
context& ctx = f.ctx();
Z3_ast r = Z3_mk_seq_mapi(ctx, f, i, list);
ctx.check_error();
return expr(ctx, r);
}
inline expr foldl(expr const& f, expr const& a, expr const& list) {
context& ctx = f.ctx();
Z3_ast r = Z3_mk_seq_foldl(ctx, f, a, list);
ctx.check_error();
return expr(ctx, r);
}
inline expr foldli(expr const& f, expr const& i, expr const& a, expr const& list) {
context& ctx = f.ctx();
Z3_ast r = Z3_mk_seq_foldli(ctx, f, i, a, list);
ctx.check_error();
return expr(ctx, r);
}
inline expr mk_or(expr_vector const& args) { inline expr mk_or(expr_vector const& args) {
array<Z3_ast> _args(args); array<Z3_ast> _args(args);
Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr()); Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());