cprover
std_expr.h File Reference

API to expression classes. More...

#include "invariant.h"
#include "std_types.h"
Include dependency graph for std_expr.h:

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...
 

Functions

const transtto_trans_expr (const exprt &expr)
 Cast a generic exprt to a transt. More...
 
transtto_trans_expr (exprt &expr)
 
const symbol_exprtto_symbol_expr (const exprt &expr)
 Cast a generic exprt to a symbol_exprt. More...
 
symbol_exprtto_symbol_expr (exprt &expr)
 Cast a generic exprt to a symbol_exprt. More...
 
const unary_exprtto_unary_expr (const exprt &expr)
 Cast a generic exprt to a unary_exprt. More...
 
unary_exprtto_unary_expr (exprt &expr)
 Cast a generic exprt to a unary_exprt. More...
 
const abs_exprtto_abs_expr (const exprt &expr)
 Cast a generic exprt to a abs_exprt. More...
 
abs_exprtto_abs_expr (exprt &expr)
 Cast a generic exprt to a abs_exprt. More...
 
const unary_minus_exprtto_unary_minus_expr (const exprt &expr)
 Cast a generic exprt to a unary_minus_exprt. More...
 
unary_minus_exprtto_unary_minus_expr (exprt &expr)
 Cast a generic exprt to a unary_minus_exprt. More...
 
const binary_exprtto_binary_expr (const exprt &expr)
 Cast a generic exprt to a binary_exprt. More...
 
binary_exprtto_binary_expr (exprt &expr)
 Cast a generic exprt to a binary_exprt. More...
 
const binary_relation_exprtto_binary_relation_expr (const exprt &expr)
 Cast a generic exprt to a binary_relation_exprt. More...
 
binary_relation_exprtto_binary_relation_expr (exprt &expr)
 Cast a generic exprt to a binary_relation_exprt. More...
 
const multi_ary_exprtto_multi_ary_expr (const exprt &expr)
 Cast a generic exprt to a multi_ary_exprt. More...
 
multi_ary_exprtto_multi_ary_expr (exprt &expr)
 Cast a generic exprt to a multi_ary_exprt. More...
 
const plus_exprtto_plus_expr (const exprt &expr)
 Cast a generic exprt to a plus_exprt. More...
 
plus_exprtto_plus_expr (exprt &expr)
 Cast a generic exprt to a plus_exprt. More...
 
const minus_exprtto_minus_expr (const exprt &expr)
 Cast a generic exprt to a minus_exprt. More...
 
minus_exprtto_minus_expr (exprt &expr)
 Cast a generic exprt to a minus_exprt. More...
 
const mult_exprtto_mult_expr (const exprt &expr)
 Cast a generic exprt to a mult_exprt. More...
 
mult_exprtto_mult_expr (exprt &expr)
 Cast a generic exprt to a mult_exprt. More...
 
const div_exprtto_div_expr (const exprt &expr)
 Cast a generic exprt to a div_exprt. More...
 
div_exprtto_div_expr (exprt &expr)
 Cast a generic exprt to a div_exprt. More...
 
const mod_exprtto_mod_expr (const exprt &expr)
 Cast a generic exprt to a mod_exprt. More...
 
mod_exprtto_mod_expr (exprt &expr)
 Cast a generic exprt to a mod_exprt. More...
 
const rem_exprtto_rem_expr (const exprt &expr)
 Cast a generic exprt to a rem_exprt. More...
 
rem_exprtto_rem_expr (exprt &expr)
 Cast a generic exprt to a rem_exprt. More...
 
const power_exprtto_power_expr (const exprt &expr)
 Cast a generic exprt to a power_exprt. More...
 
power_exprtto_power_expr (exprt &expr)
 Cast a generic exprt to a power_exprt. More...
 
const factorial_power_exprtto_factorial_power_expr (const exprt &expr)
 Cast a generic exprt to a factorial_power_exprt. More...
 
factorial_power_exprtto_factorial_expr (exprt &expr)
 Cast a generic exprt to a factorial_power_exprt. More...
 
const equal_exprtto_equal_expr (const exprt &expr)
 Cast a generic exprt to an equal_exprt. More...
 
equal_exprtto_equal_expr (exprt &expr)
 Cast a generic exprt to an equal_exprt. More...
 
const notequal_exprtto_notequal_expr (const exprt &expr)
 Cast a generic exprt to an notequal_exprt. More...
 
notequal_exprtto_notequal_expr (exprt &expr)
 Cast a generic exprt to an notequal_exprt. More...
 
const index_exprtto_index_expr (const exprt &expr)
 Cast a generic exprt to an index_exprt. More...
 
index_exprtto_index_expr (exprt &expr)
 Cast a generic exprt to an index_exprt. More...
 
const array_of_exprtto_array_of_expr (const exprt &expr)
 Cast a generic exprt to an array_of_exprt. More...
 
array_of_exprtto_array_of_expr (exprt &expr)
 Cast a generic exprt to an array_of_exprt. More...
 
