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());
56 const std::map<irep_idt, exprt> &substitutions,
59 if(src.
id() == ID_symbol)
61 auto s_it = substitutions.find(
to_symbol_expr(src).get_identifier());
62 if(s_it == substitutions.end())
71 bool op_changed =
false;
77 if(op_result.has_value())
79 op = op_result.value();
96 std::map<symbol_exprt, exprt> value_map;
98 for(std::size_t i = 0; i <
variables.size(); i++)
106 std::map<irep_idt, exprt> substitutions;
108 for(std::size_t i = 0; i <
variables.size(); i++)
109 substitutions[
variables[i].get_identifier()] = arguments[i];
114 if(substitute_result.has_value())
115 return substitute_result.value();
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.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
typet & type()
Return the type of the expression.
std::size_t size() const
Amount of nodes this expression tree contains.
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
const irep_idt & id() const
lambda_exprt(const variablest &, const exprt &_where)
exprt application(const operandst &) const
mathematical_function_typet & type()
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
static optionalt< exprt > substitute_symbols_rec(const std::map< irep_idt, exprt > &substitutions, exprt src)
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.
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.