CBMC
|
API to expression classes for 'mathematical' expressions. More...
Go to the source code of this file.
Classes | |
class | transt |
Transition system, consisting of state invariant, initial state predicate, and transition predicate. More... | |
class | power_exprt |
Exponentiation. More... | |
class | factorial_power_exprt |
Falling factorial power. More... | |
class | tuple_exprt |
class | function_application_exprt |
Application of (mathematical) function. More... | |
class | quantifier_exprt |
A base class for quantifier expressions. More... | |
class | forall_exprt |
A forall expression. More... | |
class | exists_exprt |
An exists expression. More... | |
class | lambda_exprt |
A (mathematical) lambda expression. More... | |
API to expression classes for 'mathematical' expressions.
Definition in file mathematical_expr.h.
|
inline |
Definition at line 394 of file mathematical_expr.h.
|
inline |
Definition at line 147 of file mathematical_expr.h.
|
inline |
Definition at line 352 of file mathematical_expr.h.
|
inline |
Definition at line 230 of file mathematical_expr.h.
|
inline |
Definition at line 445 of file mathematical_expr.h.
|
inline |
Definition at line 103 of file mathematical_expr.h.
|
inline |
Definition at line 300 of file mathematical_expr.h.
|
inline |
Definition at line 61 of file mathematical_expr.h.
|
inline |
Definition at line 404 of file mathematical_expr.h.
|
inline |
Definition at line 412 of file mathematical_expr.h.
|
inline |
Cast an exprt to a factorial_power_exprt.
expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 173 of file mathematical_expr.h.
|
inline |
Cast an exprt to a factorial_power_exprt.
expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 163 of file mathematical_expr.h.
|
inline |
Definition at line 362 of file mathematical_expr.h.
|
inline |
Definition at line 370 of file mathematical_expr.h.
|
inline |
Cast an exprt to a function_application_exprt.
expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 247 of file mathematical_expr.h.
|
inline |
Cast an exprt to a function_application_exprt.
expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 257 of file mathematical_expr.h.
|
inline |
Cast an exprt to a lambda_exprt.
expr must be known to be lambda_exprt.
expr | Source expression |
Definition at line 461 of file mathematical_expr.h.
|
inline |
Cast an exprt to a lambda_exprt.
expr must be known to be lambda_exprt.
expr | Source expression |
Definition at line 472 of file mathematical_expr.h.
|
inline |
Cast an exprt to a power_exprt.
expr must be known to be power_exprt.
expr | Source expression |
Definition at line 119 of file mathematical_expr.h.
|
inline |
Cast an exprt to a power_exprt.
expr must be known to be power_exprt.
expr | Source expression |
Definition at line 128 of file mathematical_expr.h.
|
inline |
Cast an exprt to a quantifier_exprt.
expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 319 of file mathematical_expr.h.
|
inline |
Cast an exprt to a quantifier_exprt.
expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 328 of file mathematical_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 75 of file mathematical_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 84 of file mathematical_expr.h.
|
inline |
Definition at line 399 of file mathematical_expr.h.
|
inline |
Definition at line 152 of file mathematical_expr.h.
|
inline |
Definition at line 357 of file mathematical_expr.h.
|
inline |
Definition at line 235 of file mathematical_expr.h.
|
inline |
Definition at line 450 of file mathematical_expr.h.
|
inline |
Definition at line 108 of file mathematical_expr.h.
|
inline |
Definition at line 305 of file mathematical_expr.h.
|
inline |
Definition at line 66 of file mathematical_expr.h.