std_expr.h File Reference

API to expression classes. More...

#include "expr_cast.h"
#include "invariant.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	symbol_exprt
	Expression to hold a symbol (variable) More...
struct	std::hash<::symbol_exprt >
class	decorated_symbol_exprt
	Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local. More...
class	nondet_symbol_exprt
	Expression to hold a nondeterministic choice. More...
class	unary_exprt
	Generic base class for unary expressions. More...
class	abs_exprt
	Absolute value. More...
class	unary_minus_exprt
	The unary minus expression. More...
class	unary_plus_exprt
	The unary plus expression. More...
class	predicate_exprt
	A base class for expressions that are predicates, i.e., Boolean-typed. More...
class	unary_predicate_exprt
	A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument. More...
class	sign_exprt
	Sign of an expression Predicate is true if _op is negative, false otherwise. More...
class	binary_exprt
	A base class for binary expressions. More...
class	binary_predicate_exprt
	A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments. More...
class	binary_relation_exprt
	A base class for relations, i.e., binary predicates whose two operands have the same type. More...
class	greater_than_exprt
	Binary greater than operator expression. More...
class	greater_than_or_equal_exprt
	Binary greater than or equal operator expression. More...
class	less_than_exprt
	Binary less than operator expression. More...
class	less_than_or_equal_exprt
	Binary less than or equal operator expression. 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 defined as lhs-(rhs * truncate(lhs/rhs)). More...
class	euclidean_mod_exprt
	Boute's Euclidean definition of Modulo – to match SMT-LIB2. 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	empty_union_exprt
	Union constructor to support unions without any member (a GCC/Clang feature). More...
class	struct_exprt
	Struct constructor from list of elements. More...
class	complex_exprt
	Complex constructor from a pair of numbers. More...
class	complex_real_exprt
	Real part of the expression describing a complex number. More...
class	complex_imag_exprt
	Imaginary part of the expression describing a complex number. More...
class	typecast_exprt
	Semantic type conversion. More...
class	and_exprt
	Boolean AND. More...
class	nand_exprt
	Boolean NAND. More...
class	implies_exprt
	Boolean implication. More...
class	or_exprt
	Boolean OR. More...
class	nor_exprt
	Boolean NOR. More...
class	xor_exprt
	Boolean XOR. More...
class	xnor_exprt
	Boolean XNOR. More...
class	not_exprt
	Boolean negation. More...
class	if_exprt
	The trinary if-then-else operator. More...
class	with_exprt
	Operator to update elements in structs and arrays. More...
class	index_designatort
class	member_designatort
class	update_exprt
	Operator to update elements in structs and arrays. More...
class	member_exprt
	Extract member of struct or union. More...
class	type_exprt
	An expression denoting a type. More...
class	constant_exprt
	A constant literal expression. More...
class	true_exprt
	The Boolean constant true. More...
class	false_exprt
	The Boolean constant false. More...
class	nil_exprt
	The NIL expression. More...
class	infinity_exprt
	An expression denoting infinity. More...
class	binding_exprt
	A base class for variable bindings (quantifiers, let, lambda) More...
class	let_exprt
	A let expression. More...
class	cond_exprt
	this is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true. More...
class	array_comprehension_exprt
	Expression to define a mapping from an argument (index) to elements. More...
class	class_method_descriptor_exprt
	An expression describing a method on a class. More...
class	named_term_exprt
	Expression that introduces a new symbol that is equal to the operand. More...

Namespaces
namespace	std
	STL namespace.

Functions
const ternary_exprt &	to_ternary_expr (const exprt &expr)
	Cast an exprt to a ternary_exprt.
ternary_exprt &	to_ternary_expr (exprt &expr)
	Cast an exprt to a ternary_exprt.
template<>
bool	can_cast_expr< symbol_exprt > (const exprt &base)
void	validate_expr (const symbol_exprt &value)
const symbol_exprt &	to_symbol_expr (const exprt &expr)
	Cast an exprt to a symbol_exprt.
symbol_exprt &	to_symbol_expr (exprt &expr)
	Cast an exprt to a symbol_exprt.
template<>
bool	can_cast_expr< nondet_symbol_exprt > (const exprt &base)
void	validate_expr (const nondet_symbol_exprt &value)
const nondet_symbol_exprt &	to_nondet_symbol_expr (const exprt &expr)
	Cast an exprt to a nondet_symbol_exprt.
nondet_symbol_exprt &	to_nondet_symbol_expr (exprt &expr)
	Cast an exprt to a nondet_symbol_exprt.
template<>
bool	can_cast_expr< unary_exprt > (const exprt &base)
void	validate_expr (const unary_exprt &value)
const unary_exprt &	to_unary_expr (const exprt &expr)
	Cast an exprt to a unary_exprt.
unary_exprt &	to_unary_expr (exprt &expr)
	Cast an exprt to a unary_exprt.
template<>
bool	can_cast_expr< abs_exprt > (const exprt &base)
void	validate_expr (const abs_exprt &value)
const abs_exprt &	to_abs_expr (const exprt &expr)
	Cast an exprt to a abs_exprt.
abs_exprt &	to_abs_expr (exprt &expr)
	Cast an exprt to a abs_exprt.
template<>
bool	can_cast_expr< unary_minus_exprt > (const exprt &base)
void	validate_expr (const unary_minus_exprt &value)
const unary_minus_exprt &	to_unary_minus_expr (const exprt &expr)
	Cast an exprt to a unary_minus_exprt.
unary_minus_exprt &	to_unary_minus_expr (exprt &expr)
	Cast an exprt to a unary_minus_exprt.
template<>
bool	can_cast_expr< unary_plus_exprt > (const exprt &base)
void	validate_expr (const unary_plus_exprt &value)
const unary_plus_exprt &	to_unary_plus_expr (const exprt &expr)
	Cast an exprt to a unary_plus_exprt.
unary_plus_exprt &	to_unary_plus_expr (exprt &expr)
	Cast an exprt to a unary_minus_exprt.
template<>
bool	can_cast_expr< sign_exprt > (const exprt &base)
void	validate_expr (const sign_exprt &expr)
const sign_exprt &	to_sign_expr (const exprt &expr)
	Cast an exprt to a sign_exprt.
sign_exprt &	to_sign_expr (exprt &expr)
	Cast an exprt to a sign_exprt.
template<>
bool	can_cast_expr< binary_exprt > (const exprt &base)
void	validate_expr (const binary_exprt &value)
const binary_exprt &	to_binary_expr (const exprt &expr)
	Cast an exprt to a binary_exprt.
binary_exprt &	to_binary_expr (exprt &expr)
	Cast an exprt to a binary_exprt.
