cprover
std_expr.h File Reference

API to expression classes. More...

#include "base_type.h"
#include "expr_cast.h"
#include "invariant.h"
#include "mathematical_types.h"
#include "std_types.h"
+ Include dependency graph for std_expr.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  transt
 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) 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. 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  power_exprt
 Exponentiation. More...
 
class  factorial_power_exprt
 Falling factorial power. 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  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  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 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  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  quantifier_exprt
 A base class for quantifier expressions. More...
 
class  forall_exprt
 A forall expression. More...
 
class  exists_exprt
 An exists 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...
 

Functions

const transtto_trans_expr (const exprt &expr)
 Cast an exprt to a transt expr must be known to be transt. More...
 
transtto_trans_expr (exprt &expr)
 Cast an exprt to a transt expr must be known to be transt. More...
 
template<>
bool can_cast_expr< transt > (const exprt &base)
 
void validate_expr (const transt &value)
 
const symbol_exprtto_symbol_expr (const exprt &expr)
 Cast an exprt to a symbol_exprt. More...
 
symbol_exprtto_symbol_expr (exprt &expr)
 Cast an exprt to a symbol_exprt. More...
 
template<>
bool can_cast_expr< symbol_exprt > (const exprt &base)
 
void validate_expr (const symbol_exprt &value)
 
const nondet_symbol_exprtto_nondet_symbol_expr (const exprt &expr)
 Cast an exprt to a nondet_symbol_exprt. More...
 
nondet_symbol_exprtto_nondet_symbol_expr (exprt &expr)
 Cast an exprt to a nondet_symbol_exprt. More...
 
template<>
bool can_cast_expr< nondet_symbol_exprt > (const exprt &base)
 
void validate_expr (const nondet_symbol_exprt &value)
 
const unary_exprtto_unary_expr (const exprt &expr)
 Cast an exprt to a unary_exprt. More...
 
unary_exprtto_unary_expr (exprt &expr)
 Cast an exprt to a unary_exprt. More...
 
template<>
bool can_cast_expr< unary_exprt > (const exprt &base)
 
const abs_exprtto_abs_expr (const exprt &expr)
 Cast an exprt to a abs_exprt. More...
 
abs_exprtto_abs_expr (exprt &expr)
 Cast an exprt to a abs_exprt. More...
 
template<>
bool can_cast_expr< abs_exprt > (const exprt &base)
 
void validate_expr (const abs_exprt &value)
 
const unary_minus_exprtto_unary_minus_expr (const exprt &expr)
 Cast an exprt to a unary_minus_exprt. More...
 
unary_minus_exprtto_unary_minus_expr (exprt &expr)
 Cast an exprt to a unary_minus_exprt. More...
 
template<>
bool can_cast_expr< unary_minus_exprt > (const exprt &base)
 
void validate_expr (const unary_minus_exprt &value)
 
const unary_plus_exprtto_unary_plus_expr (const exprt &expr)
 Cast an exprt to a unary_plus_exprt. More...
 
unary_plus_exprtto_unary_plus_expr (exprt &expr)
 Cast an exprt to a unary_minus_exprt. More...
 
template<>
bool can_cast_expr< unary_plus_exprt > (const exprt &base)
 
void validate_expr (const unary_plus_exprt &value)
 
const bswap_exprtto_bswap_expr (const exprt &expr)
 Cast an exprt to a bswap_exprt. More...
 
bswap_exprtto_bswap_expr (exprt &expr)
 Cast an exprt to a bswap_exprt. More...
 
template<>
bool can_cast_expr< bswap_exprt > (const exprt &base)
 
void validate_expr (const bswap_exprt &value)
 
const sign_exprtto_sign_expr (const exprt &expr)
 Cast an exprt to a sign_exprt. More...
 
sign_exprtto_sign_expr (exprt &expr)
 Cast an exprt to a sign_exprt. More...
 
template<>
bool can_cast_expr< sign_exprt > (const exprt &base)
 
void validate_expr (const sign_exprt &expr)
 
const binary_exprtto_binary_expr (const exprt &expr)
 Cast an exprt to a binary_exprt. More...
 
binary_exprtto_binary_expr (exprt &expr)
 Cast an exprt to a binary_exprt. More...
 
template<>
bool can_cast_expr< binary_exprt > (const exprt &base)
 
const binary_relation_exprtto_binary_relation_expr (const exprt &expr)
 Cast an exprt to a binary_relation_exprt. More...
 
binary_relation_exprtto_binary_relation_expr (exprt &expr)
 Cast an exprt to a binary_relation_exprt. More...
 
template<>
bool can_cast_expr< binary_relation_exprt > (const exprt &base)
 
const multi_ary_exprtto_multi_ary_expr (const exprt &expr)
 Cast an exprt to a multi_ary_exprt. More...
 
multi_ary_exprtto_multi_ary_expr (exprt &expr)
 Cast an exprt to a multi_ary_exprt. More...
 
const plus_exprtto_plus_expr (const exprt &expr)
 Cast an exprt to a plus_exprt. More...
 
plus_exprtto_plus_expr (exprt &expr)
 Cast an exprt to a plus_exprt. More...
 
template<>
bool can_cast_expr< plus_exprt > (const exprt &base)
 
void validate_expr (const plus_exprt &value)
 
const minus_exprtto_minus_expr (const exprt &expr)
 Cast an exprt to a minus_exprt. More...
 
minus_exprtto_minus_expr (exprt &expr)
 Cast an exprt to a minus_exprt. More...
 
template<>
bool can_cast_expr< minus_exprt > (const exprt &base)
 
void validate_expr (const minus_exprt &value)
 
const mult_exprtto_mult_expr (const exprt &expr)
 Cast an exprt to a mult_exprt. More...
 
mult_exprtto_mult_expr (exprt &expr)
 Cast an exprt to a mult_exprt. More...
 
template<>
bool can_cast_expr< mult_exprt > (const exprt &base)
 
void validate_expr (const mult_exprt &value)
 
const div_exprtto_div_expr (const exprt &expr)
 Cast an exprt to a div_exprt. More...
 
div_exprtto_div_expr (exprt &expr)
 Cast an exprt to a div_exprt. More...
 
template<>
bool can_cast_expr< div_exprt > (const exprt &base)
 
void validate_expr (const div_exprt &value)
 
const mod_exprtto_mod_expr (const exprt &expr)
 Cast an exprt to a mod_exprt. More...
 
mod_exprtto_mod_expr (exprt &expr)
 Cast an exprt to a mod_exprt. More...
 
template<>
bool can_cast_expr< mod_exprt > (const exprt &base)
 
void validate_expr (const mod_exprt &value)
 
const rem_exprtto_rem_expr (const exprt &expr)
 Cast an exprt to a rem_exprt. More...
 
rem_exprtto_rem_expr (exprt &expr)
 Cast an exprt to a rem_exprt. More...
 
template<>
bool can_cast_expr< rem_exprt > (const exprt &base)
 
void validate_expr (const rem_exprt &value)
 
const power_exprtto_power_expr (const exprt &expr)
 Cast an exprt to a power_exprt. More...
 
power_exprtto_power_expr (exprt &expr)
 Cast an exprt to a power_exprt. More...
 
template<>
bool can_cast_expr< power_exprt > (const exprt &base)
 
void validate_expr (const power_exprt &value)
 
const factorial_power_exprtto_factorial_power_expr (const exprt &expr)
 Cast an exprt to a factorial_power_exprt. More...
 
factorial_power_exprtto_factorial_expr (exprt &expr)
 Cast an exprt to a factorial_power_exprt. More...
 
template<>
bool can_cast_expr< factorial_power_exprt > (const exprt &base)
 
void validate_expr (const factorial_power_exprt &value)
 
const equal_exprtto_equal_expr (const exprt &expr)
 Cast an exprt to an equal_exprt. More...
 
equal_exprtto_equal_expr (exprt &expr)
 Cast an exprt to an equal_exprt. More...
 
template<>
bool can_cast_expr< equal_exprt > (const exprt &base)
 
void validate_expr (const equal_exprt &value)
 
const notequal_exprtto_notequal_expr (const exprt &expr)
 Cast an exprt to an notequal_exprt. More...
 
notequal_exprtto_notequal_expr (exprt &expr)
 Cast an exprt to an notequal_exprt. More...
 
template<>
bool can_cast_expr< notequal_exprt > (const exprt &base)
 
void validate_expr (const notequal_exprt &value)
 
const index_exprtto_index_expr (const exprt &expr)
 Cast an exprt to an index_exprt. More...
 
index_exprtto_index_expr (exprt &expr)
 Cast an exprt to an index_exprt. More...
 
template<>
bool can_cast_expr< index_exprt > (const exprt &base)
 
void validate_expr (const index_exprt &value)
 
const array_of_exprtto_array_of_expr (const exprt &expr)
 Cast an exprt to an array_of_exprt. More...
 
array_of_exprtto_array_of_expr (exprt &expr)
 Cast an exprt to an array_of_exprt. More...
 
template<>
bool can_cast_expr< array_of_exprt > (const exprt &base)
 
void validate_expr (const array_of_exprt &value)
 
const array_exprtto_array_expr (const exprt &expr)
 Cast an exprt to an array_exprt. More...
 
array_exprtto_array_expr (exprt &expr)
 Cast an exprt to an array_exprt. More...
 
template<>
bool can_cast_expr< array_exprt > (const exprt &base)
 
template<>
bool can_cast_expr< array_list_exprt > (const exprt &base)
 
void validate_expr (const array_list_exprt &value)
 
const vector_exprtto_vector_expr (const exprt &expr)
 Cast an exprt to an vector_exprt. More...
 
vector_exprtto_vector_expr (exprt &expr)
 Cast an exprt to an vector_exprt. More...
 
template<>
bool can_cast_expr< vector_exprt > (const exprt &base)
 
const union_exprtto_union_expr (const exprt &expr)
 Cast an exprt to a union_exprt. More...
 
union_exprtto_union_expr (exprt &expr)
 Cast an exprt to a union_exprt. More...
 
template<>
bool can_cast_expr< union_exprt > (const exprt &base)
 
void validate_expr (const union_exprt &value)
 
const struct_exprtto_struct_expr (const exprt &expr)
 Cast an exprt to a struct_exprt. More...
 
struct_exprtto_struct_expr (exprt &expr)
 Cast an exprt to a struct_exprt. More...
 
template<>
bool can_cast_expr< struct_exprt > (const exprt &base)
 
const complex_exprtto_complex_expr (const exprt &expr)
 Cast an exprt to a complex_exprt. More...
 
complex_exprtto_complex_expr (exprt &expr)
 Cast an exprt to a complex_exprt. More...
 
template<>
bool can_cast_expr< complex_exprt > (const exprt &base)
 
void validate_expr (const complex_exprt &value)
 
const complex_real_exprtto_complex_real_expr (const exprt &expr)
 Cast an exprt to a complex_real_exprt. More...
 
complex_real_exprtto_complex_real_expr (exprt &expr)
 Cast an exprt to a complex_real_exprt. More...
 
template<>
bool can_cast_expr< complex_real_exprt > (const exprt &base)
 
void validate_expr (const complex_real_exprt &expr)
 
