allow frem to have a close-enough value

still mark it as approximated
AliveToolkit · Aug 22, 2023 · d075b4a · d075b4a
1 parent 9b8b86b
commit d075b4a
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 1 deletion.
diff --git a/ir/instr.cpp b/ir/instr.cpp
@@ -839,7 +839,7 @@ StateValue FpBinOp::toSMT(State &s) const {
   case FRem:
     fn = [&](const expr &a, const expr &b, FpRoundingMode rm) {
       // TODO; Z3 has no support for LLVM's frem which is actually an fmod
-      auto val = expr::mkUF("fmod", {a, b}, a);
+      auto val = a.frem(b);
       s.doesApproximation("frem", val);
       return val;
     };

diff --git a/smt/expr.cpp b/smt/expr.cpp
@@ -1173,6 +1173,11 @@ expr expr::fdiv(const expr &rhs, const expr &rm) const {
   return simplify_const(Z3_mk_fpa_div(ctx(), rm(), ast(), rhs()), *this, rhs);
 }
 
+expr expr::frem(const expr &rhs) const {
+  C(rhs);
+  return simplify_const(Z3_mk_fpa_rem(ctx(), ast(), rhs()), *this, rhs);
+}
+
 expr expr::fabs() const {
   if (isBV())
     return expr::mkUInt(0, 1).concat(extract(bits() - 2, 0));

diff --git a/smt/expr.h b/smt/expr.h
@@ -233,6 +233,7 @@ class expr {
   expr fsub(const expr &rhs, const expr &rm) const;
   expr fmul(const expr &rhs, const expr &rm) const;
   expr fdiv(const expr &rhs, const expr &rm) const;
+  expr frem(const expr &rhs) const;
   expr fabs() const;
   expr fneg() const;
   expr copysign(const expr &sign) const;