mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

add pb shorthands to C++. Issue

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-14 07:58:39 -07:00
parent 7634f8b93e
commit 0668ba5f6c
3 changed files with 52 additions and 9 deletions

6
src/api/api_pb.cpp
View file

@ -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);

49
src/api/c++/z3++.h
View file

@ -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<Z3_app> 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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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<Z3_ast> _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();

6
src/api/z3_api.h
View file

@ -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);
/**