const complex_imag_exprtto_complex_imag_expr (const exprt &expr)
 Cast an exprt to a complex_imag_exprt. More...
 
complex_imag_exprtto_complex_imag_expr (exprt &expr)
 Cast an exprt to a complex_imag_exprt. More...
 
template<>
bool can_cast_expr< complex_imag_exprt > (const exprt &base)
 
void validate_expr (const complex_imag_exprt &expr)
 
const object_descriptor_exprtto_object_descriptor_expr (const exprt &expr)
 Cast an exprt to an object_descriptor_exprt. More...
 
object_descriptor_exprtto_object_descriptor_expr (exprt &expr)
 Cast an exprt to an object_descriptor_exprt. More...
 
template<>
bool can_cast_expr< object_descriptor_exprt > (const exprt &base)
 
void validate_expr (const object_descriptor_exprt &value)
 
const dynamic_object_exprtto_dynamic_object_expr (const exprt &expr)
 Cast an exprt to a dynamic_object_exprt. More...
 
dynamic_object_exprtto_dynamic_object_expr (exprt &expr)
 Cast an exprt to a dynamic_object_exprt. More...
 
template<>
bool can_cast_expr< dynamic_object_exprt > (const exprt &base)
 
void validate_expr (const dynamic_object_exprt &value)
 
const typecast_exprtto_typecast_expr (const exprt &expr)
 Cast an exprt to a typecast_exprt. More...
 
typecast_exprtto_typecast_expr (exprt &expr)
 Cast an exprt to a typecast_exprt. More...
 
template<>
bool can_cast_expr< typecast_exprt > (const exprt &base)
 
void validate_expr (const typecast_exprt &value)
 
const floatbv_typecast_exprtto_floatbv_typecast_expr (const exprt &expr)
 Cast an exprt to a floatbv_typecast_exprt. More...
 
floatbv_typecast_exprtto_floatbv_typecast_expr (exprt &expr)
 Cast an exprt to a floatbv_typecast_exprt. More...
 
template<>
bool can_cast_expr< floatbv_typecast_exprt > (const exprt &base)
 
void validate_expr (const floatbv_typecast_exprt &value)
 
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 More...
 
const and_exprtto_and_expr (const exprt &expr)
 Cast an exprt to a and_exprt. More...
 
and_exprtto_and_expr (exprt &expr)
 Cast an exprt to a and_exprt. More...
 
template<>
bool can_cast_expr< and_exprt > (const exprt &base)
 
const implies_exprtto_implies_expr (const exprt &expr)
 Cast an exprt to a implies_exprt. More...
 
implies_exprtto_implies_expr (exprt &expr)
 Cast an exprt to a implies_exprt. More...
 
template<>
bool can_cast_expr< implies_exprt > (const exprt &base)
 
void validate_expr (const implies_exprt &value)
 
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 More...
 
const or_exprtto_or_expr (const exprt &expr)
 Cast an exprt to a or_exprt. More...
 
or_exprtto_or_expr (exprt &expr)
 Cast an exprt to a or_exprt. More...
 
template<>
bool can_cast_expr< or_exprt > (const exprt &base)
 
const xor_exprtto_xor_expr (const exprt &expr)
 Cast an exprt to a xor_exprt. More...
 
xor_exprtto_xor_expr (exprt &expr)
 Cast an exprt to a bitxor_exprt. More...
 
template<>
bool can_cast_expr< xor_exprt > (const exprt &base)
 
const bitnot_exprtto_bitnot_expr (const exprt &expr)
 Cast an exprt to a bitnot_exprt. More...
 
bitnot_exprtto_bitnot_expr (exprt &expr)
 Cast an exprt to a bitnot_exprt. More...
 
template<>
bool can_cast_expr< bitnot_exprt > (const exprt &base)
 
const bitor_exprtto_bitor_expr (const exprt &expr)
 Cast an exprt to a bitor_exprt. More...
 
bitor_exprtto_bitor_expr (exprt &expr)
 Cast an exprt to a bitor_exprt. More...
 
template<>
bool can_cast_expr< bitor_exprt > (const exprt &base)
 
const bitxor_exprtto_bitxor_expr (const exprt &expr)
 Cast an exprt to a bitxor_exprt. More...
 
bitxor_exprtto_bitxor_expr (exprt &expr)
 Cast an exprt to a bitxor_exprt. More...
 
template<>
bool can_cast_expr< bitxor_exprt > (const exprt &base)
 
const bitand_exprtto_bitand_expr (const exprt &expr)
 Cast an exprt to a bitand_exprt. More...
 
bitand_exprtto_bitand_expr (exprt &expr)
 Cast an exprt to a bitand_exprt. More...
 
template<>
bool can_cast_expr< bitand_exprt > (const exprt &base)
 
const shift_exprtto_shift_expr (const exprt &expr)
 Cast an exprt to a shift_exprt. More...
 
shift_exprtto_shift_expr (exprt &expr)
 Cast an exprt to a shift_exprt. More...
 
const shl_exprtto_shl_expr (const exprt &expr)
 Cast an exprt to a shl_exprt. More...
 
shl_exprtto_shl_expr (exprt &expr)
 Cast an exprt to a shl_exprt. More...
 
const replication_exprtto_replication_expr (const exprt &expr)
 Cast an exprt to a replication_exprt. More...
 
replication_exprtto_replication_expr (exprt &expr)
 Cast an exprt to a replication_exprt. More...
 
template<>
bool can_cast_expr< replication_exprt > (const exprt &base)
 
void validate_expr (const replication_exprt &value)
 
const extractbit_exprtto_extractbit_expr (const exprt &expr)
 Cast an exprt to an extractbit_exprt. More...
 
extractbit_exprtto_extractbit_expr (exprt &expr)
 Cast an exprt to an extractbit_exprt. More...
 
template<>
bool can_cast_expr< extractbit_exprt > (const exprt &base)
 
void validate_expr (const extractbit_exprt &value)
 
const extractbits_exprtto_extractbits_expr (const exprt &expr)
 Cast an exprt to an extractbits_exprt. More...
 
extractbits_exprtto_extractbits_expr (exprt &expr)
 Cast an exprt to an extractbits_exprt. More...
 
template<>
bool can_cast_expr< extractbits_exprt > (const exprt &base)
 
void validate_expr (const extractbits_exprt &value)
 
const address_of_exprtto_address_of_expr (const exprt &expr)
 Cast an exprt to an address_of_exprt. More...
 
address_of_exprtto_address_of_expr (exprt &expr)
 Cast an exprt to an address_of_exprt. More...
 
template<>
bool can_cast_expr< address_of_exprt > (const exprt &base)
 
void validate_expr (const address_of_exprt &value)
 
const not_exprtto_not_expr (const exprt &expr)
 Cast an exprt to an not_exprt. More...
 
not_exprtto_not_expr (exprt &expr)
 Cast an exprt to an not_exprt. More...
 
template<>
bool can_cast_expr< not_exprt > (const exprt &base)
 
void validate_expr (const not_exprt &value)
 
const dereference_exprtto_dereference_expr (const exprt &expr)
 Cast an exprt to a dereference_exprt. More...
 
dereference_exprtto_dereference_expr (exprt &expr)
 Cast an exprt to a dereference_exprt. More...
 
template<>
bool can_cast_expr< dereference_exprt > (const exprt &base)
 
void validate_expr (const dereference_exprt &value)
 
const if_exprtto_if_expr (const exprt &expr)
 Cast an exprt to an if_exprt. More...
 
if_exprtto_if_expr (exprt &expr)
 Cast an exprt to an if_exprt. More...
 
template<>
bool can_cast_expr< if_exprt > (const exprt &base)
 
void validate_expr (const if_exprt &value)
 
const with_exprtto_with_expr (const exprt &expr)
 Cast an exprt to a with_exprt. More...
 
with_exprtto_with_expr (exprt &expr)
 Cast an exprt to a with_exprt. More...
 
template<>
bool can_cast_expr< with_exprt > (const exprt &base)
 
void validate_expr (const with_exprt &value)
 
const index_designatortto_index_designator (const exprt &expr)
 Cast an exprt to an index_designatort. More...
 
index_designatortto_index_designator (exprt &expr)
 Cast an exprt to an index_designatort. More...
 
template<>
bool can_cast_expr< index_designatort > (const exprt &base)
 
void validate_expr (const index_designatort &value)
 
const member_designatortto_member_designator (const exprt &expr)
 Cast an exprt to an member_designatort. More...
 
member_designatortto_member_designator (exprt &expr)
 Cast an exprt to an member_designatort. More...
 
template<>
bool can_cast_expr< member_designatort > (const exprt &base)
 
void validate_expr (const member_designatort &value)
 
const update_exprtto_update_expr (const exprt &expr)
 Cast an exprt to an update_exprt. More...
 
update_exprtto_update_expr (exprt &expr)
 Cast an exprt to an update_exprt. More...
 
template<>
bool can_cast_expr< update_exprt > (const exprt &base)
 
void validate_expr (const update_exprt &value)
 
const member_exprtto_member_expr (const exprt &expr)
 Cast an exprt to a member_exprt. More...
 
member_exprtto_member_expr (exprt &expr)
 Cast an exprt to a member_exprt. More...
 
template<>
bool can_cast_expr< member_exprt > (const exprt &base)
 
void validate_expr (const member_exprt &value)
 
const isnan_exprtto_isnan_expr (const exprt &expr)
 Cast an exprt to a isnan_exprt. More...
 
isnan_exprtto_isnan_expr (exprt &expr)
 Cast an exprt to a isnan_exprt. More...
 
template<>
bool can_cast_expr< isnan_exprt > (const exprt &base)
 
void validate_expr (const isnan_exprt &value)
 
const isinf_exprtto_isinf_expr (const exprt &expr)
 Cast an exprt to a isinf_exprt. More...
 
isinf_exprtto_isinf_expr (exprt &expr)
 Cast an exprt to a isinf_exprt. More...
 
template<>
bool can_cast_expr< isinf_exprt > (const exprt &base)
 
void validate_expr (const isinf_exprt &value)
 
const isfinite_exprtto_isfinite_expr (const exprt &expr)
 Cast an exprt to a isfinite_exprt. More...
 
isfinite_exprtto_isfinite_expr (exprt &expr)
 Cast an exprt to a isfinite_exprt. More...
 
template<>
bool can_cast_expr< isfinite_exprt > (const exprt &base)
 
void validate_expr (const isfinite_exprt &value)
 
const isnormal_exprtto_isnormal_expr (const exprt &expr)
 Cast an exprt to a isnormal_exprt. More...
 
isnormal_exprtto_isnormal_expr (exprt &expr)
 Cast an exprt to a isnormal_exprt. More...
 
template<>
bool can_cast_expr< isnormal_exprt > (const exprt &base)
 
void validate_expr (const isnormal_exprt &value)
 
const ieee_float_equal_exprtto_ieee_float_equal_expr (const exprt &expr)
 Cast an exprt to an ieee_float_equal_exprt. More...
 
ieee_float_equal_exprtto_ieee_float_equal_expr (exprt &expr)
 Cast an exprt to an ieee_float_equal_exprt. More...
 
