API to expression classes for bitvectors. More...

#include "bitvector_types.h"
#include "std_expr.h"

Include dependency graph for bitvector_expr.h:

This graph shows which files directly or indirectly include this file:

Classes
class	bswap_exprt
	The byte swap expression. More...

class	bitnot_exprt
	Bit-wise negation of bit-vectors. More...

class	bitor_exprt
	Bit-wise OR Any number of operands that is greater or equal one. More...

class	bitnor_exprt
	Bit-wise NOR. More...

class	bitxor_exprt
	Bit-wise XOR Any number of operands that is greater or equal one. More...

class	bitxnor_exprt
	Bit-wise XNOR. More...

class	bitand_exprt
	Bit-wise AND Any number of operands that is greater or equal one. More...

class	bitnand_exprt
	Bit-wise NAND. More...

class	shift_exprt
	A base class for shift and rotate operators. More...

class	shl_exprt
	Left shift. More...

class	ashr_exprt
	Arithmetic right shift. More...

class	lshr_exprt
	Logical right shift. 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	update_bit_exprt
	Replaces a sub-range of a bit-vector operand. More...

class	update_bits_exprt
	Replaces a sub-range of a bit-vector operand. More...

class	replication_exprt
	Bit-vector replication. More...

class	concatenation_exprt
	Concatenation of bit-vector operands. More...

class	popcount_exprt
	The popcount (counting the number of bits set to 1) expression. More...

class	binary_overflow_exprt
	A Boolean expression returning true, iff operation `kind` would result in an overflow when applied to operands `lhs` and `rhs`. More...

class	plus_overflow_exprt

class	minus_overflow_exprt

class	mult_overflow_exprt

class	shl_overflow_exprt

class	unary_overflow_exprt
	A Boolean expression returning true, iff operation `kind` would result in an overflow when applied to the (single) operand. More...

class	unary_minus_overflow_exprt
	A Boolean expression returning true, iff negation would result in an overflow when applied to the (single) operand. More...

class	count_leading_zeros_exprt
	The count leading zeros (counting the number of zero bits starting from the most-significant bit) expression. More...

class	count_trailing_zeros_exprt
	The count trailing zeros (counting the number of zero bits starting from the least-significant bit) expression. More...

class	bitreverse_exprt
	Reverse the order of bits in a bit-vector. More...

class	saturating_plus_exprt
	The saturating plus expression. More...

class	saturating_minus_exprt
	Saturating subtraction expression. More...

class	overflow_result_exprt
	An expression returning both the result of the arithmetic operation under wrap-around semantics as well as a Boolean to signify overflow. More...

class	find_first_set_exprt
	Returns one plus the index of the least-significant one bit, or zero if the operand is zero. More...

class	zero_extend_exprt
	zero extension The operand is converted to the given type by either a) truncating if the new type is shorter, or b) padding with most-significant zero bits if the new type is larger, or c) reinterprets the operand as the given type if their widths match. More...

class	onehot_exprt
	A Boolean expression returning true iff the given operand consists of exactly one '1' and '0' otherwise. More...

class	onehot0_exprt
	A Boolean expression returning true iff the given operand consists of exactly one '0' and '1' otherwise. More...

Functions
template<>
bool	can_cast_expr< bswap_exprt > (const exprt &base)

void	validate_expr (const bswap_exprt &value)

const bswap_exprt &	to_bswap_expr (const exprt &expr)
	Cast an exprt to a bswap_exprt.

bswap_exprt &	to_bswap_expr (exprt &expr)
	Cast an exprt to a bswap_exprt.

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

void	validate_expr (const bitnot_exprt &value)

const bitnot_exprt &	to_bitnot_expr (const exprt &expr)
	Cast an exprt to a bitnot_exprt.

bitnot_exprt &	to_bitnot_expr (exprt &expr)
	Cast an exprt to a bitnot_exprt.

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

const bitor_exprt &	to_bitor_expr (const exprt &expr)
	Cast an exprt to a bitor_exprt.

bitor_exprt &	to_bitor_expr (exprt &expr)
	Cast an exprt to a bitor_exprt.

template<>
bool	can_cast_expr< bitnor_exprt > (const exprt &base)

const bitnor_exprt &	to_bitnor_expr (const exprt &expr)
	Cast an exprt to a bitnor_exprt.

bitnor_exprt &	to_bitnor_expr (exprt &expr)
	Cast an exprt to a bitnor_exprt.

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

const bitxor_exprt &	to_bitxor_expr (const exprt &expr)
	Cast an exprt to a bitxor_exprt.

bitxor_exprt &	to_bitxor_expr (exprt &expr)
	Cast an exprt to a bitxor_exprt.

template<>
bool	can_cast_expr< bitxnor_exprt > (const exprt &base)

const bitxnor_exprt &	to_bitxnor_expr (const exprt &expr)
	Cast an exprt to a bitxnor_exprt.

bitxnor_exprt &	to_bitxnor_expr (exprt &expr)
	Cast an exprt to a bitxnor_exprt.

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

