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 410 of file mathematical_expr.h.
|
inline |
Definition at line 163 of file mathematical_expr.h.
|
inline |
Definition at line 368 of file mathematical_expr.h.
|
inline |
Definition at line 246 of file mathematical_expr.h.
|
inline |
Definition at line 461 of file mathematical_expr.h.
|
inline |
Definition at line 126 of file mathematical_expr.h.
|
inline |
Definition at line 316 of file mathematical_expr.h.
|
inline |
Definition at line 61 of file mathematical_expr.h.
|
inline |
Definition at line 420 of file mathematical_expr.h.
|
inline |
Definition at line 428 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 189 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 179 of file mathematical_expr.h.
|
inline |
Definition at line 378 of file mathematical_expr.h.
|
inline |
Definition at line 386 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 263 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 273 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 477 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 488 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 137 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 145 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 335 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 344 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 415 of file mathematical_expr.h.
|
inline |
Definition at line 168 of file mathematical_expr.h.
|
inline |
Definition at line 373 of file mathematical_expr.h.
|
inline |
Definition at line 251 of file mathematical_expr.h.
|
inline |
Definition at line 466 of file mathematical_expr.h.
|
inline |
Definition at line 321 of file mathematical_expr.h.
|
inline |
Definition at line 66 of file mathematical_expr.h.