template<>
bool can_cast_expr< ieee_float_equal_exprt > (const exprt &base)
 
void validate_expr (const ieee_float_equal_exprt &value)
 
const ieee_float_notequal_exprtto_ieee_float_notequal_expr (const exprt &expr)
 Cast an exprt to an ieee_float_notequal_exprt. More...
 
ieee_float_notequal_exprtto_ieee_float_notequal_expr (exprt &expr)
 Cast an exprt to an ieee_float_notequal_exprt. More...
 
template<>
bool can_cast_expr< ieee_float_notequal_exprt > (const exprt &base)
 
void validate_expr (const ieee_float_notequal_exprt &value)
 
const ieee_float_op_exprtto_ieee_float_op_expr (const exprt &expr)
 Cast an exprt to an ieee_float_op_exprt. More...
 
ieee_float_op_exprtto_ieee_float_op_expr (exprt &expr)
 Cast an exprt to an ieee_float_op_exprt. More...
 
const constant_exprtto_constant_expr (const exprt &expr)
 Cast an exprt to a constant_exprt. More...
 
constant_exprtto_constant_expr (exprt &expr)
 Cast an exprt to a constant_exprt. More...
 
template<>
bool can_cast_expr< constant_exprt > (const exprt &base)
 
const function_application_exprtto_function_application_expr (const exprt &expr)
 Cast an exprt to a function_application_exprt. More...
 
function_application_exprtto_function_application_expr (exprt &expr)
 Cast an exprt to a function_application_exprt. More...
 
template<>
bool can_cast_expr< function_application_exprt > (const exprt &base)
 
void validate_expr (const function_application_exprt &value)
 
const concatenation_exprtto_concatenation_expr (const exprt &expr)
 Cast an exprt to a concatenation_exprt. More...
 
concatenation_exprtto_concatenation_expr (exprt &expr)
 Cast an exprt to a concatenation_exprt. More...
 
template<>
bool can_cast_expr< concatenation_exprt > (const exprt &base)
 
const let_exprtto_let_expr (const exprt &expr)
 Cast an exprt to a let_exprt. More...
 
let_exprtto_let_expr (exprt &expr)
 Cast an exprt to a let_exprt. More...
 
template<>
bool can_cast_expr< let_exprt > (const exprt &base)
 
void validate_expr (const let_exprt &value)
 
const quantifier_exprtto_quantifier_expr (const exprt &expr)
 Cast an exprt to a quantifier_exprt. More...
 
quantifier_exprtto_quantifier_expr (exprt &expr)
 Cast an exprt to a quantifier_exprt. More...
 
template<>
bool can_cast_expr< quantifier_exprt > (const exprt &base)
 
void validate_expr (const quantifier_exprt &value)
 
const exists_exprtto_exists_expr (const exprt &expr)
 
exists_exprtto_exists_expr (exprt &expr)
 
const popcount_exprtto_popcount_expr (const exprt &expr)
 Cast an exprt to a popcount_exprt. More...
 
popcount_exprtto_popcount_expr (exprt &expr)
 Cast an exprt to a popcount_exprt. More...
 
template<>
bool can_cast_expr< popcount_exprt > (const exprt &base)
 
void validate_expr (const popcount_exprt &value)
 
const cond_exprtto_cond_expr (const exprt &expr)
 Cast an exprt to a cond_exprt. More...
 
cond_exprtto_cond_expr (exprt &expr)
 Cast an exprt to a popcount_exprt. More...
 

Detailed Description

API to expression classes.

Definition in file std_expr.h.

Function Documentation

◆ can_cast_expr< abs_exprt >()

template<>
bool can_cast_expr< abs_exprt > ( const exprt base)
inline

Definition at line 469 of file std_expr.h.

◆ can_cast_expr< address_of_exprt >()

template<>
bool can_cast_expr< address_of_exprt > ( const exprt base)
inline

Definition at line 3352 of file std_expr.h.

◆ can_cast_expr< and_exprt >()

template<>
bool can_cast_expr< and_exprt > ( const exprt base)
inline

Definition at line 2508 of file std_expr.h.

◆ can_cast_expr< array_exprt >()

template<>
bool can_cast_expr< array_exprt > ( const exprt base)
inline

Definition at line 1789 of file std_expr.h.

◆ can_cast_expr< array_list_exprt >()

template<>
bool can_cast_expr< array_list_exprt > ( const exprt base)
inline

Definition at line 1812 of file std_expr.h.

◆ can_cast_expr< array_of_exprt >()

template<>
bool can_cast_expr< array_of_exprt > ( const exprt base)
inline

Definition at line 1744 of file std_expr.h.

◆ can_cast_expr< binary_exprt >()

template<>
bool can_cast_expr< binary_exprt > ( const exprt base)
inline

Definition at line 838 of file std_expr.h.

◆ can_cast_expr< binary_relation_exprt >()

template<>
bool can_cast_expr< binary_relation_exprt > ( const exprt base)
inline

Definition at line 975 of file std_expr.h.

◆ can_cast_expr< bitand_exprt >()

template<>
bool can_cast_expr< bitand_exprt > ( const exprt base)
inline

Definition at line 2883 of file std_expr.h.

◆ can_cast_expr< bitnot_exprt >()

template<>
bool can_cast_expr< bitnot_exprt > ( const exprt base)
inline

Definition at line 2725 of file std_expr.h.

◆ can_cast_expr< bitor_exprt >()

template<>
bool can_cast_expr< bitor_exprt > ( const exprt base)
inline

Definition at line 2775 of file std_expr.h.

◆ can_cast_expr< bitxor_exprt >()

template<>
bool can_cast_expr< bitxor_exprt > ( const exprt base)
inline

Definition at line 2829 of file std_expr.h.

◆ can_cast_expr< bswap_exprt >()

template<>
bool can_cast_expr< bswap_exprt > ( const exprt base)
inline

Definition at line 631 of file std_expr.h.

◆ can_cast_expr< complex_exprt >()

template<>
bool can_cast_expr< complex_exprt > ( const exprt base)
inline

Definition at line 2065 of file std_expr.h.

◆ can_cast_expr< complex_imag_exprt >()

template<>
bool can_cast_expr< complex_imag_exprt > ( const exprt base)
inline

Definition at line 2157 of file std_expr.h.

◆ can_cast_expr< complex_real_exprt >()

template<>
bool can_cast_expr< complex_real_exprt > ( const exprt base)
inline

Definition at line 2110 of file std_expr.h.

◆ can_cast_expr< concatenation_exprt >()

template<>
bool can_cast_expr< concatenation_exprt > ( const exprt base)
inline

Definition at line 4662 of file std_expr.h.

◆ can_cast_expr< constant_exprt >()

template<>
bool can_cast_expr< constant_exprt > ( const exprt base)
inline

Definition at line 4491 of file std_expr.h.

◆ can_cast_expr< dereference_exprt >()

template<>
bool can_cast_expr< dereference_exprt > ( const exprt base)
inline

Definition at line 3472 of file std_expr.h.

◆ can_cast_expr< div_exprt >()

template<>
bool can_cast_expr< div_exprt > ( const exprt base)
inline

Definition at line 1292 of file std_expr.h.

◆ can_cast_expr< dynamic_object_exprt >()

template<>
bool can_cast_expr< dynamic_object_exprt > ( const exprt base)
inline

Definition at line 2300 of file std_expr.h.

◆ can_cast_expr< equal_exprt >()

template<>
bool can_cast_expr< equal_exprt > ( const exprt base)
inline

Definition at line 1550 of file std_expr.h.

◆ can_cast_expr< extractbit_exprt >()

template<>
bool can_cast_expr< extractbit_exprt > ( const exprt base)
inline

Definition at line 3201 of file std_expr.h.

◆ can_cast_expr< extractbits_exprt >()

template<>
bool can_cast_expr< extractbits_exprt > ( const exprt base)
inline

Definition at line 3299 of file std_expr.h.

◆ can_cast_expr< factorial_power_exprt >()

template<>
bool can_cast_expr< factorial_power_exprt > ( const exprt base)
inline

Definition at line 1488 of file std_expr.h.

◆ can_cast_expr< floatbv_typecast_exprt >()

template<>
bool can_cast_expr< floatbv_typecast_exprt > ( const exprt base)
inline

Definition at line 2433 of file std_expr.h.

◆ can_cast_expr< function_application_exprt >()

template<>
bool can_cast_expr< function_application_exprt > ( const exprt base)
inline

Definition at line 4598 of file std_expr.h.

◆ can_cast_expr< ieee_float_equal_exprt >()

template<>
bool can_cast_expr< ieee_float_equal_exprt > ( const exprt base)
inline

Definition at line 4272 of file std_expr.h.

◆ can_cast_expr< ieee_float_notequal_exprt >()

template<>
bool can_cast_expr< ieee_float_notequal_exprt > ( const exprt base)
inline

Definition at line 4325 of file std_expr.h.

◆ can_cast_expr< if_exprt >()

template<>
bool can_cast_expr< if_exprt > ( const exprt base)
inline

Definition at line 3557 of file std_expr.h.

◆ can_cast_expr< implies_exprt >()

template<>
bool can_cast_expr< implies_exprt > ( const exprt base)
inline

Definition at line 2554 of file std_expr.h.

◆ can_cast_expr< index_designatort >()

template<>
bool can_cast_expr< index_designatort > ( const exprt base)
inline

Definition at line 3701 of file std_expr.h.

◆ can_cast_expr< index_exprt >()

template<>
bool can_cast_expr< index_exprt > ( const exprt base)
inline

Definition at line 1683 of file std_expr.h.

◆ can_cast_expr< isfinite_exprt >()

template<>
bool can_cast_expr< isfinite_exprt > ( const exprt base)
inline

Definition at line 4175 of file std_expr.h.

◆ can_cast_expr< isinf_exprt >()

template<>
bool can_cast_expr< isinf_exprt > ( const exprt base)
inline

Definition at line 4129 of file std_expr.h.

◆ can_cast_expr< isnan_exprt >()

template<>
bool can_cast_expr< isnan_exprt > ( const exprt base)
inline

Definition at line 4079 of file std_expr.h.

◆ can_cast_expr< isnormal_exprt >()

template<>
bool can_cast_expr< isnormal_exprt > ( const exprt base)
inline

Definition at line 4221 of file std_expr.h.

◆ can_cast_expr< let_exprt >()

template<>
bool can_cast_expr< let_exprt > ( const exprt base)
inline

Definition at line 4752 of file std_expr.h.

◆ can_cast_expr< member_designatort >()

template<>
bool can_cast_expr< member_designatort > ( const exprt base)
inline

Definition at line 3751 of file std_expr.h.

◆ can_cast_expr< member_exprt >()

template<>
bool can_cast_expr< member_exprt > ( const exprt base)
inline

Definition at line 4033 of file std_expr.h.

◆ can_cast_expr< minus_exprt >()

template<>
bool can_cast_expr< minus_exprt > ( const exprt base)
inline

Definition at line 1163 of file std_expr.h.

◆ can_cast_expr< mod_exprt >()

template<>
bool can_cast_expr< mod_exprt > ( const exprt base)
inline

Definition at line 1340 of file std_expr.h.

◆ can_cast_expr< mult_exprt >()

