Method fole

smt/expr.cpp:1350–1352

}

expr expr::fole(const expr &rhs) const {
  return binop_fold(rhs, Z3_mk_fpa_leq);
}

expr expr::fone(const expr &rhs) const {
  return ford(rhs) && !binop_commutative(rhs, Z3_mk_fpa_eq);