Skip to content

Commit

Permalink
bit-vector overflow/underflow operators exposed over C++ API
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Oct 8, 2019
1 parent 27765ee commit b6c1334
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 0 deletions.
47 changes: 47 additions & 0 deletions src/api/c++/z3++.h
View file
Expand Up @@ -1118,6 +1118,17 @@ namespace z3 {
friend expr min(expr const& a, expr const& b);
friend expr max(expr const& a, expr const& b);

friend expr bv2int(expr const& a, bool is_signed);
friend expr int2bv(expr const& a, unsigned n);
friend expr bvadd_no_overflow(expr const& a, expr const& b);
friend expr bvadd_no_underflow(expr const& a, expr const& b);
friend expr bvsub_no_overflow(expr const& a, expr const& b);
friend expr bvsub_no_underflow(expr const& a, expr const& b);
friend expr bvsdiv_no_overflow(expr const& a, expr const& b);
friend expr bvneg_no_overflow(expr const& a);
friend expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed);
friend expr bvmul_no_underflow(expr const& a, expr const& b);

expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Expand Down Expand Up @@ -1625,6 +1636,7 @@ namespace z3 {
return expr(a.ctx(), r);
}


/**
\brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
Expand Down Expand Up @@ -1740,6 +1752,41 @@ namespace z3 {
*/
inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }

/**
\brief bit-vector and integer conversions.
*/
inline expr bv2int(expr const& a, bool is_signed) { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
inline expr int2bv(expr const& a, unsigned n) { Z3_ast r = Z3_mk_intbv2(a.ctx(), a, n); a.check_error(); return expr(a.ctx(), r); }

/**
\brief bit-vector overflow/underflow checks
*/
inline expr bvadd_no_overflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvadd_no_underflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvsub_no_overflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvsub_no_underflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvsdiv_no_overflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvneg_no_overflow(expr const& a) {
Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvmul_no_overflow(expr const& a, expr const& b, bool is_signed) {
check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
}
inline expr bvmul_no_underflow(expr const& a, expr const& b) {
check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
}


/**
\brief Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
*/
Expand Down
8 changes: 8 additions & 0 deletions src/api/z3_api.h
View file
Expand Up @@ -2989,6 +2989,7 @@ extern "C" {
of \c t1 and \c t2 does not overflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvadd_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
*/
Expand All @@ -2999,6 +3000,7 @@ extern "C" {
of \c t1 and \c t2 does not underflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvadd_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Expand All @@ -3009,6 +3011,7 @@ extern "C" {
of \c t1 and \c t2 does not overflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvsub_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Expand All @@ -3019,6 +3022,7 @@ extern "C" {
of \c t1 and \c t2 does not underflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvsub_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
*/
Expand All @@ -3029,6 +3033,7 @@ extern "C" {
of \c t1 and \c t2 does not overflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvsdiv_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Expand All @@ -3039,6 +3044,7 @@ extern "C" {
\c t1 is interpreted as a signed bit-vector.
The node \c t1 must have bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvneg_no_overflow', AST, (_in(CONTEXT), _in(AST)))
*/
Expand All @@ -3049,6 +3055,7 @@ extern "C" {
of \c t1 and \c t2 does not overflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvmul_no_overflow', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(BOOL)))
*/
Expand All @@ -3059,6 +3066,7 @@ extern "C" {
of \c t1 and \c t2 does not underflow.
The nodes \c t1 and \c t2 must have the same bit-vector sort.
The returned node is of sort Bool.
def_API('Z3_mk_bvmul_no_underflow', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Expand Down

0 comments on commit b6c1334

Please sign in to comment.