const bitand_exprt &	to_bitand_expr (const exprt &expr)
	Cast an exprt to a bitand_exprt.

bitand_exprt &	to_bitand_expr (exprt &expr)
	Cast an exprt to a bitand_exprt.

template<>
bool	can_cast_expr< bitnand_exprt > (const exprt &base)

const bitnand_exprt &	to_bitnand_expr (const exprt &expr)
	Cast an exprt to a bitnand_exprt.

bitnand_exprt &	to_bitnand_expr (exprt &expr)
	Cast an exprt to a bitnand_exprt.

template<>
bool	can_cast_expr< shift_exprt > (const exprt &base)

void	validate_expr (const shift_exprt &value)

const shift_exprt &	to_shift_expr (const exprt &expr)
	Cast an exprt to a shift_exprt.

shift_exprt &	to_shift_expr (exprt &expr)
	Cast an exprt to a shift_exprt.

template<>
bool	can_cast_expr< shl_exprt > (const exprt &base)

const shl_exprt &	to_shl_expr (const exprt &expr)
	Cast an exprt to a shl_exprt.

shl_exprt &	to_shl_expr (exprt &expr)
	Cast an exprt to a shl_exprt.

template<>
bool	can_cast_expr< ashr_exprt > (const exprt &base)

template<>
bool	can_cast_expr< lshr_exprt > (const exprt &base)

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

void	validate_expr (const extractbit_exprt &value)

const extractbit_exprt &	to_extractbit_expr (const exprt &expr)
	Cast an exprt to an extractbit_exprt.

extractbit_exprt &	to_extractbit_expr (exprt &expr)
	Cast an exprt to an extractbit_exprt.

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

void	validate_expr (const extractbits_exprt &value)

const extractbits_exprt &	to_extractbits_expr (const exprt &expr)
	Cast an exprt to an extractbits_exprt.

extractbits_exprt &	to_extractbits_expr (exprt &expr)
	Cast an exprt to an extractbits_exprt.

template<>
bool	can_cast_expr< update_bit_exprt > (const exprt &base)

const update_bit_exprt &	to_update_bit_expr (const exprt &expr)
	Cast an exprt to an update_bit_exprt.

update_bit_exprt &	to_update_bit_expr (exprt &expr)
	Cast an exprt to an update_bit_exprt.

template<>
bool	can_cast_expr< update_bits_exprt > (const exprt &base)

const update_bits_exprt &	to_update_bits_expr (const exprt &expr)
	Cast an exprt to an update_bits_exprt.

update_bits_exprt &	to_update_bits_expr (exprt &expr)
	Cast an exprt to an update_bits_exprt.

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

void	validate_expr (const replication_exprt &value)

const replication_exprt &	to_replication_expr (const exprt &expr)
	Cast an exprt to a replication_exprt.

replication_exprt &	to_replication_expr (exprt &expr)
	Cast an exprt to a replication_exprt.

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

const concatenation_exprt &	to_concatenation_expr (const exprt &expr)
	Cast an exprt to a concatenation_exprt.

concatenation_exprt &	to_concatenation_expr (exprt &expr)
	Cast an exprt to a concatenation_exprt.

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

void	validate_expr (const popcount_exprt &value)

const popcount_exprt &	to_popcount_expr (const exprt &expr)
	Cast an exprt to a popcount_exprt.

popcount_exprt &	to_popcount_expr (exprt &expr)
	Cast an exprt to a popcount_exprt.

template<>
bool	can_cast_expr< binary_overflow_exprt > (const exprt &base)

void	validate_expr (const binary_overflow_exprt &value)

const binary_overflow_exprt &	to_binary_overflow_expr (const exprt &expr)
	Cast an exprt to a binary_overflow_exprt.

binary_overflow_exprt &	to_binary_overflow_expr (exprt &expr)
	Cast an exprt to a binary_overflow_exprt.

template<>
bool	can_cast_expr< plus_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< minus_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< mult_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< shl_overflow_exprt > (const exprt &base)

template<>
bool	can_cast_expr< unary_overflow_exprt > (const exprt &base)

void	validate_expr (const unary_overflow_exprt &value)

template<>
bool	can_cast_expr< unary_minus_overflow_exprt > (const exprt &base)

void	validate_expr (const unary_minus_overflow_exprt &value)

const unary_overflow_exprt &	to_unary_overflow_expr (const exprt &expr)
	Cast an exprt to a unary_overflow_exprt.

unary_overflow_exprt &	to_unary_overflow_expr (exprt &expr)
	Cast an exprt to a unary_overflow_exprt.

template<>
bool	can_cast_expr< count_leading_zeros_exprt > (const exprt &base)

void	validate_expr (const count_leading_zeros_exprt &value)

const count_leading_zeros_exprt &	to_count_leading_zeros_expr (const exprt &expr)
	Cast an exprt to a count_leading_zeros_exprt.

count_leading_zeros_exprt &	to_count_leading_zeros_expr (exprt &expr)
	Cast an exprt to a count_leading_zeros_exprt.

