print floats in counterexamples
MODIFY
ir/type.cpp
ir/type.cpp
@@ -340,7 +340,14 @@ pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
}
void FloatType::printVal(ostream &os, const expr &e) const {
- os << e;
+ if (e.isNaN().simplify().isTrue()) {
+ os << "NaN";
+ } else if (e.isInf().simplify().isTrue()) {
+ os << (e.isFPNeg().simplify().isTrue() ? "-oo" : "+oo");
+ } else {
+ e.float2BV().printHexadecimal(os);
+ os << " (" << e.float2Real().simplify().numeral_string() << ')';
+ }
}
void FloatType::print(ostream &os) const {

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -711,6 +711,16 @@ expr expr::isNaN() const {
return Z3_mk_fpa_is_nan(ctx(), ast());
}
+expr expr::isInf() const {
+ C();
+ return Z3_mk_fpa_is_infinite(ctx(), ast());
+}
+
+expr expr::isFPNeg() const {
+ C();
+ return Z3_mk_fpa_is_negative(ctx(), ast());
+}
+
// TODO: make rounding mode customizable
expr expr::fadd(const expr &rhs) const {
C(rhs);
@@ -1126,6 +1136,11 @@ expr expr::float2BV() const {
return Z3_mk_fpa_to_ieee_bv(ctx(), ast());
}
+expr expr::float2Real() const {
+ C();
+ return Z3_mk_fpa_to_real(ctx(), ast());
+}
+
expr expr::BV2float(const expr &type) const {
C(type);
return Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort());
@@ -1242,28 +1257,7 @@ expr expr::subst(const expr &from, const expr &to) const {
}
void expr::printUnsigned(ostream &os) const {
- uint64_t num;
- if (simplify().isUInt(num)) {
- os << num;
- return;
- }
-
- expr zero = mkUInt(0, sort());
- expr ten = mkUInt(10, sort());
- expr n = *this;
-
- string str;
- uint64_t d;
-
- do {
- expr digit = n.urem(ten).simplify();
- ENSURE(digit.isUInt(d));
- str.push_back('0' + d);
- n = n.udiv(ten).simplify();
- } while (!n.eq(zero));
-
- reverse(str.begin(), str.end());
- os << str;
+ os << numeral_string();
}
void expr::printSigned(ostream &os) const {
@@ -1280,6 +1274,11 @@ void expr::printHexadecimal(ostream &os) const {
os << (rem == 0 ? *this : zext(4 - rem)).simplify();
}
+string expr::numeral_string() const {
+ C();
+ return Z3_get_numeral_decimal_string(ctx(), ast(), 12);
+}
+
ostream& operator<<(ostream &os, const expr &e) {
return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}

MODIFY
smt/expr.h
smt/expr.h
#include <cstdint>
#include <ostream>
#include <set>
+#include <string>
#include <utility>
#include <vector>
@@ -155,6 +156,9 @@ public:
expr ctpop() const;
expr isNaN() const;
+ expr isInf() const;
+ expr isFPNeg() const;
+
expr fadd(const expr &rhs) const;
expr fsub(const expr &rhs) const;
expr fmul(const expr &rhs) const;
@@ -221,6 +225,7 @@ public:
expr toBVBool() const;
expr float2BV() const;
+ expr float2Real() const;
expr BV2float(const expr &type) const;
// we don't expose SMT expr types, so range must be passed as a dummy value
@@ -245,6 +250,7 @@ public:
void printUnsigned(std::ostream &os) const;
void printSigned(std::ostream &os) const;
void printHexadecimal(std::ostream &os) const;
+ std::string numeral_string() const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only

print floats in counterexamples