From 0668ba5f6c916e85b2efc48d4e473680f11bdf3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 07:58:39 -0700 Subject: [PATCH] add pb shorthands to C++. Issue #694 Signed-off-by: Nikolaj Bjorner --- src/api/api_pb.cpp | 6 +++--- src/api/c++/z3++.h | 49 +++++++++++++++++++++++++++++++++++++++++++--- src/api/z3_api.h | 6 +++--- 3 files changed, 52 insertions(+), 9 deletions(-) diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp index f19fd8661..bb4a40c9a 100644 --- a/src/api/api_pb.cpp +++ b/src/api/api_pb.cpp @@ -52,7 +52,7 @@ extern "C" { } Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, - Z3_ast const args[], int _coeffs[], + Z3_ast const args[], int const _coeffs[], int k) { Z3_TRY; LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); @@ -70,7 +70,7 @@ extern "C" { } Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, - Z3_ast const args[], int _coeffs[], + Z3_ast const args[], int const _coeffs[], int k) { Z3_TRY; LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); @@ -88,7 +88,7 @@ extern "C" { } Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, - Z3_ast const args[], int _coeffs[], + Z3_ast const args[], int const _coeffs[], int k) { Z3_TRY; LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6250f324b..b6157f3ff 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -935,7 +935,6 @@ namespace z3 { friend expr operator>=(expr const & a, expr const & b); - friend expr wasoperator(expr const & a, expr const & b); friend expr operator>=(expr const & a, int b); friend expr operator>=(int a, expr const & b); @@ -947,6 +946,12 @@ namespace z3 { friend expr operator>(expr const & a, int b); friend expr operator>(int a, expr const & b); + friend expr pble(expr_vector const& es, int const * coeffs, int bound); + friend expr pbge(expr_vector const& es, int const * coeffs, int bound); + friend expr pbeq(expr_vector const& es, int const * coeffs, int bound); + friend expr atmost(expr_vector const& es, unsigned bound); + friend expr atleast(expr_vector const& es, unsigned bound); + 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); @@ -1566,8 +1571,46 @@ namespace z3 { array vars(xs); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); } - - + inline expr pble(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); + context& ctx = es[0].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); + return expr(ctx, r); + } + inline expr pbge(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); + context& ctx = es[0].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); + return expr(ctx, r); + } + inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) { + assert(es.size() > 0); + context& ctx = es[0].ctx(); + array _es(es); + Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound); + ctx.check_error(); + return expr(ctx, r); + } + inline expr atmost(expr_vector const& es, unsigned bound) { + assert(es.size() > 0); + context& ctx = es[0].ctx(); + array _es(es); + Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound); + ctx.check_error(); + return expr(ctx, r); + } + inline expr atleast(expr_vector const& es, unsigned bound) { + assert(es.size() > 0); + context& ctx = es[0].ctx(); + array _es(es); + Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound); + ctx.check_error(); + return expr(ctx, r); + } inline expr sum(expr_vector const& args) { assert(args.size() > 0); context& ctx = args[0].ctx(); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ee35c002e..272c94dda 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4006,7 +4006,7 @@ extern "C" { def_API('Z3_mk_pble', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT))) */ Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, - Z3_ast const args[], int coeffs[], + Z3_ast const args[], int const coeffs[], int k); /** @@ -4017,7 +4017,7 @@ extern "C" { def_API('Z3_mk_pbge', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT))) */ Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, - Z3_ast const args[], int coeffs[], + Z3_ast const args[], int const coeffs[], int k); /** @@ -4028,7 +4028,7 @@ extern "C" { def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT))) */ Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, - Z3_ast const args[], int coeffs[], + Z3_ast const args[], int const coeffs[], int k); /**