#include <boolbv.h>

Inheritance diagram for boolbvt:

Collaboration diagram for boolbvt:

Classes
class	quantifiert

Public Types
enum class	unbounded_arrayt { U_NONE , U_ALL , U_AUTO }

Public Types inherited from arrayst
typedef equalityt	SUB

Public Types inherited from equalityt
using	SUB = prop_conv_solvert

Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literalt >	symbolst

typedef std::unordered_map< exprt, literalt, irep_hash >	cachet

Public Types inherited from decision_proceduret
enum class	resultt { D_SATISFIABLE , D_UNSATISFIABLE , D_ERROR }
	Result of running the decision procedure. More...

Public Member Functions
	boolbvt (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)

virtual const bvt &	convert_bv (const exprt &expr, const std::optional< std::size_t > expected_width={})
	Convert expression to vector of literalts, using an internal cache to speed up conversion if available.

virtual bvt	convert_bitvector (const exprt &expr)
	Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.

exprt	get (const exprt &expr) const override
	Return `expr` with variables replaced by values from satisfying assignment if available.

void	set_to (const exprt &expr, bool value) override
	For a Boolean expression `expr`, add the constraint 'expr' if `value` is `true`, otherwise add 'not expr'.

void	print_assignment (std::ostream &out) const override
	Print satisfying assignment to `out`.

exprt	handle (const exprt &) override
	Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void	clear_cache () override

void	finish_eager_conversion () override

mp_integer	get_value (const bvt &bv)

mp_integer	get_value (const bvt &bv, std::size_t offset, std::size_t width)

const boolbv_mapt &	get_map () const

virtual std::size_t	boolbv_width (const typet &type) const

virtual endianness_mapt	endianness_map (const typet &type, bool little_endian) const

virtual endianness_mapt	endianness_map (const typet &type) const

Public Member Functions inherited from arrayst
	arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)

literalt	record_array_equality (const equal_exprt &expr)

void	record_array_index (const index_exprt &expr)

Public Member Functions inherited from equalityt
	equalityt (propt &_prop, message_handlert &message_handler)

virtual literalt	equality (const exprt &e1, const exprt &e2)

void	finish_eager_conversion () override

Public Member Functions inherited from prop_conv_solvert
	prop_conv_solvert (propt &_prop, message_handlert &message_handler)

virtual	~prop_conv_solvert ()=default

decision_proceduret::resultt	dec_solve (const exprt &) override
	Implementation of the decision procedure.

void	print_assignment (std::ostream &out) const override
	Print satisfying assignment to `out`.

std::string	decision_procedure_text () const override
	Return a textual description of the decision procedure.

exprt	get (const exprt &expr) const override
	Return `expr` with variables replaced by values from satisfying assignment if available.

tvt	l_get (literalt a) const override
	Return value of literal `l` from satisfying assignment.

exprt	handle (const exprt &expr) override
	Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

void	set_frozen (literalt)

void	set_frozen (const bvt &)

void	set_all_frozen ()

literalt	convert (const exprt &expr) override
	Convert a Boolean expression and return the corresponding literal.

bool	is_in_conflict (const exprt &expr) const override
	Returns true if an expression is in the final conflict leading to UNSAT.

void	set_to (const exprt &expr, bool value) override
	For a Boolean expression `expr`, add the constraint 'current_context => expr' if `value` is `true`, otherwise add 'current_context => not expr'.

void	push () override
	Push a new context on the stack This context becomes a child context nested in the current context.

void	push (const std::vector< exprt > &assumptions) override
	Push `assumptions` in form of `literal_exprt`

void	pop () override
	Pop whatever is on top of the stack.

const cachet &	get_cache () const

const symbolst &	get_symbols () const

void	set_time_limit_seconds (uint32_t lim) override
	Set the limit for the solver to time out in seconds.

std::size_t	get_number_of_solver_calls () const override
	Return the number of incremental solver calls.

hardness_collectort *	get_hardness_collector ()

Public Member Functions inherited from conflict_providert
virtual	~conflict_providert ()=default

Public Member Functions inherited from prop_convt
virtual	~prop_convt ()

Public Member Functions inherited from stack_decision_proceduret
virtual	~stack_decision_proceduret ()=default

Public Member Functions inherited from decision_proceduret
void	set_to_true (const exprt &)
	For a Boolean expression `expr`, add the constraint 'expr'.

void	set_to_false (const exprt &)
	For a Boolean expression `expr`, add the constraint 'not expr'.

resultt	operator() ()
	Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.

resultt	operator() (const exprt &assumption)
	Run the decision procedure to solve the problem under the given assumption.

virtual	~decision_proceduret ()

Public Member Functions inherited from solver_resource_limitst
virtual	~solver_resource_limitst ()=default

