|
| array_comprehension_exprt (symbol_exprt arg, exprt body, array_typet _type) |
const array_typet & | type () const |
array_typet & | type () |
const symbol_exprt & | arg () const |
symbol_exprt & | arg () |
const exprt & | body () const |
exprt & | body () |
| binding_exprt (irep_idt _id, const variablest &_variables, exprt _where, typet _type) |
| construct the binding expression
|
variablest & | variables () |
const variablest & | variables () const |
exprt & | where () |
const exprt & | where () const |
exprt | instantiate (const exprt::operandst &) const |
| substitute free occurrences of the variables in where() by the given values
|
exprt | instantiate (const variablest &) const |
| substitute free occurrences of the variables in where() by a set of different symbols
|
| binary_exprt (const exprt &_lhs, const irep_idt &_id, exprt _rhs) |
| binary_exprt (exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type) |
exprt & | lhs () |
const exprt & | lhs () const |
exprt & | rhs () |
const exprt & | rhs () const |
const exprt & | op2 () const =delete |
exprt & | op2 ()=delete |
const exprt & | op3 () const =delete |
exprt & | op3 ()=delete |
exprt & | op0 () |
const exprt & | op0 () const |
exprt & | op1 () |
const exprt & | op1 () const |
| exprt () |
| exprt (const irep_idt &_id) |
| exprt (irep_idt _id, typet _type) |
| exprt (irep_idt _id, typet _type, operandst &&_operands) |
| exprt (const irep_idt &id, typet type, source_locationt loc) |
typet & | type () |
| Return the type of the expression.
|
const typet & | type () const |
bool | has_operands () const |
| Return true if there is at least one operand.
|
operandst & | operands () |
const operandst & | operands () const |
exprt & | with_source_location (source_locationt location) & |
| Add the source location from location , if it is non-nil.
|
exprt && | with_source_location (source_locationt location) && |
| Add the source location from location , if it is non-nil.
|
exprt & | with_source_location (const exprt &other) & |
| Add the source location from other , if it has any.
|
exprt && | with_source_location (const exprt &other) && |
| Add the source location from other , if it has any.
|
void | reserve_operands (operandst::size_type n) |
void | copy_to_operands (const exprt &expr) |
| Copy the given argument to the end of exprt's operands.
|
void | add_to_operands (const exprt &expr) |
| Add the given argument to the end of exprt's operands.
|
void | add_to_operands (exprt &&expr) |
| Add the given argument to the end of exprt's operands.
|
void | add_to_operands (exprt &&e1, exprt &&e2) |
| Add the given arguments to the end of exprt's operands.
|
void | add_to_operands (exprt &&e1, exprt &&e2, exprt &&e3) |
| Add the given arguments to the end of exprt's operands.
|
bool | is_constant () const |
| Return whether the expression is a constant.
|
bool | is_true () const |
| Return whether the expression is a constant representing true.
|
bool | is_false () const |
| Return whether the expression is a constant representing false.
|
bool | is_zero () const |
| Return whether the expression is a constant representing 0.
|
bool | is_one () const |
| Return whether the expression is a constant representing 1.
|
bool | is_boolean () const |
| Return whether the expression represents a Boolean.
|
const source_locationt & | find_source_location () const |
| Get a source_locationt from the expression or from its operands (non-recursively).
|
const source_locationt & | source_location () const |
source_locationt & | add_source_location () |
void | drop_source_location () |
void | visit (class expr_visitort &visitor) |
| These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children have been visited.
|
void | visit (class const_expr_visitort &visitor) const |
void | visit_pre (std::function< void(exprt &)>) |
void | visit_pre (std::function< void(const exprt &)>) const |
void | visit_post (std::function< void(exprt &)>) |
| These are post-order traversal visitors, i.e., the visitor is executed on a node after its children have been visited.
|
void | visit_post (std::function< void(const exprt &)>) const |
depth_iteratort | depth_begin () |
depth_iteratort | depth_end () |
const_depth_iteratort | depth_begin () const |
const_depth_iteratort | depth_end () const |
const_depth_iteratort | depth_cbegin () const |
const_depth_iteratort | depth_cend () const |
depth_iteratort | depth_begin (std::function< exprt &()> mutate_root) const |
const_unique_depth_iteratort | unique_depth_begin () const |
const_unique_depth_iteratort | unique_depth_end () const |
const_unique_depth_iteratort | unique_depth_cbegin () const |
const_unique_depth_iteratort | unique_depth_cend () const |
bool | is_nil () const |
bool | is_not_nil () const |
| irept (const irep_idt &_id) |
| irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub) |
| irept ()=default |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_idt &name) const |
irept & | add (const irep_idt &name) |
irept & | add (const irep_idt &name, irept irep) |
const std::string & | get_string (const irep_idt &name) const |
const irep_idt & | get (const irep_idt &name) const |
bool | get_bool (const irep_idt &name) const |
signed int | get_int (const irep_idt &name) const |
std::size_t | get_size_t (const irep_idt &name) const |
long long | get_long_long (const irep_idt &name) const |
void | set (const irep_idt &name, const irep_idt &value) |
void | set (const irep_idt &name, irept irep) |
void | set (const irep_idt &name, const long long value) |
void | set_size_t (const irep_idt &name, const std::size_t value) |
void | remove (const irep_idt &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_idt &name, irept &irep) |
bool | operator== (const irept &other) const |
bool | operator!= (const irept &other) const |
void | swap (irept &irep) |
bool | operator< (const irept &other) const |
| defines ordering on the internal representation
|
bool | ordering (const irept &other) const |
| defines ordering on the internal representation
|
int | compare (const irept &i) const |
| defines ordering on the internal representation comments are ignored
|
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
std::size_t | hash () const |
std::size_t | full_hash () const |
bool | full_eq (const irept &other) const |
std::string | pretty (unsigned indent=0, unsigned max_indent=0) const |
| sharing_treet (irep_idt _id) |
sharing_treet & | operator= (const sharing_treet &irep) |
| ~sharing_treet () |
const dt & | read () const |
dt & | write () |
|
using | variablest = std::vector<symbol_exprt> |
typedef std::vector< exprt > | operandst |
using | baset = tree_implementationt |
using | dt |
using | subt |
using | named_subt |
using | tree_implementationt |
| Used to refer to this class from derived classes.
|
static void | check (const exprt &expr, const validation_modet vm=validation_modet::INVARIANT) |
static void | validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
static void | check (const exprt &, const validation_modet) |
| Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are not checked).
|
static void | validate (const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT) |
| Check that the expression is well-formed, assuming that its subexpressions and type have all ready been checked for well-formedness.
|
static void | validate_full (const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT) |
| Check that the expression is well-formed (full check, including checks of all subexpressions and the type)
|
static bool | is_comment (const irep_idt &name) |
static std::size_t | number_of_non_comments (const named_subt &) |
| count the number of named_sub elements that are not comments
|
| expr_protectedt (irep_idt _id, typet _type) |
| expr_protectedt (irep_idt _id, typet _type, operandst _operands) |
exprt & | op0 () |
const exprt & | op0 () const |
exprt & | op1 () |
const exprt & | op1 () const |
exprt & | op2 () |
const exprt & | op2 () const |
exprt & | op3 () |
const exprt & | op3 () const |
exprt & | op0 () |
exprt & | op1 () |
exprt & | op2 () |
exprt & | op3 () |
const exprt & | op0 () const |
const exprt & | op1 () const |
const exprt & | op2 () const |
const exprt & | op3 () const |
exprt & | add_expr (const irep_idt &name) |
const exprt & | find_expr (const irep_idt &name) const |
void | detach () |
static void | remove_ref (dt *old_data) |
static void | nonrecursive_destructor (dt *old_data) |
| Does the same as remove_ref, but using an explicit stack instead of recursion.
|
dt * | data |
static dt | empty_d |
Expression to define a mapping from an argument (index) to elements.
This enables constructing an array via an anonymous function. Not all kinds of array comprehension can be expressed, only those of the form [f(x) | x in {0, 1, ... array_size-1}]. The LHS and RHS are the argument (x) and body (f(x)) of the anonymous function, respectively. The range is given by the type of the expression, which has to be an array_typet (which includes a value for array_size).
Definition at line 3547 of file std_expr.h.