template<>
bool can_cast_expr< mult_exprt > ( const exprt base)
inline

Definition at line 1216 of file std_expr.h.

◆ can_cast_expr< nondet_symbol_exprt >()

template<>
bool can_cast_expr< nondet_symbol_exprt > ( const exprt base)
inline

Definition at line 331 of file std_expr.h.

◆ can_cast_expr< not_exprt >()

template<>
bool can_cast_expr< not_exprt > ( const exprt base)
inline

Definition at line 3399 of file std_expr.h.

◆ can_cast_expr< notequal_exprt >()

template<>
bool can_cast_expr< notequal_exprt > ( const exprt base)
inline

Definition at line 1600 of file std_expr.h.

◆ can_cast_expr< object_descriptor_exprt >()

template<>
bool can_cast_expr< object_descriptor_exprt > ( const exprt base)
inline

Definition at line 2231 of file std_expr.h.

◆ can_cast_expr< or_exprt >()

template<>
bool can_cast_expr< or_exprt > ( const exprt base)
inline

Definition at line 2629 of file std_expr.h.

◆ can_cast_expr< plus_exprt >()

template<>
bool can_cast_expr< plus_exprt > ( const exprt base)
inline

Definition at line 1111 of file std_expr.h.

◆ can_cast_expr< popcount_exprt >()

template<>
bool can_cast_expr< popcount_exprt > ( const exprt base)
inline

Definition at line 4910 of file std_expr.h.

◆ can_cast_expr< power_exprt >()

template<>
bool can_cast_expr< power_exprt > ( const exprt base)
inline

Definition at line 1436 of file std_expr.h.

◆ can_cast_expr< quantifier_exprt >()

template<>
bool can_cast_expr< quantifier_exprt > ( const exprt base)
inline

Definition at line 4819 of file std_expr.h.

◆ can_cast_expr< rem_exprt >()

template<>
bool can_cast_expr< rem_exprt > ( const exprt base)
inline

Definition at line 1388 of file std_expr.h.

◆ can_cast_expr< replication_exprt >()

template<>
bool can_cast_expr< replication_exprt > ( const exprt base)
inline

Definition at line 3124 of file std_expr.h.

◆ can_cast_expr< sign_exprt >()

template<>
bool can_cast_expr< sign_exprt > ( const exprt base)
inline

Definition at line 739 of file std_expr.h.

◆ can_cast_expr< struct_exprt >()

template<>
bool can_cast_expr< struct_exprt > ( const exprt base)
inline

Definition at line 1990 of file std_expr.h.

◆ can_cast_expr< symbol_exprt >()

template<>
bool can_cast_expr< symbol_exprt > ( const exprt base)
inline

Definition at line 277 of file std_expr.h.

◆ can_cast_expr< transt >()

template<>
bool can_cast_expr< transt > ( const exprt base)
inline

Definition at line 143 of file std_expr.h.

◆ can_cast_expr< typecast_exprt >()

template<>
bool can_cast_expr< typecast_exprt > ( const exprt base)
inline

Definition at line 2360 of file std_expr.h.

◆ can_cast_expr< unary_exprt >()

template<>
bool can_cast_expr< unary_exprt > ( const exprt base)
inline

Definition at line 423 of file std_expr.h.

◆ can_cast_expr< unary_minus_exprt >()

template<>
bool can_cast_expr< unary_minus_exprt > ( const exprt base)
inline

Definition at line 526 of file std_expr.h.

◆ can_cast_expr< unary_plus_exprt >()

template<>
bool can_cast_expr< unary_plus_exprt > ( const exprt base)
inline

Definition at line 569 of file std_expr.h.

◆ can_cast_expr< union_exprt >()

template<>
bool can_cast_expr< union_exprt > ( const exprt base)
inline

Definition at line 1938 of file std_expr.h.

◆ can_cast_expr< update_exprt >()

template<>
bool can_cast_expr< update_exprt > ( const exprt base)
inline

Definition at line 3844 of file std_expr.h.

◆ can_cast_expr< vector_exprt >()

template<>
bool can_cast_expr< vector_exprt > ( const exprt base)
inline

Definition at line 1862 of file std_expr.h.

◆ can_cast_expr< with_exprt >()

template<>
bool can_cast_expr< with_exprt > ( const exprt base)
inline

Definition at line 3643 of file std_expr.h.

◆ can_cast_expr< xor_exprt >()

template<>
bool can_cast_expr< xor_exprt > ( const exprt base)
inline

Definition at line 2673 of file std_expr.h.

◆ conjunction()

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 48 of file std_expr.cpp.

◆ disjunction()

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.

◆ to_abs_expr() [1/2]

const abs_exprt& to_abs_expr ( const exprt expr)
inline

Cast an exprt to a abs_exprt.

expr must be known to be abs_exprt.

Parameters
exprSource expression
Returns
Object of type abs_exprt

Definition at line 450 of file std_expr.h.

◆ to_abs_expr() [2/2]

abs_exprt& to_abs_expr ( exprt expr)
inline

Cast an exprt to a abs_exprt.

expr must be known to be abs_exprt.

Parameters
exprSource expression
Returns
Object of type abs_exprt

Definition at line 460 of file std_expr.h.

◆ to_address_of_expr() [1/2]

const address_of_exprt& to_address_of_expr ( const exprt expr)
inline

Cast an exprt to an address_of_exprt.

expr must be known to be address_of_exprt.

Parameters
exprSource expression
Returns
Object of type address_of_exprt

Definition at line 3337 of file std_expr.h.

◆ to_address_of_expr() [2/2]

address_of_exprt& to_address_of_expr ( exprt expr)
inline

Cast an exprt to an address_of_exprt.

expr must be known to be address_of_exprt.

Parameters
exprSource expression
Returns
Object of type address_of_exprt

Definition at line 3345 of file std_expr.h.

◆ to_and_expr() [1/2]

const and_exprt& to_and_expr ( const exprt expr)
inline

Cast an exprt to a and_exprt.

expr must be known to be and_exprt.

Parameters
exprSource expression
Returns
Object of type and_exprt

Definition at line 2489 of file std_expr.h.

◆ to_and_expr() [2/2]

and_exprt& to_and_expr ( exprt expr)
inline

Cast an exprt to a and_exprt.

expr must be known to be and_exprt.

Parameters
exprSource expression
Returns
Object of type and_exprt

Definition at line 2499 of file std_expr.h.

◆ to_array_expr() [1/2]

const array_exprt& to_array_expr ( const exprt expr)
inline

Cast an exprt to an array_exprt.

expr must be known to be array_exprt.

Parameters
exprSource expression
Returns
Object of type array_exprt

Definition at line 1776 of file std_expr.h.

◆ to_array_expr() [2/2]

array_exprt& to_array_expr ( exprt expr)
inline

Cast an exprt to an array_exprt.

expr must be known to be array_exprt.

Parameters
exprSource expression
Returns
Object of type array_exprt

Definition at line 1783 of file std_expr.h.

◆ to_array_of_expr() [1/2]

const array_of_exprt& to_array_of_expr ( const exprt expr)
inline

Cast an exprt to an array_of_exprt.

expr must be known to be array_of_exprt.

Parameters
exprSource expression
Returns
Object of type array_of_exprt

Definition at line 1725 of file std_expr.h.

◆ to_array_of_expr() [2/2]

array_of_exprt& to_array_of_expr ( exprt expr)
inline

Cast an exprt to an array_of_exprt.

expr must be known to be array_of_exprt.

Parameters
exprSource expression
Returns
Object of type array_of_exprt

Definition at line 1735 of file std_expr.h.

◆ to_binary_expr() [1/2]

const binary_exprt& to_binary_expr ( const exprt expr)
inline

Cast an exprt to a binary_exprt.

expr must be known to be binary_exprt.

Parameters
exprSource expression
Returns
Object of type binary_exprt

Definition at line 821 of file std_expr.h.

◆ to_binary_expr() [2/2]

binary_exprt& to_binary_expr ( exprt expr)
inline

Cast an exprt to a binary_exprt.

expr must be known to be binary_exprt.

Parameters
exprSource expression
Returns
Object of type binary_exprt

Definition at line 830 of file std_expr.h.

◆ to_binary_relation_expr() [1/2]

const binary_relation_exprt& to_binary_relation_expr ( const exprt expr)
inline

Cast an exprt to a binary_relation_exprt.

expr must be known to be binary_relation_exprt.

Parameters
exprSource expression
Returns
Object of type binary_relation_exprt

Definition at line 958 of file std_expr.h.

◆ to_binary_relation_expr() [2/2]

binary_relation_exprt& to_binary_relation_expr ( exprt expr)
inline

Cast an exprt to a binary_relation_exprt.

expr must be known to be binary_relation_exprt.

Parameters
exprSource expression
Returns
Object of type binary_relation_exprt

Definition at line 967 of file std_expr.h.

◆ to_bitand_expr() [1/2]

const bitand_exprt& to_bitand_expr ( const exprt expr)
inline

Cast an exprt to a bitand_exprt.

expr must be known to be bitand_exprt.

Parameters
exprSource expression
Returns
Object of type bitand_exprt

Definition at line 2864 of file std_expr.h.

◆ to_bitand_expr() [2/2]

bitand_exprt& to_bitand_expr ( exprt expr)
inline

Cast an exprt to a bitand_exprt.

expr must be known to be bitand_exprt.

Parameters
exprSource expression
Returns
Object of type bitand_exprt

Definition at line 2874 of file std_expr.h.

◆ to_bitnot_expr() [1/2]

const bitnot_exprt& to_bitnot_expr ( const exprt expr)
inline

Cast an exprt to a bitnot_exprt.

expr must be known to be bitnot_exprt.

Parameters
exprSource expression
Returns
Object of type bitnot_exprt

Definition at line 2708 of file std_expr.h.

◆ to_bitnot_expr() [2/2]

bitnot_exprt& to_bitnot_expr ( exprt expr)
inline

Cast an exprt to a bitnot_exprt.

expr must be known to be bitnot_exprt.

Parameters
exprSource expression
Returns
Object of type bitnot_exprt

Definition at line 2717 of file std_expr.h.

◆ to_bitor_expr() [1/2]

const bitor_exprt& to_bitor_expr ( const exprt expr)
inline

Cast an exprt to a bitor_exprt.

expr must be known to be bitor_exprt.

Parameters
exprSource expression
Returns
Object of type bitor_exprt

Definition at line 2756 of file std_expr.h.

◆ to_bitor_expr() [2/2]

bitor_exprt& to_bitor_expr ( exprt expr)
inline

Cast an exprt to a bitor_exprt.

expr must be known to be bitor_exprt.

Parameters
exprSource expression
Returns
Object of type bitor_exprt

Definition at line 2766 of file std_expr.h.

◆ to_bitxor_expr() [1/2]

const bitxor_exprt& to_bitxor_expr ( const exprt expr)
inline

Cast an exprt to a bitxor_exprt.

expr must be known to be bitxor_exprt.

Parameters
exprSource expression
Returns
Object of type bitxor_exprt

Definition at line 2810 of file std_expr.h.

◆ to_bitxor_expr() [2/2]

bitxor_exprt& to_bitxor_expr ( exprt expr)
inline

