77 value.set_sign(
false);
174 result.
op2()=rounding_mode;
219 if(value.has_value())
288 "expression type of operand must match type of expression");
291 "expression type of operand must match type of expression");
303 if(rounding_mode.has_value())
308 v1.rounding_mode=
v0.rounding_mode;
386 return std::move(isnan);
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
bool is_one() const
Return whether the expression is a constant representing 1.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
Semantic type conversion from/to floating-point formats.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
mp_integer to_integer() const
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
rounding_modet rounding_mode
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
const irep_idt & id() const
Evaluates to true if the operand is NaN.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
resultt simplify_isnan(const unary_exprt &)
resultt simplify_abs(const abs_exprt &)
resultt simplify_isnormal(const unary_exprt &)
resultt simplify_floatbv_typecast(const floatbv_typecast_exprt &)
resultt simplify_isinf(const unary_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_node(exprt)
resultt simplify_floatbv_op(const ieee_float_op_exprt &)
resultt simplify_ieee_float_relation(const binary_relation_exprt &)
resultt simplify_sign(const sign_exprt &)
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
exprt simplify_expr(exprt src, const namespacet &ns)
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.