cprover
|
API to expression classes. More...
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... | |
struct | std::hash<::symbol_exprt > |
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 | 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 | typecast_exprt |
Semantic type conversion. 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 | not_exprt |
Boolean negation. 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 | 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 | 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 | 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 354 of file std_expr.h.
|
inline |
Definition at line 1870 of file std_expr.h.
|
inline |
Definition at line 3059 of file std_expr.h.
|
inline |
Definition at line 1400 of file std_expr.h.
|
inline |
Definition at line 1452 of file std_expr.h.
|
inline |
Definition at line 1345 of file std_expr.h.
|
inline |
Definition at line 611 of file std_expr.h.
|
inline |
Definition at line 707 of file std_expr.h.
|
inline |
Definition at line 3199 of file std_expr.h.
|
inline |
Definition at line 1654 of file std_expr.h.
|
inline |
Definition at line 1743 of file std_expr.h.
|
inline |
Definition at line 1698 of file std_expr.h.
|
inline |
Definition at line 2970 of file std_expr.h.
|
inline |
Definition at line 2689 of file std_expr.h.
|
inline |
Definition at line 1013 of file std_expr.h.
|
inline |
Definition at line 1163 of file std_expr.h.
|
inline |
Definition at line 2135 of file std_expr.h.
|
inline |
Definition at line 1906 of file std_expr.h.
|
inline |
Definition at line 2271 of file std_expr.h.
|
inline |
Definition at line 1280 of file std_expr.h.
|
inline |
Definition at line 2912 of file std_expr.h.
|
inline |
Definition at line 2320 of file std_expr.h.
|
inline |
Definition at line 2595 of file std_expr.h.
|
inline |
Definition at line 898 of file std_expr.h.
|
inline |
Definition at line 1058 of file std_expr.h.
|
inline |
Definition at line 944 of file std_expr.h.
|
inline |
Definition at line 2743 of file std_expr.h.
|
inline |
Definition at line 244 of file std_expr.h.
|
inline |
Definition at line 2050 of file std_expr.h.
|
inline |
Definition at line 1206 of file std_expr.h.
|
inline |
Definition at line 1978 of file std_expr.h.
|
inline |
Definition at line 853 of file std_expr.h.
|
inline |
Definition at line 1103 of file std_expr.h.
|
inline |
Definition at line 515 of file std_expr.h.
|
inline |
Definition at line 1594 of file std_expr.h.
|
inline |
Definition at line 173 of file std_expr.h.
|
inline |
Definition at line 2639 of file std_expr.h.
|
inline |
Definition at line 1798 of file std_expr.h.
|
inline |
Definition at line 312 of file std_expr.h.
|
inline |
Definition at line 404 of file std_expr.h.
|
inline |
Definition at line 448 of file std_expr.h.
|
inline |
Definition at line 1546 of file std_expr.h.
|
inline |
Definition at line 2404 of file std_expr.h.
|
inline |
Definition at line 1489 of file std_expr.h.
|
inline |
Definition at line 2214 of file std_expr.h.
|
inline |
Definition at line 2014 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 41 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 370 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 379 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 1881 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 1888 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 3076 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 3086 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 1411 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 1418 of file std_expr.h.
|
inline |
Definition at line 1462 of file std_expr.h.
|
inline |
Definition at line 1470 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 1361 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 1370 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 627 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 634 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 723 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 730 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 3189 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 1670 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 1679 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 1760 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 1769 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 1715 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 1724 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 2987 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 2996 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 2700 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 2707 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 1029 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 1038 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 1179 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 1187 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 2151 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 2160 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 1922 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 1931 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 2287 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 2296 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 1296 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 1305 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 2928 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 2937 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 2336 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 2345 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 2611 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 2620 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 914 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 923 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 1074 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 1083 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 960 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 969 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 815 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 821 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 260 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 270 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 2066 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 2075 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 1222 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 1231 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 1989 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 1996 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 869 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 878 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 1119 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 1128 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 531 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 540 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 1605 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 1612 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 189 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 198 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 2650 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 2658 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 1814 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 1823 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 328 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 336 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 420 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 429 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 464 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 473 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 1562 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 1571 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 2421 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 2430 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 1500 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 1507 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 2234 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 2243 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 2025 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 2032 of file std_expr.h.
|
inline |
Definition at line 359 of file std_expr.h.
|
inline |
Definition at line 3064 of file std_expr.h.
|
inline |
Definition at line 1457 of file std_expr.h.
|
inline |
Definition at line 1350 of file std_expr.h.
|
inline |
Definition at line 616 of file std_expr.h.
|
inline |
Definition at line 712 of file std_expr.h.
|
inline |
Definition at line 3165 of file std_expr.h.
|
inline |
Definition at line 1659 of file std_expr.h.
|
inline |
Definition at line 1748 of file std_expr.h.
|
inline |
Definition at line 1703 of file std_expr.h.
|
inline |
Definition at line 2975 of file std_expr.h.
|
inline |
Definition at line 1018 of file std_expr.h.
|
inline |
Definition at line 1168 of file std_expr.h.
|
inline |
Definition at line 2140 of file std_expr.h.
|
inline |
Definition at line 1911 of file std_expr.h.
|
inline |
Definition at line 2276 of file std_expr.h.
|
inline |
Definition at line 1285 of file std_expr.h.
|
inline |
Definition at line 2917 of file std_expr.h.
|
inline |
Definition at line 2325 of file std_expr.h.
|
inline |
Definition at line 2600 of file std_expr.h.
|
inline |
Definition at line 903 of file std_expr.h.
|
inline |
Definition at line 1063 of file std_expr.h.
|
inline |
Definition at line 949 of file std_expr.h.
|
inline |
Definition at line 249 of file std_expr.h.
|
inline |
Definition at line 2055 of file std_expr.h.
|
inline |
Definition at line 1211 of file std_expr.h.
|
inline |
Definition at line 858 of file std_expr.h.
|
inline |
Definition at line 1108 of file std_expr.h.
|
inline |
Definition at line 520 of file std_expr.h.
|
inline |
Definition at line 178 of file std_expr.h.
|
inline |
Definition at line 1803 of file std_expr.h.
|
inline |
Definition at line 317 of file std_expr.h.
|
inline |
Definition at line 409 of file std_expr.h.
|
inline |
Definition at line 453 of file std_expr.h.
|
inline |
Definition at line 1551 of file std_expr.h.
|
inline |
Definition at line 2409 of file std_expr.h.
|
inline |
Definition at line 2219 of file std_expr.h.