template<>
bool	can_cast_expr< binary_relation_exprt > (const exprt &base)
void	validate_expr (const binary_relation_exprt &value)
template<>
bool	can_cast_expr< greater_than_exprt > (const exprt &base)
void	validate_expr (const greater_than_exprt &value)
template<>
bool	can_cast_expr< greater_than_or_equal_exprt > (const exprt &base)
void	validate_expr (const greater_than_or_equal_exprt &value)
template<>
bool	can_cast_expr< less_than_exprt > (const exprt &base)
void	validate_expr (const less_than_exprt &value)
template<>
bool	can_cast_expr< less_than_or_equal_exprt > (const exprt &base)
void	validate_expr (const less_than_or_equal_exprt &value)
const binary_relation_exprt &	to_binary_relation_expr (const exprt &expr)
	Cast an exprt to a binary_relation_exprt.
binary_relation_exprt &	to_binary_relation_expr (exprt &expr)
	Cast an exprt to a binary_relation_exprt.
const multi_ary_exprt &	to_multi_ary_expr (const exprt &expr)
	Cast an exprt to a multi_ary_exprt.
multi_ary_exprt &	to_multi_ary_expr (exprt &expr)
	Cast an exprt to a multi_ary_exprt.
template<>
bool	can_cast_expr< plus_exprt > (const exprt &base)
void	validate_expr (const plus_exprt &value)
const plus_exprt &	to_plus_expr (const exprt &expr)
	Cast an exprt to a plus_exprt.
plus_exprt &	to_plus_expr (exprt &expr)
	Cast an exprt to a plus_exprt.
template<>
bool	can_cast_expr< minus_exprt > (const exprt &base)
void	validate_expr (const minus_exprt &value)
const minus_exprt &	to_minus_expr (const exprt &expr)
	Cast an exprt to a minus_exprt.
minus_exprt &	to_minus_expr (exprt &expr)
	Cast an exprt to a minus_exprt.
template<>
bool	can_cast_expr< mult_exprt > (const exprt &base)
void	validate_expr (const mult_exprt &value)
const mult_exprt &	to_mult_expr (const exprt &expr)
	Cast an exprt to a mult_exprt.
mult_exprt &	to_mult_expr (exprt &expr)
	Cast an exprt to a mult_exprt.
template<>
bool	can_cast_expr< div_exprt > (const exprt &base)
void	validate_expr (const div_exprt &value)
const div_exprt &	to_div_expr (const exprt &expr)
	Cast an exprt to a div_exprt.
div_exprt &	to_div_expr (exprt &expr)
	Cast an exprt to a div_exprt.
template<>
bool	can_cast_expr< mod_exprt > (const exprt &base)
void	validate_expr (const mod_exprt &value)
const mod_exprt &	to_mod_expr (const exprt &expr)
	Cast an exprt to a mod_exprt.
mod_exprt &	to_mod_expr (exprt &expr)
	Cast an exprt to a mod_exprt.
template<>
bool	can_cast_expr< euclidean_mod_exprt > (const exprt &base)
void	validate_expr (const euclidean_mod_exprt &value)
const euclidean_mod_exprt &	to_euclidean_mod_expr (const exprt &expr)
	Cast an exprt to a euclidean_mod_exprt.
euclidean_mod_exprt &	to_euclidean_mod_expr (exprt &expr)
	Cast an exprt to a euclidean_mod_exprt.
template<>
bool	can_cast_expr< equal_exprt > (const exprt &base)
void	validate_expr (const equal_exprt &value)
const equal_exprt &	to_equal_expr (const exprt &expr)
	Cast an exprt to an equal_exprt.
equal_exprt &	to_equal_expr (exprt &expr)
	Cast an exprt to an equal_exprt.
template<>
bool	can_cast_expr< notequal_exprt > (const exprt &base)
void	validate_expr (const notequal_exprt &value)
const notequal_exprt &	to_notequal_expr (const exprt &expr)
	Cast an exprt to an notequal_exprt.
notequal_exprt &	to_notequal_expr (exprt &expr)
	Cast an exprt to an notequal_exprt.
template<>
bool	can_cast_expr< index_exprt > (const exprt &base)
void	validate_expr (const index_exprt &value)
const index_exprt &	to_index_expr (const exprt &expr)
	Cast an exprt to an index_exprt.
index_exprt &	to_index_expr (exprt &expr)
	Cast an exprt to an index_exprt.
template<>
bool	can_cast_expr< array_of_exprt > (const exprt &base)
void	validate_expr (const array_of_exprt &value)
const array_of_exprt &	to_array_of_expr (const exprt &expr)
	Cast an exprt to an array_of_exprt.
array_of_exprt &	to_array_of_expr (exprt &expr)
	Cast an exprt to an array_of_exprt.
template<>
bool	can_cast_expr< array_exprt > (const exprt &base)
const array_exprt &	to_array_expr (const exprt &expr)
	Cast an exprt to an array_exprt.
array_exprt &	to_array_expr (exprt &expr)
	Cast an exprt to an array_exprt.
template<>
bool	can_cast_expr< array_list_exprt > (const exprt &base)
void	validate_expr (const array_list_exprt &value)
const array_list_exprt &	to_array_list_expr (const exprt &expr)
array_list_exprt &	to_array_list_expr (exprt &expr)
template<>
bool	can_cast_expr< vector_exprt > (const exprt &base)
const vector_exprt &	to_vector_expr (const exprt &expr)
	Cast an exprt to an vector_exprt.
vector_exprt &	to_vector_expr (exprt &expr)
	Cast an exprt to an vector_exprt.
template<>
bool	can_cast_expr< union_exprt > (const exprt &base)
void	validate_expr (const union_exprt &value)
const union_exprt &	to_union_expr (const exprt &expr)
	Cast an exprt to a union_exprt.
union_exprt &	to_union_expr (exprt &expr)
	Cast an exprt to a union_exprt.
template<>
bool	can_cast_expr< empty_union_exprt > (const exprt &base)
void	validate_expr (const empty_union_exprt &value)
const empty_union_exprt &	to_empty_union_expr (const exprt &expr)
	Cast an exprt to an empty_union_exprt.
empty_union_exprt &	to_empty_union_expr (exprt &expr)
	Cast an exprt to an empty_union_exprt.
template<>
bool	can_cast_expr< struct_exprt > (const exprt &base)
const struct_exprt &	to_struct_expr (const exprt &expr)
	Cast an exprt to a struct_exprt.
struct_exprt &	to_struct_expr (exprt &expr)
	Cast an exprt to a struct_exprt.
