mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

undefine min/max #1927

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-11 09:50:52 -08:00
parent a000747605
commit 69e2f33ecf
1 changed files with 48 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,6 +28,9 @@ Notes:
#include<z3.h>
#include<limits.h>
#undef min
#undef max
/**
\defgroup cppapi C++ API
@ -1478,9 +1481,51 @@ namespace z3 {
inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr min(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_min(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr max(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_fpa_max(a.ctx(), a, b); return expr(a.ctx(), r); }
inline expr abs(expr const & a) { Z3_ast r = Z3_mk_fpa_abs(a.ctx(), a); return expr(a.ctx(), r); }
inline expr min(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r;
if (a.is_arith()) {
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
}
else if (a.is_bv()) {
r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
}
else {
assert(a.is_fpa());
r = Z3_mk_fpa_min(a.ctx(), a, b);
}
return expr(a.ctx(), r);
}
inline expr max(expr const& a, expr const& b) {
check_context(a, b);
Z3_ast r;
if (a.is_arith()) {
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
}
else if (a.is_bv()) {
r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
}
else {
assert(a.is_fpa());
r = Z3_mk_fpa_max(a.ctx(), a, b);
}
return expr(a.ctx(), r);
}
inline expr abs(expr const & a) {
Z3_ast r;
if (a.is_int()) {
expr zero = a.ctx().int_val(0);
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
}
else if (a.is_real()) {
expr zero = a.ctx().real_val(0);
r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, zero);
}
else {
r = Z3_mk_fpa_abs(a.ctx(), a);
}
return expr(a.ctx(), r);
}
inline expr sqrt(expr const & a, expr const& rm) {
check_context(a, rm);
assert(a.is_fpa());