13#ifndef CPROVER_UTIL_MATHEMATICAL_TYPES_H
14#define CPROVER_UTIL_MATHEMATICAL_TYPES_H
67 ID_mathematical_function,
107 return type.
id() == ID_mathematical_function;
Unbounded, signed integers (mathematical integers, not bitvectors)
const irep_idt & id() const
A type for mathematical functions (do not confuse with functions/methods in code)
const domaint & domain() const
const typet & codomain() const
Return the codomain, i.e., the set of values that the function maps to (the "target").
typet & codomain()
Return the codomain, i.e., the set of values that the function maps to (the "target").
void add_variable(const typet &_type)
mathematical_function_typet(const domaint &_domain, const typet &_codomain)
std::vector< typet > domaint
Natural numbers including zero (mathematical integers, not bitvectors)
Unbounded, signed rational numbers.
Unbounded, signed real numbers.
Type with multiple subtypes.
The type of an expression, extends irept.
Templated functions to cast to specific exprt-derived classes.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
bool can_cast_type< mathematical_function_typet >(const typet &type)
Check whether a reference to a typet is a mathematical_function_typet.
#define PRECONDITION(CONDITION)
Defines typet, type_with_subtypet and type_with_subtypest.
const type_with_subtypest & to_type_with_subtypes(const typet &type)