Public Attributes
unbounded_arrayt	unbounded_array

Public Attributes inherited from prop_conv_solvert
bool	use_cache = true

bool	equality_propagation = true

bool	freeze_all = false

Protected Types
typedef arrayst	SUB

typedef std::unordered_map< const exprt, bvt, irep_hash >	bv_cachet

typedef std::list< quantifiert >	quantifier_listt

typedef std::vector< std::size_t >	offset_mapt

Protected Types inherited from arrayst
enum class	lazy_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_LET }

enum class	constraint_typet { ARRAY_ACKERMANN , ARRAY_WITH , ARRAY_IF , ARRAY_OF , ARRAY_TYPECAST , ARRAY_CONSTANT , ARRAY_COMPREHENSION , ARRAY_EQUALITY , ARRAY_LET }

typedef std::list< array_equalityt >	array_equalitiest

typedef std::set< exprt >	index_sett

typedef std::map< std::size_t, index_sett >	index_mapt

typedef std::map< constraint_typet, size_t >	array_constraint_countt

Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hash >	elementst

typedef std::map< std::pair< unsigned, unsigned >, literalt >	equalitiest

typedef std::map< unsigned, exprt >	elements_revt

typedef std::unordered_map< const typet, typestructt, irep_hash >	typemapt

Protected Member Functions
literalt	convert_rest (const exprt &expr) override

virtual bool	boolbv_set_equality_to_true (const equal_exprt &expr)

bvt	conversion_failed (const exprt &expr)
	Print that the expression of x has failed conversion, then return a vector of x's width.

bool	type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)

virtual literalt	convert_bv_rel (const binary_relation_exprt &)
	Flatten <, >, <= and >= expressions.

virtual literalt	convert_typecast (const typecast_exprt &expr)
	conversion from bitvector types to boolean

virtual literalt	convert_reduction (const unary_exprt &expr)

virtual literalt	convert_onehot (const unary_exprt &expr)

virtual literalt	convert_extractbit (const extractbit_exprt &expr)

virtual literalt	convert_binary_overflow (const binary_overflow_exprt &expr)

virtual literalt	convert_unary_overflow (const unary_overflow_exprt &expr)

virtual literalt	convert_equality (const equal_exprt &expr)

virtual literalt	convert_verilog_case_equality (const binary_relation_exprt &expr)

virtual literalt	convert_ieee_float_rel (const binary_relation_exprt &)

virtual literalt	convert_quantifier (const quantifier_exprt &expr)

virtual bvt	convert_index (const exprt &array, const mp_integer &index)
	index operator with constant index

virtual bvt	convert_index (const index_exprt &expr)

virtual bvt	convert_bswap (const bswap_exprt &expr)

virtual bvt	convert_byte_extract (const byte_extract_exprt &expr)

virtual bvt	convert_byte_update (const byte_update_exprt &expr)

virtual bvt	convert_constraint_select_one (const exprt &expr)

virtual bvt	convert_if (const if_exprt &expr)

virtual bvt	convert_struct (const struct_exprt &expr)

virtual bvt	convert_array (const exprt &expr)
	Flatten array.

virtual bvt	convert_complex (const complex_exprt &expr)

virtual bvt	convert_complex_real (const complex_real_exprt &expr)

virtual bvt	convert_complex_imag (const complex_imag_exprt &expr)

virtual bvt	convert_array_comprehension (const array_comprehension_exprt &)

virtual bvt	convert_let (const let_exprt &)

virtual bvt	convert_array_of (const array_of_exprt &expr)
	Flatten arrays constructed from a single element.

virtual bvt	convert_union (const union_exprt &expr)

virtual bvt	convert_empty_union (const empty_union_exprt &expr)

virtual bvt	convert_bv_typecast (const typecast_exprt &expr)

virtual bvt	convert_add_sub (const exprt &expr)

virtual bvt	convert_mult (const mult_exprt &expr)

virtual bvt	convert_div (const div_exprt &expr)

virtual bvt	convert_mod (const mod_exprt &expr)

virtual bvt	convert_floatbv_op (const ieee_float_op_exprt &)

virtual bvt	convert_floatbv_mod_rem (const binary_exprt &)

virtual bvt	convert_floatbv_typecast (const floatbv_typecast_exprt &expr)

virtual bvt	convert_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)

virtual bvt	convert_member (const member_exprt &expr)

virtual bvt	convert_with (const with_exprt &expr)

virtual bvt	convert_update (const update_exprt &)

virtual bvt	convert_update_bit (const update_bit_exprt &)

virtual bvt	convert_update_bits (const update_bits_exprt &)

virtual bvt	convert_case (const exprt &expr)

virtual bvt	convert_cond (const cond_exprt &)

virtual bvt	convert_shift (const binary_exprt &expr)