Cast an exprt to a bitxor_exprt.

expr must be known to be bitxor_exprt.

Parameters
exprSource expression
Returns
Object of type bitxor_exprt

Definition at line 2820 of file std_expr.h.

◆ to_bswap_expr() [1/2]

const bswap_exprt& to_bswap_expr ( const exprt expr)
inline

Cast an exprt to a bswap_exprt.

expr must be known to be bswap_exprt.

Parameters
exprSource expression
Returns
Object of type bswap_exprt

Definition at line 611 of file std_expr.h.

◆ to_bswap_expr() [2/2]

bswap_exprt& to_bswap_expr ( exprt expr)
inline

Cast an exprt to a bswap_exprt.

expr must be known to be bswap_exprt.

Parameters
exprSource expression
Returns
Object of type bswap_exprt

Definition at line 621 of file std_expr.h.

◆ to_complex_expr() [1/2]

const complex_exprt& to_complex_expr ( const exprt expr)
inline

Cast an exprt to a complex_exprt.

expr must be known to be complex_exprt.

Parameters
exprSource expression
Returns
Object of type complex_exprt

Definition at line 2046 of file std_expr.h.

◆ to_complex_expr() [2/2]

complex_exprt& to_complex_expr ( exprt expr)
inline

Cast an exprt to a complex_exprt.

expr must be known to be complex_exprt.

Parameters
exprSource expression
Returns
Object of type complex_exprt

Definition at line 2056 of file std_expr.h.

◆ to_complex_imag_expr() [1/2]

const complex_imag_exprt& to_complex_imag_expr ( const exprt expr)
inline

Cast an exprt to a complex_imag_exprt.

expr must be known to be a complex_imag_exprt.

Parameters
exprSource expression
Returns
Object of type complex_imag_exprt

Definition at line 2137 of file std_expr.h.

◆ to_complex_imag_expr() [2/2]

complex_imag_exprt& to_complex_imag_expr ( exprt expr)
inline

Cast an exprt to a complex_imag_exprt.

expr must be known to be a complex_imag_exprt.

Parameters
exprSource expression
Returns
Object of type complex_imag_exprt

Definition at line 2147 of file std_expr.h.

◆ to_complex_real_expr() [1/2]

const complex_real_exprt& to_complex_real_expr ( const exprt expr)
inline

Cast an exprt to a complex_real_exprt.

expr must be known to be a complex_real_exprt.

Parameters
exprSource expression
Returns
Object of type complex_real_exprt

Definition at line 2090 of file std_expr.h.

◆ to_complex_real_expr() [2/2]

complex_real_exprt& to_complex_real_expr ( exprt expr)
inline

Cast an exprt to a complex_real_exprt.

expr must be known to be a complex_real_exprt.

Parameters
exprSource expression
Returns
Object of type complex_real_exprt

Definition at line 2100 of file std_expr.h.

◆ to_concatenation_expr() [1/2]

const concatenation_exprt& to_concatenation_expr ( const exprt expr)
inline

Cast an exprt to a concatenation_exprt.

expr must be known to be concatenation_exprt.

Parameters
exprSource expression
Returns
Object of type concatenation_exprt

Definition at line 4643 of file std_expr.h.

◆ to_concatenation_expr() [2/2]

concatenation_exprt& to_concatenation_expr ( exprt expr)
inline

Cast an exprt to a concatenation_exprt.

expr must be known to be concatenation_exprt.

Parameters
exprSource expression
Returns
Object of type concatenation_exprt

Definition at line 4653 of file std_expr.h.

◆ to_cond_expr() [1/2]

const cond_exprt& to_cond_expr ( const exprt expr)
inline

Cast an exprt to a cond_exprt.

expr must be known to be cond_exprt.

Parameters
exprSource expression
Returns
Object of type cond_exprt

Definition at line 4953 of file std_expr.h.

◆ to_cond_expr() [2/2]

cond_exprt& to_cond_expr ( exprt expr)
inline

Cast an exprt to a popcount_exprt.

expr must be known to be popcount_exprt.

Parameters
exprSource expression
Returns
Object of type popcount_exprt

Definition at line 4962 of file std_expr.h.

◆ to_constant_expr() [1/2]

const constant_exprt& to_constant_expr ( const exprt expr)
inline

Cast an exprt to a constant_exprt.

expr must be known to be constant_exprt.

Parameters
exprSource expression
Returns
Object of type constant_exprt

Definition at line 4478 of file std_expr.h.

◆ to_constant_expr() [2/2]

constant_exprt& to_constant_expr ( exprt expr)
inline

Cast an exprt to a constant_exprt.

expr must be known to be constant_exprt.

Parameters
exprSource expression
Returns
Object of type constant_exprt

Definition at line 4485 of file std_expr.h.

◆ to_dereference_expr() [1/2]

const dereference_exprt& to_dereference_expr ( const exprt expr)
inline

Cast an exprt to a dereference_exprt.

expr must be known to be dereference_exprt.

Parameters
exprSource expression
Returns
Object of type dereference_exprt

Definition at line 3453 of file std_expr.h.

◆ to_dereference_expr() [2/2]

dereference_exprt& to_dereference_expr ( exprt expr)
inline

Cast an exprt to a dereference_exprt.

expr must be known to be dereference_exprt.

Parameters
exprSource expression
Returns
Object of type dereference_exprt

Definition at line 3463 of file std_expr.h.

◆ to_div_expr() [1/2]

const div_exprt& to_div_expr ( const exprt expr)
inline

Cast an exprt to a div_exprt.

expr must be known to be div_exprt.

Parameters
exprSource expression
Returns
Object of type div_exprt

Definition at line 1273 of file std_expr.h.

◆ to_div_expr() [2/2]

div_exprt& to_div_expr ( exprt expr)
inline

Cast an exprt to a div_exprt.

expr must be known to be div_exprt.

Parameters
exprSource expression
Returns
Object of type div_exprt

Definition at line 1283 of file std_expr.h.

◆ to_dynamic_object_expr() [1/2]

const dynamic_object_exprt& to_dynamic_object_expr ( const exprt expr)
inline

Cast an exprt to a dynamic_object_exprt.

expr must be known to be dynamic_object_exprt.

Parameters
exprSource expression
Returns
Object of type dynamic_object_exprt

Definition at line 2280 of file std_expr.h.

◆ to_dynamic_object_expr() [2/2]

dynamic_object_exprt& to_dynamic_object_expr ( exprt expr)
inline

Cast an exprt to a dynamic_object_exprt.

expr must be known to be dynamic_object_exprt.

Parameters
exprSource expression
Returns
Object of type dynamic_object_exprt

Definition at line 2291 of file std_expr.h.

◆ to_equal_expr() [1/2]

const equal_exprt& to_equal_expr ( const exprt expr)
inline

Cast an exprt to an equal_exprt.

expr must be known to be equal_exprt.

Parameters
exprSource expression
Returns
Object of type equal_exprt

Definition at line 1535 of file std_expr.h.

◆ to_equal_expr() [2/2]

equal_exprt& to_equal_expr ( exprt expr)
inline

Cast an exprt to an equal_exprt.

expr must be known to be equal_exprt.

Parameters
exprSource expression
Returns
Object of type equal_exprt

Definition at line 1543 of file std_expr.h.

◆ to_exists_expr() [1/2]

const exists_exprt& to_exists_expr ( const exprt expr)
inline

Definition at line 4850 of file std_expr.h.

◆ to_exists_expr() [2/2]

exists_exprt& to_exists_expr ( exprt expr)
inline

Definition at line 4859 of file std_expr.h.

◆ to_extractbit_expr() [1/2]

const extractbit_exprt& to_extractbit_expr ( const exprt expr)
inline

Cast an exprt to an extractbit_exprt.

expr must be known to be extractbit_exprt.

Parameters
exprSource expression
Returns
Object of type extractbit_exprt

Definition at line 3182 of file std_expr.h.

◆ to_extractbit_expr() [2/2]

extractbit_exprt& to_extractbit_expr ( exprt expr)
inline

Cast an exprt to an extractbit_exprt.

expr must be known to be extractbit_exprt.

Parameters
exprSource expression
Returns
Object of type extractbit_exprt

Definition at line 3192 of file std_expr.h.

◆ to_extractbits_expr() [1/2]

const extractbits_exprt& to_extractbits_expr ( const exprt expr)
inline

Cast an exprt to an extractbits_exprt.

expr must be known to be extractbits_exprt.

Parameters
exprSource expression
Returns
Object of type extractbits_exprt

Definition at line 3280 of file std_expr.h.

◆ to_extractbits_expr() [2/2]

extractbits_exprt& to_extractbits_expr ( exprt expr)
inline

Cast an exprt to an extractbits_exprt.

expr must be known to be extractbits_exprt.

Parameters
exprSource expression
Returns
Object of type extractbits_exprt

Definition at line 3290 of file std_expr.h.

◆ to_factorial_expr()

factorial_power_exprt& to_factorial_expr ( exprt expr)
inline

Cast an exprt to a factorial_power_exprt.

expr must be known to be factorial_power_exprt.

Parameters
exprSource expression
Returns
Object of type factorial_power_exprt

Definition at line 1479 of file std_expr.h.

◆ to_factorial_power_expr()

const factorial_power_exprt& to_factorial_power_expr ( const exprt expr)
inline

Cast an exprt to a factorial_power_exprt.

expr must be known to be factorial_power_exprt.

Parameters
exprSource expression
Returns
Object of type factorial_power_exprt

Definition at line 1469 of file std_expr.h.

◆ to_floatbv_typecast_expr() [1/2]

const floatbv_typecast_exprt& to_floatbv_typecast_expr ( const exprt expr)
inline

Cast an exprt to a floatbv_typecast_exprt.

expr must be known to be floatbv_typecast_exprt.

Parameters
exprSource expression
Returns
Object of type floatbv_typecast_exprt

Definition at line 2413 of file std_expr.h.

◆ to_floatbv_typecast_expr() [2/2]

floatbv_typecast_exprt& to_floatbv_typecast_expr ( exprt expr)
inline

Cast an exprt to a floatbv_typecast_exprt.

expr must be known to be floatbv_typecast_exprt.

Parameters
exprSource expression
Returns
Object of type floatbv_typecast_exprt

Definition at line 2423 of file std_expr.h.

◆ to_function_application_expr() [1/2]

const function_application_exprt& to_function_application_expr ( const exprt expr)
inline

Cast an exprt to a function_application_exprt.

expr must be known to be function_application_exprt.

Parameters
exprSource expression
Returns
Object of type function_application_exprt

Definition at line 4577 of file std_expr.h.

◆ to_function_application_expr() [2/2]

function_application_exprt& to_function_application_expr ( exprt expr)
inline

Cast an exprt to a function_application_exprt.

expr must be known to be function_application_exprt.

Parameters
exprSource expression
Returns
Object of type function_application_exprt

Definition at line 4588 of file std_expr.h.

◆ to_ieee_float_equal_expr() [1/2]

const ieee_float_equal_exprt& to_ieee_float_equal_expr ( const exprt expr)
inline

Cast an exprt to an ieee_float_equal_exprt.

expr must be known to be ieee_float_equal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_equal_exprt