template<>
bool	can_cast_expr< count_trailing_zeros_exprt > (const exprt &base)

void	validate_expr (const count_trailing_zeros_exprt &value)

const count_trailing_zeros_exprt &	to_count_trailing_zeros_expr (const exprt &expr)
	Cast an exprt to a count_trailing_zeros_exprt.

count_trailing_zeros_exprt &	to_count_trailing_zeros_expr (exprt &expr)
	Cast an exprt to a count_trailing_zeros_exprt.

template<>
bool	can_cast_expr< bitreverse_exprt > (const exprt &base)

void	validate_expr (const bitreverse_exprt &value)

const bitreverse_exprt &	to_bitreverse_expr (const exprt &expr)
	Cast an exprt to a bitreverse_exprt.

bitreverse_exprt &	to_bitreverse_expr (exprt &expr)
	Cast an exprt to a bitreverse_exprt.

template<>
bool	can_cast_expr< saturating_plus_exprt > (const exprt &base)

void	validate_expr (const saturating_plus_exprt &value)

const saturating_plus_exprt &	to_saturating_plus_expr (const exprt &expr)
	Cast an exprt to a saturating_plus_exprt.

saturating_plus_exprt &	to_saturating_plus_expr (exprt &expr)
	Cast an exprt to a saturating_plus_exprt.

template<>
bool	can_cast_expr< saturating_minus_exprt > (const exprt &base)

void	validate_expr (const saturating_minus_exprt &value)

const saturating_minus_exprt &	to_saturating_minus_expr (const exprt &expr)
	Cast an exprt to a saturating_minus_exprt.

saturating_minus_exprt &	to_saturating_minus_expr (exprt &expr)
	Cast an exprt to a saturating_minus_exprt.

template<>
bool	can_cast_expr< overflow_result_exprt > (const exprt &base)

void	validate_expr (const overflow_result_exprt &value)

const overflow_result_exprt &	to_overflow_result_expr (const exprt &expr)
	Cast an exprt to a overflow_result_exprt.

overflow_result_exprt &	to_overflow_result_expr (exprt &expr)
	Cast an exprt to a overflow_result_exprt.

template<>
bool	can_cast_expr< find_first_set_exprt > (const exprt &base)

void	validate_expr (const find_first_set_exprt &value)

const find_first_set_exprt &	to_find_first_set_expr (const exprt &expr)
	Cast an exprt to a find_first_set_exprt.

find_first_set_exprt &	to_find_first_set_expr (exprt &expr)
	Cast an exprt to a find_first_set_exprt.

template<>
bool	can_cast_expr< zero_extend_exprt > (const exprt &base)

const zero_extend_exprt &	to_zero_extend_expr (const exprt &expr)
	Cast an exprt to a zero_extend_exprt.

zero_extend_exprt &	to_zero_extend_expr (exprt &expr)
	Cast an exprt to a zero_extend_exprt.

const onehot_exprt &	to_onehot_expr (const exprt &expr)
	Cast an exprt to a onehot_exprt.

onehot_exprt &	to_onehot_expr (exprt &expr)
	Cast an exprt to a onehot_exprt.

const onehot0_exprt &	to_onehot0_expr (const exprt &expr)
	Cast an exprt to a onehot0_exprt.

onehot0_exprt &	to_onehot0_expr (exprt &expr)
	Cast an exprt to a onehot0_exprt.

Detailed Description

API to expression classes for bitvectors.

Definition in file bitvector_expr.h.

Function Documentation

◆ can_cast_expr< ashr_exprt >()

template<>

bool can_cast_expr< ashr_exprt > ( const exprt & base )

inline

Definition at line 545 of file bitvector_expr.h.

◆ can_cast_expr< binary_overflow_exprt >()

template<>

bool can_cast_expr< binary_overflow_exprt > ( const exprt & base )

inline

Definition at line 1109 of file bitvector_expr.h.

◆ can_cast_expr< bitand_exprt >()

template<>

bool can_cast_expr< bitand_exprt > ( const exprt & base )

inline

Definition at line 345 of file bitvector_expr.h.

◆ can_cast_expr< bitnand_exprt >()

template<>

bool can_cast_expr< bitnand_exprt > ( const exprt & base )

inline

Definition at line 396 of file bitvector_expr.h.

◆ can_cast_expr< bitnor_exprt >()

template<>

bool can_cast_expr< bitnor_exprt > ( const exprt & base )

inline

Definition at line 198 of file bitvector_expr.h.

◆ can_cast_expr< bitnot_exprt >()

template<>

bool can_cast_expr< bitnot_exprt > ( const exprt & base )

inline

Definition at line 91 of file bitvector_expr.h.

◆ can_cast_expr< bitor_exprt >()

template<>

bool can_cast_expr< bitor_exprt > ( const exprt & base )

inline

Definition at line 147 of file bitvector_expr.h.

◆ can_cast_expr< bitreverse_exprt >()

template<>

bool can_cast_expr< bitreverse_exprt > ( const exprt & base )

inline

Definition at line 1521 of file bitvector_expr.h.