const array_exprtto_array_expr (const exprt &expr)
 Cast a generic exprt to an array_exprt. More...
 
array_exprtto_array_expr (exprt &expr)
 Cast a generic exprt to an array_exprt. More...
 
const vector_exprtto_vector_expr (const exprt &expr)
 Cast a generic exprt to an vector_exprt. More...
 
vector_exprtto_vector_expr (exprt &expr)
 Cast a generic exprt to an vector_exprt. More...
 
const union_exprtto_union_expr (const exprt &expr)
 Cast a generic exprt to a union_exprt. More...
 
union_exprtto_union_expr (exprt &expr)
 Cast a generic exprt to a union_exprt. More...
 
const struct_exprtto_struct_expr (const exprt &expr)
 Cast a generic exprt to a struct_exprt. More...
 
struct_exprtto_struct_expr (exprt &expr)
 Cast a generic exprt to a struct_exprt. More...
 
const complex_exprtto_complex_expr (const exprt &expr)
 Cast a generic exprt to a complex_exprt. More...
 
complex_exprtto_complex_expr (exprt &expr)
 Cast a generic exprt to a complex_exprt. More...
 
const object_descriptor_exprtto_object_descriptor_expr (const exprt &expr)
 Cast a generic exprt to an object_descriptor_exprt. More...
 
object_descriptor_exprtto_object_descriptor_expr (exprt &expr)
 Cast a generic exprt to an object_descriptor_exprt. More...
 
const dynamic_object_exprtto_dynamic_object_expr (const exprt &expr)
 Cast a generic exprt to a dynamic_object_exprt. More...
 
dynamic_object_exprtto_dynamic_object_expr (exprt &expr)
 Cast a generic exprt to a dynamic_object_exprt. More...
 
const typecast_exprtto_typecast_expr (const exprt &expr)
 Cast a generic exprt to a typecast_exprt. More...
 
typecast_exprtto_typecast_expr (exprt &expr)
 Cast a generic exprt to a typecast_exprt. More...
 
const floatbv_typecast_exprtto_floatbv_typecast_expr (const exprt &expr)
 Cast a generic exprt to a floatbv_typecast_exprt. More...
 
floatbv_typecast_exprtto_floatbv_typecast_expr (exprt &expr)
 Cast a generic exprt to a floatbv_typecast_exprt. More...
 
exprt conjunction (const exprt::operandst &)
 
const and_exprtto_and_expr (const exprt &expr)
 Cast a generic exprt to a and_exprt. More...
 
and_exprtto_and_expr (exprt &expr)
 Cast a generic exprt to a and_exprt. More...
 
const implies_exprtto_implies_expr (const exprt &expr)
 Cast a generic exprt to a implies_exprt. More...
 
implies_exprtto_implies_expr (exprt &expr)
 Cast a generic exprt to a implies_exprt. More...
 
exprt disjunction (const exprt::operandst &)
 
const or_exprtto_or_expr (const exprt &expr)
 Cast a generic exprt to a or_exprt. More...
 
or_exprtto_or_expr (exprt &expr)
 Cast a generic exprt to a or_exprt. More...
 
const bitnot_exprtto_bitnot_expr (const exprt &expr)
 Cast a generic exprt to a bitnot_exprt. More...
 
bitnot_exprtto_bitnot_expr (exprt &expr)
 Cast a generic exprt to a bitnot_exprt. More...
 
const bitor_exprtto_bitor_expr (const exprt &expr)
 Cast a generic exprt to a bitor_exprt. More...
 
bitor_exprtto_bitor_expr (exprt &expr)
 Cast a generic exprt to a bitor_exprt. More...
 
const bitxor_exprtto_bitxor_expr (const exprt &expr)
 Cast a generic exprt to a bitxor_exprt. More...
 
bitxor_exprtto_bitxor_expr (exprt &expr)
 Cast a generic exprt to a bitxor_exprt. More...
 
const bitand_exprtto_bitand_expr (const exprt &expr)
 Cast a generic exprt to a bitand_exprt. More...
 
bitand_exprtto_bitand_expr (exprt &expr)
 Cast a generic exprt to a bitand_exprt. More...
 
const shift_exprtto_shift_expr (const exprt &expr)
 Cast a generic exprt to a shift_exprt. More...
 
shift_exprtto_shift_expr (exprt &expr)
 Cast a generic exprt to a shift_exprt. More...
 
const replication_exprtto_replication_expr (const exprt &expr)
 Cast a generic exprt to a replication_exprt. More...
 
replication_exprtto_replication_expr (exprt &expr)
 Cast a generic exprt to a replication_exprt. More...
 
const extractbit_exprtto_extractbit_expr (const exprt &expr)
 Cast a generic exprt to an extractbit_exprt. More...
 
extractbit_exprtto_extractbit_expr (exprt &expr)
 Cast a generic exprt to an extractbit_exprt. More...
 
const extractbits_exprtto_extractbits_expr (const exprt &expr)
 Cast a generic exprt to an extractbits_exprt. More...
 
