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 | null_pointer_exprt |
The null pointer constant. 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 355 of file std_expr.h.
|
inline |
Definition at line 1871 of file std_expr.h.
|
inline |
Definition at line 3071 of file std_expr.h.
|
inline |
Definition at line 1401 of file std_expr.h.
|
inline |
Definition at line 1453 of file std_expr.h.
|
inline |
Definition at line 1346 of file std_expr.h.
|
inline |
Definition at line 612 of file std_expr.h.
|
inline |
Definition at line 708 of file std_expr.h.
|
inline |
Definition at line 3211 of file std_expr.h.
|
inline |
Definition at line 1655 of file std_expr.h.
|
inline |
Definition at line 1744 of file std_expr.h.
|
inline |
Definition at line 1699 of file std_expr.h.
|
inline |
Definition at line 2982 of file std_expr.h.
|
inline |
Definition at line 2690 of file std_expr.h.
|
inline |
Definition at line 1014 of file std_expr.h.
|
inline |
Definition at line 1164 of file std_expr.h.
|
inline |
Definition at line 2136 of file std_expr.h.
|
inline |
Definition at line 1907 of file std_expr.h.
|
inline |
Definition at line 2272 of file std_expr.h.
|
inline |
Definition at line 1281 of file std_expr.h.
|
inline |
Definition at line 2924 of file std_expr.h.
|
inline |
Definition at line 2321 of file std_expr.h.
|
inline |
Definition at line 2596 of file std_expr.h.
|
inline |
Definition at line 899 of file std_expr.h.
|
inline |
Definition at line 1059 of file std_expr.h.
|
inline |
Definition at line 945 of file std_expr.h.
|
inline |
Definition at line 2744 of file std_expr.h.
|
inline |
Definition at line 245 of file std_expr.h.
|
inline |
Definition at line 2051 of file std_expr.h.
|
inline |
Definition at line 1207 of file std_expr.h.
|
inline |
Definition at line 1979 of file std_expr.h.
|
inline |
Definition at line 854 of file std_expr.h.
|
inline |
Definition at line 1104 of file std_expr.h.
|
inline |
Definition at line 516 of file std_expr.h.
|
inline |
Definition at line 1595 of file std_expr.h.
|
inline |
Definition at line 174 of file std_expr.h.
|
inline |
Definition at line 2640 of file std_expr.h.
|
inline |
Definition at line 1799 of file std_expr.h.
|
inline |
Definition at line 313 of file std_expr.h.
|
inline |
Definition at line 405 of file std_expr.h.
|
inline |
Definition at line 449 of file std_expr.h.
|
inline |
Definition at line 1547 of file std_expr.h.
|
inline |
Definition at line 2405 of file std_expr.h.
|
inline |
Definition at line 1490 of file std_expr.h.
|
inline |
Definition at line 2215 of file std_expr.h.
|
inline |
Definition at line 2015 of file std_expr.h.
exprt conjunction | ( | const exprt::operandst & | op | ) |
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 & | op | ) |
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 371 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 380 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 1882 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 1889 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 3088 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 3098 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 1412 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 1419 of file std_expr.h.
|
inline |
Definition at line 1463 of file std_expr.h.
|
inline |
Definition at line 1471 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 1362 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 1371 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 628 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 635 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 724 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 731 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 3201 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 1671 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 1680 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 1761 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 1770 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 1716 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 1725 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 2999 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 3008 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 2701 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 2708 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 1030 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 1039 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 1180 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 1188 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 2152 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 2161 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 1923 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 1932 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 2288 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 2297 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 1297 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 1306 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 2940 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 2949 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 2337 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 2346 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 2612 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 2621 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 915 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 924 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 1075 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 1084 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 961 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 970 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 816 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 822 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 261 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 271 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 2067 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 2076 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 1223 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 1232 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 1990 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 1997 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 870 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 879 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 1120 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 1129 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 532 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 541 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 1606 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 1613 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 190 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 199 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 2651 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 2659 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 1815 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 1824 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 329 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 337 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 421 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 430 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 465 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 474 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 1563 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 1572 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 2422 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 2431 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 1501 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 1508 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 2235 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 2244 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 2026 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 2033 of file std_expr.h.
|
inline |
Definition at line 360 of file std_expr.h.
|
inline |
Definition at line 3076 of file std_expr.h.
|
inline |
Definition at line 1458 of file std_expr.h.
|
inline |
Definition at line 1351 of file std_expr.h.
|
inline |
Definition at line 617 of file std_expr.h.
|
inline |
Definition at line 713 of file std_expr.h.
|
inline |
Definition at line 3177 of file std_expr.h.
|
inline |
Definition at line 1660 of file std_expr.h.
|
inline |
Definition at line 1749 of file std_expr.h.
|
inline |
Definition at line 1704 of file std_expr.h.
|
inline |
Definition at line 2987 of file std_expr.h.
|
inline |
Definition at line 1019 of file std_expr.h.
|
inline |
Definition at line 1169 of file std_expr.h.
|
inline |
Definition at line 2141 of file std_expr.h.
|
inline |
Definition at line 1912 of file std_expr.h.
|
inline |
Definition at line 2277 of file std_expr.h.
|
inline |
Definition at line 1286 of file std_expr.h.
|
inline |
Definition at line 2929 of file std_expr.h.
|
inline |
Definition at line 2326 of file std_expr.h.
|
inline |
Definition at line 2601 of file std_expr.h.
|
inline |
Definition at line 904 of file std_expr.h.
|
inline |
Definition at line 1064 of file std_expr.h.
|
inline |
Definition at line 950 of file std_expr.h.
|
inline |
Definition at line 250 of file std_expr.h.
|
inline |
Definition at line 2056 of file std_expr.h.
|
inline |
Definition at line 1212 of file std_expr.h.
|
inline |
Definition at line 859 of file std_expr.h.
|
inline |
Definition at line 1109 of file std_expr.h.
|
inline |
Definition at line 521 of file std_expr.h.
|
inline |
Definition at line 179 of file std_expr.h.
|
inline |
Definition at line 1804 of file std_expr.h.
|
inline |
Definition at line 318 of file std_expr.h.
|
inline |
Definition at line 410 of file std_expr.h.
|
inline |
Definition at line 454 of file std_expr.h.
|
inline |
Definition at line 1552 of file std_expr.h.
|
inline |
Definition at line 2410 of file std_expr.h.
|
inline |
Definition at line 2220 of file std_expr.h.