15 const exprt &_function,
19 ID_function_application,
38 domain.reserve(variables.size());
40 for(
const auto &v : variables)
41 domain.push_back(v.type());
A base class for binary expressions.
A base class for variable bindings (quantifiers, let, lambda)
std::vector< symbol_exprt > variablest
Base class for all expressions.
typet & type()
Return the type of the expression.
function_application_exprt(const exprt &_function, argumentst _arguments)
const mathematical_function_typet & function_type() const
This helper method provides the type of the expression returned by function.
exprt::operandst argumentst
lambda_exprt(const variablest &, const exprt &_where)
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
power_exprt(const exprt &_base, const exprt &_exp)
const exprt & base() const
static mathematical_function_typet lambda_type(const lambda_exprt::variablest &variables, const exprt &where)
API to expression classes for 'mathematical' expressions.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
#define PRECONDITION(CONDITION)