◆ can_cast_expr< bitxnor_exprt >()

template<>

bool can_cast_expr< bitxnor_exprt > ( const exprt & base )

inline

Definition at line 296 of file bitvector_expr.h.

◆ can_cast_expr< bitxor_exprt >()

template<>

bool can_cast_expr< bitxor_exprt > ( const exprt & base )

inline

Definition at line 245 of file bitvector_expr.h.

◆ can_cast_expr< bswap_exprt >()

template<>

bool can_cast_expr< bswap_exprt > ( const exprt & base )

inline

Definition at line 46 of file bitvector_expr.h.

◆ can_cast_expr< concatenation_exprt >()

template<>

bool can_cast_expr< concatenation_exprt > ( const exprt & base )

inline

Definition at line 976 of file bitvector_expr.h.

◆ can_cast_expr< count_leading_zeros_exprt >()

template<>

bool can_cast_expr< count_leading_zeros_exprt > ( const exprt & base )

inline

Definition at line 1377 of file bitvector_expr.h.

◆ can_cast_expr< count_trailing_zeros_exprt >()

template<>

bool can_cast_expr< count_trailing_zeros_exprt > ( const exprt & base )

inline

Definition at line 1470 of file bitvector_expr.h.

◆ can_cast_expr< extractbit_exprt >()

template<>

bool can_cast_expr< extractbit_exprt > ( const exprt & base )

inline

Definition at line 605 of file bitvector_expr.h.

◆ can_cast_expr< extractbits_exprt >()

template<>

bool can_cast_expr< extractbits_exprt > ( const exprt & base )

inline

Definition at line 679 of file bitvector_expr.h.

◆ can_cast_expr< find_first_set_exprt >()

template<>

bool can_cast_expr< find_first_set_exprt > ( const exprt & base )

inline

Definition at line 1824 of file bitvector_expr.h.

◆ can_cast_expr< lshr_exprt >()

template<>

bool can_cast_expr< lshr_exprt > ( const exprt & base )

inline

Definition at line 566 of file bitvector_expr.h.

◆ can_cast_expr< minus_overflow_exprt >()

template<>

bool can_cast_expr< minus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1181 of file bitvector_expr.h.

◆ can_cast_expr< mult_overflow_exprt >()

template<>

bool can_cast_expr< mult_overflow_exprt > ( const exprt & base )

inline

Definition at line 1200 of file bitvector_expr.h.

◆ can_cast_expr< overflow_result_exprt >()

template<>

bool can_cast_expr< overflow_result_exprt > ( const exprt & base )

inline

Definition at line 1738 of file bitvector_expr.h.

◆ can_cast_expr< plus_overflow_exprt >()

template<>

bool can_cast_expr< plus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1162 of file bitvector_expr.h.

◆ can_cast_expr< popcount_exprt >()

template<>

bool can_cast_expr< popcount_exprt > ( const exprt & base )

inline

Definition at line 1020 of file bitvector_expr.h.

◆ can_cast_expr< replication_exprt >()

template<>

bool can_cast_expr< replication_exprt > ( const exprt & base )

inline

Definition at line 920 of file bitvector_expr.h.

◆ can_cast_expr< saturating_minus_exprt >()

template<>

bool can_cast_expr< saturating_minus_exprt > ( const exprt & base )

inline

Definition at line 1619 of file bitvector_expr.h.

◆ can_cast_expr< saturating_plus_exprt >()

template<>

bool can_cast_expr< saturating_plus_exprt > ( const exprt & base )

inline

Definition at line 1574 of file bitvector_expr.h.

◆ can_cast_expr< shift_exprt >()

template<>

bool can_cast_expr< shift_exprt > ( const exprt & base )

inline

Definition at line 453 of file bitvector_expr.h.

◆ can_cast_expr< shl_exprt >()

template<>

bool can_cast_expr< shl_exprt > ( const exprt & base )

inline

Definition at line 501 of file bitvector_expr.h.

◆ can_cast_expr< shl_overflow_exprt >()

template<>

bool can_cast_expr< shl_overflow_exprt > ( const exprt & base )

inline

Definition at line 1215 of file bitvector_expr.h.

◆ can_cast_expr< unary_minus_overflow_exprt >()

template<>

bool can_cast_expr< unary_minus_overflow_exprt > ( const exprt & base )

inline

Definition at line 1285 of file bitvector_expr.h.

◆ can_cast_expr< unary_overflow_exprt >()

template<>

bool can_cast_expr< unary_overflow_exprt > ( const exprt & base )

inline

Definition at line 1247 of file bitvector_expr.h.

◆ can_cast_expr< update_bit_exprt >()

template<>

bool can_cast_expr< update_bit_exprt > ( const exprt & base )

inline

Definition at line 773 of file bitvector_expr.h.

◆ can_cast_expr< update_bits_exprt >()

template<>

bool can_cast_expr< update_bits_exprt > ( const exprt & base )

inline

Definition at line 859 of file bitvector_expr.h.

◆ can_cast_expr< zero_extend_exprt >()

template<>