template<>
bool	can_cast_expr< complex_exprt > (const exprt &base)
void	validate_expr (const complex_exprt &value)
const complex_exprt &	to_complex_expr (const exprt &expr)
	Cast an exprt to a complex_exprt.
complex_exprt &	to_complex_expr (exprt &expr)
	Cast an exprt to a complex_exprt.
template<>
bool	can_cast_expr< complex_real_exprt > (const exprt &base)
void	validate_expr (const complex_real_exprt &expr)
const complex_real_exprt &	to_complex_real_expr (const exprt &expr)
	Cast an exprt to a complex_real_exprt.
complex_real_exprt &	to_complex_real_expr (exprt &expr)
	Cast an exprt to a complex_real_exprt.
template<>
bool	can_cast_expr< complex_imag_exprt > (const exprt &base)
void	validate_expr (const complex_imag_exprt &expr)
const complex_imag_exprt &	to_complex_imag_expr (const exprt &expr)
	Cast an exprt to a complex_imag_exprt.
complex_imag_exprt &	to_complex_imag_expr (exprt &expr)
	Cast an exprt to a complex_imag_exprt.
template<>
bool	can_cast_expr< typecast_exprt > (const exprt &base)
void	validate_expr (const typecast_exprt &value)
const typecast_exprt &	to_typecast_expr (const exprt &expr)
	Cast an exprt to a typecast_exprt.
typecast_exprt &	to_typecast_expr (exprt &expr)
	Cast an exprt to a typecast_exprt.
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
exprt	conjunction (exprt a, exprt b)
	Conjunction of two expressions.
template<>
bool	can_cast_expr< and_exprt > (const exprt &base)
const and_exprt &	to_and_expr (const exprt &expr)
	Cast an exprt to a and_exprt.
and_exprt &	to_and_expr (exprt &expr)
	Cast an exprt to a and_exprt.
const nand_exprt &	to_nand_expr (const exprt &expr)
	Cast an exprt to a nand_exprt.
nand_exprt &	to_nand_expr (exprt &expr)
	Cast an exprt to a nand_exprt.
template<>
bool	can_cast_expr< implies_exprt > (const exprt &base)
void	validate_expr (const implies_exprt &value)
const implies_exprt &	to_implies_expr (const exprt &expr)
	Cast an exprt to a implies_exprt.
implies_exprt &	to_implies_expr (exprt &expr)
	Cast an exprt to a implies_exprt.
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
template<>
bool	can_cast_expr< or_exprt > (const exprt &base)
const or_exprt &	to_or_expr (const exprt &expr)
	Cast an exprt to a or_exprt.
or_exprt &	to_or_expr (exprt &expr)
	Cast an exprt to a or_exprt.
const nor_exprt &	to_nor_expr (const exprt &expr)
	Cast an exprt to a nor_exprt.
nor_exprt &	to_nor_expr (exprt &expr)
	Cast an exprt to a nor_exprt.
template<>
bool	can_cast_expr< xor_exprt > (const exprt &base)
const xor_exprt &	to_xor_expr (const exprt &expr)
	Cast an exprt to a xor_exprt.
xor_exprt &	to_xor_expr (exprt &expr)
	Cast an exprt to a xor_exprt.
template<>
bool	can_cast_expr< xnor_exprt > (const exprt &base)
const xnor_exprt &	to_xnor_expr (const exprt &expr)
	Cast an exprt to a xnor_exprt.
xnor_exprt &	to_xnor_expr (exprt &expr)
	Cast an exprt to a xnor_exprt.
template<>
bool	can_cast_expr< not_exprt > (const exprt &base)
void	validate_expr (const not_exprt &value)
const not_exprt &	to_not_expr (const exprt &expr)
	Cast an exprt to an not_exprt.
not_exprt &	to_not_expr (exprt &expr)
	Cast an exprt to an not_exprt.
template<>
bool	can_cast_expr< if_exprt > (const exprt &base)
void	validate_expr (const if_exprt &value)
const if_exprt &	to_if_expr (const exprt &expr)
	Cast an exprt to an if_exprt.
if_exprt &	to_if_expr (exprt &expr)
	Cast an exprt to an if_exprt.
template<>
bool	can_cast_expr< with_exprt > (const exprt &base)
void	validate_expr (const with_exprt &value)
const with_exprt &	to_with_expr (const exprt &expr)
	Cast an exprt to a with_exprt.
with_exprt &	to_with_expr (exprt &expr)
	Cast an exprt to a with_exprt.
template<>
bool	can_cast_expr< index_designatort > (const exprt &base)
void	validate_expr (const index_designatort &value)
const index_designatort &	to_index_designator (const exprt &expr)
	Cast an exprt to an index_designatort.
index_designatort &	to_index_designator (exprt &expr)
	Cast an exprt to an index_designatort.
template<>
bool	can_cast_expr< member_designatort > (const exprt &base)
void	validate_expr (const member_designatort &value)
const member_designatort &	to_member_designator (const exprt &expr)
	Cast an exprt to an member_designatort.
member_designatort &	to_member_designator (exprt &expr)
	Cast an exprt to an member_designatort.
template<>
bool	can_cast_expr< update_exprt > (const exprt &base)
void	validate_expr (const update_exprt &value)
const update_exprt &	to_update_expr (const exprt &expr)
	Cast an exprt to an update_exprt.
update_exprt &	to_update_expr (exprt &expr)
	Cast an exprt to an update_exprt.
template<>
bool	can_cast_expr< member_exprt > (const exprt &base)
void	validate_expr (const member_exprt &value)
const member_exprt &	to_member_expr (const exprt &expr)
	Cast an exprt to a member_exprt.
member_exprt &	to_member_expr (exprt &expr)
	Cast an exprt to a member_exprt.
template<>
bool	can_cast_expr< type_exprt > (const exprt &base)
const type_exprt &	to_type_expr (const exprt &expr)
	Cast an exprt to an type_exprt.
type_exprt &	to_type_expr (exprt &expr)
	Cast an exprt to an type_exprt.
template<>
bool	can_cast_expr< constant_exprt > (const exprt &base)
void	validate_expr (const constant_exprt &value)
const constant_exprt &	to_constant_expr (const exprt &expr)
	Cast an exprt to a constant_exprt.
constant_exprt &	to_constant_expr (exprt &expr)
	Cast an exprt to a constant_exprt.
bool	operator== (const exprt &lhs, bool rhs)
	Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.
bool	operator!= (const exprt &lhs, bool rhs)
	Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.
bool	operator== (const exprt &lhs, int rhs)
	Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs.
bool	operator!= (const exprt &lhs, int rhs)
	Returns the negation of operator==(const exprt &, int).
bool	operator== (const exprt &lhs, std::nullptr_t)
	Return whether the expression lhs is a constant representing the NULL pointer.
