From 1dd2de61ecbe17ac9b66bd1f9df6a9dc4bb1b7c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 07:43:26 -0700 Subject: [PATCH] add sum shorthand to C++. Issue #694 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index bfd4eb2c4..8b523d91c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -890,6 +890,7 @@ namespace z3 { friend expr operator+(expr const & a, expr const & b); friend expr operator+(expr const & a, int b); friend expr operator+(int a, expr const & b); + friend expr sum(expr_vector const& args); friend expr operator*(expr const & a, expr const & b); friend expr operator*(expr const & a, int b); @@ -1561,6 +1562,15 @@ namespace z3 { } + inline expr sum(expr_vector const& args) { + assert(args.size() > 0); + context& ctx = args[0].ctx(); + array _args(args); + Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr()); + ctx.check_error(); + return expr(ctx, r); + } + inline expr distinct(expr_vector const& args) { assert(args.size() > 0); context& ctx = args[0].ctx();