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 379 of file mathematical_expr.h.
|
inline |
Definition at line 147 of file mathematical_expr.h.
|
inline |
Definition at line 342 of file mathematical_expr.h.
|
inline |
Definition at line 225 of file mathematical_expr.h.
|
inline |
Definition at line 430 of file mathematical_expr.h.
|
inline |
Definition at line 103 of file mathematical_expr.h.
|
inline |
Definition at line 295 of file mathematical_expr.h.
|
inline |
Definition at line 61 of file mathematical_expr.h.
|
inline |
Definition at line 389 of file mathematical_expr.h.
|
inline |
Definition at line 397 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 352 of file mathematical_expr.h.
|
inline |
Definition at line 360 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 242 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 252 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 446 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 457 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 314 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 323 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 384 of file mathematical_expr.h.
|
inline |
Definition at line 152 of file mathematical_expr.h.
|
inline |
Definition at line 347 of file mathematical_expr.h.
|
inline |
Definition at line 230 of file mathematical_expr.h.
|
inline |
Definition at line 435 of file mathematical_expr.h.
|
inline |
Definition at line 108 of file mathematical_expr.h.
|
inline |
Definition at line 300 of file mathematical_expr.h.
|
inline |
Definition at line 66 of file mathematical_expr.h.