#include <arrays.h>

Inheritance diagram for arrayst:

Collaboration diagram for arrayst:

Classes
struct	array_equalityt

struct	lazy_constraintt

Public Types
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
	arrayst (const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)

void	finish_eager_conversion () override

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.

virtual void	clear_cache ()

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

Protected Types
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
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)

virtual bool	is_unbounded_array (const typet &type) const =0

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_rest (const exprt &expr)

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
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
Public Attributes inherited from prop_conv_solvert
bool	use_cache = true

bool	equality_propagation = true

bool	freeze_all = false

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

Detailed Description

Definition at line 32 of file arrays.h.

Member Typedef Documentation

◆ array_constraint_countt

typedef std::map<constraint_typet, size_t> arrayst::array_constraint_countt

protected

Definition at line 132 of file arrays.h.

◆ array_equalitiest

typedef std::list<array_equalityt> arrayst::array_equalitiest

protected

Definition at line 74 of file arrays.h.

◆ index_mapt

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

protected

Definition at line 84 of file arrays.h.

◆ index_sett

typedef std::set<exprt> arrayst::index_sett

protected

Definition at line 81 of file arrays.h.

◆ SUB

typedef equalityt arrayst::SUB

Definition at line 50 of file arrays.h.

Member Enumeration Documentation

◆ constraint_typet

enum class arrayst::constraint_typet

strongprotected

Enumerator
ARRAY_ACKERMANN
ARRAY_WITH
ARRAY_IF
ARRAY_OF
ARRAY_TYPECAST
ARRAY_CONSTANT
ARRAY_COMPREHENSION
ARRAY_EQUALITY
ARRAY_LET

Definition at line 119 of file arrays.h.

◆ lazy_typet

enum class arrayst::lazy_typet

strongprotected

Enumerator
ARRAY_ACKERMANN
ARRAY_WITH
ARRAY_IF
ARRAY_OF
ARRAY_TYPECAST
ARRAY_CONSTANT
ARRAY_COMPREHENSION
ARRAY_LET

Definition at line 88 of file arrays.h.

Constructor & Destructor Documentation

◆ arrayst()

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

Definition at line 29 of file arrays.cpp.

Member Function Documentation

◆ add_array_Ackermann_constraints()

void arrayst::add_array_Ackermann_constraints ( )

protected

Definition at line 330 of file arrays.cpp.

◆ add_array_constraint()

void arrayst::add_array_constraint	(	const lazy_constraintt &	lazy,
		bool	refine = `true`
	)

protected

adds array constraints (refine=true...lazily for the refinement loop)

Definition at line 255 of file arrays.cpp.

◆ add_array_constraints() [1/2]

void arrayst::add_array_constraints ( )

protected

Definition at line 280 of file arrays.cpp.

◆ add_array_constraints() [2/2]

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

protected

Definition at line 475 of file arrays.cpp.

◆ add_array_constraints_array_constant()

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

protected

Definition at line 734 of file arrays.cpp.

◆ add_array_constraints_array_of()

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

protected

Definition at line 709 of file arrays.cpp.

◆ add_array_constraints_comprehension()

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

protected

Definition at line 815 of file arrays.cpp.

◆ add_array_constraints_equality()

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

protected

Definition at line 441 of file arrays.cpp.

◆ add_array_constraints_if()

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

protected

Definition at line 839 of file arrays.cpp.

◆ add_array_constraints_update()

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

protected

Definition at line 652 of file arrays.cpp.

◆ add_array_constraints_with()

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

protected

Definition at line 573 of file arrays.cpp.

◆ collect_arrays()

void arrayst::collect_arrays ( const exprt & a )

protected

Definition at line 131 of file arrays.cpp.

◆ collect_indices() [1/2]

void arrayst::collect_indices ( )

protected

Definition at line 83 of file arrays.cpp.

◆ collect_indices() [2/2]

void arrayst::collect_indices ( const exprt & a )

protected

Definition at line 91 of file arrays.cpp.

◆ display_array_constraint_count()

void arrayst::display_array_constraint_count ( )

protected

Definition at line 918 of file arrays.cpp.

◆ enum_to_string()

std::string arrayst::enum_to_string ( constraint_typet type )

protected

Definition at line 891 of file arrays.cpp.

◆ finish_eager_conversion()

void arrayst::finish_eager_conversion ( )

inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Reimplemented in bv_pointers_widet, boolbvt, and bv_pointerst.

Definition at line 41 of file arrays.h.

◆ finish_eager_conversion_arrays()

virtual void arrayst::finish_eager_conversion_arrays ( )

inlineprotectedvirtual

Reimplemented in bv_refinementt.

Definition at line 60 of file arrays.h.

◆ is_unbounded_array()

virtual bool arrayst::is_unbounded_array ( const typet & type ) const

protectedpure virtual

Implemented in boolbvt.

◆ record_array_equality()

literalt arrayst::record_array_equality ( const equal_exprt & expr )

Definition at line 55 of file arrays.cpp.

◆ record_array_index()

void arrayst::record_array_index ( const index_exprt & expr )

Definition at line 45 of file arrays.cpp.

◆ update_index_map() [1/2]

void arrayst::update_index_map ( bool update_all )

protected

Definition at line 407 of file arrays.cpp.

◆ update_index_map() [2/2]

void arrayst::update_index_map ( std::size_t i )

protected

merge the indices into the root

Definition at line 393 of file arrays.cpp.

Member Data Documentation

◆ array_comprehension_args

std::unordered_set<irep_idt> arrayst::array_comprehension_args

protected

Definition at line 165 of file arrays.h.

◆ array_constraint_count

array_constraint_countt arrayst::array_constraint_count

protected

Definition at line 133 of file arrays.h.

◆ array_equalities

array_equalitiest arrayst::array_equalities

protected

Definition at line 75 of file arrays.h.

◆ arrays

union_find<exprt, irep_hash> arrayst::arrays

protected

Definition at line 78 of file arrays.h.

◆ expr_map

std::map<exprt, bool> arrayst::expr_map

protected

Definition at line 117 of file arrays.h.

◆ get_array_constraints

bool arrayst::get_array_constraints

protected

Definition at line 114 of file arrays.h.

◆ incremental_cache

bool arrayst::incremental_cache

protected

Definition at line 113 of file arrays.h.

◆ index_map

index_mapt arrayst::index_map

protected

Definition at line 85 of file arrays.h.

◆ lazy_array_constraints

std::list<lazy_constraintt> arrayst::lazy_array_constraints

protected

Definition at line 115 of file arrays.h.

◆ lazy_arrays

bool arrayst::lazy_arrays

protected

Definition at line 112 of file arrays.h.

◆ log

messaget arrayst::log

protected

Definition at line 57 of file arrays.h.

◆ message_handler

message_handlert& arrayst::message_handler

protected

Definition at line 58 of file arrays.h.

◆ ns

const namespacet& arrayst::ns

protected

Definition at line 56 of file arrays.h.

◆ update_indices

std::set<std::size_t> arrayst::update_indices

protected

Definition at line 161 of file arrays.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/flattening/arrays.h
/home/runner/work/cbmc/cbmc/src/solvers/flattening/arrays.cpp

Classes

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ array_constraint_countt

◆ array_equalitiest

◆ index_mapt

◆ index_sett

◆ SUB

Member Enumeration Documentation

◆ constraint_typet

◆ lazy_typet

Constructor & Destructor Documentation

◆ arrayst()

Member Function Documentation

◆ add_array_Ackermann_constraints()

◆ add_array_constraint()

◆ add_array_constraints() [1/2]

◆ add_array_constraints() [2/2]

◆ add_array_constraints_array_constant()

◆ add_array_constraints_array_of()

◆ add_array_constraints_comprehension()

◆ add_array_constraints_equality()

◆ add_array_constraints_if()

◆ add_array_constraints_update()

◆ add_array_constraints_with()

◆ collect_arrays()

◆ collect_indices() [1/2]

◆ collect_indices() [2/2]

◆ display_array_constraint_count()

◆ enum_to_string()

◆ finish_eager_conversion()

◆ finish_eager_conversion_arrays()

◆ is_unbounded_array()

◆ record_array_equality()

◆ record_array_index()

◆ update_index_map() [1/2]

◆ update_index_map() [2/2]

Member Data Documentation

◆ array_comprehension_args

◆ array_constraint_count

◆ array_equalities

◆ arrays

◆ expr_map

◆ get_array_constraints

◆ incremental_cache

◆ index_map

◆ lazy_array_constraints

◆ lazy_arrays

◆ log

◆ message_handler

◆ ns

◆ update_indices