mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
add sum shorthand to C++. Issue #694
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5a79722071
commit
1dd2de61ec
|
@ -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<Z3_ast> _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();
|
||||
|
|
Loading…
Reference in a new issue