Go to the documentation of this file.
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
66 {std::move(_op0), std::move(_op1), std::move(_op2)})
107 set(ID_identifier, identifier);
112 return get(ID_identifier);
144 return get_bool(ID_C_static_lifetime);
149 return set(ID_C_static_lifetime,
true);
154 remove(ID_C_static_lifetime);
164 return set(ID_C_thread_local,
true);
169 remove(ID_C_thread_local);
176 return base.
id() == ID_symbol;
235 set(ID_identifier, identifier);
240 return get(ID_identifier);
247 return base.
id() == ID_nondet_symbol;
357 return base.
id() == ID_abs;
394 :
unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
407 return base.
id() == ID_unary_minus;
451 return base.
id() == ID_unary_plus;
518 return base.
id() == ID_sign;
559 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
570 "binary expression must have two operands");
667 expr.
type().
id() == ID_bool,
668 "result of binary predicate expression should be of type bool");
702 expr_binary.op0().type() == expr_binary.op1().type(),
703 "lhs and rhs of binary relation expression should have same type");
755 :
expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
856 return base.
id() == ID_plus;
893 :
binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
901 return base.
id() == ID_minus;
947 return base.
id() == ID_mult;
984 :
binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1016 return base.
id() == ID_div;
1053 :
binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1061 return base.
id() == ID_mod;
1098 :
binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1106 return base.
id() == ID_rem;
1166 return base.
id() == ID_equal;
1209 return base.
id() == ID_notequal;
1246 :
binary_exprt(_array, ID_index, std::move(_index), _array.
type().subtype())
1283 return base.
id() == ID_index;
1320 :
unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1348 return base.
id() == ID_array_of;
1403 return base.
id() == ID_array;
1431 :
multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1455 return base.
id() == ID_array_list;
1492 return base.
id() == ID_vector;
1520 :
unary_exprt(ID_union, std::move(_value), std::move(_type))
1527 return get(ID_component_name);
1532 set(ID_component_name, component_name);
1542 set(ID_component_number, narrow_cast<long long>(component_number));
1549 return base.
id() == ID_union;
1597 return base.
id() == ID_struct;
1657 return base.
id() == ID_complex;
1701 return base.
id() == ID_complex_real;
1707 expr, 1,
"real part retrieval operation must have one operand");
1746 return base.
id() == ID_complex_imag;
1752 expr, 1,
"imaginary part retrieval operation must have one operand");
1801 return base.
id() == ID_typecast;
1845 {std::move(
op0), std::move(
op1), std::move(
op2)},
1853 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
1873 return base.
id() == ID_and;
1885 return static_cast<const and_exprt &
>(expr);
1909 return base.
id() == ID_implies;
1953 {std::move(
op0), std::move(
op1), std::move(
op2)},
1961 {std::move(
op0), std::move(
op1), std::move(
op2), std::move(
op3)},
1981 return base.
id() == ID_or;
1993 return static_cast<const or_exprt &
>(expr);
2000 return static_cast<or_exprt &
>(expr);
2017 return base.
id() == ID_xor;
2029 return static_cast<const xor_exprt &
>(expr);
2053 return base.
id() == ID_not;
2138 return base.
id() == ID_if;
2179 {_old, std::move(_where), std::move(_new_value)})
2217 return base.
id() == ID_with;
2223 value, 3,
"array/structure update must have at least 3 operands",
true);
2226 "array/structure update must have an odd number of operands");
2274 return base.
id() == ID_index_designator;
2311 set(ID_component_name, _component_name);
2316 return get(ID_component_name);
2323 return base.
id() == ID_member_designator;
2363 std::move(_designator),
2364 std::move(_new_value),
2407 return base.
id() == ID_update;
2413 value, 3,
"Array/structure update must have three operands");
2446 const exprt &_array,
2447 const exprt &_index,
2448 const exprt &_new_value):
2449 exprt(ID_array_update, _array.type())
2464 const exprt &array()
const
2474 const exprt &index()
const
2484 const exprt &new_value()
const
2490 template<>
inline bool can_cast_expr<array_update_exprt>(
const exprt &base)
2492 return base.
id()==ID_array_update;
2506 inline const array_update_exprt &to_array_update_expr(
const exprt &expr)
2509 const array_update_exprt &ret =
static_cast<const array_update_exprt &
>(expr);
2515 inline array_update_exprt &to_array_update_expr(
exprt &expr)
2518 array_update_exprt &ret =
static_cast<array_update_exprt &
>(expr);
2544 return get(ID_component_name);
2549 set(ID_component_name, component_name);
2586 "member expression must have one operand");
2598 return base.
id() == ID_member;
2642 return base.
id() == ID_type;
2678 return get(ID_value);
2683 set(ID_value, value);
2692 return base.
id() == ID_constant;
2746 return base.
id() == ID_nil;
2926 return base.
id() == ID_let;
2984 return base.
id() == ID_cond;
2990 value.
operands().size() % 2 == 0,
"cond must have even number of operands");
3033 ID_array_comprehension,
3073 return base.
id() == ID_array_comprehension;
3138 set(ID_identifier, std::move(
id));
3150 return get(ID_component_name);
3158 return get(ID_C_class);
3165 return get(ID_C_base_name);
3173 return get(ID_identifier);
3182 "class method descriptor must have a mangled method name.");
3184 !value.
class_id().
empty(),
"class method descriptor must have a class id.");
3187 "class method descriptor must have a base method name.");
3191 "class method descriptor must have an identifier in the expected format.");
3213 return base.
id() == ID_virtual_function;
3216 #endif // CPROVER_UTIL_STD_EXPR_H
Operator to update elements in structs and arrays.
const exprt & array() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
if_exprt(exprt cond, const exprt &t, exprt f)
bool can_cast_expr< symbol_exprt >(const exprt &base)
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
bool can_cast_expr< union_exprt >(const exprt &base)
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
static exprt conditional_cast(const exprt &expr, const typet &type)
bool can_cast_expr< rem_exprt >(const exprt &base)
const exprt & index() const
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
A base class for multi-ary expressions Associativity is not specified.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
bool can_cast_expr< cond_exprt >(const exprt &base)
member_exprt(exprt op, const irep_idt &component_name, typet _type)
bool can_cast_expr< array_list_exprt >(const exprt &base)
bool can_cast_expr< mod_exprt >(const exprt &base)
const exprt & where() const
if_exprt(exprt cond, exprt t, exprt f, typet type)
member_designatort(const irep_idt &_component_name)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
bool can_cast_expr< index_designatort >(const exprt &base)
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
array_list_exprt(operandst _operands, array_typet _type)
const operandst & operands() const =delete
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Expression to hold a nondeterministic choice.
and_exprt(exprt::operandst _operands)
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
void copy_to_operands(const exprt &, const exprt &)=delete
const irep_idt & get_identifier() const
const exprt & rhs() const
std::size_t size() const
Amount of nodes this expression tree contains.
const exprt & real() const
unary_minus_exprt(exprt _op, typet _type)
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
bool can_cast_expr< not_exprt >(const exprt &base)
The type of an expression, extends irept.
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
An expression with three operands.
mult_exprt(exprt _lhs, exprt _rhs)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
bool can_cast_expr< sign_exprt >(const exprt &base)
bool can_cast_expr< unary_exprt >(const exprt &base)
const exprt & true_case() const
The trinary if-then-else operator.
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
div_exprt(exprt _lhs, exprt _rhs)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
plus_exprt(exprt _lhs, exprt _rhs)
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Real part of the expression describing a complex number.
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Union constructor from single element.
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
The plus expression Associativity is not specified.
bool can_cast_expr< xor_exprt >(const exprt &base)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Base class for all expressions.
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
const exprt & op1() const =delete
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Generic base class for unary expressions.
array_exprt(operandst _operands, array_typet _type)
index_exprt(exprt _array, exprt _index, typet _type)
void clear_static_lifetime()
A base class for binary expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
irep_idt get_component_name() const
Complex numbers made of pair of given subtype.
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Sign of an expression Predicate is true if _op is negative, false otherwise.
bool can_cast_expr< binary_exprt >(const exprt &base)
const exprt::operandst & designator() const
const array_typet & type() const
predicate_exprt(const irep_idt &_id)
const exprt & old() const
static void validate(const exprt &, validation_modet)
const symbol_exprt & arg() const
cond_exprt(operandst _operands, typet _type)
bool can_cast_expr< minus_exprt >(const exprt &base)
const array_list_exprt & to_array_list_expr(const exprt &expr)
index_designatort(exprt _index)
void copy_to_operands(const exprt &, const exprt &, const exprt &)=delete
void move_to_operands(exprt &)=delete
Vector constructor from list of elements.
size_t operator()(const ::symbol_exprt &sym)
index_exprt(const exprt &_array, exprt _index)
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Expression to hold a symbol (variable)
bool can_cast_expr< array_exprt >(const exprt &base)
void validate_expr(const symbol_exprt &value)
bool can_cast_expr< member_exprt >(const exprt &base)
minus_exprt(exprt _lhs, exprt _rhs)
std::size_t get_component_number() const
const array_typet & type() const
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
bool can_cast_expr< equal_exprt >(const exprt &base)
An expression denoting infinity.
void add(exprt index, exprt value)
add an index/value pair
bool can_cast_expr< implies_exprt >(const exprt &base)
const exprt & op3() const =delete
void set_component_name(const irep_idt &component_name)
const exprt & op3() const =delete
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
An expression describing a method on a class.
Struct constructor from list of elements.
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
typet & type()
Return the type of the expression.
exprt & value()
convenience accessor for the value of a single binding
or_exprt(exprt::operandst _operands)
An expression without operands.
bool get_bool(const irep_namet &name) const
bool can_cast_expr< let_exprt >(const exprt &base)
bool can_cast_expr< and_exprt >(const exprt &base)
std::size_t get_component_number() const
const array_typet & type() const
const exprt & where() const
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
and_exprt(exprt op0, exprt op1, exprt op2)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
xor_exprt(exprt _op0, exprt _op1)
rem_exprt(exprt _lhs, exprt _rhs)
notequal_exprt(exprt _lhs, exprt _rhs)
void move_to_operands(exprt &, exprt &, exprt &)=delete
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
const exprt & value() const
convenience accessor for the value of a single binding
bool can_cast_expr< abs_exprt >(const exprt &base)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
complex_real_exprt(const exprt &op)
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
and_exprt(exprt op0, exprt op1)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
The null pointer constant.
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
const std::string & id2string(const irep_idt &d)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
void set_static_lifetime()
const irep_idt & get_name() const
symbol_exprt(const irep_idt &identifier, typet type)
const exprt & compound() const
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
A base class for expressions that are predicates, i.e., Boolean-typed.
const exprt & op1() const
bool can_cast_expr< plus_exprt >(const exprt &base)
const exprt & new_value() const
const exprt & struct_op() const
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
#define PRECONDITION(CONDITION)
operandst & operands()=delete
remove all operand methods
bool can_cast_expr< array_of_exprt >(const exprt &base)
const irep_idt & get_identifier() const
Array constructor from single element.
void set_identifier(const irep_idt &identifier)
const exprt & index() const
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
bool is_thread_local() const
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
bool can_cast_expr< notequal_exprt >(const exprt &base)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
bool can_cast_expr< nil_exprt >(const exprt &base)
const exprt & body() const
null_pointer_exprt(pointer_typet type)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Binary multiplication Associativity is not specified.
std::vector< symbol_exprt > variablest
const exprt & old() const
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
mod_exprt(exprt _lhs, exprt _rhs)
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
The unary minus expression.
const exprt & op3() const =delete
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const variablest & variables() const
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
struct_exprt(operandst _operands, typet _type)
const irep_idt & id() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const binding_exprt & binding() const
void remove(const irep_namet &name)
A base class for variable bindings (quantifiers, let, lambda)
bool can_cast_expr< div_exprt >(const exprt &base)
std::vector< exprt > operandst
Complex constructor from a pair of numbers.
The Boolean constant false.
const operandst & values() const
vector_exprt(operandst _operands, vector_typet _type)
The unary plus expression.
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
const exprt & cond() const
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
const exprt & dividend() const
The dividend of a division is the number that is being divided.
const exprt & imag() const
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const array_typet & type() const
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
exprt & dividend()
The dividend of a division is the number that is being divided.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Operator to update elements in structs and arrays.
const exprt & op0() const =delete
exprt::operandst & designator()
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
const exprt & op0() const
unary_plus_exprt(exprt op)
dstring_hash irep_id_hash
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
bool can_cast_expr< index_exprt >(const exprt &base)
unary_exprt(const irep_idt &_id, const exprt &_op)
irep_idt get_component_name() const
unary_minus_exprt(exprt _op)
Extract member of struct or union.
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
equal_exprt(exprt _lhs, exprt _rhs)
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
bool can_cast_expr< complex_real_exprt >(const exprt &base)
An expression denoting a type.
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
plus_exprt(operandst _operands, typet _type)
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
infinity_exprt(typet _type)
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
std::size_t get_size_t(const irep_namet &name) const
bool can_cast_expr< or_exprt >(const exprt &base)
void copy_to_operands(const exprt &expr)=delete
decorated_symbol_exprt(const irep_idt &identifier, typet type)
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
bool value_is_zero_string() const
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
member_exprt(exprt op, const struct_typet::componentt &c)
const exprt & op2() const =delete
bool can_cast_expr< type_exprt >(const exprt &base)
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const exprt & false_case() const
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
A base class for relations, i.e., binary predicates whose two operands have the same type.
typecast_exprt(exprt op, typet _type)
Templated functions to cast to specific exprt-derived classes.
const exprt & op1() const =delete
Imaginary part of the expression describing a complex number.
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
nullary_exprt(const irep_idt &_id, typet _type)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const exprt & lhs() const
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
void clear_thread_local()
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
or_exprt(exprt op0, exprt op1, exprt op2)
const exprt & op2() const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool can_cast_expr< typecast_exprt >(const exprt &base)
bool can_cast_expr< vector_exprt >(const exprt &base)
irep_idt get_component_name() const
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
const irept & get_nil_irep()
const exprt & where() const
convenience accessor for binding().where()
bool can_cast_expr< if_exprt >(const exprt &base)
const exprt & what() const
exprt & component(const irep_idt &name, const namespacet &ns)
Array constructor from a list of index-element pairs Operands are index/value pairs,...
constant_exprt(const irep_idt &_value, typet _type)
bool can_cast_expr< constant_exprt >(const exprt &base)
bool is_static_lifetime() const
bool can_cast_expr< complex_exprt >(const exprt &base)
or_exprt(exprt op0, exprt op1)
const exprt & op2() const =delete
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
Semantic type conversion.
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
unary_predicate_exprt(const irep_idt &_id, exprt _op)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
complex_imag_exprt(const exprt &op)
Expression to define a mapping from an argument (index) to elements.
The Boolean constant true.
A constant literal expression.
const exprt & op2() const =delete
const exprt & op3() const =delete
implies_exprt(exprt op0, exprt op1)
bool can_cast_expr< struct_exprt >(const exprt &base)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
exprt & where()
convenience accessor for binding().where()
binding_exprt & binding()
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
void set_component_number(std::size_t component_number)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
void set_value(const irep_idt &value)
const irep_idt & get_value() const
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
array_of_exprt(exprt _what, array_typet _type)
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Array constructor from list of elements.
bool can_cast_expr< with_exprt >(const exprt &base)
void set_component_name(const irep_idt &component_name)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
void set_identifier(const irep_idt &identifier)
const exprt & new_value() const
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Base class for all expressions.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
bool can_cast_expr< member_designatort >(const exprt &base)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
bool can_cast_expr< update_exprt >(const exprt &base)
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
void move_to_operands(exprt &, exprt &)=delete
bool can_cast_expr< mult_exprt >(const exprt &base)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
nondet_symbol_exprt(const irep_idt &identifier, typet type)
const exprt & op3() const