cprover
|
API to expression classes. More...
Go to the source code of this file.
Classes | |
class | transt |
A transition system, consisting of state invariant, initial state predicate, and transition predicate. More... | |
class | symbol_exprt |
Expression to hold a symbol (variable) More... | |
class | decorated_symbol_exprt |
Expression to hold a symbol (variable) 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 | predicate_exprt |
A generic base class for expressions that are predicates, i.e., boolean-typed. More... | |
class | unary_predicate_exprt |
A generic 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 More... | |
class | binary_exprt |
A generic base class for binary expressions. More... | |
class | binary_predicate_exprt |
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments. More... | |
class | binary_relation_exprt |
A generic base class for relations, i.e., binary predicates. More... | |
class | multi_ary_exprt |
A generic base class for multi-ary expressions. More... | |
class | plus_exprt |
The plus expression. More... | |
class | minus_exprt |
binary minus More... | |
class | mult_exprt |
binary multiplication More... | |
class | div_exprt |
division (integer and real) More... | |
class | mod_exprt |
binary modulo More... | |
class | rem_exprt |
remainder of division More... | |
class | power_exprt |
exponentiation More... | |
class | factorial_power_exprt |
falling factorial power More... | |
class | equal_exprt |
equality More... | |
class | notequal_exprt |
inequality 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 | 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 | object_descriptor_exprt |
split an expression into a base object and a (byte) offset More... | |
class | dynamic_object_exprt |
TO_BE_DOCUMENTED. 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 | 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 | replication_exprt |
Bit-vector replication. 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. 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 | function_application_exprt |
application of (mathematical) function More... | |
class | concatenation_exprt |
Concatenation of bit-vector operands. More... | |
class | infinity_exprt |
An expression denoting infinity. More... | |
class | let_exprt |
A let expression. More... | |
class | forall_exprt |
A forall expression. More... | |
class | exists_exprt |
An exists expression. More... | |
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 50 of file std_expr.cpp.
References exprt::operands().
Referenced by bmc_all_propertiest::goalt::as_expr(), path_symext::assign_rec(), partial_order_concurrencyt::before(), collect_mcdc_controlling_rec(), acceleration_utilst::do_arrays(), instantiate_quantifier(), instrument_intervals(), interval_domaint::make_expression(), bmc_covert::operator()(), operator-=(), operator|=(), and replacement_conjunction().
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 26 of file std_expr.cpp.
References exprt::operands().
Referenced by bmc_covert::goalt::as_expr(), cover_goalst::constraint(), symex_target_equationt::convert_assertions(), character_refine_preprocesst::expr_of_is_defined(), character_refine_preprocesst::expr_of_is_title_case(), character_refine_preprocesst::expr_of_is_unicode_identifier_part(), character_refine_preprocesst::expr_of_is_whitespace(), character_refine_preprocesst::in_list_expr(), instantiate_quantifier(), remove_instanceoft::lower_instanceof(), and goto_checkt::pointer_validity_check().