bool	operator!= (const exprt &lhs, std::nullptr_t)
	Returns the negation of operator==(const exprt &, std::nullptr_t).
template<>
bool	can_cast_expr< nil_exprt > (const exprt &base)
template<>
bool	can_cast_expr< binding_exprt > (const exprt &base)
void	validate_expr (const binding_exprt &binding_expr)
const binding_exprt &	to_binding_expr (const exprt &expr)
	Cast an exprt to a binding_exprt.
binding_exprt &	to_binding_expr (exprt &expr)
	Cast an exprt to a binding_exprt.
template<>
bool	can_cast_expr< let_exprt > (const exprt &base)
void	validate_expr (const let_exprt &let_expr)
const let_exprt &	to_let_expr (const exprt &expr)
	Cast an exprt to a let_exprt.
let_exprt &	to_let_expr (exprt &expr)
	Cast an exprt to a let_exprt.
template<>
bool	can_cast_expr< cond_exprt > (const exprt &base)
void	validate_expr (const cond_exprt &value)
const cond_exprt &	to_cond_expr (const exprt &expr)
	Cast an exprt to a cond_exprt.
cond_exprt &	to_cond_expr (exprt &expr)
	Cast an exprt to a cond_exprt.
template<>
bool	can_cast_expr< array_comprehension_exprt > (const exprt &base)
void	validate_expr (const array_comprehension_exprt &value)
const array_comprehension_exprt &	to_array_comprehension_expr (const exprt &expr)
	Cast an exprt to a array_comprehension_exprt.
array_comprehension_exprt &	to_array_comprehension_expr (exprt &expr)
	Cast an exprt to a array_comprehension_exprt.
void	validate_expr (const class class_method_descriptor_exprt &value)
const class_method_descriptor_exprt &	to_class_method_descriptor_expr (const exprt &expr)
	Cast an exprt to a class_method_descriptor_exprt.
template<>
bool	can_cast_expr< class_method_descriptor_exprt > (const exprt &base)
template<>
bool	can_cast_expr< named_term_exprt > (const exprt &base)
void	validate_expr (const named_term_exprt &value)
const named_term_exprt &	to_named_term_expr (const exprt &expr)
	Cast an exprt to a named_term_exprt.
named_term_exprt &	to_named_term_expr (exprt &expr)
	Cast an exprt to a array_comprehension_exprt.

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 450 of file std_expr.h.

can_cast_expr< and_exprt >()

template<>

bool can_cast_expr< and_exprt > ( const exprt &  base )

inline

Definition at line 2166 of file std_expr.h.

can_cast_expr< array_comprehension_exprt >()

template<>

bool can_cast_expr< array_comprehension_exprt > ( const exprt &  base )

inline

Definition at line 3640 of file std_expr.h.

can_cast_expr< array_exprt >()

template<>

bool can_cast_expr< array_exprt > ( const exprt &  base )

inline

Definition at line 1654 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 1706 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 1587 of file std_expr.h.

can_cast_expr< binary_exprt >()

template<>

bool can_cast_expr< binary_exprt > ( const exprt &  base )

inline

Definition at line 699 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 795 of file std_expr.h.

can_cast_expr< binding_exprt >()

template<>

bool can_cast_expr< binding_exprt > ( const exprt &  base )

inline

Definition at line 3332 of file std_expr.h.

can_cast_expr< class_method_descriptor_exprt >()

template<>

bool can_cast_expr< class_method_descriptor_exprt > ( const exprt &  base )

inline

Definition at line 3778 of file std_expr.h.

can_cast_expr< complex_exprt >()

template<>

bool can_cast_expr< complex_exprt > ( const exprt &  base )

inline

Definition at line 1949 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 2036 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 1993 of file std_expr.h.

can_cast_expr< cond_exprt >()

template<>

bool can_cast_expr< cond_exprt > ( const exprt &  base )

inline

Definition at line 3547 of file std_expr.h.

can_cast_expr< constant_exprt >()

template<>

bool can_cast_expr< constant_exprt > ( const exprt &  base )

inline

Definition at line 3173 of file std_expr.h.

can_cast_expr< div_exprt >()

template<>

bool can_cast_expr< div_exprt > ( const exprt &  base )

inline

Definition at line 1190 of file std_expr.h.

can_cast_expr< empty_union_exprt >()

template<>

bool can_cast_expr< empty_union_exprt > ( const exprt &  base )

inline

Definition at line 1843 of file std_expr.h.

can_cast_expr< equal_exprt >()

template<>

bool can_cast_expr< equal_exprt > ( const exprt &  base )

inline

Definition at line 1391 of file std_expr.h.

can_cast_expr< euclidean_mod_exprt >()

template<>

bool can_cast_expr< euclidean_mod_exprt > ( const exprt &  base )

inline

Definition at line 1329 of file std_expr.h.

can_cast_expr< greater_than_exprt >()

template<>

bool can_cast_expr< greater_than_exprt > ( const exprt &  base )

inline

Definition at line 816 of file std_expr.h.

can_cast_expr< greater_than_or_equal_exprt >()

template<>

bool can_cast_expr< greater_than_or_equal_exprt > ( const exprt &  base )

inline

Definition at line 837 of file std_expr.h.

can_cast_expr< if_exprt >()

template<>

bool can_cast_expr< if_exprt > ( const exprt &  base )

inline

Definition at line 2566 of file std_expr.h.

can_cast_expr< implies_exprt >()

template<>

bool can_cast_expr< implies_exprt > ( const exprt &  base )

inline

Definition at line 2239 of file std_expr.h.

can_cast_expr< index_designatort >()

template<>

bool can_cast_expr< index_designatort > ( const exprt &  base )

inline

Definition at line 2698 of file std_expr.h.

can_cast_expr< index_exprt >()

template<>

bool can_cast_expr< index_exprt > ( const exprt &  base )

inline

Definition at line 1522 of file std_expr.h.

can_cast_expr< less_than_exprt >()

template<>

bool can_cast_expr< less_than_exprt > ( const exprt &  base )

inline

Definition at line 858 of file std_expr.h.

can_cast_expr< less_than_or_equal_exprt >()

template<>

bool can_cast_expr< less_than_or_equal_exprt > ( const exprt &  base )

inline

Definition at line 879 of file std_expr.h.

can_cast_expr< let_exprt >()

template<>

bool can_cast_expr< let_exprt > ( const exprt &  base )

inline

Definition at line 3486 of file std_expr.h.

can_cast_expr< member_designatort >()

template<>

bool can_cast_expr< member_designatort > ( const exprt &  base )

inline

Definition at line 2747 of file std_expr.h.

