smt expr: optimize FP (if cond (neg x) x) for some ops:
isNaN, isInf, isFPZero, fabs
These show up with fast-math
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -979,15 +979,25 @@ expr expr::abs() const {
return mkIf(sge(mkUInt(0, s)), *this, mkInt(-1, s) * *this);
}
+#define fold_fp_neg(fn) \
+ do { \
+ expr cond, neg, v, v2; \
+ if (isIf(cond, neg, v) && neg.isFPNeg(v2) && v.eq(v2)) \
+ return v.fn(); \
+} while (0)
+
expr expr::isNaN() const {
+ fold_fp_neg(isNaN);
return unop_fold(Z3_mk_fpa_is_nan);
}
expr expr::isInf() const {
+ fold_fp_neg(isInf);
return unop_fold(Z3_mk_fpa_is_infinite);
}
expr expr::isFPZero() const {
+ fold_fp_neg(isFPZero);
return unop_fold(Z3_mk_fpa_is_zero);
}
@@ -1040,6 +1050,7 @@ expr expr::fdiv(const expr &rhs, const expr &rm) const {
}
expr expr::fabs() const {
+ fold_fp_neg(fabs);
return unop_fold(Z3_mk_fpa_abs);
}

smt expr: optimize FP (if cond (neg x) x) for some ops:
isNaN, isInf, isFPZero, fabs
These show up with fast-math