From b12074507859db333772d57671f3fb84a05460d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 May 2024 20:20:05 -0700 Subject: [PATCH] add C++ bindings for sequence operations Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 81a67066e..81d5bcaa9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2497,6 +2497,34 @@ namespace z3 { 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) { array _args(args); Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());