can_cast_expr< member_exprt >()

template<>

bool can_cast_expr< member_exprt > ( const exprt &  base )

inline

Definition at line 3048 of file std_expr.h.

can_cast_expr< minus_exprt >()

template<>

bool can_cast_expr< minus_exprt > ( const exprt &  base )

inline

Definition at line 1070 of file std_expr.h.

can_cast_expr< mod_exprt >()

template<>

bool can_cast_expr< mod_exprt > ( const exprt &  base )

inline

Definition at line 1261 of file std_expr.h.

can_cast_expr< mult_exprt >()

template<>

bool can_cast_expr< mult_exprt > ( const exprt &  base )

inline

Definition at line 1121 of file std_expr.h.

can_cast_expr< named_term_exprt >()

template<>

bool can_cast_expr< named_term_exprt > ( const exprt &  base )

inline

Definition at line 3823 of file std_expr.h.

can_cast_expr< nil_exprt >()

template<>

bool can_cast_expr< nil_exprt > ( const exprt &  base )

inline

Definition at line 3264 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 327 of file std_expr.h.

can_cast_expr< not_exprt >()

template<>

bool can_cast_expr< not_exprt > ( const exprt &  base )

inline

Definition at line 2468 of file std_expr.h.

can_cast_expr< notequal_exprt >()

template<>

bool can_cast_expr< notequal_exprt > ( const exprt &  base )

inline

Definition at line 1434 of file std_expr.h.

can_cast_expr< or_exprt >()

template<>

bool can_cast_expr< or_exprt > ( const exprt &  base )

inline

Definition at line 2311 of file std_expr.h.

can_cast_expr< plus_exprt >()

template<>

bool can_cast_expr< plus_exprt > ( const exprt &  base )

inline

Definition at line 1025 of file std_expr.h.

can_cast_expr< sign_exprt >()

template<>

bool can_cast_expr< sign_exprt > ( const exprt &  base )

inline

Definition at line 605 of file std_expr.h.

can_cast_expr< struct_exprt >()

template<>

bool can_cast_expr< struct_exprt > ( const exprt &  base )

inline

Definition at line 1889 of file std_expr.h.

can_cast_expr< symbol_exprt >()

template<>

bool can_cast_expr< symbol_exprt > ( const exprt &  base )

inline

Definition at line 256 of file std_expr.h.

can_cast_expr< type_exprt >()

template<>

bool can_cast_expr< type_exprt > ( const exprt &  base )

inline

Definition at line 3090 of file std_expr.h.

can_cast_expr< typecast_exprt >()

template<>

bool can_cast_expr< typecast_exprt > ( const exprt &  base )

inline

Definition at line 2091 of file std_expr.h.

can_cast_expr< unary_exprt >()

template<>

bool can_cast_expr< unary_exprt > ( const exprt &  base )

inline

Definition at line 410 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 498 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 540 of file std_expr.h.

can_cast_expr< union_exprt >()

template<>

bool can_cast_expr< union_exprt > ( const exprt &  base )

inline

Definition at line 1800 of file std_expr.h.

can_cast_expr< update_exprt >()

template<>

bool can_cast_expr< update_exprt > ( const exprt &  base )

inline

Definition at line 2849 of file std_expr.h.

can_cast_expr< vector_exprt >()

template<>

bool can_cast_expr< vector_exprt > ( const exprt &  base )

inline

Definition at line 1743 of file std_expr.h.

can_cast_expr< with_exprt >()

template<>

bool can_cast_expr< with_exprt > ( const exprt &  base )

inline

Definition at line 2645 of file std_expr.h.

can_cast_expr< xnor_exprt >()

template<>

bool can_cast_expr< xnor_exprt > ( const exprt &  base )

inline

Definition at line 2433 of file std_expr.h.

can_cast_expr< xor_exprt >()

template<>

bool can_cast_expr< xor_exprt > ( const exprt &  base )

inline

Definition at line 2389 of file std_expr.h.

conjunction() [1/2]

exprt conjunction

(

const exprt::operandst &

op

)

1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise

Definition at line 275 of file std_expr.cpp.

conjunction() [2/2]

exprt conjunction	(	exprt	a,
		exprt	b
	)

Conjunction of two expressions.

If the second is already an and_exprt add to its operands instead of creating a new expression. If one is true, return the other expression. If one is false returns false.

Definition at line 252 of file std_expr.cpp.

disjunction()

exprt disjunction

(

const exprt::operandst &

op

)

1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise

Definition at line 240 of file std_expr.cpp.

operator!=() [1/3]

bool operator!=	(	const exprt &	lhs,
		bool	rhs
	)

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.

Definition at line 37 of file std_expr.cpp.

operator!=() [2/3]

bool operator!=	(	const exprt &	lhs,
		int	rhs
	)

Returns the negation of operator==(const exprt &, int).

Definition at line 60 of file std_expr.cpp.

operator!=() [3/3]

bool operator!=	(	const exprt &	lhs,
		std::nullptr_t	rhs
	)

Returns the negation of operator==(const exprt &, std::nullptr_t).

Definition at line 192 of file std_expr.cpp.

operator==() [1/3]

bool operator==	(	const exprt &	lhs,
		bool	rhs
	)

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.

Definition at line 32 of file std_expr.cpp.

operator==() [2/3]

bool operator==	(	const exprt &	lhs,
		int	rhs
	)

Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs.

For value 0 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv, ID_pointer.
For ID_pointer, returns true iff the value is a zero string or a null pointer.
For value 1 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv.
For all other types, return false.

Definition at line 52 of file std_expr.cpp.

operator==() [3/3]

bool operator==	(	const exprt &	lhs,
		std::nullptr_t	rhs
	)

Return whether the expression lhs is a constant representing the NULL pointer.

Definition at line 186 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

expr	Source expression

Returns

Object of type abs_exprt

Definition at line 466 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

expr	Source expression

Returns

Object of type abs_exprt

Definition at line 474 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

expr	Source expression

Returns

Object of type and_exprt

Definition at line 2177 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

expr	Source expression

Returns

Object of type and_exprt

Definition at line 2184 of file std_expr.h.

to_array_comprehension_expr() [1/2]

const array_comprehension_exprt & to_array_comprehension_expr ( const exprt &  expr )

inline

Cast an exprt to a array_comprehension_exprt.

expr must be known to be array_comprehension_exprt.

Parameters

expr	Source expression

Returns

Object of type array_comprehension_exprt

Definition at line 3657 of file std_expr.h.

to_array_comprehension_expr() [2/2]

array_comprehension_exprt & to_array_comprehension_expr ( exprt &  expr )

inline