Definition at line 4252 of file std_expr.h.

◆ to_ieee_float_equal_expr() [2/2]

ieee_float_equal_exprt& to_ieee_float_equal_expr ( exprt expr)
inline

Cast an exprt to an ieee_float_equal_exprt.

expr must be known to be ieee_float_equal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_equal_exprt

Definition at line 4262 of file std_expr.h.

◆ to_ieee_float_notequal_expr() [1/2]

const ieee_float_notequal_exprt& to_ieee_float_notequal_expr ( const exprt expr)
inline

Cast an exprt to an ieee_float_notequal_exprt.

expr must be known to be ieee_float_notequal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_notequal_exprt

Definition at line 4304 of file std_expr.h.

◆ to_ieee_float_notequal_expr() [2/2]

ieee_float_notequal_exprt& to_ieee_float_notequal_expr ( exprt expr)
inline

Cast an exprt to an ieee_float_notequal_exprt.

expr must be known to be ieee_float_notequal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_notequal_exprt

Definition at line 4315 of file std_expr.h.

◆ to_ieee_float_op_expr() [1/2]

const ieee_float_op_exprt& to_ieee_float_op_expr ( const exprt expr)
inline

Cast an exprt to an ieee_float_op_exprt.

expr must be known to be ieee_float_op_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_op_exprt

Definition at line 4393 of file std_expr.h.

◆ to_ieee_float_op_expr() [2/2]

ieee_float_op_exprt& to_ieee_float_op_expr ( exprt expr)
inline

Cast an exprt to an ieee_float_op_exprt.

expr must be known to be ieee_float_op_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_op_exprt

Definition at line 4402 of file std_expr.h.

◆ to_if_expr() [1/2]

const if_exprt& to_if_expr ( const exprt expr)
inline

Cast an exprt to an if_exprt.

expr must be known to be if_exprt.

Parameters
exprSource expression
Returns
Object of type if_exprt

Definition at line 3538 of file std_expr.h.

◆ to_if_expr() [2/2]

if_exprt& to_if_expr ( exprt expr)
inline

Cast an exprt to an if_exprt.

expr must be known to be if_exprt.

Parameters
exprSource expression
Returns
Object of type if_exprt

Definition at line 3548 of file std_expr.h.

◆ to_implies_expr() [1/2]

const implies_exprt& to_implies_expr ( const exprt expr)
inline

Cast an exprt to a implies_exprt.

expr must be known to be implies_exprt.

Parameters
exprSource expression
Returns
Object of type implies_exprt

Definition at line 2539 of file std_expr.h.

◆ to_implies_expr() [2/2]

implies_exprt& to_implies_expr ( exprt expr)
inline

Cast an exprt to a implies_exprt.

expr must be known to be implies_exprt.

Parameters
exprSource expression
Returns
Object of type implies_exprt

Definition at line 2547 of file std_expr.h.

◆ to_index_designator() [1/2]

const index_designatort& to_index_designator ( const exprt expr)
inline

Cast an exprt to an index_designatort.

expr must be known to be index_designatort.

Parameters
exprSource expression
Returns
Object of type index_designatort

Definition at line 3682 of file std_expr.h.

◆ to_index_designator() [2/2]

index_designatort& to_index_designator ( exprt expr)
inline

Cast an exprt to an index_designatort.

expr must be known to be index_designatort.

Parameters
exprSource expression
Returns
Object of type index_designatort

Definition at line 3692 of file std_expr.h.

◆ to_index_expr() [1/2]

const index_exprt& to_index_expr ( const exprt expr)
inline

Cast an exprt to an index_exprt.

expr must be known to be index_exprt.

Parameters
exprSource expression
Returns
Object of type index_exprt

Definition at line 1664 of file std_expr.h.

◆ to_index_expr() [2/2]

index_exprt& to_index_expr ( exprt expr)
inline

Cast an exprt to an index_exprt.

expr must be known to be index_exprt.

Parameters
exprSource expression
Returns
Object of type index_exprt

Definition at line 1674 of file std_expr.h.

◆ to_isfinite_expr() [1/2]

const isfinite_exprt& to_isfinite_expr ( const exprt expr)
inline

Cast an exprt to a isfinite_exprt.

expr must be known to be isfinite_exprt.

Parameters
exprSource expression
Returns
Object of type isfinite_exprt

Definition at line 4160 of file std_expr.h.

◆ to_isfinite_expr() [2/2]

isfinite_exprt& to_isfinite_expr ( exprt expr)
inline

Cast an exprt to a isfinite_exprt.

expr must be known to be isfinite_exprt.

Parameters
exprSource expression
Returns
Object of type isfinite_exprt

Definition at line 4168 of file std_expr.h.

◆ to_isinf_expr() [1/2]

const isinf_exprt& to_isinf_expr ( const exprt expr)
inline

Cast an exprt to a isinf_exprt.

expr must be known to be isinf_exprt.

Parameters
exprSource expression
Returns
Object of type isinf_exprt

Definition at line 4110 of file std_expr.h.

◆ to_isinf_expr() [2/2]

isinf_exprt& to_isinf_expr ( exprt expr)
inline

Cast an exprt to a isinf_exprt.

expr must be known to be isinf_exprt.

Parameters
exprSource expression
Returns
Object of type isinf_exprt

Definition at line 4120 of file std_expr.h.

◆ to_isnan_expr() [1/2]

const isnan_exprt& to_isnan_expr ( const exprt expr)
inline

Cast an exprt to a isnan_exprt.

expr must be known to be isnan_exprt.

Parameters
exprSource expression
Returns
Object of type isnan_exprt

Definition at line 4064 of file std_expr.h.

◆ to_isnan_expr() [2/2]

isnan_exprt& to_isnan_expr ( exprt expr)
inline

Cast an exprt to a isnan_exprt.

expr must be known to be isnan_exprt.

Parameters
exprSource expression
Returns
Object of type isnan_exprt

Definition at line 4072 of file std_expr.h.

◆ to_isnormal_expr() [1/2]

const isnormal_exprt& to_isnormal_expr ( const exprt expr)
inline

Cast an exprt to a isnormal_exprt.

expr must be known to be isnormal_exprt.

Parameters
exprSource expression
Returns
Object of type isnormal_exprt

Definition at line 4206 of file std_expr.h.

◆ to_isnormal_expr() [2/2]

isnormal_exprt& to_isnormal_expr ( exprt expr)
inline

Cast an exprt to a isnormal_exprt.

expr must be known to be isnormal_exprt.

Parameters
exprSource expression
Returns
Object of type isnormal_exprt

Definition at line 4214 of file std_expr.h.

◆ to_let_expr() [1/2]

const let_exprt& to_let_expr ( const exprt expr)
inline

Cast an exprt to a let_exprt.

expr must be known to be let_exprt.

Parameters
exprSource expression
Returns
Object of type let_exprt

Definition at line 4737 of file std_expr.h.

◆ to_let_expr() [2/2]

let_exprt& to_let_expr ( exprt expr)
inline

Cast an exprt to a let_exprt.

expr must be known to be let_exprt.

Parameters
exprSource expression
Returns
Object of type let_exprt

Definition at line 4745 of file std_expr.h.

◆ to_member_designator() [1/2]

const member_designatort& to_member_designator ( const exprt expr)
inline

Cast an exprt to an member_designatort.

expr must be known to be member_designatort.

Parameters
exprSource expression
Returns
Object of type member_designatort

Definition at line 3732 of file std_expr.h.

◆ to_member_designator() [2/2]

member_designatort& to_member_designator ( exprt expr)
inline

Cast an exprt to an member_designatort.

expr must be known to be member_designatort.

Parameters
exprSource expression
Returns
Object of type member_designatort

Definition at line 3742 of file std_expr.h.

◆ to_member_expr() [1/2]

const member_exprt& to_member_expr ( const exprt expr)
inline

Cast an exprt to a member_exprt.

expr must be known to be member_exprt.

Parameters
exprSource expression
Returns
Object of type member_exprt

Definition at line 4014 of file std_expr.h.

◆ to_member_expr() [2/2]

member_exprt& to_member_expr ( exprt expr)
inline

Cast an exprt to a member_exprt.

expr must be known to be member_exprt.

Parameters
exprSource expression
Returns
Object of type member_exprt

Definition at line 4024 of file std_expr.h.

◆ to_minus_expr() [1/2]

const minus_exprt& to_minus_expr ( const exprt expr)
inline

Cast an exprt to a minus_exprt.

expr must be known to be minus_exprt.

Parameters
exprSource expression
Returns
Object of type minus_exprt

Definition at line 1144 of file std_expr.h.

◆ to_minus_expr() [2/2]

minus_exprt& to_minus_expr ( exprt expr)
inline

Cast an exprt to a minus_exprt.

expr must be known to be minus_exprt.

Parameters
exprSource expression
Returns
Object of type minus_exprt

Definition at line 1154 of file std_expr.h.

◆ to_mod_expr() [1/2]

const mod_exprt& to_mod_expr ( const exprt expr)
inline

Cast an exprt to a mod_exprt.

expr must be known to be mod_exprt.

Parameters
exprSource expression
Returns
Object of type mod_exprt

Definition at line 1325 of file std_expr.h.

◆ to_mod_expr() [2/2]

mod_exprt& to_mod_expr ( exprt expr)
inline

Cast an exprt to a mod_exprt.

expr must be known to be mod_exprt.

Parameters
exprSource expression
Returns
Object of type mod_exprt

Definition at line 1333 of file std_expr.h.

◆ to_mult_expr() [1/2]

const mult_exprt& to_mult_expr ( const exprt expr)
inline

Cast an exprt to a mult_exprt.

expr must be known to be mult_exprt.

Parameters
exprSource expression
Returns
Object of type mult_exprt

Definition at line 1197 of file std_expr.h.

◆ to_mult_expr() [2/2]

mult_exprt& to_mult_expr ( exprt expr)
inline

Cast an exprt to a mult_exprt.

expr must be known to be mult_exprt.

Parameters
exprSource expression
Returns
Object of type mult_exprt

Definition at line 1207 of file std_expr.h.

◆ to_multi_ary_expr() [1/2]

const multi_ary_exprt& to_multi_ary_expr ( const exprt expr)
inline

Cast an exprt to a multi_ary_exprt.

expr must be known to be multi_ary_exprt.

Parameters
exprSource expression
Returns
Object of type multi_ary_exprt

Definition at line 1038 of file std_expr.h.

◆ to_multi_ary_expr() [2/2]

multi_ary_exprt& to_multi_ary_expr ( exprt expr)
inline

Cast an exprt to a multi_ary_exprt.

expr must be known to be multi_ary_exprt.

Parameters
exprSource expression
Returns
Object of type multi_ary_exprt

Definition at line 1044 of file std_expr.h.

◆ to_nondet_symbol_expr() [1/2]

const nondet_symbol_exprt& to_nondet_symbol_expr ( const exprt expr)
inline

Cast an exprt to a nondet_symbol_exprt.

expr must be known to be nondet_symbol_exprt.

Parameters
exprSource expression
Returns
Object of type nondet_symbol_exprt

Definition at line 316 of file std_expr.h.

◆ to_nondet_symbol_expr() [2/2]