bool can_cast_expr< zero_extend_exprt > ( const exprt & base )

inline

Definition at line 1876 of file bitvector_expr.h.

◆ to_binary_overflow_expr() [1/2]

const binary_overflow_exprt & to_binary_overflow_expr ( const exprt & expr )

inline

Cast an exprt to a binary_overflow_exprt.

expr must be known to be binary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type binary_overflow_exprt

Definition at line 1126 of file bitvector_expr.h.

◆ to_binary_overflow_expr() [2/2]

binary_overflow_exprt & to_binary_overflow_expr ( exprt & expr )

inline

Cast an exprt to a binary_overflow_exprt.

expr must be known to be binary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type binary_overflow_exprt

Definition at line 1138 of file bitvector_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

expr	Source expression

Returns: Object of type bitand_exprt

Definition at line 356 of file bitvector_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

expr	Source expression

Returns: Object of type bitand_exprt

Definition at line 363 of file bitvector_expr.h.

◆ to_bitnand_expr() [1/2]

const bitnand_exprt & to_bitnand_expr ( const exprt & expr )

inline

Cast an exprt to a bitnand_exprt.

expr must be known to be bitnand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnand_exprt

Definition at line 407 of file bitvector_expr.h.

◆ to_bitnand_expr() [2/2]

bitnand_exprt & to_bitnand_expr ( exprt & expr )

inline

Cast an exprt to a bitnand_exprt.

expr must be known to be bitnand_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnand_exprt

Definition at line 414 of file bitvector_expr.h.

◆ to_bitnor_expr() [1/2]

const bitnor_exprt & to_bitnor_expr ( const exprt & expr )

inline

Cast an exprt to a bitnor_exprt.

expr must be known to be bitnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnor_exprt

Definition at line 209 of file bitvector_expr.h.

◆ to_bitnor_expr() [2/2]

bitnor_exprt & to_bitnor_expr ( exprt & expr )

inline

Cast an exprt to a bitnor_exprt.

expr must be known to be bitnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitnor_exprt

Definition at line 216 of file bitvector_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

expr	Source expression

Returns: Object of type bitnot_exprt

Definition at line 107 of file bitvector_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

expr	Source expression

Returns: Object of type bitnot_exprt

Definition at line 116 of file bitvector_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

expr	Source expression

Returns: Object of type bitor_exprt

Definition at line 158 of file bitvector_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

expr	Source expression

Returns: Object of type bitor_exprt

Definition at line 165 of file bitvector_expr.h.

◆ to_bitreverse_expr() [1/2]

const bitreverse_exprt & to_bitreverse_expr ( const exprt & expr )

inline

Cast an exprt to a bitreverse_exprt.

expr must be known to be bitreverse_exprt.

Parameters

expr	Source expression

Returns: Object of type bitreverse_exprt

Definition at line 1537 of file bitvector_expr.h.

◆ to_bitreverse_expr() [2/2]

bitreverse_exprt & to_bitreverse_expr ( exprt & expr )

inline

Cast an exprt to a bitreverse_exprt.

expr must be known to be bitreverse_exprt.

Parameters

expr	Source expression

Returns: Object of type bitreverse_exprt

Definition at line 1546 of file bitvector_expr.h.

◆ to_bitxnor_expr() [1/2]

const bitxnor_exprt & to_bitxnor_expr ( const exprt & expr )

inline

Cast an exprt to a bitxnor_exprt.

expr must be known to be bitxnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxnor_exprt

Definition at line 307 of file bitvector_expr.h.

◆ to_bitxnor_expr() [2/2]

bitxnor_exprt & to_bitxnor_expr ( exprt & expr )

inline

Cast an exprt to a bitxnor_exprt.

expr must be known to be bitxnor_exprt.

Parameters

expr	Source expression

Returns: Object of type bitxnor_exprt

Definition at line 315 of file bitvector_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

expr	Source expression

Returns: Object of type bitxor_exprt

Definition at line 256 of file bitvector_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

expr	Source expression

Returns: Object of type bitxor_exprt

Definition at line 263 of file bitvector_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

expr	Source expression

Returns: Object of type bswap_exprt

Definition at line 64 of file bitvector_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

expr	Source expression

Returns: Object of type bswap_exprt

Definition at line 73 of file bitvector_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

expr	Source expression

Returns: Object of type concatenation_exprt

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

expr	Source expression

Returns: Object of type concatenation_exprt

Definition at line 994 of file bitvector_expr.h.

◆ to_count_leading_zeros_expr() [1/2]

const count_leading_zeros_exprt & to_count_leading_zeros_expr ( const exprt & expr )

inline

Cast an exprt to a count_leading_zeros_exprt.

expr must be known to be count_leading_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_leading_zeros_exprt

Definition at line 1394 of file bitvector_expr.h.

◆ to_count_leading_zeros_expr() [2/2]

count_leading_zeros_exprt & to_count_leading_zeros_expr ( exprt & expr )

inline

Cast an exprt to a count_leading_zeros_exprt.

expr must be known to be count_leading_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_leading_zeros_exprt