Cast an exprt to a array_comprehension_exprt.

expr must be known to be array_comprehension_exprt.

Parameters

expr	Source expression

Returns

Object of type array_comprehension_exprt

Definition at line 3667 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

expr	Source expression

Returns

Object of type array_exprt

Definition at line 1665 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

expr	Source expression

Returns

Object of type array_exprt

Definition at line 1672 of file std_expr.h.

to_array_list_expr() [1/2]

const array_list_exprt & to_array_list_expr ( const exprt &  expr )

inline

Definition at line 1716 of file std_expr.h.

to_array_list_expr() [2/2]

array_list_exprt & to_array_list_expr ( exprt &  expr )

inline

Definition at line 1724 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

expr	Source expression

Returns

Object of type array_of_exprt

Definition at line 1603 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

expr	Source expression

Returns

Object of type array_of_exprt

Definition at line 1611 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

expr	Source expression

Returns

Object of type binary_exprt

Definition at line 715 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

expr	Source expression

Returns

Object of type binary_exprt

Definition at line 722 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

expr	Source expression

Returns

Object of type binary_relation_exprt

Definition at line 895 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

expr	Source expression

Returns

Object of type binary_relation_exprt

Definition at line 902 of file std_expr.h.

to_binding_expr() [1/2]

const binding_exprt & to_binding_expr ( const exprt &  expr )

inline

Cast an exprt to a binding_exprt.

expr must be known to be binding_exprt.

Parameters

expr	Source expression

Returns

Object of type binding_exprt

Definition at line 3350 of file std_expr.h.

to_binding_expr() [2/2]

binding_exprt & to_binding_expr ( exprt &  expr )

inline

Cast an exprt to a binding_exprt.

expr must be known to be binding_exprt.

Parameters

expr	Source expression

Returns

Object of type binding_exprt

Definition at line 3366 of file std_expr.h.

to_class_method_descriptor_expr()

const class_method_descriptor_exprt & to_class_method_descriptor_expr ( const exprt &  expr )

inline

Cast an exprt to a class_method_descriptor_exprt.

expr must be known to be class_method_descriptor_exprt.

Parameters

expr	Source expression

Returns

Object of type class_method_descriptor_exprt

Definition at line 3770 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

expr	Source expression

Returns

Object of type complex_exprt

Definition at line 1965 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

expr	Source expression

Returns

Object of type complex_exprt

Definition at line 1974 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

expr	Source expression

Returns

Object of type complex_imag_exprt

Definition at line 2053 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

expr	Source expression

Returns

Object of type complex_imag_exprt

Definition at line 2062 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

expr	Source expression

Returns

Object of type complex_real_exprt

Definition at line 2010 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

expr	Source expression

Returns

Object of type complex_real_exprt

Definition at line 2018 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

expr	Source expression

Returns

Object of type cond_exprt

Definition at line 3564 of file std_expr.h.

to_cond_expr() [2/2]

cond_exprt & to_cond_expr ( exprt &  expr )

inline

Cast an exprt to a cond_exprt.

expr must be known to be cond_exprt.

Parameters

expr	Source expression

Returns

Object of type cond_exprt

Definition at line 3573 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

expr	Source expression

Returns

Object of type constant_exprt

Definition at line 3189 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

expr	Source expression

Returns

Object of type constant_exprt

Definition at line 3197 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

expr	Source expression

Returns

Object of type div_exprt

Definition at line 1206 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

expr	Source expression

Returns

Object of type div_exprt

Definition at line 1215 of file std_expr.h.

to_empty_union_expr() [1/2]

const empty_union_exprt & to_empty_union_expr ( const exprt &  expr )

inline

Cast an exprt to an empty_union_exprt.

expr must be known to be empty_union_exprt.

Parameters

expr	Source expression

Returns

Object of type empty_union_exprt

Definition at line 1860 of file std_expr.h.

to_empty_union_expr() [2/2]

empty_union_exprt & to_empty_union_expr ( exprt &  expr )

inline

Cast an exprt to an empty_union_exprt.

expr must be known to be empty_union_exprt.

Parameters

expr	Source expression

Returns

Object of type empty_union_exprt

Definition at line 1868 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

expr	Source expression

Returns

Object of type equal_exprt

Definition at line 1407 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

expr	Source expression

Returns

Object of type equal_exprt

Definition at line 1415 of file std_expr.h.

to_euclidean_mod_expr() [1/2]

const euclidean_mod_exprt & to_euclidean_mod_expr ( const exprt &  expr )

inline

Cast an exprt to a euclidean_mod_exprt.

expr must be known to be euclidean_mod_exprt.

Parameters

expr	Source expression

Returns

Object of type euclidean_mod_exprt

Definition at line 1345 of file std_expr.h.

to_euclidean_mod_expr() [2/2]

euclidean_mod_exprt & to_euclidean_mod_expr ( exprt &  expr )

inline

Cast an exprt to a euclidean_mod_exprt.

expr must be known to be euclidean_mod_exprt.

Parameters

expr	Source expression

Returns

Object of type euclidean_mod_exprt

Definition at line 1355 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

expr	Source expression

Returns

Object of type if_exprt

Definition at line 2582 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

expr	Source expression

Returns

Object of type if_exprt

Definition at line 2591 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

expr	Source expression

Returns

Object of type implies_exprt

Definition at line 2255 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

expr	Source expression

Returns

Object of type implies_exprt

Definition at line 2264 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

expr	Source expression

Returns

Object of type index_designatort

Definition at line 2714 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

expr	Source expression

Returns

Object of type index_designatort

Definition at line 2723 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

expr	Source expression

Returns

Object of type index_exprt

Definition at line 1538 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

expr	Source expression

Returns

Object of type index_exprt

Definition at line 1547 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

expr	Source expression

Returns

Object of type let_exprt

Definition at line 3502 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

expr	Source expression

Returns

Object of type let_exprt

Definition at line 3511 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

expr	Source expression

Returns

Object of type member_designatort

Definition at line 2763 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

expr	Source expression

Returns

Object of type member_designatort

Definition at line 2772 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

expr	Source expression

Returns

Object of type member_exprt

Definition at line 3064 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

expr	Source expression

Returns

Object of type member_exprt

Definition at line 3072 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

expr	Source expression

Returns

Object of type minus_exprt

Definition at line 1086 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

expr	Source expression

Returns

Object of type minus_exprt

Definition at line 1095 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

expr	Source expression

Returns

Object of type mod_exprt

Definition at line 1277 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

expr	Source expression

Returns

Object of type mod_exprt

Definition at line 1286 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

expr	Source expression

Returns

Object of type mult_exprt

Definition at line 1137 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

expr	Source expression

