From 0b1d5645097d41eec4c43946407e08d57b41ad64 Mon Sep 17 00:00:00 2001 From: hume Date: Tue, 14 Mar 2017 18:11:00 +0800 Subject: [PATCH 1/3] added no exception support to z3++.h --- src/api/c++/z3++.h | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index bfd4eb2c4..ac0e2c84a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -86,7 +86,13 @@ namespace z3 { }; inline std::ostream & operator<<(std::ostream & out, exception const & e) { out << e.msg(); return out; } - +#if !defined(Z3_THROW) +#if __cpp_exceptions || _CPPUNWIND +#define Z3_THROW(x) throw x +#else +#define Z3_THROW(x) {} +#endif +#endif // !defined(Z3_THROW) /** \brief Z3 global configuration object. @@ -165,7 +171,7 @@ namespace z3 { Z3_error_code check_error() const { Z3_error_code e = Z3_get_error_code(m_ctx); if (e != Z3_OK && enable_exceptions()) - throw exception(Z3_get_error_msg(m_ctx, e)); + Z3_THROW(exception(Z3_get_error_msg(m_ctx, e))); return e; } @@ -701,7 +707,7 @@ namespace z3 { if (!is_numeral_i(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - throw exception("numeral does not fit in machine int"); + Z3_THROW(exception("numeral does not fit in machine int")); } return result; } @@ -721,7 +727,7 @@ namespace z3 { if (!is_numeral_u(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - throw exception("numeral does not fit in machine uint"); + Z3_THROW(exception("numeral does not fit in machine uint")); } return result; } @@ -738,7 +744,7 @@ namespace z3 { if (!is_numeral_i64(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - throw exception("numeral does not fit in machine __int64"); + Z3_THROW(exception("numeral does not fit in machine __int64")); } return result; } @@ -755,7 +761,7 @@ namespace z3 { if (!is_numeral_u64(result)) { assert(ctx().enable_exceptions()); if (!ctx().enable_exceptions()) return 0; - throw exception("numeral does not fit in machine __uint64"); + Z3_THROW(exception("numeral does not fit in machine __uint64")); } return result; } @@ -1699,7 +1705,7 @@ namespace z3 { Z3_bool status = Z3_model_eval(ctx(), m_model, n, model_completion, &r); check_error(); if (status == Z3_FALSE && ctx().enable_exceptions()) - throw exception("failed to evaluate expression"); + Z3_THROW(exception("failed to evaluate expression")); return expr(ctx(), r); } @@ -2023,7 +2029,7 @@ namespace z3 { } inline tactic par_or(unsigned n, tactic const* tactics) { if (n == 0) { - throw exception("a non-zero number of tactics need to be passed to par_or"); + Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or")); } array buffer(n); for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i]; From 1dd2de61ecbe17ac9b66bd1f9df6a9dc4bb1b7c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 07:43:26 -0700 Subject: [PATCH 2/3] 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(); From 0668ba5f6c916e85b2efc48d4e473680f11bdf3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Mar 2017 07:58:39 -0700 Subject: [PATCH 3/3] 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); /**