Definition at line 1404 of file bitvector_expr.h.

◆ to_count_trailing_zeros_expr() [1/2]

const count_trailing_zeros_exprt & to_count_trailing_zeros_expr ( const exprt & expr )

inline

Cast an exprt to a count_trailing_zeros_exprt.

expr must be known to be count_trailing_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_trailing_zeros_exprt

Definition at line 1487 of file bitvector_expr.h.

◆ to_count_trailing_zeros_expr() [2/2]

count_trailing_zeros_exprt & to_count_trailing_zeros_expr ( exprt & expr )

inline

Cast an exprt to a count_trailing_zeros_exprt.

expr must be known to be count_trailing_zeros_exprt.

Parameters

expr	Source expression

Returns: Object of type count_trailing_zeros_exprt

Definition at line 1497 of file bitvector_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

expr	Source expression

Returns: Object of type extractbit_exprt

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

expr	Source expression

Returns: Object of type extractbit_exprt

Definition at line 630 of file bitvector_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

expr	Source expression

Returns: Object of type extractbits_exprt

Definition at line 695 of file bitvector_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

expr	Source expression

Returns: Object of type extractbits_exprt

Definition at line 704 of file bitvector_expr.h.

◆ to_find_first_set_expr() [1/2]

const find_first_set_exprt & to_find_first_set_expr ( const exprt & expr )

inline

Cast an exprt to a find_first_set_exprt.

expr must be known to be find_first_set_exprt.

Parameters

expr	Source expression

Returns: Object of type find_first_set_exprt

Definition at line 1840 of file bitvector_expr.h.

◆ to_find_first_set_expr() [2/2]

find_first_set_exprt & to_find_first_set_expr ( exprt & expr )

inline

Cast an exprt to a find_first_set_exprt.

expr must be known to be find_first_set_exprt.

Parameters

expr	Source expression

Returns: Object of type find_first_set_exprt

Definition at line 1850 of file bitvector_expr.h.

◆ to_onehot0_expr() [1/2]

const onehot0_exprt & to_onehot0_expr ( const exprt & expr )

inline

Cast an exprt to a onehot0_exprt.

expr must be known to be onehot0_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot0_exprt

Definition at line 1957 of file bitvector_expr.h.

◆ to_onehot0_expr() [2/2]

onehot0_exprt & to_onehot0_expr ( exprt & expr )

inline

Cast an exprt to a onehot0_exprt.

expr must be known to be onehot0_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot0_exprt

Definition at line 1965 of file bitvector_expr.h.

◆ to_onehot_expr() [1/2]

const onehot_exprt & to_onehot_expr ( const exprt & expr )

inline

Cast an exprt to a onehot_exprt.

expr must be known to be onehot_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot_exprt

Definition at line 1922 of file bitvector_expr.h.

◆ to_onehot_expr() [2/2]

onehot_exprt & to_onehot_expr ( exprt & expr )

inline

Cast an exprt to a onehot_exprt.

expr must be known to be onehot_exprt.

Parameters

expr	Source expression

Returns: Object of type onehot_exprt

Definition at line 1930 of file bitvector_expr.h.

◆ to_overflow_result_expr() [1/2]

const overflow_result_exprt & to_overflow_result_expr ( const exprt & expr )

inline

Cast an exprt to a overflow_result_exprt.

expr must be known to be overflow_result_exprt.

Parameters

expr	Source expression

Returns: Object of type overflow_result_exprt

Definition at line 1763 of file bitvector_expr.h.

◆ to_overflow_result_expr() [2/2]

overflow_result_exprt & to_overflow_result_expr ( exprt & expr )

inline

Cast an exprt to a overflow_result_exprt.

expr must be known to be overflow_result_exprt.

Parameters

expr	Source expression

Returns: Object of type overflow_result_exprt

Definition at line 1773 of file bitvector_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

expr	Source expression

Returns: Object of type popcount_exprt

Definition at line 1036 of file bitvector_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

expr	Source expression

Returns: Object of type popcount_exprt

Definition at line 1045 of file bitvector_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

expr	Source expression

Returns: Object of type replication_exprt

Definition at line 936 of file bitvector_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

expr	Source expression

Returns: Object of type replication_exprt

Definition at line 945 of file bitvector_expr.h.

◆ to_saturating_minus_expr() [1/2]

const saturating_minus_exprt & to_saturating_minus_expr ( const exprt & expr )

inline

Cast an exprt to a saturating_minus_exprt.

expr must be known to be saturating_minus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_minus_exprt

Definition at line 1635 of file bitvector_expr.h.

◆ to_saturating_minus_expr() [2/2]

saturating_minus_exprt & to_saturating_minus_expr ( exprt & expr )

inline

Cast an exprt to a saturating_minus_exprt.

expr must be known to be saturating_minus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_minus_exprt

Definition at line 1645 of file bitvector_expr.h.

◆ to_saturating_plus_expr() [1/2]

const saturating_plus_exprt & to_saturating_plus_expr ( const exprt & expr )

inline

Cast an exprt to a saturating_plus_exprt.