virtual bvt	convert_bitwise (const exprt &expr)

virtual bvt	convert_unary_minus (const unary_minus_exprt &expr)

virtual bvt	convert_abs (const abs_exprt &expr)

virtual bvt	convert_concatenation (const concatenation_exprt &expr)

virtual bvt	convert_replication (const replication_exprt &expr)

virtual bvt	convert_constant (const constant_exprt &expr)

virtual bvt	convert_extractbits (const extractbits_exprt &expr)

virtual bvt	convert_symbol (const exprt &expr)

virtual bvt	convert_bv_reduction (const unary_exprt &expr)

virtual bvt	convert_not (const not_exprt &expr)

virtual bvt	convert_power (const binary_exprt &expr)

virtual bvt	convert_function_application (const function_application_exprt &expr)

virtual bvt	convert_bitreverse (const bitreverse_exprt &expr)

virtual bvt	convert_saturating_add_sub (const binary_exprt &expr)

virtual bvt	convert_overflow_result (const overflow_result_exprt &expr)

bvt	convert_update_bits (bvt src, const exprt &index, const bvt &new_value)

void	convert_with (const typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void	convert_with_bv (const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void	convert_with_array (const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void	convert_with_union (const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void	convert_with_struct (const struct_typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)

void	convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)

virtual exprt	bv_get_unbounded_array (const exprt &) const

virtual exprt	bv_get_rec (const exprt &expr, const bvt &bv, std::size_t offset) const

exprt	bv_get (const bvt &bv, const typet &type) const

exprt	bv_get_cache (const exprt &expr) const

bool	is_unbounded_array (const typet &type) const override

void	finish_eager_conversion_quantifiers ()

offset_mapt	build_offset_map (const struct_typet &src)

binding_exprt::variablest	fresh_binding (const binding_exprt &)
	create new, unique variables for the given binding

Protected Member Functions inherited from arrayst
virtual void	finish_eager_conversion_arrays ()

void	add_array_constraint (const lazy_constraintt &lazy, bool refine=true)
	adds array constraints (refine=true...lazily for the refinement loop)

void	display_array_constraint_count ()

std::string	enum_to_string (constraint_typet)

void	add_array_constraints ()

void	add_array_Ackermann_constraints ()

void	add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality)

void	add_array_constraints (const index_sett &index_set, const exprt &expr)

void	add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt)

void	add_array_constraints_with (const index_sett &index_set, const with_exprt &expr)

void	add_array_constraints_update (const index_sett &index_set, const update_exprt &expr)

void	add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt)

void	add_array_constraints_array_constant (const index_sett &index_set, const array_exprt &exprt)

void	add_array_constraints_comprehension (const index_sett &index_set, const array_comprehension_exprt &expr)

void	update_index_map (bool update_all)

void	update_index_map (std::size_t i)
	merge the indices into the root

void	collect_arrays (const exprt &a)

void	collect_indices ()

void	collect_indices (const exprt &a)

Protected Member Functions inherited from equalityt
virtual literalt	equality2 (const exprt &e1, const exprt &e2)

virtual void	add_equality_constraints ()

virtual void	add_equality_constraints (const typestructt &typestruct)

Protected Member Functions inherited from prop_conv_solvert
virtual std::optional< bool >	get_bool (const exprt &expr) const
	Get a boolean value from the model if the formula is satisfiable.

virtual literalt	convert_bool (const exprt &expr)

virtual bool	set_equality_to_true (const equal_exprt &expr)

virtual literalt	get_literal (const irep_idt &symbol)

virtual void	ignoring (const exprt &expr)

Protected Attributes
boolbv_widtht	bv_width

bv_utilst	bv_utils

functionst	functions

boolbv_mapt	map

bv_cachet	bv_cache

quantifier_listt	quantifier_list

numberingt< irep_idt >	string_numbering

std::size_t	scope_counter = 0

Protected Attributes inherited from arrayst
const namespacet &	ns

messaget	log

message_handlert &	message_handler

array_equalitiest	array_equalities

union_find< exprt, irep_hash >	arrays

index_mapt	index_map

bool	lazy_arrays

bool	incremental_cache

bool	get_array_constraints

std::list< lazy_constraintt >	lazy_array_constraints

std::map< exprt, bool >	expr_map

array_constraint_countt	array_constraint_count

std::set< std::size_t >	update_indices

std::unordered_set< irep_idt >	array_comprehension_args

Protected Attributes inherited from equalityt
typemapt	typemap

Protected Attributes inherited from prop_conv_solvert
bool	post_processing_done = false

symbolst	symbols

cachet	cache

propt &	prop

messaget	log

bvt	assumption_stack
	Assumptions on the stack.

