cprover
|
API to expression classes for 'mathematical' expressions. More...
#include "std_expr.h"
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... | |
API to expression classes for 'mathematical' expressions.
Definition in file mathematical_expr.h.
|
inline |
Definition at line 146 of file mathematical_expr.h.
|
inline |
Definition at line 233 of file mathematical_expr.h.
|
inline |
Definition at line 102 of file mathematical_expr.h.
|
inline |
Definition at line 303 of file mathematical_expr.h.
|
inline |
Definition at line 60 of file mathematical_expr.h.
|
inline |
Definition at line 375 of file mathematical_expr.h.
|
inline |
Definition at line 383 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 172 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 162 of file mathematical_expr.h.
|
inline |
Definition at line 349 of file mathematical_expr.h.
|
inline |
Definition at line 357 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 250 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 260 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 118 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 127 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 322 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 331 of file mathematical_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 74 of file mathematical_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 83 of file mathematical_expr.h.
|
inline |
Definition at line 151 of file mathematical_expr.h.
|
inline |
Definition at line 238 of file mathematical_expr.h.
|
inline |
Definition at line 107 of file mathematical_expr.h.
|
inline |
Definition at line 308 of file mathematical_expr.h.
|
inline |
Definition at line 65 of file mathematical_expr.h.