Returns

Object of type mult_exprt

Definition at line 1146 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

expr	Source expression

Returns

Object of type multi_ary_exprt

Definition at line 987 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

expr	Source expression

Returns

Object of type multi_ary_exprt

Definition at line 993 of file std_expr.h.

to_named_term_expr() [1/2]

const named_term_exprt & to_named_term_expr ( const exprt &  expr )

inline

Cast an exprt to a named_term_exprt.

expr must be known to be named_term_exprt.

Parameters

expr	Source expression

Returns

Object of type named_term_exprt

Definition at line 3839 of file std_expr.h.

to_named_term_expr() [2/2]

named_term_exprt & to_named_term_expr ( exprt &  expr )

inline

Cast an exprt to a array_comprehension_exprt.

expr must be known to be array_comprehension_exprt.

Parameters

expr	Source expression

Returns

Object of type array_comprehension_exprt

Definition at line 3848 of file std_expr.h.

to_nand_expr() [1/2]

const nand_exprt & to_nand_expr ( const exprt &  expr )

inline

Cast an exprt to a nand_exprt.

expr must be known to be nand_exprt.

Parameters

expr	Source expression

Returns

Object of type nand_exprt

Definition at line 2215 of file std_expr.h.

to_nand_expr() [2/2]

nand_exprt & to_nand_expr ( exprt &  expr )

inline

Cast an exprt to a nand_exprt.

expr must be known to be nand_exprt.

Parameters

expr	Source expression

Returns

Object of type nand_exprt

Definition at line 2222 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

expr	Source expression

Returns

Object of type nondet_symbol_exprt

Definition at line 343 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

expr	Source expression

Returns

Object of type nondet_symbol_exprt

Definition at line 351 of file std_expr.h.

to_nor_expr() [1/2]

const nor_exprt & to_nor_expr ( const exprt &  expr )

inline

Cast an exprt to a nor_exprt.

expr must be known to be nor_exprt.

Parameters

expr	Source expression

Returns

Object of type nor_exprt

Definition at line 2360 of file std_expr.h.

to_nor_expr() [2/2]

nor_exprt & to_nor_expr ( exprt &  expr )

inline

Cast an exprt to a nor_exprt.

expr must be known to be nor_exprt.

Parameters

expr	Source expression

Returns

Object of type nor_exprt

Definition at line 2367 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

expr	Source expression

Returns

Object of type not_exprt

Definition at line 2484 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

expr	Source expression

Returns

Object of type not_exprt

Definition at line 2492 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

expr	Source expression

Returns

Object of type notequal_exprt

Definition at line 1450 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

expr	Source expression

Returns

Object of type notequal_exprt

Definition at line 1459 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

expr	Source expression

Returns

Object of type or_exprt

Definition at line 2322 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

expr	Source expression

Returns

Object of type or_exprt

Definition at line 2329 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

expr	Source expression

Returns

Object of type plus_exprt

Definition at line 1041 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

expr	Source expression

Returns

Object of type plus_exprt

Definition at line 1050 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

expr	Source expression

Returns

Object of type sign_exprt

Definition at line 621 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

expr	Source expression

Returns

Object of type sign_exprt

Definition at line 629 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

expr	Source expression

Returns

Object of type struct_exprt

Definition at line 1900 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

expr	Source expression

Returns

Object of type struct_exprt

Definition at line 1907 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

expr	Source expression

Returns

Object of type symbol_exprt

Definition at line 272 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

expr	Source expression

Returns

Object of type symbol_exprt

Definition at line 281 of file std_expr.h.

to_ternary_expr() [1/2]

const ternary_exprt & to_ternary_expr ( const exprt &  expr )

inline

Cast an exprt to a ternary_exprt.

expr must be known to be ternary_exprt.

Parameters

expr	Source expression

Returns

Object of type ternary_exprt

Definition at line 116 of file std_expr.h.

to_ternary_expr() [2/2]

ternary_exprt & to_ternary_expr ( exprt &  expr )

inline

Cast an exprt to a ternary_exprt.

expr must be known to be ternary_exprt.

Parameters

expr	Source expression

Returns

Object of type ternary_exprt

Definition at line 123 of file std_expr.h.

to_type_expr() [1/2]

const type_exprt & to_type_expr ( const exprt &  expr )

inline

Cast an exprt to an type_exprt.

expr must be known to be type_exprt.

Parameters

expr	Source expression

Returns

Object of type type_exprt

Definition at line 3101 of file std_expr.h.

to_type_expr() [2/2]

type_exprt & to_type_expr ( exprt &  expr )

inline

Cast an exprt to an type_exprt.

expr must be known to be type_exprt.

Parameters

expr	Source expression

Returns

Object of type type_exprt

Definition at line 3109 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

expr	Source expression

Returns

Object of type typecast_exprt

Definition at line 2107 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

expr	Source expression

Returns

Object of type typecast_exprt

Definition at line 2115 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

expr	Source expression

Returns

Object of type unary_exprt

Definition at line 426 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

expr	Source expression

Returns

Object of type unary_exprt

Definition at line 433 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

expr	Source expression

Returns

Object of type unary_minus_exprt

Definition at line 514 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

expr	Source expression

Returns

Object of type unary_minus_exprt

Definition at line 522 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

expr	Source expression

Returns

Object of type unary_plus_exprt

Definition at line 556 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

expr	Source expression

Returns

Object of type unary_minus_exprt

Definition at line 564 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

expr	Source expression

Returns

Object of type union_exprt

Definition at line 1816 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

expr	Source expression

Returns

Object of type union_exprt

Definition at line 1824 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

expr	Source expression

Returns

Object of type update_exprt

Definition at line 2866 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

expr	Source expression

Returns

Object of type update_exprt

Definition at line 2875 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

expr	Source expression

Returns

Object of type vector_exprt

Definition at line 1754 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

expr	Source expression

Returns

Object of type vector_exprt

Definition at line 1761 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

expr	Source expression

Returns

Object of type with_exprt

Definition at line 2661 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

expr	Source expression

Returns

Object of type with_exprt

Definition at line 2670 of file std_expr.h.

to_xnor_expr() [1/2]

const xnor_exprt & to_xnor_expr ( const exprt &  expr )

inline

Cast an exprt to a xnor_exprt.

expr must be known to be xnor_exprt.

Parameters

expr	Source expression

Returns

Object of type xnor_exprt

Definition at line 2444 of file std_expr.h.

to_xnor_expr() [2/2]

xnor_exprt & to_xnor_expr ( exprt &  expr )

inline

Cast an exprt to a xnor_exprt.

expr must be known to be xnor_exprt.

Parameters

expr	Source expression

