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

bit-vector overflow/underflow operators exposed over C++ API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-08 10:12:18 -07:00
parent 27765ee0f4
commit b6c13340bd
2 changed files with 55 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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); }
@ -1625,6 +1636,7 @@ namespace z3 {
return expr(a.ctx(), r);
}
/**
\brief Create the if-then-else expression <tt>ite(c, t, e)</tt>
@ -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.
*/

8
src/api/z3_api.h
View file

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