smt: peephole for nan check
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -572,6 +572,10 @@ bool expr::isFPNeg(expr &val) const {
return isUnOp(val, Z3_OP_FPA_NEG);
}
+bool expr::isFAbs(expr &val) const {
+ return isUnOp(val, Z3_OP_FPA_ABS);
+}
+
bool expr::isIsFPZero() const {
if (isBV()) {
// extract(bits()-2, 0) == 0
@@ -1087,7 +1091,7 @@ expr expr::isNaN() const {
fold_fp_neg(isNaN);
expr v;
- if (isFPNeg(v))
+ if (isFPNeg(v) || isFAbs(v))
return v.isNaN();
return unop_fold(Z3_mk_fpa_is_nan);

MODIFY
smt/expr.h
smt/expr.h
@@ -148,6 +148,7 @@ public:
bool isFPMul(expr &rounding, expr &lhs, expr &rhs) const;
bool isFPDiv(expr &rounding, expr &lhs, expr &rhs) const;
bool isFPNeg(expr &neg) const;
+ bool isFAbs(expr &val) const;
bool isIsFPZero() const;
bool isNaNCheck(expr &fp) const;
bool isfloat2BV(expr &fp) const;

smt: peephole for nan check