Returns

Object of type xnor_exprt

Definition at line 2451 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

expr	Source expression

Returns

Object of type xor_exprt

Definition at line 2400 of file std_expr.h.

to_xor_expr() [2/2]

xor_exprt & to_xor_expr ( exprt &  expr )

inline

Cast an exprt to a xor_exprt.

expr must be known to be xor_exprt.

Parameters

expr	Source expression

Returns

Object of type xor_exprt

Definition at line 2407 of file std_expr.h.

validate_expr() [1/45]

void validate_expr ( const abs_exprt &  value )

inline

Definition at line 455 of file std_expr.h.

validate_expr() [2/45]

void validate_expr ( const array_comprehension_exprt &  value )

inline

Definition at line 3645 of file std_expr.h.

validate_expr() [3/45]

void validate_expr ( const array_list_exprt &  value )

inline

Definition at line 1711 of file std_expr.h.

validate_expr() [4/45]

void validate_expr ( const array_of_exprt &  value )

inline

Definition at line 1592 of file std_expr.h.

validate_expr() [5/45]

void validate_expr ( const binary_exprt &  value )

inline

Definition at line 704 of file std_expr.h.

validate_expr() [6/45]

void validate_expr ( const binary_relation_exprt &  value )

inline

Definition at line 800 of file std_expr.h.

validate_expr() [7/45]

void validate_expr ( const binding_exprt &  binding_expr )

inline

Definition at line 3338 of file std_expr.h.

validate_expr() [8/45]

void validate_expr ( const class class_method_descriptor_exprt &  value )

inline

Definition at line 3746 of file std_expr.h.

validate_expr() [9/45]

void validate_expr ( const complex_exprt &  value )

inline

Definition at line 1954 of file std_expr.h.

validate_expr() [10/45]

void validate_expr ( const complex_imag_exprt &  expr )

inline

Definition at line 2041 of file std_expr.h.

validate_expr() [11/45]

void validate_expr ( const complex_real_exprt &  expr )

inline

Definition at line 1998 of file std_expr.h.

validate_expr() [12/45]

void validate_expr ( const cond_exprt &  value )

inline

Definition at line 3552 of file std_expr.h.

validate_expr() [13/45]

void validate_expr ( const constant_exprt &  value )

inline

Definition at line 3178 of file std_expr.h.

validate_expr() [14/45]

void validate_expr ( const div_exprt &  value )

inline

Definition at line 1195 of file std_expr.h.

validate_expr() [15/45]

void validate_expr ( const empty_union_exprt &  value )

inline

Definition at line 1848 of file std_expr.h.

validate_expr() [16/45]

void validate_expr ( const equal_exprt &  value )

inline

Definition at line 1396 of file std_expr.h.

validate_expr() [17/45]

void validate_expr ( const euclidean_mod_exprt &  value )

inline

Definition at line 1334 of file std_expr.h.

validate_expr() [18/45]

void validate_expr ( const greater_than_exprt &  value )

inline

Definition at line 821 of file std_expr.h.

validate_expr() [19/45]

void validate_expr ( const greater_than_or_equal_exprt &  value )

inline

Definition at line 842 of file std_expr.h.

validate_expr() [20/45]

void validate_expr ( const if_exprt &  value )

inline

Definition at line 2571 of file std_expr.h.

validate_expr() [21/45]

void validate_expr ( const implies_exprt &  value )

inline

Definition at line 2244 of file std_expr.h.

validate_expr() [22/45]

void validate_expr ( const index_designatort &  value )

inline

Definition at line 2703 of file std_expr.h.

validate_expr() [23/45]

void validate_expr ( const index_exprt &  value )

inline

Definition at line 1527 of file std_expr.h.

validate_expr() [24/45]

void validate_expr ( const less_than_exprt &  value )

inline

Definition at line 863 of file std_expr.h.

validate_expr() [25/45]

void validate_expr ( const less_than_or_equal_exprt &  value )

inline

Definition at line 884 of file std_expr.h.

validate_expr() [26/45]

void validate_expr ( const let_exprt &  let_expr )

inline

Definition at line 3491 of file std_expr.h.

validate_expr() [27/45]

void validate_expr ( const member_designatort &  value )

inline

Definition at line 2752 of file std_expr.h.

validate_expr() [28/45]

void validate_expr ( const member_exprt &  value )

inline

Definition at line 3053 of file std_expr.h.

validate_expr() [29/45]

void validate_expr ( const minus_exprt &  value )

inline

Definition at line 1075 of file std_expr.h.

validate_expr() [30/45]

void validate_expr ( const mod_exprt &  value )

inline

Definition at line 1266 of file std_expr.h.

validate_expr() [31/45]

void validate_expr ( const mult_exprt &  value )

inline

Definition at line 1126 of file std_expr.h.

validate_expr() [32/45]

void validate_expr ( const named_term_exprt &  value )

inline

Definition at line 3828 of file std_expr.h.

validate_expr() [33/45]

void validate_expr ( const nondet_symbol_exprt &  value )

inline

Definition at line 332 of file std_expr.h.

validate_expr() [34/45]

void validate_expr ( const not_exprt &  value )

inline

Definition at line 2473 of file std_expr.h.

validate_expr() [35/45]

void validate_expr ( const notequal_exprt &  value )

inline

Definition at line 1439 of file std_expr.h.

validate_expr() [36/45]

void validate_expr ( const plus_exprt &  value )

inline

Definition at line 1030 of file std_expr.h.

validate_expr() [37/45]

void validate_expr ( const sign_exprt &  expr )

inline

Definition at line 610 of file std_expr.h.

validate_expr() [38/45]

void validate_expr ( const symbol_exprt &  value )

inline

Definition at line 261 of file std_expr.h.

validate_expr() [39/45]

void validate_expr ( const typecast_exprt &  value )

inline

Definition at line 2096 of file std_expr.h.

validate_expr() [40/45]

void validate_expr ( const unary_exprt &  value )

inline

Definition at line 415 of file std_expr.h.

validate_expr() [41/45]

void validate_expr ( const unary_minus_exprt &  value )

inline

Definition at line 503 of file std_expr.h.

validate_expr() [42/45]

void validate_expr ( const unary_plus_exprt &  value )

inline

Definition at line 545 of file std_expr.h.

validate_expr() [43/45]

void validate_expr ( const union_exprt &  value )

inline

Definition at line 1805 of file std_expr.h.

validate_expr() [44/45]

void validate_expr ( const update_exprt &  value )

inline

Definition at line 2854 of file std_expr.h.

validate_expr() [45/45]

void validate_expr ( const with_exprt &  value )

inline

Definition at line 2650 of file std_expr.h.