expr must be known to be saturating_plus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_plus_exprt

Definition at line 1590 of file bitvector_expr.h.

◆ to_saturating_plus_expr() [2/2]

saturating_plus_exprt & to_saturating_plus_expr ( exprt & expr )

inline

Cast an exprt to a saturating_plus_exprt.

expr must be known to be saturating_plus_exprt.

Parameters

expr	Source expression

Returns: Object of type saturating_plus_exprt

Definition at line 1600 of file bitvector_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

expr	Source expression

Returns: Object of type shift_exprt

Definition at line 470 of file bitvector_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

expr	Source expression

Returns: Object of type shift_exprt

Definition at line 478 of file bitvector_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

expr	Source expression

Returns: Object of type shl_exprt

Definition at line 512 of file bitvector_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

expr	Source expression

Returns: Object of type shl_exprt

Definition at line 521 of file bitvector_expr.h.

◆ to_unary_overflow_expr() [1/2]

const unary_overflow_exprt & to_unary_overflow_expr ( const exprt & expr )

inline

Cast an exprt to a unary_overflow_exprt.

expr must be known to be unary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type unary_overflow_exprt

Definition at line 1302 of file bitvector_expr.h.

◆ to_unary_overflow_expr() [2/2]

unary_overflow_exprt & to_unary_overflow_expr ( exprt & expr )

inline

Cast an exprt to a unary_overflow_exprt.

expr must be known to be unary_overflow_exprt.

Parameters

expr	Source expression

Returns: Object of type unary_overflow_exprt

Definition at line 1312 of file bitvector_expr.h.

◆ to_update_bit_expr() [1/2]

const update_bit_exprt & to_update_bit_expr ( const exprt & expr )

inline

Cast an exprt to an update_bit_exprt.

expr must be known to be update_bit_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bit_exprt

Definition at line 784 of file bitvector_expr.h.

◆ to_update_bit_expr() [2/2]

update_bit_exprt & to_update_bit_expr ( exprt & expr )

inline

Cast an exprt to an update_bit_exprt.

expr must be known to be update_bit_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bit_exprt

Definition at line 792 of file bitvector_expr.h.

◆ to_update_bits_expr() [1/2]

const update_bits_exprt & to_update_bits_expr ( const exprt & expr )

inline

Cast an exprt to an update_bits_exprt.

expr must be known to be update_bits_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bits_exprt

Definition at line 870 of file bitvector_expr.h.

◆ to_update_bits_expr() [2/2]

update_bits_exprt & to_update_bits_expr ( exprt & expr )

inline

Cast an exprt to an update_bits_exprt.

expr must be known to be update_bits_exprt.

Parameters

expr	Source expression

Returns: Object of type update_bits_exprt

Definition at line 878 of file bitvector_expr.h.

◆ to_zero_extend_expr() [1/2]

const zero_extend_exprt & to_zero_extend_expr ( const exprt & expr )

inline

Cast an exprt to a zero_extend_exprt.

expr must be known to be zero_extend_exprt.

Parameters

expr	Source expression

Returns: Object of type zero_extend_exprt

Definition at line 1887 of file bitvector_expr.h.

◆ to_zero_extend_expr() [2/2]

zero_extend_exprt & to_zero_extend_expr ( exprt & expr )

inline

Cast an exprt to a zero_extend_exprt.

expr must be known to be zero_extend_exprt.

Parameters

expr	Source expression

Returns: Object of type zero_extend_exprt

Definition at line 1895 of file bitvector_expr.h.

◆ validate_expr() [1/17]

void validate_expr ( const binary_overflow_exprt & value )

inline

Definition at line 1114 of file bitvector_expr.h.

◆ validate_expr() [2/17]

void validate_expr ( const bitnot_exprt & value )

inline

Definition at line 96 of file bitvector_expr.h.

◆ validate_expr() [3/17]

void validate_expr ( const bitreverse_exprt & value )

inline

Definition at line 1526 of file bitvector_expr.h.

◆ validate_expr() [4/17]

void validate_expr ( const bswap_exprt & value )

inline

Definition at line 51 of file bitvector_expr.h.

◆ validate_expr() [5/17]

void validate_expr ( const count_leading_zeros_exprt & value )

inline

Definition at line 1382 of file bitvector_expr.h.

◆ validate_expr() [6/17]

void validate_expr ( const count_trailing_zeros_exprt & value )

inline

Definition at line 1475 of file bitvector_expr.h.

◆ validate_expr() [7/17]

void validate_expr ( const extractbit_exprt & value )

inline

Definition at line 610 of file bitvector_expr.h.

◆ validate_expr() [8/17]

void validate_expr ( const extractbits_exprt & value )

inline

Definition at line 684 of file bitvector_expr.h.

◆ validate_expr() [9/17]

void validate_expr ( const find_first_set_exprt & value )

inline

Definition at line 1829 of file bitvector_expr.h.

◆ validate_expr() [10/17]

void validate_expr ( const overflow_result_exprt & value )

inline

Definition at line 1743 of file bitvector_expr.h.