nondet_symbol_exprt& to_nondet_symbol_expr ( exprt expr)
inline

Cast an exprt to a nondet_symbol_exprt.

expr must be known to be nondet_symbol_exprt.

Parameters
exprSource expression
Returns
Object of type nondet_symbol_exprt

Definition at line 324 of file std_expr.h.

◆ to_not_expr() [1/2]

const not_exprt& to_not_expr ( const exprt expr)
inline

Cast an exprt to an not_exprt.

expr must be known to be not_exprt.

Parameters
exprSource expression
Returns
Object of type not_exprt

Definition at line 3384 of file std_expr.h.

◆ to_not_expr() [2/2]

not_exprt& to_not_expr ( exprt expr)
inline

Cast an exprt to an not_exprt.

expr must be known to be not_exprt.

Parameters
exprSource expression
Returns
Object of type not_exprt

Definition at line 3392 of file std_expr.h.

◆ to_notequal_expr() [1/2]

const notequal_exprt& to_notequal_expr ( const exprt expr)
inline

Cast an exprt to an notequal_exprt.

expr must be known to be notequal_exprt.

Parameters
exprSource expression
Returns
Object of type notequal_exprt

Definition at line 1581 of file std_expr.h.

◆ to_notequal_expr() [2/2]

notequal_exprt& to_notequal_expr ( exprt expr)
inline

Cast an exprt to an notequal_exprt.

expr must be known to be notequal_exprt.

Parameters
exprSource expression
Returns
Object of type notequal_exprt

Definition at line 1591 of file std_expr.h.

◆ to_object_descriptor_expr() [1/2]

const object_descriptor_exprt& to_object_descriptor_expr ( const exprt expr)
inline

Cast an exprt to an object_descriptor_exprt.

expr must be known to be object_descriptor_exprt.

Parameters
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 2210 of file std_expr.h.

◆ to_object_descriptor_expr() [2/2]

object_descriptor_exprt& to_object_descriptor_expr ( exprt expr)
inline

Cast an exprt to an object_descriptor_exprt.

expr must be known to be object_descriptor_exprt.

Parameters
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 2221 of file std_expr.h.

◆ to_or_expr() [1/2]

const or_exprt& to_or_expr ( const exprt expr)
inline

Cast an exprt to a or_exprt.

expr must be known to be or_exprt.

Parameters
exprSource expression
Returns
Object of type or_exprt

Definition at line 2610 of file std_expr.h.

◆ to_or_expr() [2/2]

or_exprt& to_or_expr ( exprt expr)
inline

Cast an exprt to a or_exprt.

expr must be known to be or_exprt.

Parameters
exprSource expression
Returns
Object of type or_exprt

Definition at line 2620 of file std_expr.h.

◆ to_plus_expr() [1/2]

const plus_exprt& to_plus_expr ( const exprt expr)
inline

Cast an exprt to a plus_exprt.

expr must be known to be plus_exprt.

Parameters
exprSource expression
Returns
Object of type plus_exprt

Definition at line 1092 of file std_expr.h.

◆ to_plus_expr() [2/2]

plus_exprt& to_plus_expr ( exprt expr)
inline

Cast an exprt to a plus_exprt.

expr must be known to be plus_exprt.

Parameters
exprSource expression
Returns
Object of type plus_exprt

Definition at line 1102 of file std_expr.h.

◆ to_popcount_expr() [1/2]

const popcount_exprt& to_popcount_expr ( const exprt expr)
inline

Cast an exprt to a popcount_exprt.

expr must be known to be popcount_exprt.

Parameters
exprSource expression
Returns
Object of type popcount_exprt

Definition at line 4894 of file std_expr.h.

◆ to_popcount_expr() [2/2]

popcount_exprt& to_popcount_expr ( exprt expr)
inline

Cast an exprt to a popcount_exprt.

expr must be known to be popcount_exprt.

Parameters
exprSource expression
Returns
Object of type popcount_exprt

Definition at line 4902 of file std_expr.h.

◆ to_power_expr() [1/2]

const power_exprt& to_power_expr ( const exprt expr)
inline

Cast an exprt to a power_exprt.

expr must be known to be power_exprt.

Parameters
exprSource expression
Returns
Object of type power_exprt

Definition at line 1421 of file std_expr.h.

◆ to_power_expr() [2/2]

power_exprt& to_power_expr ( exprt expr)
inline

Cast an exprt to a power_exprt.

expr must be known to be power_exprt.

Parameters
exprSource expression
Returns
Object of type power_exprt

Definition at line 1429 of file std_expr.h.

◆ to_quantifier_expr() [1/2]

const quantifier_exprt& to_quantifier_expr ( const exprt expr)
inline

Cast an exprt to a quantifier_exprt.

expr must be known to be quantifier_exprt.

Parameters
exprSource expression
Returns
Object of type quantifier_exprt

Definition at line 4800 of file std_expr.h.

◆ to_quantifier_expr() [2/2]

quantifier_exprt& to_quantifier_expr ( exprt expr)
inline

Cast an exprt to a quantifier_exprt.

expr must be known to be quantifier_exprt.

Parameters
exprSource expression
Returns
Object of type quantifier_exprt

Definition at line 4810 of file std_expr.h.

◆ to_rem_expr() [1/2]

const rem_exprt& to_rem_expr ( const exprt expr)
inline

Cast an exprt to a rem_exprt.

expr must be known to be rem_exprt.

Parameters
exprSource expression
Returns
Object of type rem_exprt

Definition at line 1373 of file std_expr.h.

◆ to_rem_expr() [2/2]

rem_exprt& to_rem_expr ( exprt expr)
inline

Cast an exprt to a rem_exprt.

expr must be known to be rem_exprt.

Parameters
exprSource expression
Returns
Object of type rem_exprt

Definition at line 1381 of file std_expr.h.

◆ to_replication_expr() [1/2]

const replication_exprt& to_replication_expr ( const exprt expr)
inline

Cast an exprt to a replication_exprt.

expr must be known to be replication_exprt.

Parameters
exprSource expression
Returns
Object of type replication_exprt

Definition at line 3105 of file std_expr.h.

◆ to_replication_expr() [2/2]

replication_exprt& to_replication_expr ( exprt expr)
inline

Cast an exprt to a replication_exprt.

expr must be known to be replication_exprt.

Parameters
exprSource expression
Returns
Object of type replication_exprt

Definition at line 3115 of file std_expr.h.

◆ to_shift_expr() [1/2]

const shift_exprt& to_shift_expr ( const exprt expr)
inline

Cast an exprt to a shift_exprt.

expr must be known to be shift_exprt.

Parameters
exprSource expression
Returns
Object of type shift_exprt

Definition at line 2949 of file std_expr.h.

◆ to_shift_expr() [2/2]

shift_exprt& to_shift_expr ( exprt expr)
inline

Cast an exprt to a shift_exprt.

expr must be known to be shift_exprt.

Parameters
exprSource expression
Returns
Object of type shift_exprt

Definition at line 2958 of file std_expr.h.

◆ to_shl_expr() [1/2]

const shl_exprt& to_shl_expr ( const exprt expr)
inline

Cast an exprt to a shl_exprt.

expr must be known to be shl_exprt.

Parameters
exprSource expression
Returns
Object of type shl_exprt

Definition at line 3001 of file std_expr.h.

◆ to_shl_expr() [2/2]

shl_exprt& to_shl_expr ( exprt expr)
inline

Cast an exprt to a shl_exprt.

expr must be known to be shl_exprt.

Parameters
exprSource expression
Returns
Object of type shl_exprt

Definition at line 3010 of file std_expr.h.

◆ to_sign_expr() [1/2]

const sign_exprt& to_sign_expr ( const exprt expr)
inline

Cast an exprt to a sign_exprt.

expr must be known to be a sign_exprt.

Parameters
exprSource expression
Returns
Object of type sign_exprt

Definition at line 721 of file std_expr.h.

◆ to_sign_expr() [2/2]

sign_exprt& to_sign_expr ( exprt expr)
inline

Cast an exprt to a sign_exprt.

expr must be known to be a sign_exprt.

Parameters
exprSource expression
Returns
Object of type sign_exprt

Definition at line 730 of file std_expr.h.

◆ to_struct_expr() [1/2]

const struct_exprt& to_struct_expr ( const exprt expr)
inline

Cast an exprt to a struct_exprt.

expr must be known to be struct_exprt.

Parameters
exprSource expression
Returns
Object of type struct_exprt

Definition at line 1977 of file std_expr.h.

◆ to_struct_expr() [2/2]

struct_exprt& to_struct_expr ( exprt expr)
inline

Cast an exprt to a struct_exprt.

expr must be known to be struct_exprt.

Parameters
exprSource expression
Returns
Object of type struct_exprt

Definition at line 1984 of file std_expr.h.

◆ to_symbol_expr() [1/2]

const symbol_exprt& to_symbol_expr ( const exprt expr)
inline

Cast an exprt to a symbol_exprt.

expr must be known to be symbol_exprt.

Parameters
exprSource expression
Returns
Object of type symbol_exprt

Definition at line 262 of file std_expr.h.

◆ to_symbol_expr() [2/2]

symbol_exprt& to_symbol_expr ( exprt expr)
inline

Cast an exprt to a symbol_exprt.

expr must be known to be symbol_exprt.

Parameters
exprSource expression
Returns
Object of type symbol_exprt

Definition at line 270 of file std_expr.h.

◆ to_trans_expr() [1/2]

const transt& to_trans_expr ( const exprt expr)
inline

Cast an exprt to a transt expr must be known to be transt.

Parameters
exprSource expression
Returns
Object of type transt

Definition at line 124 of file std_expr.h.

◆ to_trans_expr() [2/2]

transt& to_trans_expr ( exprt expr)
inline

Cast an exprt to a transt expr must be known to be transt.

Parameters
exprSource expression
Returns
Object of type transt

Definition at line 134 of file std_expr.h.

◆ to_typecast_expr() [1/2]

const typecast_exprt& to_typecast_expr ( const exprt expr)
inline

Cast an exprt to a typecast_exprt.

expr must be known to be typecast_exprt.

Parameters
exprSource expression
Returns
Object of type typecast_exprt

Definition at line 2341 of file std_expr.h.

◆ to_typecast_expr() [2/2]

typecast_exprt& to_typecast_expr ( exprt expr)
inline

Cast an exprt to a typecast_exprt.

expr must be known to be typecast_exprt.

Parameters
exprSource expression
Returns
Object of type typecast_exprt

Definition at line 2351 of file std_expr.h.

◆ to_unary_expr() [1/2]

const unary_exprt& to_unary_expr ( const exprt expr)
inline

Cast an exprt to a unary_exprt.

expr must be known to be unary_exprt.

Parameters
exprSource expression
Returns
Object of type unary_exprt

Definition at line 406 of file std_expr.h.

◆ to_unary_expr() [2/2]

unary_exprt& to_unary_expr ( exprt expr)
inline

Cast an exprt to a unary_exprt.

expr must be known to be unary_exprt.

Parameters
exprSource expression
Returns
Object of type unary_exprt

Definition at line 415 of file std_expr.h.

◆ to_unary_minus_expr() [1/2]

