cprover
|
API to expression classes. More...
#include "as_const.h"
#include "expr_cast.h"
#include "invariant.h"
#include "narrow.h"
#include "std_types.h"
Go to the source code of this file.
Classes | |
class | nullary_exprt |
An expression without operands. More... | |
class | ternary_exprt |
An expression with three operands. More... | |
class | symbol_exprt |
Expression to hold a symbol (variable) More... | |
class | decorated_symbol_exprt |
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local. More... | |
class | nondet_symbol_exprt |
Expression to hold a nondeterministic choice. More... | |
class | unary_exprt |
Generic base class for unary expressions. More... | |
class | abs_exprt |
Absolute value. More... | |
class | unary_minus_exprt |
The unary minus expression. More... | |
class | unary_plus_exprt |
The unary plus expression. More... | |
class | bswap_exprt |
The byte swap expression. More... | |
class | predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed. More... | |
class | unary_predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument. More... | |
class | sign_exprt |
Sign of an expression Predicate is true if _op is negative, false otherwise. More... | |
class | binary_exprt |
A base class for binary expressions. More... | |
class | binary_predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments. More... | |
class | binary_relation_exprt |
A base class for relations, i.e., binary predicates whose two operands have the same type. More... | |
class | multi_ary_exprt |
A base class for multi-ary expressions Associativity is not specified. More... | |
class | plus_exprt |
The plus expression Associativity is not specified. More... | |
class | minus_exprt |
Binary minus. More... | |
class | mult_exprt |
Binary multiplication Associativity is not specified. More... | |
class | div_exprt |
Division. More... | |
class | mod_exprt |
Modulo. More... | |
class | rem_exprt |
Remainder of division. More... | |
class | equal_exprt |
Equality. More... | |
class | notequal_exprt |
Disequality. More... | |
class | index_exprt |
Array index operator. More... | |
class | array_of_exprt |
Array constructor from single element. More... | |
class | array_exprt |
Array constructor from list of elements. More... | |
class | array_list_exprt |
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating. More... | |
class | vector_exprt |
Vector constructor from list of elements. More... | |
class | union_exprt |
Union constructor from single element. More... | |
class | struct_exprt |
Struct constructor from list of elements. More... | |
class | complex_exprt |
Complex constructor from a pair of numbers. More... | |
class | complex_real_exprt |
Real part of the expression describing a complex number. More... | |
class | complex_imag_exprt |
Imaginary part of the expression describing a complex number. More... | |
class | object_descriptor_exprt |
Split an expression into a base object and a (byte) offset. More... | |
class | dynamic_object_exprt |
Representation of heap-allocated objects. More... | |
class | is_dynamic_object_exprt |
Evaluates to true if the operand is a pointer to a dynamic object. More... | |
class | typecast_exprt |
Semantic type conversion. More... | |
class | floatbv_typecast_exprt |
Semantic type conversion from/to floating-point formats. More... | |
class | and_exprt |
Boolean AND. More... | |
class | implies_exprt |
Boolean implication. More... | |
class | or_exprt |
Boolean OR. More... | |
class | xor_exprt |
Boolean XOR. More... | |
class | bitnot_exprt |
Bit-wise negation of bit-vectors. More... | |
class | bitor_exprt |
Bit-wise OR. More... | |
class | bitxor_exprt |
Bit-wise XOR. More... | |
class | bitand_exprt |
Bit-wise AND. More... | |
class | shift_exprt |
A base class for shift operators. More... | |
class | shl_exprt |
Left shift. More... | |
class | ashr_exprt |
Arithmetic right shift. More... | |
class | lshr_exprt |
Logical right shift. More... | |
class | extractbit_exprt |
Extracts a single bit of a bit-vector operand. More... | |
class | extractbits_exprt |
Extracts a sub-range of a bit-vector operand. More... | |
class | address_of_exprt |
Operator to return the address of an object. More... | |
class | not_exprt |
Boolean negation. More... | |
class | dereference_exprt |
Operator to dereference a pointer. More... | |
class | if_exprt |
The trinary if-then-else operator. More... | |
class | with_exprt |
Operator to update elements in structs and arrays. More... | |
class | index_designatort |
class | member_designatort |
class | update_exprt |
Operator to update elements in structs and arrays. More... | |
class | member_exprt |
Extract member of struct or union. More... | |
class | isnan_exprt |
Evaluates to true if the operand is NaN. More... | |
class | isinf_exprt |
Evaluates to true if the operand is infinite. More... | |
class | isfinite_exprt |
Evaluates to true if the operand is finite. More... | |
class | isnormal_exprt |
Evaluates to true if the operand is a normal number. More... | |
class | ieee_float_equal_exprt |
IEEE-floating-point equality. More... | |
class | ieee_float_notequal_exprt |
IEEE floating-point disequality. More... | |
class | ieee_float_op_exprt |
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2). More... | |
class | type_exprt |
An expression denoting a type. More... | |
class | constant_exprt |
A constant literal expression. More... | |
class | true_exprt |
The Boolean constant true. More... | |
class | false_exprt |
The Boolean constant false. More... | |
class | nil_exprt |
The NIL expression. More... | |
class | null_pointer_exprt |
The null pointer constant. More... | |
class | replication_exprt |
Bit-vector replication. More... | |
class | concatenation_exprt |
Concatenation of bit-vector operands. More... | |
class | infinity_exprt |
An expression denoting infinity. More... | |
class | binding_exprt |
A base class for variable bindings (quantifiers, let, lambda) More... | |
class | let_exprt |
A let expression. More... | |
class | popcount_exprt |
The popcount (counting the number of bits set to 1) expression. More... | |
class | cond_exprt |
this is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true. More... | |
class | array_comprehension_exprt |
Expression to define a mapping from an argument (index) to elements. More... | |
class | class_method_descriptor_exprt |
An expression describing a method on a class. More... | |
API to expression classes.
Definition in file std_expr.h.
|
inline |
Definition at line 342 of file std_expr.h.
|
inline |
Definition at line 2807 of file std_expr.h.
|
inline |
Definition at line 2173 of file std_expr.h.
|
inline |
Definition at line 4468 of file std_expr.h.
|
inline |
Definition at line 1451 of file std_expr.h.
|
inline |
Definition at line 1503 of file std_expr.h.
|
inline |
Definition at line 1396 of file std_expr.h.
|
inline |
Definition at line 662 of file std_expr.h.
|
inline |
Definition at line 758 of file std_expr.h.
|
inline |
Definition at line 2469 of file std_expr.h.
|
inline |
Definition at line 2352 of file std_expr.h.
|
inline |
Definition at line 2397 of file std_expr.h.
|
inline |
Definition at line 2433 of file std_expr.h.
|
inline |
Definition at line 497 of file std_expr.h.
|
inline |
Definition at line 4608 of file std_expr.h.
|
inline |
Definition at line 1705 of file std_expr.h.
|
inline |
Definition at line 1794 of file std_expr.h.
|
inline |
Definition at line 1749 of file std_expr.h.
|
inline |
Definition at line 4084 of file std_expr.h.
|
inline |
Definition at line 4379 of file std_expr.h.
|
inline |
Definition at line 3928 of file std_expr.h.
|
inline |
Definition at line 2928 of file std_expr.h.
|
inline |
Definition at line 1064 of file std_expr.h.
|
inline |
Definition at line 1947 of file std_expr.h.
|
inline |
Definition at line 1214 of file std_expr.h.
|
inline |
Definition at line 2661 of file std_expr.h.
|
inline |
Definition at line 2750 of file std_expr.h.
|
inline |
Definition at line 2100 of file std_expr.h.
|
inline |
Definition at line 3701 of file std_expr.h.
|
inline |
Definition at line 3750 of file std_expr.h.
|
inline |
Definition at line 3833 of file std_expr.h.
|
inline |
Definition at line 3013 of file std_expr.h.
|
inline |
Definition at line 2209 of file std_expr.h.
|
inline |
Definition at line 3149 of file std_expr.h.
|
inline |
Definition at line 1331 of file std_expr.h.
|
inline |
Definition at line 3608 of file std_expr.h.
|
inline |
Definition at line 3563 of file std_expr.h.
|
inline |
Definition at line 3518 of file std_expr.h.
|
inline |
Definition at line 3653 of file std_expr.h.
|
inline |
Definition at line 4273 of file std_expr.h.
|
inline |
Definition at line 3198 of file std_expr.h.
|
inline |
Definition at line 3473 of file std_expr.h.
|
inline |
Definition at line 949 of file std_expr.h.
|
inline |
Definition at line 1109 of file std_expr.h.
|
inline |
Definition at line 995 of file std_expr.h.
|
inline |
Definition at line 3982 of file std_expr.h.
|
inline |
Definition at line 232 of file std_expr.h.
|
inline |
Definition at line 2852 of file std_expr.h.
|
inline |
Definition at line 1257 of file std_expr.h.
|
inline |
Definition at line 1882 of file std_expr.h.
|
inline |
Definition at line 2281 of file std_expr.h.
|
inline |
Definition at line 904 of file std_expr.h.
|
inline |
Definition at line 4322 of file std_expr.h.
|
inline |
Definition at line 1154 of file std_expr.h.
|
inline |
Definition at line 4028 of file std_expr.h.
|
inline |
Definition at line 2527 of file std_expr.h.
|
inline |
Definition at line 566 of file std_expr.h.
|
inline |
Definition at line 1645 of file std_expr.h.
|
inline |
Definition at line 161 of file std_expr.h.
|
inline |
Definition at line 3878 of file std_expr.h.
|
inline |
Definition at line 2031 of file std_expr.h.
|
inline |
Definition at line 300 of file std_expr.h.
|
inline |
Definition at line 392 of file std_expr.h.
|
inline |
Definition at line 436 of file std_expr.h.
|
inline |
Definition at line 1597 of file std_expr.h.
|
inline |
Definition at line 3282 of file std_expr.h.
|
inline |
Definition at line 1540 of file std_expr.h.
|
inline |
Definition at line 3092 of file std_expr.h.
|
inline |
Definition at line 2317 of file std_expr.h.
exprt conjunction | ( | const exprt::operandst & | ) |
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise
Definition at line 51 of file std_expr.cpp.
exprt disjunction | ( | const exprt::operandst & | ) |
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise
Definition at line 29 of file std_expr.cpp.
Cast an exprt to a abs_exprt.
expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 358 of file std_expr.h.
Cast an exprt to a abs_exprt.
expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 367 of file std_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 2823 of file std_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 2832 of file std_expr.h.
Cast an exprt to a and_exprt.
expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2184 of file std_expr.h.
Cast an exprt to a and_exprt.
expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2191 of file std_expr.h.
|
inline |
Cast an exprt to a array_comprehension_exprt.
expr must be known to be array_comprehension_exprt.
expr | Source expression |
Definition at line 4485 of file std_expr.h.
|
inline |
Cast an exprt to a array_comprehension_exprt.
expr must be known to be array_comprehension_exprt.
expr | Source expression |
Definition at line 4495 of file std_expr.h.
|
inline |
Cast an exprt to an array_exprt.
expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1462 of file std_expr.h.
|
inline |
Cast an exprt to an array_exprt.
expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1469 of file std_expr.h.
|
inline |
Definition at line 1513 of file std_expr.h.
|
inline |
Definition at line 1521 of file std_expr.h.
|
inline |
Cast an exprt to an array_of_exprt.
expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1412 of file std_expr.h.
|
inline |
Cast an exprt to an array_of_exprt.
expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1421 of file std_expr.h.
|
inline |
Cast an exprt to a binary_exprt.
expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 678 of file std_expr.h.
|
inline |
Cast an exprt to a binary_exprt.
expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 685 of file std_expr.h.
|
inline |
Cast an exprt to a binary_relation_exprt.
expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 774 of file std_expr.h.
|
inline |
Cast an exprt to a binary_relation_exprt.
expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 781 of file std_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2480 of file std_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2487 of file std_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2368 of file std_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2377 of file std_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2408 of file std_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2415 of file std_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2444 of file std_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2451 of file std_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 515 of file std_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 524 of file std_expr.h.
|
inline |
Cast an exprt to a class_method_descriptor_exprt.
expr must be known to be class_method_descriptor_exprt.
expr | Source expression |
Definition at line 4598 of file std_expr.h.
|
inline |
Cast an exprt to a complex_exprt.
expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1721 of file std_expr.h.
|
inline |
Cast an exprt to a complex_exprt.
expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1730 of file std_expr.h.
|
inline |
Cast an exprt to a complex_imag_exprt.
expr must be known to be a complex_imag_exprt.
expr | Source expression |
Definition at line 1811 of file std_expr.h.
|
inline |
Cast an exprt to a complex_imag_exprt.
expr must be known to be a complex_imag_exprt.
expr | Source expression |
Definition at line 1820 of file std_expr.h.
|
inline |
Cast an exprt to a complex_real_exprt.
expr must be known to be a complex_real_exprt.
expr | Source expression |
Definition at line 1766 of file std_expr.h.
|
inline |
Cast an exprt to a complex_real_exprt.
expr must be known to be a complex_real_exprt.
expr | Source expression |
Definition at line 1775 of file std_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4095 of file std_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4102 of file std_expr.h.
|
inline |
Cast an exprt to a cond_exprt.
expr must be known to be cond_exprt.
expr | Source expression |
Definition at line 4396 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4405 of file std_expr.h.
|
inline |
Cast an exprt to a constant_exprt.
expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 3939 of file std_expr.h.
|
inline |
Cast an exprt to a constant_exprt.
expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 3946 of file std_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 2944 of file std_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 2953 of file std_expr.h.
Cast an exprt to a div_exprt.
expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1080 of file std_expr.h.
Cast an exprt to a div_exprt.
expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1089 of file std_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 1963 of file std_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 1974 of file std_expr.h.
|
inline |
Cast an exprt to an equal_exprt.
expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1230 of file std_expr.h.
|
inline |
Cast an exprt to an equal_exprt.
expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1238 of file std_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 2677 of file std_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 2686 of file std_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 2766 of file std_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 2775 of file std_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2116 of file std_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2126 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 3717 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 3727 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 3766 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 3777 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 3851 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 3860 of file std_expr.h.
Cast an exprt to an if_exprt.
expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3029 of file std_expr.h.
Cast an exprt to an if_exprt.
expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3038 of file std_expr.h.
|
inline |
Cast an exprt to a implies_exprt.
expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2225 of file std_expr.h.
|
inline |
Cast an exprt to a implies_exprt.
expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2234 of file std_expr.h.
|
inline |
Cast an exprt to an index_designatort.
expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3165 of file std_expr.h.
|
inline |
Cast an exprt to an index_designatort.
expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3174 of file std_expr.h.
|
inline |
Cast an exprt to an index_exprt.
expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1347 of file std_expr.h.
|
inline |
Cast an exprt to an index_exprt.
expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1356 of file std_expr.h.
|
inline |
Definition at line 1993 of file std_expr.h.
|
inline |
Definition at line 2003 of file std_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 3624 of file std_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 3633 of file std_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 3579 of file std_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 3588 of file std_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 3534 of file std_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 3543 of file std_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 3669 of file std_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 3678 of file std_expr.h.
Cast an exprt to a let_exprt.
expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4289 of file std_expr.h.
Cast an exprt to a let_exprt.
expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4298 of file std_expr.h.
|
inline |
Cast an exprt to an member_designatort.
expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3214 of file std_expr.h.
|
inline |
Cast an exprt to an member_designatort.
expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3223 of file std_expr.h.
|
inline |
Cast an exprt to a member_exprt.
expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3489 of file std_expr.h.
|
inline |
Cast an exprt to a member_exprt.
expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3498 of file std_expr.h.
|
inline |
Cast an exprt to a minus_exprt.
expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 965 of file std_expr.h.
|
inline |
Cast an exprt to a minus_exprt.
expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 974 of file std_expr.h.
Cast an exprt to a mod_exprt.
expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1125 of file std_expr.h.
Cast an exprt to a mod_exprt.
expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1134 of file std_expr.h.
|
inline |
Cast an exprt to a mult_exprt.
expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1011 of file std_expr.h.
|
inline |
Cast an exprt to a mult_exprt.
expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1020 of file std_expr.h.
|
inline |
Cast an exprt to a multi_ary_exprt.
expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 866 of file std_expr.h.
|
inline |
Cast an exprt to a multi_ary_exprt.
expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 872 of file std_expr.h.
|
inline |
Cast an exprt to a nondet_symbol_exprt.
expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 248 of file std_expr.h.
|
inline |
Cast an exprt to a nondet_symbol_exprt.
expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 258 of file std_expr.h.
Cast an exprt to an not_exprt.
expr must be known to be not_exprt.
expr | Source expression |
Definition at line 2868 of file std_expr.h.
Cast an exprt to an not_exprt.
expr must be known to be not_exprt.
expr | Source expression |
Definition at line 2877 of file std_expr.h.
|
inline |
Cast an exprt to an notequal_exprt.
expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1273 of file std_expr.h.
|
inline |
Cast an exprt to an notequal_exprt.
expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1282 of file std_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 1898 of file std_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 1909 of file std_expr.h.
Cast an exprt to a or_exprt.
expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2292 of file std_expr.h.
Cast an exprt to a or_exprt.
expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2299 of file std_expr.h.
|
inline |
Cast an exprt to a plus_exprt.
expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 920 of file std_expr.h.
|
inline |
Cast an exprt to a plus_exprt.
expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 929 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4338 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4347 of file std_expr.h.
Cast an exprt to a rem_exprt.
expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1170 of file std_expr.h.
Cast an exprt to a rem_exprt.
expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1179 of file std_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 4044 of file std_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 4053 of file std_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2543 of file std_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2551 of file std_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 2580 of file std_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 2589 of file std_expr.h.
|
inline |
Cast an exprt to a sign_exprt.
expr must be known to be a sign_exprt.
expr | Source expression |
Definition at line 582 of file std_expr.h.
|
inline |
Cast an exprt to a sign_exprt.
expr must be known to be a sign_exprt.
expr | Source expression |
Definition at line 591 of file std_expr.h.
|
inline |
Cast an exprt to a struct_exprt.
expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1656 of file std_expr.h.
|
inline |
Cast an exprt to a struct_exprt.
expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1663 of file std_expr.h.
|
inline |
Cast an exprt to a symbol_exprt.
expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 177 of file std_expr.h.
|
inline |
Cast an exprt to a symbol_exprt.
expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 186 of file std_expr.h.
|
inline |
Cast an exprt to an type_exprt.
expr must be known to be type_exprt.
expr | Source expression |
Definition at line 3889 of file std_expr.h.
|
inline |
Cast an exprt to an type_exprt.
expr must be known to be type_exprt.
expr | Source expression |
Definition at line 3897 of file std_expr.h.
|
inline |
Cast an exprt to a typecast_exprt.
expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2047 of file std_expr.h.
|
inline |
Cast an exprt to a typecast_exprt.
expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2056 of file std_expr.h.
|
inline |
Cast an exprt to a unary_exprt.
expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 316 of file std_expr.h.
|
inline |
Cast an exprt to a unary_exprt.
expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 324 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 408 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 417 of file std_expr.h.
|
inline |
Cast an exprt to a unary_plus_exprt.
expr must be known to be unary_plus_exprt.
expr | Source expression |
Definition at line 452 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 461 of file std_expr.h.
|
inline |
Cast an exprt to a union_exprt.
expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1613 of file std_expr.h.
|
inline |
Cast an exprt to a union_exprt.
expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1622 of file std_expr.h.
|
inline |
Cast an exprt to an update_exprt.
expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3299 of file std_expr.h.
|
inline |
Cast an exprt to an update_exprt.
expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3308 of file std_expr.h.
|
inline |
Cast an exprt to an vector_exprt.
expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1551 of file std_expr.h.
|
inline |
Cast an exprt to an vector_exprt.
expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1558 of file std_expr.h.
|
inline |
Cast an exprt to a with_exprt.
expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3112 of file std_expr.h.
|
inline |
Cast an exprt to a with_exprt.
expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3121 of file std_expr.h.
Cast an exprt to a xor_exprt.
expr must be known to be xor_exprt.
expr | Source expression |
Definition at line 2328 of file std_expr.h.
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2335 of file std_expr.h.
|
inline |
Definition at line 347 of file std_expr.h.
|
inline |
Definition at line 2812 of file std_expr.h.
|
inline |
Definition at line 4473 of file std_expr.h.
|
inline |
Definition at line 1508 of file std_expr.h.
|
inline |
Definition at line 1401 of file std_expr.h.
|
inline |
Definition at line 667 of file std_expr.h.
|
inline |
Definition at line 763 of file std_expr.h.
|
inline |
Definition at line 2357 of file std_expr.h.
|
inline |
Definition at line 502 of file std_expr.h.
|
inline |
Definition at line 4574 of file std_expr.h.
|
inline |
Definition at line 1710 of file std_expr.h.
|
inline |
Definition at line 1799 of file std_expr.h.
|
inline |
Definition at line 1754 of file std_expr.h.
|
inline |
Definition at line 4384 of file std_expr.h.
|
inline |
Definition at line 2933 of file std_expr.h.
|
inline |
Definition at line 1069 of file std_expr.h.
|
inline |
Definition at line 1952 of file std_expr.h.
|
inline |
Definition at line 1219 of file std_expr.h.
|
inline |
Definition at line 2666 of file std_expr.h.
|
inline |
Definition at line 2755 of file std_expr.h.
|
inline |
Definition at line 2105 of file std_expr.h.
|
inline |
Definition at line 3706 of file std_expr.h.
|
inline |
Definition at line 3755 of file std_expr.h.
|
inline |
Definition at line 3839 of file std_expr.h.
|
inline |
Definition at line 3018 of file std_expr.h.
|
inline |
Definition at line 2214 of file std_expr.h.
|
inline |
Definition at line 3154 of file std_expr.h.
|
inline |
Definition at line 1336 of file std_expr.h.
|
inline |
Definition at line 3613 of file std_expr.h.
|
inline |
Definition at line 3568 of file std_expr.h.
|
inline |
Definition at line 3523 of file std_expr.h.
|
inline |
Definition at line 3658 of file std_expr.h.
|
inline |
Definition at line 4278 of file std_expr.h.
|
inline |
Definition at line 3203 of file std_expr.h.
|
inline |
Definition at line 3478 of file std_expr.h.
|
inline |
Definition at line 954 of file std_expr.h.
|
inline |
Definition at line 1114 of file std_expr.h.
|
inline |
Definition at line 1000 of file std_expr.h.
|
inline |
Definition at line 237 of file std_expr.h.
|
inline |
Definition at line 2857 of file std_expr.h.
|
inline |
Definition at line 1262 of file std_expr.h.
|
inline |
Definition at line 1887 of file std_expr.h.
|
inline |
Definition at line 909 of file std_expr.h.
|
inline |
Definition at line 4327 of file std_expr.h.
|
inline |
Definition at line 1159 of file std_expr.h.
|
inline |
Definition at line 4033 of file std_expr.h.
|
inline |
Definition at line 2532 of file std_expr.h.
|
inline |
Definition at line 571 of file std_expr.h.
|
inline |
Definition at line 166 of file std_expr.h.
|
inline |
Definition at line 2036 of file std_expr.h.
|
inline |
Definition at line 305 of file std_expr.h.
|
inline |
Definition at line 397 of file std_expr.h.
|
inline |
Definition at line 441 of file std_expr.h.
|
inline |
Definition at line 1602 of file std_expr.h.
|
inline |
Definition at line 3287 of file std_expr.h.
|
inline |
Definition at line 3097 of file std_expr.h.