Add floatbv_mod_exprt and floatbv_rem_exprt classes

This documents the existing use of the floatbv_mod and floatbv_rem
expressions.

Author: kroening

src/util/floatbv_expr.h

@@ -438,6 +438,108 @@ inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
   return ret;
 }
 
+/// \brief IEEE floating-point mod
+class floatbv_mod_exprt : public binary_exprt
+{
+public:
+  floatbv_mod_exprt(exprt op, exprt rounding)
+    : binary_exprt(op, ID_floatbv_mod, std::move(rounding), op.type())
+  {
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &rounding_mode()
+  {
+    return op1();
+  }
+
+  const exprt &rounding_mode() const
+  {
+    return op1();
+  }
+};
+
+/// \brief Cast an exprt to a \ref floatbv_mod_exprt
+///
+/// \a expr must be known to be \ref floatbv_mod_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref floatbv_mod_exprt
+inline const floatbv_mod_exprt &to_floatbv_mod_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_floatbv_mod);
+  floatbv_mod_exprt::check(expr);
+  return static_cast<const floatbv_mod_exprt &>(expr);
+}
+
+/// \copydoc to_floatbv_mod_expr(const exprt &)
+inline floatbv_mod_exprt &to_floatbv_mod_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_floatbv_mod);
+  floatbv_mod_exprt::check(expr);
+  return static_cast<floatbv_mod_exprt &>(expr);
+}
+
+/// \brief IEEE floating-point rem
+class floatbv_rem_exprt : public binary_exprt
+{
+public:
+  floatbv_rem_exprt(exprt op, exprt rounding)
+    : binary_exprt(op, ID_floatbv_rem, std::move(rounding), op.type())
+  {
+  }
+
+  exprt &op()
+  {
+    return op0();
+  }
+
+  const exprt &op() const
+  {
+    return op0();
+  }
+
+  exprt &rounding_mode()
+  {
+    return op1();
+  }
+
+  const exprt &rounding_mode() const
+  {
+    return op1();
+  }
+};
+
+/// \brief Cast an exprt to a \ref floatbv_rem_exprt
+///
+/// \a expr must be known to be \ref floatbv_rem_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref floatbv_rem_exprt
+inline const floatbv_rem_exprt &to_floatbv_rem_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_floatbv_rem);
+  floatbv_rem_exprt::check(expr);
+  return static_cast<const floatbv_rem_exprt &>(expr);
+}
+
+/// \copydoc to_floatbv_rem_expr(const exprt &)
+inline floatbv_rem_exprt &to_floatbv_rem_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_floatbv_rem);
+  floatbv_rem_exprt::check(expr);
+  return static_cast<floatbv_rem_exprt &>(expr);
+}
+
 /// \brief returns the a rounding mode expression for a given
 /// IEEE rounding mode, encoded using the recommendation in
 /// C11 5.2.4.2.2

src/util/format_expr.cpp

@@ -354,7 +354,8 @@ void format_expr_configt::setup()
   expr_map[ID_floatbv_minus] = ternary_expr;
   expr_map[ID_floatbv_mult] = ternary_expr;
   expr_map[ID_floatbv_div] = ternary_expr;
-  expr_map[ID_floatbv_mod] = ternary_expr;
+  expr_map[ID_floatbv_mod] = binary_prefix_expr;
+  expr_map[ID_floatbv_rem] = binary_prefix_expr;
 
   expr_map[ID_constant] =
     [](std::ostream &os, const exprt &expr) -> std::ostream & {