const unary_minus_exprt& to_unary_minus_expr ( const exprt expr)
inline

Cast an exprt to a unary_minus_exprt.

expr must be known to be unary_minus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_minus_exprt

Definition at line 507 of file std_expr.h.

◆ to_unary_minus_expr() [2/2]

unary_minus_exprt& to_unary_minus_expr ( exprt expr)
inline

Cast an exprt to a unary_minus_exprt.

expr must be known to be unary_minus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_minus_exprt

Definition at line 517 of file std_expr.h.

◆ to_unary_plus_expr() [1/2]

const unary_plus_exprt& to_unary_plus_expr ( const exprt expr)
inline

Cast an exprt to a unary_plus_exprt.

expr must be known to be unary_plus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_plus_exprt

Definition at line 551 of file std_expr.h.

◆ to_unary_plus_expr() [2/2]

unary_plus_exprt& to_unary_plus_expr ( exprt expr)
inline

Cast an exprt to a unary_minus_exprt.

expr must be known to be unary_minus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_minus_exprt

Definition at line 560 of file std_expr.h.

◆ to_union_expr() [1/2]

const union_exprt& to_union_expr ( const exprt expr)
inline

Cast an exprt to a union_exprt.

expr must be known to be union_exprt.

Parameters
exprSource expression
Returns
Object of type union_exprt

Definition at line 1919 of file std_expr.h.

◆ to_union_expr() [2/2]

union_exprt& to_union_expr ( exprt expr)
inline

Cast an exprt to a union_exprt.

expr must be known to be union_exprt.

Parameters
exprSource expression
Returns
Object of type union_exprt

Definition at line 1929 of file std_expr.h.

◆ to_update_expr() [1/2]

const update_exprt& to_update_expr ( const exprt expr)
inline

Cast an exprt to an update_exprt.

expr must be known to be update_exprt.

Parameters
exprSource expression
Returns
Object of type update_exprt

Definition at line 3825 of file std_expr.h.

◆ to_update_expr() [2/2]

update_exprt& to_update_expr ( exprt expr)
inline

Cast an exprt to an update_exprt.

expr must be known to be update_exprt.

Parameters
exprSource expression
Returns
Object of type update_exprt

Definition at line 3835 of file std_expr.h.

◆ to_vector_expr() [1/2]

const vector_exprt& to_vector_expr ( const exprt expr)
inline

Cast an exprt to an vector_exprt.

expr must be known to be vector_exprt.

Parameters
exprSource expression
Returns
Object of type vector_exprt

Definition at line 1849 of file std_expr.h.

◆ to_vector_expr() [2/2]

vector_exprt& to_vector_expr ( exprt expr)
inline

Cast an exprt to an vector_exprt.

expr must be known to be vector_exprt.

Parameters
exprSource expression
Returns
Object of type vector_exprt

Definition at line 1856 of file std_expr.h.

◆ to_with_expr() [1/2]

const with_exprt& to_with_expr ( const exprt expr)
inline

Cast an exprt to a with_exprt.

expr must be known to be with_exprt.

Parameters
exprSource expression
Returns
Object of type with_exprt

Definition at line 3624 of file std_expr.h.

◆ to_with_expr() [2/2]

with_exprt& to_with_expr ( exprt expr)
inline

Cast an exprt to a with_exprt.

expr must be known to be with_exprt.

Parameters
exprSource expression
Returns
Object of type with_exprt

Definition at line 3634 of file std_expr.h.

◆ to_xor_expr() [1/2]

const xor_exprt& to_xor_expr ( const exprt expr)
inline

Cast an exprt to a xor_exprt.

expr must be known to be xor_exprt.

Parameters
exprSource expression
Returns
Object of type xor_exprt

Definition at line 2660 of file std_expr.h.

◆ to_xor_expr() [2/2]

xor_exprt& to_xor_expr ( exprt expr)
inline

Cast an exprt to a bitxor_exprt.

expr must be known to be bitxor_exprt.

Parameters
exprSource expression
Returns
Object of type bitxor_exprt

Definition at line 2667 of file std_expr.h.

◆ validate_expr() [1/52]

void validate_expr ( const transt value)
inline

Definition at line 147 of file std_expr.h.

◆ validate_expr() [2/52]

void validate_expr ( const symbol_exprt value)
inline

Definition at line 281 of file std_expr.h.

◆ validate_expr() [3/52]

void validate_expr ( const nondet_symbol_exprt value)
inline

Definition at line 335 of file std_expr.h.

◆ validate_expr() [4/52]

void validate_expr ( const abs_exprt value)
inline

Definition at line 473 of file std_expr.h.

◆ validate_expr() [5/52]

void validate_expr ( const unary_minus_exprt value)
inline

Definition at line 530 of file std_expr.h.

◆ validate_expr() [6/52]

void validate_expr ( const unary_plus_exprt value)
inline

Definition at line 573 of file std_expr.h.

◆ validate_expr() [7/52]

void validate_expr ( const bswap_exprt value)
inline

Definition at line 635 of file std_expr.h.

◆ validate_expr() [8/52]

void validate_expr ( const sign_exprt expr)
inline

Definition at line 743 of file std_expr.h.

◆ validate_expr() [9/52]

void validate_expr ( const plus_exprt value)
inline

Definition at line 1115 of file std_expr.h.

◆ validate_expr() [10/52]

void validate_expr ( const minus_exprt value)
inline

Definition at line 1167 of file std_expr.h.

◆ validate_expr() [11/52]

void validate_expr ( const mult_exprt value)
inline

Definition at line 1220 of file std_expr.h.

◆ validate_expr() [12/52]

void validate_expr ( const div_exprt value)
inline

Definition at line 1296 of file std_expr.h.

◆ validate_expr() [13/52]

void validate_expr ( const mod_exprt value)
inline

Definition at line 1344 of file std_expr.h.

◆ validate_expr() [14/52]

void validate_expr ( const rem_exprt value)
inline

Definition at line 1392 of file std_expr.h.

◆ validate_expr() [15/52]

void validate_expr ( const power_exprt value)
inline

Definition at line 1440 of file std_expr.h.

◆ validate_expr() [16/52]

void validate_expr ( const factorial_power_exprt value)
inline

Definition at line 1493 of file std_expr.h.

◆ validate_expr() [17/52]

void validate_expr ( const equal_exprt value)
inline

Definition at line 1554 of file std_expr.h.

◆ validate_expr() [18/52]

void validate_expr ( const notequal_exprt value)
inline

Definition at line 1604 of file std_expr.h.

◆ validate_expr() [19/52]

void validate_expr ( const index_exprt value)
inline

Definition at line 1687 of file std_expr.h.

◆ validate_expr() [20/52]

void validate_expr ( const array_of_exprt value)
inline

Definition at line 1748 of file std_expr.h.

◆ validate_expr() [21/52]

void validate_expr ( const array_list_exprt value)
inline

Definition at line 1817 of file std_expr.h.

◆ validate_expr() [22/52]

void validate_expr ( const union_exprt value)
inline

Definition at line 1942 of file std_expr.h.

◆ validate_expr() [23/52]

void validate_expr ( const complex_exprt value)
inline

Definition at line 2069 of file std_expr.h.

◆ validate_expr() [24/52]

void validate_expr ( const complex_real_exprt expr)
inline

Definition at line 2115 of file std_expr.h.

◆ validate_expr() [25/52]

void validate_expr ( const complex_imag_exprt expr)
inline

Definition at line 2162 of file std_expr.h.

◆ validate_expr() [26/52]

void validate_expr ( const object_descriptor_exprt value)
inline

Definition at line 2235 of file std_expr.h.

◆ validate_expr() [27/52]

void validate_expr ( const dynamic_object_exprt value)
inline

Definition at line 2305 of file std_expr.h.

◆ validate_expr() [28/52]

void validate_expr ( const typecast_exprt value)
inline

Definition at line 2364 of file std_expr.h.

◆ validate_expr() [29/52]

void validate_expr ( const floatbv_typecast_exprt value)
inline

Definition at line 2437 of file std_expr.h.

◆ validate_expr() [30/52]

void validate_expr ( const implies_exprt value)
inline

Definition at line 2558 of file std_expr.h.

◆ validate_expr() [31/52]

void validate_expr ( const replication_exprt value)
inline

Definition at line 3128 of file std_expr.h.

◆ validate_expr() [32/52]

void validate_expr ( const extractbit_exprt value)
inline

Definition at line 3205 of file std_expr.h.

◆ validate_expr() [33/52]

void validate_expr ( const extractbits_exprt value)
inline

Definition at line 3303 of file std_expr.h.

◆ validate_expr() [34/52]

void validate_expr ( const address_of_exprt value)
inline

Definition at line 3356 of file std_expr.h.

◆ validate_expr() [35/52]

void validate_expr ( const not_exprt value)
inline

Definition at line 3404 of file std_expr.h.

◆ validate_expr() [36/52]

void validate_expr ( const dereference_exprt value)
inline

Definition at line 3476 of file std_expr.h.

◆ validate_expr() [37/52]

void validate_expr ( const if_exprt value)
inline

Definition at line 3561 of file std_expr.h.

◆ validate_expr() [38/52]

void validate_expr ( const with_exprt value)
inline

Definition at line 3647 of file std_expr.h.

◆ validate_expr() [39/52]

void validate_expr ( const index_designatort value)
inline

Definition at line 3705 of file std_expr.h.

◆ validate_expr() [40/52]

void validate_expr ( const member_designatort value)
inline

Definition at line 3755 of file std_expr.h.

◆ validate_expr() [41/52]

void validate_expr ( const update_exprt value)
inline

Definition at line 3848 of file std_expr.h.

◆ validate_expr() [42/52]

void validate_expr ( const member_exprt value)
inline

Definition at line 4037 of file std_expr.h.

◆ validate_expr() [43/52]

void validate_expr ( const isnan_exprt value)
inline

Definition at line 4083 of file std_expr.h.

◆ validate_expr() [44/52]

void validate_expr ( const isinf_exprt value)
inline

Definition at line 4133 of file std_expr.h.

◆ validate_expr() [45/52]

void validate_expr ( const isfinite_exprt value)
inline

Definition at line 4179 of file std_expr.h.

◆ validate_expr() [46/52]

void validate_expr ( const isnormal_exprt value)
inline

Definition at line 4225 of file std_expr.h.

◆ validate_expr() [47/52]

void validate_expr ( const ieee_float_equal_exprt value)
inline

Definition at line 4276 of file std_expr.h.

◆ validate_expr() [48/52]

void validate_expr ( const ieee_float_notequal_exprt value)
inline

Definition at line 4329 of file std_expr.h.

◆ validate_expr() [49/52]

void validate_expr ( const function_application_exprt value)
inline

Definition at line 4602 of file std_expr.h.

◆ validate_expr() [50/52]

void validate_expr ( const let_exprt value)
inline

Definition at line 4756 of file std_expr.h.

◆ validate_expr() [51/52]

void validate_expr ( const quantifier_exprt value)
inline

Definition at line 4824 of file std_expr.h.

◆ validate_expr() [52/52]

void validate_expr ( const popcount_exprt value)
inline

Definition at line 4914 of file std_expr.h.