◆ validate_expr() [11/17]

void validate_expr ( const popcount_exprt & value )

inline

Definition at line 1025 of file bitvector_expr.h.

◆ validate_expr() [12/17]

void validate_expr ( const replication_exprt & value )

inline

Definition at line 925 of file bitvector_expr.h.

◆ validate_expr() [13/17]

void validate_expr ( const saturating_minus_exprt & value )

inline

Definition at line 1624 of file bitvector_expr.h.

◆ validate_expr() [14/17]

void validate_expr ( const saturating_plus_exprt & value )

inline

Definition at line 1579 of file bitvector_expr.h.

◆ validate_expr() [15/17]

void validate_expr ( const shift_exprt & value )

inline

Definition at line 459 of file bitvector_expr.h.

◆ validate_expr() [16/17]

void validate_expr ( const unary_minus_overflow_exprt & value )

inline

Definition at line 1290 of file bitvector_expr.h.

◆ validate_expr() [17/17]

void validate_expr ( const unary_overflow_exprt & value )

inline

Definition at line 1252 of file bitvector_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_expr< ashr_exprt >()

◆ can_cast_expr< binary_overflow_exprt >()

◆ can_cast_expr< bitand_exprt >()

◆ can_cast_expr< bitnand_exprt >()

◆ can_cast_expr< bitnor_exprt >()

◆ can_cast_expr< bitnot_exprt >()

◆ can_cast_expr< bitor_exprt >()

◆ can_cast_expr< bitreverse_exprt >()

◆ can_cast_expr< bitxnor_exprt >()

◆ can_cast_expr< bitxor_exprt >()

◆ can_cast_expr< bswap_exprt >()

◆ can_cast_expr< concatenation_exprt >()

◆ can_cast_expr< count_leading_zeros_exprt >()

◆ can_cast_expr< count_trailing_zeros_exprt >()

◆ can_cast_expr< extractbit_exprt >()

◆ can_cast_expr< extractbits_exprt >()

◆ can_cast_expr< find_first_set_exprt >()

◆ can_cast_expr< lshr_exprt >()

◆ can_cast_expr< minus_overflow_exprt >()

◆ can_cast_expr< mult_overflow_exprt >()

◆ can_cast_expr< overflow_result_exprt >()

◆ can_cast_expr< plus_overflow_exprt >()

◆ can_cast_expr< popcount_exprt >()

◆ can_cast_expr< replication_exprt >()

◆ can_cast_expr< saturating_minus_exprt >()

◆ can_cast_expr< saturating_plus_exprt >()

◆ can_cast_expr< shift_exprt >()

◆ can_cast_expr< shl_exprt >()

◆ can_cast_expr< shl_overflow_exprt >()

◆ can_cast_expr< unary_minus_overflow_exprt >()

◆ can_cast_expr< unary_overflow_exprt >()

◆ can_cast_expr< update_bit_exprt >()

◆ can_cast_expr< update_bits_exprt >()

◆ can_cast_expr< zero_extend_exprt >()

◆ to_binary_overflow_expr() [1/2]

◆ to_binary_overflow_expr() [2/2]

◆ to_bitand_expr() [1/2]

◆ to_bitand_expr() [2/2]

◆ to_bitnand_expr() [1/2]

◆ to_bitnand_expr() [2/2]

◆ to_bitnor_expr() [1/2]

◆ to_bitnor_expr() [2/2]

◆ to_bitnot_expr() [1/2]

◆ to_bitnot_expr() [2/2]

◆ to_bitor_expr() [1/2]

◆ to_bitor_expr() [2/2]

◆ to_bitreverse_expr() [1/2]

◆ to_bitreverse_expr() [2/2]

◆ to_bitxnor_expr() [1/2]

◆ to_bitxnor_expr() [2/2]

◆ to_bitxor_expr() [1/2]

◆ to_bitxor_expr() [2/2]

◆ to_bswap_expr() [1/2]

◆ to_bswap_expr() [2/2]

◆ to_concatenation_expr() [1/2]

◆ to_concatenation_expr() [2/2]

◆ to_count_leading_zeros_expr() [1/2]

◆ to_count_leading_zeros_expr() [2/2]

◆ to_count_trailing_zeros_expr() [1/2]

◆ to_count_trailing_zeros_expr() [2/2]

◆ to_extractbit_expr() [1/2]

◆ to_extractbit_expr() [2/2]

◆ to_extractbits_expr() [1/2]

◆ to_extractbits_expr() [2/2]

◆ to_find_first_set_expr() [1/2]

◆ to_find_first_set_expr() [2/2]

◆ to_onehot0_expr() [1/2]

◆ to_onehot0_expr() [2/2]

◆ to_onehot_expr() [1/2]

◆ to_onehot_expr() [2/2]

◆ to_overflow_result_expr() [1/2]

◆ to_overflow_result_expr() [2/2]

◆ to_popcount_expr() [1/2]

◆ to_popcount_expr() [2/2]

◆ to_replication_expr() [1/2]

◆ to_replication_expr() [2/2]