Go to the documentation of this file.
9 #ifndef CPROVER_UTIL_MATHEMATICAL_EXPR_H
10 #define CPROVER_UTIL_MATHEMATICAL_EXPR_H
62 return base.
id() == ID_trans;
104 return base.
id() == ID_power;
148 return base.
id() == ID_factorial_power;
196 SINCE(2019, 3, 3,
"use function_application_exprt(fkt, arg) instead"))
203 ID_function_application,
235 return base.
id() == ID_function_application;
305 return base.
id() == ID_forall || base.
id() == ID_exists;
313 op.id() == ID_symbol,
"quantified variable shall be a symbol");
391 #endif // CPROVER_UTIL_MATHEMATICAL_EXPR_H
const argumentst & arguments() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_cast_expr< factorial_power_exprt >(const exprt &base)
bool can_cast_expr< quantifier_exprt >(const exprt &base)
A base class for multi-ary expressions Associativity is not specified.
function_application_exprt(const symbol_exprt &_function, const argumentst &_arguments, const typet &_type)
The type of an expression, extends irept.
void validate_expr(const transt &value)
An expression with three operands.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const factorial_power_exprt & to_factorial_power_expr(const exprt &expr)
Cast an exprt to a factorial_power_exprt.
Base class for all expressions.
A base class for binary expressions.
A base class for quantifier expressions.
const symbol_exprt & symbol() const
Expression to hold a symbol (variable)
power_exprt(const exprt &_base, const exprt &_exp)
exprt::operandst argumentst
Transition system, consisting of state invariant, initial state predicate, and transition predicate.
forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
transt(const irep_idt &_id, const exprt &_op0, const exprt &_op1, const exprt &_op2, const typet &_type)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
constructor for multiple variables
const exprt & init() const
#define PRECONDITION(CONDITION)
const transt & to_trans_expr(const exprt &expr)
Cast an exprt to a transt expr must be known to be transt.
Application of (mathematical) function.
std::vector< symbol_exprt > variablest
const irep_idt & id() const
A base class for variable bindings (quantifiers, let, lambda)
std::vector< exprt > operandst
tuple_exprt(exprt::operandst operands)
bool can_cast_expr< power_exprt >(const exprt &base)
#define SINCE(year, month, day, msg)
const exprt & invar() const
factorial_power_exprt(const exprt &_base, const exprt &_exp)
const exists_exprt & to_exists_expr(const exprt &expr)
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
bool can_cast_expr< function_application_exprt >(const exprt &base)
bool can_cast_expr< transt >(const exprt &base)
factorial_power_exprt & to_factorial_expr(exprt &expr)
Cast an exprt to a factorial_power_exprt.
const exprt & trans() const
const power_exprt & to_power_expr(const exprt &expr)
Cast an exprt to a power_exprt.
API to expression classes.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
exists_exprt(const symbol_exprt &_symbol, const exprt &_where)
const forall_exprt & to_forall_expr(const exprt &expr)
quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
constructor for single variable