9 #ifndef CPROVER_UTIL_MATHEMATICAL_EXPR_H
10 #define CPROVER_UTIL_MATHEMATICAL_EXPR_H
63 return base.
id() == ID_trans;
105 return base.
id() == ID_power;
149 return base.
id() == ID_factorial_power;
232 return base.
id() == ID_function_application;
302 return base.
id() == ID_forall || base.
id() == ID_exists;
310 op.id() == ID_symbol,
"quantified variable shall be a symbol");
354 return base.
id() == ID_forall;
396 return base.
id() == ID_exists;
447 return base.
id() == ID_lambda;
466 expr.
type().
id() == ID_mathematical_function,
467 "lambda must have right type");
477 expr.
type().
id() == ID_mathematical_function,
478 "lambda must have right type");
A base class for binary expressions.
A base class for variable bindings (quantifiers, let, lambda)
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
std::vector< symbol_exprt > variablest
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
factorial_power_exprt(const exprt &_base, const exprt &_exp)
forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
Application of (mathematical) function.
function_application_exprt(const exprt &_function, argumentst _arguments)
const argumentst & arguments() const
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
A (mathematical) lambda expression.
lambda_exprt(const variablest &, const exprt &_where)
const mathematical_function_typet & type() const
exprt application(const operandst &arguments) const
mathematical_function_typet & type()
A type for mathematical functions (do not confuse with functions/methods in code)
A base class for multi-ary expressions Associativity is not specified.
power_exprt(const exprt &_base, const exprt &_exp)
A base class for quantifier expressions.
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
constructor for single variable
const symbol_exprt & symbol() const
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
constructor for multiple variables
Expression to hold a symbol (variable)
An expression with three operands.
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
const exprt & invar() const
const exprt & init() const
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
const exprt & trans() const
tuple_exprt(exprt::operandst operands, typet type)
tuple_exprt(exprt::operandst operands)
The type of an expression, extends irept.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
bool can_cast_expr< forall_exprt >(const exprt &base)
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const exists_exprt & to_exists_expr(const exprt &expr)
bool can_cast_expr< quantifier_exprt >(const exprt &base)
bool can_cast_expr< exists_exprt >(const exprt &base)
void validate_expr(const transt &value)
bool can_cast_expr< function_application_exprt >(const exprt &base)
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
bool can_cast_expr< lambda_exprt >(const exprt &base)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const forall_exprt & to_forall_expr(const exprt &expr)
bool can_cast_expr< transt >(const exprt &base)
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
bool can_cast_expr< power_exprt >(const exprt &base)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.