CBMC
|
A base class for variable bindings (quantifiers, let, lambda) More...
#include <std_expr.h>
Public Types | |
using | variablest = std::vector< symbol_exprt > |
![]() | |
typedef std::vector< exprt > | operandst |
![]() | |
using | baset = tree_implementationt |
![]() | |
using | dt = tree_nodet< irept, forward_list_as_mapt< irep_idt, irept >, true > |
using | subt = typename dt::subt |
using | named_subt = typename dt::named_subt |
using | tree_implementationt = sharing_treet |
Used to refer to this class from derived classes. | |
Additional Inherited Members | |
![]() | |
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 |
A base class for variable bindings (quantifiers, let, lambda)
Definition at line 3233 of file std_expr.h.
using binding_exprt::variablest = std::vector<symbol_exprt> |
Definition at line 3236 of file std_expr.h.
|
inline |
construct the binding expression
Definition at line 3239 of file std_expr.h.
exprt binding_exprt::instantiate | ( | const exprt::operandst & | values | ) | const |
substitute free occurrences of the variables in where() by the given values
Definition at line 225 of file std_expr.cpp.
exprt binding_exprt::instantiate | ( | const variablest & | new_variables | ) | const |
substitute free occurrences of the variables in where() by a set of different symbols
Definition at line 255 of file std_expr.cpp.
|
inline |
Definition at line 3255 of file std_expr.h.
|
inline |
Definition at line 3260 of file std_expr.h.
|
inline |
Definition at line 3265 of file std_expr.h.
Definition at line 3270 of file std_expr.h.