std::size_t	context_literal_counter = 0
	To generate unique literal names for contexts.

std::vector< size_t >	context_size_stack
	`assumption_stack` is segmented in contexts; Number of assumptions in each context on the stack

Additional Inherited Members
Static Protected Attributes inherited from prop_conv_solvert
static const char *	context_prefix = "prop_conv::context$"

Detailed Description

Definition at line 46 of file boolbv.h.

Member Typedef Documentation

◆ bv_cachet

typedef std::unordered_map<const exprt, bvt, irep_hash> boolbvt::bv_cachet

protected

Definition at line 135 of file boolbv.h.

◆ offset_mapt

typedef std::vector<std::size_t> boolbvt::offset_mapt

protected

Definition at line 279 of file boolbv.h.

◆ quantifier_listt

typedef std::list<quantifiert> boolbvt::quantifier_listt

protected

Definition at line 274 of file boolbv.h.

◆ SUB

typedef arrayst boolbvt::SUB

protected

Definition at line 131 of file boolbv.h.

Member Enumeration Documentation

◆ unbounded_arrayt

enum class boolbvt::unbounded_arrayt

strong

Enumerator
U_NONE
U_ALL
U_AUTO

Definition at line 88 of file boolbv.h.

Constructor & Destructor Documentation

◆ boolbvt()

boolbvt::boolbvt	(	const namespacet &	_ns,
		propt &	_prop,
		message_handlert &	message_handler,
		bool	get_array_constraints = `false`
	)

inline

Definition at line 49 of file boolbv.h.

Member Function Documentation

◆ boolbv_set_equality_to_true()

bool boolbvt::boolbv_set_equality_to_true ( const equal_exprt & expr )

protectedvirtual

Definition at line 497 of file boolbv.cpp.

◆ boolbv_width()

virtual std::size_t boolbvt::boolbv_width ( const typet & type ) const

inlinevirtual

Reimplemented in bv_pointers_widet.

Definition at line 103 of file boolbv.h.

◆ build_offset_map()

boolbvt::offset_mapt boolbvt::build_offset_map ( const struct_typet & src )

protected

Definition at line 586 of file boolbv.cpp.

◆ bv_get()

exprt boolbvt::bv_get	(	const bvt &	bv,
		const typet &	type
	)		const

protected

Definition at line 261 of file boolbv_get.cpp.

◆ bv_get_cache()

exprt boolbvt::bv_get_cache ( const exprt & expr ) const

protected

Definition at line 268 of file boolbv_get.cpp.

◆ bv_get_rec()

exprt boolbvt::bv_get_rec	(	const exprt &	expr,
		const bvt &	bv,
		std::size_t	offset
	)		const

protectedvirtual

Reimplemented in bv_pointers_widet, and bv_pointerst.

Definition at line 52 of file boolbv_get.cpp.

◆ bv_get_unbounded_array()

exprt boolbvt::bv_get_unbounded_array ( const exprt & expr ) const

protectedvirtual

Definition at line 280 of file boolbv_get.cpp.

◆ clear_cache()

void boolbvt::clear_cache ( )

inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Definition at line 75 of file boolbv.h.

◆ conversion_failed()

bvt boolbvt::conversion_failed ( const exprt & expr )

protected

Print that the expression of x has failed conversion, then return a vector of x's width.

Definition at line 94 of file boolbv.cpp.

◆ convert_abs()

bvt boolbvt::convert_abs ( const abs_exprt & expr )

protectedvirtual

Definition at line 17 of file boolbv_abs.cpp.

◆ convert_add_sub()

bvt boolbvt::convert_add_sub ( const exprt & expr )

protectedvirtual

Definition at line 16 of file boolbv_add_sub.cpp.

◆ convert_array()

bvt boolbvt::convert_array ( const exprt & expr )

protectedvirtual

Flatten array.

Loop over each element and convert them in turn, limiting each result's width to initial array bit size divided by number of elements. Return an empty vector if the width is zero or the array has no elements.

Definition at line 16 of file boolbv_array.cpp.

◆ convert_array_comprehension()

bvt boolbvt::convert_array_comprehension ( const array_comprehension_exprt & expr )

protectedvirtual

Definition at line 267 of file boolbv.cpp.

◆ convert_array_of()

bvt boolbvt::convert_array_of ( const array_of_exprt & expr )

protectedvirtual

Flatten arrays constructed from a single element.

Definition at line 16 of file boolbv_array_of.cpp.

◆ convert_binary_overflow()

literalt boolbvt::convert_binary_overflow ( const binary_overflow_exprt & expr )

protectedvirtual

Definition at line 114 of file boolbv_overflow.cpp.

◆ convert_bitreverse()

