cprover
|
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 147 of file mathematical_expr.h.
|
inline |
Definition at line 227 of file mathematical_expr.h.
|
inline |
Definition at line 407 of file mathematical_expr.h.
|
inline |
Definition at line 103 of file mathematical_expr.h.
|
inline |
Definition at line 297 of file mathematical_expr.h.
|
inline |
Definition at line 61 of file mathematical_expr.h.
|
inline |
Definition at line 369 of file mathematical_expr.h.
|
inline |
Definition at line 377 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 343 of file mathematical_expr.h.
|
inline |
Definition at line 351 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 244 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 254 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 423 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 434 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 316 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 325 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 152 of file mathematical_expr.h.
|
inline |
Definition at line 232 of file mathematical_expr.h.
|
inline |
Definition at line 412 of file mathematical_expr.h.
|
inline |
Definition at line 108 of file mathematical_expr.h.
|
inline |
Definition at line 302 of file mathematical_expr.h.
|
inline |
Definition at line 66 of file mathematical_expr.h.