extractbits_exprtto_extractbits_expr (exprt &expr)
 Cast a generic exprt to an extractbits_exprt. More...
 
const address_of_exprtto_address_of_expr (const exprt &expr)
 Cast a generic exprt to an address_of_exprt. More...
 
address_of_exprtto_address_of_expr (exprt &expr)
 Cast a generic exprt to an address_of_exprt. More...
 
const not_exprtto_not_expr (const exprt &expr)
 Cast a generic exprt to an not_exprt. More...
 
not_exprtto_not_expr (exprt &expr)
 Cast a generic exprt to an not_exprt. More...
 
const dereference_exprtto_dereference_expr (const exprt &expr)
 Cast a generic exprt to a dereference_exprt. More...
 
dereference_exprtto_dereference_expr (exprt &expr)
 Cast a generic exprt to a dereference_exprt. More...
 
const if_exprtto_if_expr (const exprt &expr)
 Cast a generic exprt to an if_exprt. More...
 
if_exprtto_if_expr (exprt &expr)
 Cast a generic exprt to an if_exprt. More...
 
const with_exprtto_with_expr (const exprt &expr)
 Cast a generic exprt to a with_exprt. More...
 
with_exprtto_with_expr (exprt &expr)
 Cast a generic exprt to a with_exprt. More...
 
const index_designatortto_index_designator (const exprt &expr)
 Cast a generic exprt to an index_designatort. More...
 
index_designatortto_index_designator (exprt &expr)
 Cast a generic exprt to an index_designatort. More...
 
const member_designatortto_member_designator (const exprt &expr)
 Cast a generic exprt to an member_designatort. More...
 
member_designatortto_member_designator (exprt &expr)
 Cast a generic exprt to an member_designatort. More...
 
const update_exprtto_update_expr (const exprt &expr)
 Cast a generic exprt to an update_exprt. More...
 
update_exprtto_update_expr (exprt &expr)
 Cast a generic exprt to an update_exprt. More...
 
const member_exprtto_member_expr (const exprt &expr)
 Cast a generic exprt to a member_exprt. More...
 
member_exprtto_member_expr (exprt &expr)
 Cast a generic exprt to a member_exprt. More...
 
const isnan_exprtto_isnan_expr (const exprt &expr)
 Cast a generic exprt to a isnan_exprt. More...
 
isnan_exprtto_isnan_expr (exprt &expr)
 Cast a generic exprt to a isnan_exprt. More...
 
const isinf_exprtto_isinf_expr (const exprt &expr)
 Cast a generic exprt to a isinf_exprt. More...
 
isinf_exprtto_isinf_expr (exprt &expr)
 Cast a generic exprt to a isinf_exprt. More...
 
const isfinite_exprtto_isfinite_expr (const exprt &expr)
 Cast a generic exprt to a isfinite_exprt. More...
 
isfinite_exprtto_isfinite_expr (exprt &expr)
 Cast a generic exprt to a isfinite_exprt. More...
 
const isnormal_exprtto_isnormal_expr (const exprt &expr)
 Cast a generic exprt to a isnormal_exprt. More...
 
isnormal_exprtto_isnormal_expr (exprt &expr)
 Cast a generic exprt to a isnormal_exprt. More...
 
const ieee_float_equal_exprtto_ieee_float_equal_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_equal_exprt. More...
 
ieee_float_equal_exprtto_ieee_float_equal_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_equal_exprt. More...
 
const ieee_float_notequal_exprtto_ieee_float_notequal_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_notequal_exprt. More...
 
ieee_float_notequal_exprtto_ieee_float_notequal_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_notequal_exprt. More...
 
const ieee_float_op_exprtto_ieee_float_op_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_op_exprt. More...
 
ieee_float_op_exprtto_ieee_float_op_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_op_exprt. More...
 
const constant_exprtto_constant_expr (const exprt &expr)
 Cast a generic exprt to a constant_exprt. More...
 
constant_exprtto_constant_expr (exprt &expr)
 Cast a generic exprt to a constant_exprt. More...
 
const function_application_exprtto_function_application_expr (const exprt &expr)
 Cast a generic exprt to a function_application_exprt. More...
 
function_application_exprtto_function_application_expr (exprt &expr)
 Cast a generic exprt to a function_application_exprt. More...
 
const concatenation_exprtto_concatenation_expr (const exprt &expr)
 Cast a generic exprt to a concatenation_exprt. More...
 
concatenation_exprtto_concatenation_expr (exprt &expr)
 Cast a generic exprt to a concatenation_exprt. More...
 
const let_exprtto_let_expr (const exprt &expr)
 Cast a generic exprt to a let_exprt. More...
 
let_exprtto_let_expr (exprt &expr)
 Cast a generic exprt to a let_exprt. More...
 

Detailed Description

API to expression classes.

Author
Daniel Kroening kroen.nosp@m.ing@.nosp@m.kroen.nosp@m.ing..nosp@m.com
Date
Sun Jul 31 21:54:44 BST 2011

Definition in file std_expr.h.

Function Documentation

◆ conjunction()

◆ disjunction()