bvt boolbvt::convert_bitreverse ( const bitreverse_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_bitreverse.cpp.

◆ convert_bitvector()

bvt boolbvt::convert_bitvector ( const exprt & expr )

virtual

Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.

Parameters

expr	Expression to convert

Returns: A vector of literals corresponding to the outputs of the Boolean circuit

Reimplemented in bv_pointers_widet, and bv_pointerst.

Definition at line 108 of file boolbv.cpp.

◆ convert_bitwise()

bvt boolbvt::convert_bitwise ( const exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_bitwise.cpp.

◆ convert_bswap()

bvt boolbvt::convert_bswap ( const bswap_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_bswap.cpp.

◆ convert_bv()

const bvt & boolbvt::convert_bv	(	const exprt &	expr,
		const std::optional< std::size_t >	expected_width = `{}`
	)

virtual

Convert expression to vector of literalts, using an internal cache to speed up conversion if available.

Also assert the resultant vector is of a specific size, and freeze any elements if appropriate.

Definition at line 39 of file boolbv.cpp.

◆ convert_bv_reduction()

bvt boolbvt::convert_bv_reduction ( const unary_exprt & expr )

protectedvirtual

Definition at line 54 of file boolbv_reduction.cpp.

◆ convert_bv_rel()

literalt boolbvt::convert_bv_rel ( const binary_relation_exprt & expr )

protectedvirtual

Flatten <, >, <= and >= expressions.

Definition at line 18 of file boolbv_bv_rel.cpp.

◆ convert_bv_typecast()

bvt boolbvt::convert_bv_typecast ( const typecast_exprt & expr )

protectedvirtual

Definition at line 19 of file boolbv_typecast.cpp.

◆ convert_byte_extract()

bvt boolbvt::convert_byte_extract ( const byte_extract_exprt & expr )

protectedvirtual

Definition at line 33 of file boolbv_byte_extract.cpp.

◆ convert_byte_update()

bvt boolbvt::convert_byte_update ( const byte_update_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_byte_update.cpp.

◆ convert_case()

bvt boolbvt::convert_case ( const exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_case.cpp.

◆ convert_complex()

bvt boolbvt::convert_complex ( const complex_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_complex.cpp.

◆ convert_complex_imag()

bvt boolbvt::convert_complex_imag ( const complex_imag_exprt & expr )

protectedvirtual

Definition at line 48 of file boolbv_complex.cpp.

◆ convert_complex_real()

bvt boolbvt::convert_complex_real ( const complex_real_exprt & expr )

protectedvirtual

Definition at line 37 of file boolbv_complex.cpp.

◆ convert_concatenation()

bvt boolbvt::convert_concatenation ( const concatenation_exprt & expr )

protectedvirtual

Definition at line 14 of file boolbv_concatenation.cpp.

◆ convert_cond()

bvt boolbvt::convert_cond ( const cond_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_cond.cpp.

◆ convert_constant()

bvt boolbvt::convert_constant ( const constant_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_constant.cpp.

◆ convert_constraint_select_one()

bvt boolbvt::convert_constraint_select_one ( const exprt & expr )

protectedvirtual

Definition at line 12 of file boolbv_constraint_select_one.cpp.

◆ convert_div()

bvt boolbvt::convert_div ( const div_exprt & expr )

protectedvirtual

Reimplemented in bv_refinementt.

Definition at line 13 of file boolbv_div.cpp.

◆ convert_empty_union()

bvt boolbvt::convert_empty_union ( const empty_union_exprt & expr )

protectedvirtual

Definition at line 38 of file boolbv_union.cpp.

◆ convert_equality()

literalt boolbvt::convert_equality ( const equal_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_equality.cpp.

◆ convert_extractbit()

literalt boolbvt::convert_extractbit ( const extractbit_exprt & expr )

protectedvirtual

Definition at line 19 of file boolbv_extractbit.cpp.

◆ convert_extractbits()

bvt boolbvt::convert_extractbits ( const extractbits_exprt & expr )

protectedvirtual

Definition at line 14 of file boolbv_extractbits.cpp.

◆ convert_floatbv_mod_rem()

bvt boolbvt::convert_floatbv_mod_rem ( const binary_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_floatbv_mod_rem.cpp.

◆ convert_floatbv_op()

bvt boolbvt::convert_floatbv_op ( const ieee_float_op_exprt & expr )

protectedvirtual

Reimplemented in bv_refinementt.

Definition at line 101 of file boolbv_floatbv_op.cpp.

◆ convert_floatbv_round_to_integral()

bvt boolbvt::convert_floatbv_round_to_integral ( const floatbv_round_to_integral_exprt & expr )

protectedvirtual

Definition at line 83 of file boolbv_floatbv_op.cpp.

◆ convert_floatbv_typecast()

bvt boolbvt::convert_floatbv_typecast ( const floatbv_typecast_exprt & expr )

protectedvirtual

Definition at line 17 of file boolbv_floatbv_op.cpp.

◆ convert_function_application()

bvt boolbvt::convert_function_application ( const function_application_exprt & expr )

protectedvirtual

Definition at line 326 of file boolbv.cpp.

◆ convert_ieee_float_rel()

literalt boolbvt::convert_ieee_float_rel ( const binary_relation_exprt & expr )

protectedvirtual

Definition at line 17 of file boolbv_ieee_float_rel.cpp.

◆ convert_if()

bvt boolbvt::convert_if ( const if_exprt & expr )

protectedvirtual

Definition at line 12 of file boolbv_if.cpp.

◆ convert_index() [1/2]

bvt boolbvt::convert_index	(	const exprt &	array,
		const mp_integer &	index
	)

protectedvirtual

index operator with constant index

Definition at line 281 of file boolbv_index.cpp.

◆ convert_index() [2/2]

bvt boolbvt::convert_index ( const index_exprt & expr )

protectedvirtual

Definition at line 21 of file boolbv_index.cpp.

◆ convert_let()

bvt boolbvt::convert_let ( const let_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_let.cpp.

◆ convert_member()

bvt boolbvt::convert_member ( const member_exprt & expr )

protectedvirtual

Definition at line 49 of file boolbv_member.cpp.

◆ convert_mod()

bvt boolbvt::convert_mod ( const mod_exprt & expr )

protectedvirtual

Reimplemented in bv_refinementt.

Definition at line 12 of file boolbv_mod.cpp.

◆ convert_mult()

bvt boolbvt::convert_mult ( const mult_exprt & expr )

protectedvirtual

Reimplemented in bv_refinementt.

Definition at line 13 of file boolbv_mult.cpp.

◆ convert_not()

bvt boolbvt::convert_not ( const not_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_not.cpp.

◆ convert_onehot()

literalt boolbvt::convert_onehot ( const unary_exprt & expr )

protectedvirtual

Definition at line 12 of file boolbv_onehot.cpp.

◆ convert_overflow_result()

bvt boolbvt::convert_overflow_result ( const overflow_result_exprt & expr )

protectedvirtual

Definition at line 192 of file boolbv_overflow.cpp.

◆ convert_power()

bvt boolbvt::convert_power ( const binary_exprt & expr )

protectedvirtual

Definition at line 12 of file boolbv_power.cpp.

◆ convert_quantifier()

literalt boolbvt::convert_quantifier ( const quantifier_exprt & expr )

protectedvirtual

Definition at line 261 of file boolbv_quantifier.cpp.

◆ convert_reduction()

literalt boolbvt::convert_reduction ( const unary_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_reduction.cpp.

◆ convert_replication()

bvt boolbvt::convert_replication ( const replication_exprt & expr )

protectedvirtual

Definition at line 14 of file boolbv_replication.cpp.

◆ convert_rest()

literalt boolbvt::convert_rest ( const exprt & expr )

overrideprotectedvirtual

Reimplemented from prop_conv_solvert.

Reimplemented in bv_pointers_widet, and bv_pointerst.

Definition at line 337 of file boolbv.cpp.

◆ convert_saturating_add_sub()

bvt boolbvt::convert_saturating_add_sub ( const binary_exprt & expr )

protectedvirtual

Definition at line 151 of file boolbv_add_sub.cpp.

◆ convert_shift()

bvt boolbvt::convert_shift ( const binary_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_shift.cpp.

◆ convert_struct()

bvt boolbvt::convert_struct ( const struct_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_struct.cpp.

◆ convert_symbol()

bvt boolbvt::convert_symbol ( const exprt & expr )

protectedvirtual

Definition at line 302 of file boolbv.cpp.

◆ convert_typecast()

literalt boolbvt::convert_typecast ( const typecast_exprt & expr )

protectedvirtual

conversion from bitvector types to boolean

Definition at line 617 of file boolbv_typecast.cpp.

◆ convert_unary_minus()

bvt boolbvt::convert_unary_minus ( const unary_minus_exprt & expr )

protectedvirtual

Definition at line 20 of file boolbv_unary_minus.cpp.

◆ convert_unary_overflow()

literalt boolbvt::convert_unary_overflow ( const unary_overflow_exprt & expr )

protectedvirtual

Definition at line 178 of file boolbv_overflow.cpp.

◆ convert_union()

bvt boolbvt::convert_union ( const union_exprt & expr )

protectedvirtual

Definition at line 11 of file boolbv_union.cpp.

◆ convert_update()

bvt boolbvt::convert_update ( const update_exprt & expr )

protectedvirtual

Definition at line 15 of file boolbv_update.cpp.

◆ convert_update_bit()

bvt boolbvt::convert_update_bit ( const update_bit_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_update_bit.cpp.

◆ convert_update_bits() [1/2]

bvt boolbvt::convert_update_bits	(	bvt	src,
		const exprt &	index,
		const bvt &	new_value
	)

protected

◆ convert_update_bits() [2/2]

bvt boolbvt::convert_update_bits ( const update_bits_exprt & expr )

protectedvirtual

Definition at line 13 of file boolbv_update_bits.cpp.

◆ convert_update_rec()

void boolbvt::convert_update_rec	(	const exprt::operandst &	designator,
		std::size_t	d,
		const typet &	type,
		std::size_t	offset,
		const exprt &	new_value,
		bvt &	bv
	)

protected

Definition at line 33 of file boolbv_update.cpp.

◆ convert_verilog_case_equality()

literalt boolbvt::convert_verilog_case_equality ( const binary_relation_exprt & expr )

protectedvirtual

Definition at line 59 of file boolbv_equality.cpp.

◆ convert_with() [1/2]

void boolbvt::convert_with	(	const typet &	type,
		const exprt &	where,
		const exprt &	new_value,
		const bvt &	prev_bv,
		bvt &	next_bv
	)

protected

Definition at line 83 of file boolbv_with.cpp.

◆ convert_with() [2/2]

bvt boolbvt::convert_with ( const with_exprt & expr )

protectedvirtual

Definition at line 17 of file boolbv_with.cpp.

◆ convert_with_array()

void boolbvt::convert_with_array	(	const array_typet &	type,
		const exprt &	index,
		const exprt &	new_value,
		const bvt &	prev_bv,
		bvt &	next_bv
	)

protected

Definition at line 128 of file boolbv_with.cpp.

◆ convert_with_bv()

void boolbvt::convert_with_bv	(	const exprt &	index,
		const exprt &	new_value,
		const bvt &	prev_bv,
		bvt &	next_bv
	)

protected

◆ convert_with_struct()

void boolbvt::convert_with_struct	(	const struct_typet &	type,
		const exprt &	where,
		const exprt &	new_value,
		const bvt &	prev_bv,
		bvt &	next_bv
	)

protected

Definition at line 192 of file boolbv_with.cpp.

◆ convert_with_union()

void boolbvt::convert_with_union	(	const union_typet &	type,
		const exprt &	new_value,
		const bvt &	prev_bv,
		bvt &	next_bv
	)

protected

Definition at line 239 of file boolbv_with.cpp.

◆ endianness_map() [1/2]

endianness_mapt boolbvt::endianness_map ( const typet & type ) const

virtual

Definition at line 29 of file boolbv.cpp.

◆ endianness_map() [2/2]

virtual endianness_mapt boolbvt::endianness_map	(	const typet &	type,
		bool	little_endian
	)		const

inlinevirtual

Reimplemented in bv_pointerst, and bv_pointers_widet.

Definition at line 109 of file boolbv.h.

◆ finish_eager_conversion()

void boolbvt::finish_eager_conversion ( )

inlineoverridevirtual

Reimplemented from arrayst.

Reimplemented in bv_pointers_widet, and bv_pointerst.

Definition at line 81 of file boolbv.h.

◆ finish_eager_conversion_quantifiers()

void boolbvt::finish_eager_conversion_quantifiers ( )

protected

Definition at line 286 of file boolbv_quantifier.cpp.

◆ fresh_binding()

binding_exprt::variablest boolbvt::fresh_binding ( const binding_exprt & binding )

protected

create new, unique variables for the given binding

Definition at line 557 of file boolbv.cpp.

◆ get()

exprt boolbvt::get ( const exprt & ) const

overridevirtual

Return expr with variables replaced by values from satisfying assignment if available.

Return nil if not available

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 21 of file boolbv_get.cpp.

◆ get_map()

const boolbv_mapt & boolbvt::get_map ( ) const

inline

Definition at line 98 of file boolbv.h.

◆ get_value() [1/2]

mp_integer boolbvt::get_value ( const bvt & bv )

inline

Definition at line 91 of file boolbv.h.

◆ get_value() [2/2]

mp_integer boolbvt::get_value	(	const bvt &	bv,
		std::size_t	offset,
		std::size_t	width
	)

Definition at line 376 of file boolbv_get.cpp.

◆ handle()

exprt boolbvt::handle ( const exprt & )

overridevirtual

Generate a handle, which is an expression that has the same value as the argument in any model that is generated; this offers an efficient way to refer to the expression in subsequent calls to get or set_to.

The returned expression may be the expression itself or a more compact but solver-specific representation.

Implements decision_proceduret.

Definition at line 83 of file boolbv.cpp.

◆ is_unbounded_array()

bool boolbvt::is_unbounded_array ( const typet & type ) const

overrideprotectedvirtual

Implements arrayst.

Definition at line 538 of file boolbv.cpp.

◆ print_assignment()

void boolbvt::print_assignment ( std::ostream & out ) const

overridevirtual

Print satisfying assignment to out.

Implements decision_proceduret.

Definition at line 580 of file boolbv.cpp.

◆ set_to()

void boolbvt::set_to	(	const exprt &	,
		bool	value
	)

overridevirtual

For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.

Implements decision_proceduret.

Reimplemented in string_refinementt.

Definition at line 528 of file boolbv.cpp.

◆ type_conversion()

bool boolbvt::type_conversion	(	const typet &	src_type,
		const bvt &	src,
		const typet &	dest_type,
		bvt &	dest
	)

protected

Definition at line 32 of file boolbv_typecast.cpp.

Member Data Documentation

◆ bv_cache

bv_cachet boolbvt::bv_cache

protected

Definition at line 136 of file boolbv.h.

◆ bv_utils

bv_utilst boolbvt::bv_utils

protected

Definition at line 118 of file boolbv.h.

◆ bv_width

boolbv_widtht boolbvt::bv_width

protected

Definition at line 117 of file boolbv.h.

◆ functions

functionst boolbvt::functions

protected

Definition at line 121 of file boolbv.h.

◆ map

boolbv_mapt boolbvt::map

protected

Definition at line 124 of file boolbv.h.

◆ quantifier_list

quantifier_listt boolbvt::quantifier_list

protected

Definition at line 275 of file boolbv.h.

◆ scope_counter

std::size_t boolbvt::scope_counter = 0

protected

Definition at line 286 of file boolbv.h.

◆ string_numbering

numberingt<irep_idt> boolbvt::string_numbering

protected

Definition at line 283 of file boolbv.h.

◆ unbounded_array

unbounded_arrayt boolbvt::unbounded_array

Definition at line 89 of file boolbv.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_abs.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_add_sub.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_array.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_array_of.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_bitreverse.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_bitwise.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_bswap.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_bv_rel.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_byte_extract.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_byte_update.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_case.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_complex.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_concatenation.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_cond.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_constant.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_constraint_select_one.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_div.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_equality.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_extractbit.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_extractbits.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_floatbv_mod_rem.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_floatbv_op.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_get.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_ieee_float_rel.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_if.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_index.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_let.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_member.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_mod.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_mult.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_not.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_onehot.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_overflow.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_power.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_quantifier.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_reduction.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_replication.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_shift.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_struct.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_typecast.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_unary_minus.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_union.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_update.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_update_bit.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_update_bits.cpp
/home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_with.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ bv_cachet

◆ offset_mapt

◆ quantifier_listt

◆ SUB

Member Enumeration Documentation

◆ unbounded_arrayt

Constructor & Destructor Documentation

◆ boolbvt()

Member Function Documentation

◆ boolbv_set_equality_to_true()

◆ boolbv_width()

◆ build_offset_map()

◆ bv_get()

◆ bv_get_cache()

◆ bv_get_rec()

◆ bv_get_unbounded_array()

◆ clear_cache()

◆ conversion_failed()

◆ convert_abs()

◆ convert_add_sub()

◆ convert_array()

◆ convert_array_comprehension()

◆ convert_array_of()

◆ convert_binary_overflow()

◆ convert_bitreverse()

◆ convert_bitvector()

◆ convert_bitwise()

◆ convert_bswap()

◆ convert_bv()

◆ convert_bv_reduction()

◆ convert_bv_rel()

◆ convert_bv_typecast()

◆ convert_byte_extract()

◆ convert_byte_update()

◆ convert_case()

◆ convert_complex()

◆ convert_complex_imag()

◆ convert_complex_real()

◆ convert_concatenation()

◆ convert_cond()

◆ convert_constant()

◆ convert_constraint_select_one()

◆ convert_div()

◆ convert_empty_union()

◆ convert_equality()

◆ convert_extractbit()

◆ convert_extractbits()

◆ convert_floatbv_mod_rem()

◆ convert_floatbv_op()

◆ convert_floatbv_round_to_integral()

◆ convert_floatbv_typecast()

◆ convert_function_application()

◆ convert_ieee_float_rel()

◆ convert_if()

◆ convert_index() [1/2]

◆ convert_index() [2/2]

◆ convert_let()

◆ convert_member()

◆ convert_mod()

◆ convert_mult()

◆ convert_not()

◆ convert_onehot()

◆ convert_overflow_result()

◆ convert_power()

◆ convert_quantifier()

◆ convert_reduction()

◆ convert_replication()

◆ convert_rest()

◆ convert_saturating_add_sub()

◆ convert_shift()