Pretty print for FP zeros
MODIFY
ir/type.cpp
ir/type.cpp
@@ -342,6 +342,8 @@ pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
void FloatType::printVal(ostream &os, State &s, const expr &e) const {
if (e.isNaN().simplify().isTrue()) {
os << "NaN";
+ } else if (e.isFPZero().simplify().isTrue()) {
+ os << (e.isFPNeg().simplify().isTrue() ? "-0.0" : "+0.0");
} else if (e.isInf().simplify().isTrue()) {
os << (e.isFPNeg().simplify().isTrue() ? "-oo" : "+oo");
} else {

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -717,6 +717,11 @@ expr expr::isInf() const {
return Z3_mk_fpa_is_infinite(ctx(), ast());
}
+expr expr::isFPZero() const {
+ C();
+ return Z3_mk_fpa_is_zero(ctx(), ast());
+}
+
expr expr::isFPNeg() const {
C();
return Z3_mk_fpa_is_negative(ctx(), ast());

MODIFY
smt/expr.h
smt/expr.h
@@ -157,6 +157,7 @@ public:
expr isNaN() const;
expr isInf() const;
+ expr isFPZero() const;
expr isFPNeg() const;
expr fadd(const expr &rhs) const;

Pretty print for FP zeros (#80)