floatbv_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: API to expression classes for floating-point arithmetic
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_FLOATBV_EXPR_H
#define CPROVER_UTIL_FLOATBV_EXPR_H
 
 
#include "std_expr.h"
 
class floatbv_typecast_exprt : public binary_exprt
{
public:
  floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
    : binary_exprt(
        std::move(op),
        ID_floatbv_typecast,
        std::move(rounding),
        std::move(_type))
  {
  }
 
  exprt &op()
  {
    return op0();
  }
 
  const exprt &op() const
  {
    return op0();
  }
 
  exprt &rounding_mode()
  {
    return op1();
  }
 
  const exprt &rounding_mode() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<floatbv_typecast_exprt>(const exprt &base)
{
  return base.id() == ID_floatbv_typecast;
}
 
inline void validate_expr(const floatbv_typecast_exprt &value)
{
  validate_operands(value, 2, "Float typecast must have two operands");
}
 
inline const floatbv_typecast_exprt &to_floatbv_typecast_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_floatbv_typecast);
  const floatbv_typecast_exprt &ret =
    static_cast<const floatbv_typecast_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline floatbv_typecast_exprt &to_floatbv_typecast_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_floatbv_typecast);
  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class floatbv_round_to_integral_exprt : public binary_exprt
{
public:
  floatbv_round_to_integral_exprt(exprt op, exprt rounding)
    : binary_exprt(
        op,
        ID_floatbv_round_to_integral,
        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();
  }
};
 
template <>
inline bool can_cast_expr<floatbv_round_to_integral_exprt>(const exprt &base)
{
  return base.id() == ID_floatbv_round_to_integral;
}
 
inline const floatbv_round_to_integral_exprt &
to_floatbv_round_to_integral_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_floatbv_round_to_integral);
  floatbv_round_to_integral_exprt::check(expr);
  return static_cast<const floatbv_round_to_integral_exprt &>(expr);
}
 
inline floatbv_round_to_integral_exprt &
to_floatbv_round_to_integral_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_floatbv_round_to_integral);
  floatbv_round_to_integral_exprt::check(expr);
  return static_cast<floatbv_round_to_integral_exprt &>(expr);
}
 
class isnan_exprt : public unary_predicate_exprt
{
public:
  explicit isnan_exprt(exprt op)
    : unary_predicate_exprt(ID_isnan, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<isnan_exprt>(const exprt &base)
{
  return base.id() == ID_isnan;
}
 
inline void validate_expr(const isnan_exprt &value)
{
  validate_operands(value, 1, "Is NaN must have one operand");
}
 
inline const isnan_exprt &to_isnan_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_isnan);
  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline isnan_exprt &to_isnan_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_isnan);
  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class isinf_exprt : public unary_predicate_exprt
{
public:
  explicit isinf_exprt(exprt op)
    : unary_predicate_exprt(ID_isinf, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<isinf_exprt>(const exprt &base)
{
  return base.id() == ID_isinf;
}
 
inline void validate_expr(const isinf_exprt &value)
{
  validate_operands(value, 1, "Is infinite must have one operand");
}
 
inline const isinf_exprt &to_isinf_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_isinf);
  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline isinf_exprt &to_isinf_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_isinf);
  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class isfinite_exprt : public unary_predicate_exprt
{
public:
  explicit isfinite_exprt(exprt op)
    : unary_predicate_exprt(ID_isfinite, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
{
  return base.id() == ID_isfinite;
}
 
inline void validate_expr(const isfinite_exprt &value)
{
  validate_operands(value, 1, "Is finite must have one operand");
}
 
inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_isfinite);
  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline isfinite_exprt &to_isfinite_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_isfinite);
  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class isnormal_exprt : public unary_predicate_exprt
{
public:
  explicit isnormal_exprt(exprt op)
    : unary_predicate_exprt(ID_isnormal, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
{
  return base.id() == ID_isnormal;
}
 
inline void validate_expr(const isnormal_exprt &value)
{
  validate_operands(value, 1, "Is normal must have one operand");
}
 
inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_isnormal);
  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline isnormal_exprt &to_isnormal_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_isnormal);
  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class ieee_float_equal_exprt : public binary_relation_exprt
{
public:
  ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt(
        std::move(_lhs),
        ID_ieee_float_equal,
        std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<ieee_float_equal_exprt>(const exprt &base)
{
  return base.id() == ID_ieee_float_equal;
}
 
inline void validate_expr(const ieee_float_equal_exprt &value)
{
  validate_operands(value, 2, "IEEE equality must have two operands");
}
 
inline const ieee_float_equal_exprt &to_ieee_float_equal_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_ieee_float_equal);
  const ieee_float_equal_exprt &ret =
    static_cast<const ieee_float_equal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline ieee_float_equal_exprt &to_ieee_float_equal_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_ieee_float_equal);
  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class ieee_float_notequal_exprt : public binary_relation_exprt
{
public:
  ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt(
        std::move(_lhs),
        ID_ieee_float_notequal,
        std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<ieee_float_notequal_exprt>(const exprt &base)
{
  return base.id() == ID_ieee_float_notequal;
}
 
inline void validate_expr(const ieee_float_notequal_exprt &value)
{
  validate_operands(value, 2, "IEEE inequality must have two operands");
}
 
inline const ieee_float_notequal_exprt &
to_ieee_float_notequal_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_ieee_float_notequal);
  const ieee_float_notequal_exprt &ret =
    static_cast<const ieee_float_notequal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline ieee_float_notequal_exprt &to_ieee_float_notequal_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_ieee_float_notequal);
  ieee_float_notequal_exprt &ret =
    static_cast<ieee_float_notequal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class ieee_float_op_exprt : public ternary_exprt
{
public:
  ieee_float_op_exprt(
    const exprt &_lhs,
    const irep_idt &_id,
    exprt _rhs,
    exprt _rm)
    : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
  {
  }
 
  exprt &lhs()
  {
    return op0();
  }
 
  const exprt &lhs() const
  {
    return op0();
  }
 
  exprt &rhs()
  {
    return op1();
  }
 
  const exprt &rhs() const
  {
    return op1();
  }
 
  exprt &rounding_mode()
  {
    return op2();
  }
 
  const exprt &rounding_mode() const
  {
    return op2();
  }
};
 
template <>
inline bool can_cast_expr<ieee_float_op_exprt>(const exprt &base)
{
  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
         base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
}
 
inline void validate_expr(const ieee_float_op_exprt &value)
{
  validate_operands(
    value, 3, "IEEE float operations must have three arguments");
}
 
inline const ieee_float_op_exprt &to_ieee_float_op_expr(const exprt &expr)
{
  const ieee_float_op_exprt &ret =
    static_cast<const ieee_float_op_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline ieee_float_op_exprt &to_ieee_float_op_expr(exprt &expr)
{
  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class floatbv_mod_exprt : public binary_exprt
{
public:
  floatbv_mod_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(_lhs, ID_floatbv_mod, _rhs, _lhs.type())
  {
  }
};
 
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);
}
 
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);
}
 
class floatbv_rem_exprt : public binary_exprt
{
public:
  floatbv_rem_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(_lhs, ID_floatbv_rem, _rhs, _lhs.type())
  {
  }
};
 
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);
}
 
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);
}
 
constant_exprt floatbv_rounding_mode(unsigned);
 
#endif // CPROVER_UTIL_FLOATBV_EXPR_H