fast-math: optimize handling of nsz to create fewer variables
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -610,6 +610,17 @@ static expr any_fp_zero(State &s, const expr &v) {
if (is_zero.isFalse())
return v;
+ // any-fp-zero2(any-fp-zero1(x)) -> any-fp-zero2(x)
+ {
+ expr cond, neg, negv, val;
+ if (v.isIf(cond, neg, val) && neg.isFPNeg(negv) && negv.eq(val)) {
+ expr a, b;
+ if (cond.isAnd(a, b) && a.isVar() && a.fn_name().starts_with("anyzero") &&
+ b.isIsFPZero())
+ return any_fp_zero(s, val);
+ }
+ }
+
expr var = expr::mkFreshVar("anyzero", true);
s.addQuantVar(var);
return expr::mkIf(var && is_zero, v.fneg(), v);

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -552,6 +552,10 @@ bool expr::isFPNeg(expr &val) const {
return isUnOp(val, Z3_OP_FPA_NEG);
}
+bool expr::isIsFPZero() const {
+ return isAppOf(Z3_OP_FPA_IS_ZERO);
+}
+
bool expr::isNaNCheck(expr &fp) const {
if (auto app = isAppOf(Z3_OP_FPA_IS_NAN)) {
fp = Z3_get_app_arg(ctx(), app, 0);

MODIFY
smt/expr.h
smt/expr.h
@@ -147,6 +147,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 isIsFPZero() const;
bool isNaNCheck(expr &fp) const;
bool isfloat2BV(expr &fp) const;

fast-math: optimize handling of nsz to create fewer variables