#include <array_conv.h>

Inheritance diagram for array_convt:

Classes
struct	index_map_rec
struct	idx_record
struct	array_select
struct	array_equality
struct	array_with
struct	array_of_val_rec
struct	touched_array

Public Types
typedef smt_solver_baset::ast_vec	ast_vect
typedef std::vector< ast_vect >	array_update_vect
typedef struct index_map_rec	index_map_rect
typedef boost::multi_index_container< index_map_rect, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(index_map_rect, expr2tc, idx)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(index_map_rect, unsigned int, ctx_level), std::greater< unsigned int > > > >	index_map_containert
typedef std::function< smt_astt(const expr2tc &idx)>	initial_readert
	Gives the initial value of an array at an index, as a function of that index.
typedef boost::multi_index_container< idx_record, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(idx_record, expr2tc, idx)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(idx_record, unsigned int, ctx_level), std::greater< unsigned int > > > >	idx_record_containert
typedef struct array_select	array_selectt
typedef boost::multi_index_container< array_selectt, boost::multi_index::indexed_by< boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_selectt, unsigned int, src_array_update_num), std::greater< unsigned int > >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_selectt, unsigned int, ctx_level), std::greater< unsigned int > > > >	array_select_containert
typedef struct array_with	array_witht
typedef boost::multi_index_container< array_witht, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(array_witht, unsigned int, update_level), std::greater< unsigned int > >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_witht, unsigned int, ctx_level), std::greater< unsigned int > > > >	array_update_containert
typedef struct array_of_val_rec	array_of_val_rect
typedef boost::multi_index_container< array_of_val_rect, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(array_of_val_rect, unsigned int, array_id), std::greater< unsigned int > >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_of_val_rect, unsigned int, ctx_level), std::greater< unsigned int > > > >	array_of_val_containert
typedef struct touched_array	touched_arrayt
typedef boost::multi_index_container< touched_arrayt, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(touched_arrayt, unsigned int, array_id), std::greater< unsigned int > >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(touched_arrayt, unsigned int, ctx_level), std::greater< unsigned int > > > >	touched_array_sett

Public Member Functions
	array_convt (smt_solver_baset *_ctx)
	~array_convt ()=default
smt_astt	mk_array_symbol (const std::string &name, const smt_sort *ms, smt_sortt subtype) override
expr2tc	get_array_elem (smt_astt a, uint64_t index, const type2tc &subtype) override
	Extract an element from the model of an array, at an explicit index.
smt_astt	convert_array_of (smt_astt init_val, unsigned long domain_width) override
	Create an array with a single initializer.
void	add_array_constraints_for_solving () override
virtual smt_astt	convert_array_of_wsort (smt_astt init_val, unsigned long domain_width, smt_sortt arr_sort)
void	set_initial_reader (smt_astt array, initial_readert reader)
	Makes `reader` the source of `array's` initial value at each index it is accessed at, in place of a free variable.
unsigned int	new_array_id ()
void	convert_array_assign (const array_ast *src, smt_astt sym)
smt_astt	mk_select (const array_ast array, const expr2tc &idx, const smt_sort ressort)
virtual smt_astt	mk_store (const array_ast array, const expr2tc &idx, smt_astt value, const smt_sort ressort)
smt_astt	mk_bounded_array_equality (const array_ast a1, const array_ast a2)
smt_astt	array_ite (smt_astt cond, const array_ast true_arr, const array_ast false_arr, const smt_sort *thesort)
smt_astt	encode_array_equality (const array_ast a1, const array_ast a2)
smt_astt	mk_unbounded_select (const array_ast array, const expr2tc &idx, const smt_sort ressort)
smt_astt	mk_unbounded_store (const array_ast array, const expr2tc &idx, smt_astt value, const smt_sort ressort)
smt_astt	unbounded_array_ite (smt_astt cond, const array_ast true_arr, const array_ast false_arr, const smt_sort *thesort)
void	join_array_indexes ()
void	add_array_equalities ()
void	add_array_equality (unsigned int arr1_id, unsigned int arr2_id, unsigned int arr1_update, unsigned int arr2_update, smt_astt &result, unsigned int start_pos=0)
void	execute_array_trans (array_update_vect &data, unsigned int arr, unsigned int idx, const smt_sort *subtype, unsigned int start_point)
void	execute_array_update (ast_vect &dest_data, ast_vect &src_data, const index_map_containert &idx_map, const expr2tc &idx, smt_astt val, unsigned int start_point)
void	execute_array_ite (ast_vect &dest, const ast_vect &true_vals, const ast_vect &false_vals, const index_map_containert &idx_map, smt_astt cond, unsigned int start_point)
void	execute_array_joining_ite (ast_vect &dest, unsigned int cur_id, const array_ast true_arr_ast, const array_ast false_arr_ast, const index_map_containert &idx_map, smt_astt cond, smt_sortt subtype, unsigned int start_point)
void	collate_array_values (ast_vect &vals, unsigned int base_array_id, unsigned int array_update_no, const smt_sort subtype, unsigned int start_point, smt_astt init_val=nullptr, const initial_readert reader=nullptr)
void	add_initial_ackerman_constraints (const ast_vect &vals, const index_map_containert &idx_map, unsigned int start_point)
void	add_new_indexes ()
void	execute_new_updates ()
void	apply_new_selects ()
array_ast *	new_ast (smt_sortt _s)
array_ast *	new_ast (smt_sortt _s, const std::vector< smt_astt > &_a)
void	push_array_ctx () override
void	pop_array_ctx () override
const array_with &	get_array_update (unsigned int id, unsigned int up)
Public Member Functions inherited from array_iface
	array_iface (bool _b, bool inf)
virtual smt_astt	mk_array_symbol (const std::string &name, smt_sortt sort, smt_sortt subtype)=0
smt_astt	default_convert_array_of (smt_astt init_val, unsigned long domain_width, smt_solver_baset *ctx)

Public Attributes
std::vector< idx_record_containert >	array_indexes
std::vector< smt_sortt >	array_subtypes
std::vector< array_select_containert >	array_selects
std::multimap< unsigned int, struct array_equality >	array_equalities
std::vector< array_update_containert >	array_updates
array_of_val_containert	array_of_vals
std::map< unsigned int, initial_readert >	initial_readers
std::vector< index_map_containert >	expr_index_map
std::vector< touched_array_sett >	array_relations
std::vector< unsigned int >	num_arrays_history
std::vector< std::vector< std::vector< smt_astt > > >	array_valuation
smt_solver_baset *	ctx
Public Attributes inherited from array_iface
bool	supports_bools_in_arrays
bool	can_init_infinite_arrays

Member Typedef Documentation

◆ array_of_val_containert

typedef boost::multi_index_container< array_of_val_rect, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(array_of_val_rect, unsigned int, array_id), std::greater<unsigned int> >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_of_val_rect, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::array_of_val_containert

◆ array_of_val_rect

typedef struct array_of_val_rec array_convt::array_of_val_rect

◆ array_select_containert

typedef boost::multi_index_container< array_selectt, boost::multi_index::indexed_by< boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER( array_selectt, unsigned int, src_array_update_num), std::greater<unsigned int> >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_selectt, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::array_select_containert

◆ array_selectt

typedef struct array_select array_convt::array_selectt

◆ array_update_containert

typedef boost::multi_index_container< array_witht, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(array_witht, unsigned int, update_level), std::greater<unsigned int> >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(array_witht, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::array_update_containert

◆ array_update_vect

typedef std::vector<ast_vect> array_convt::array_update_vect

◆ array_witht

typedef struct array_with array_convt::array_witht

◆ ast_vect

typedef smt_solver_baset::ast_vec array_convt::ast_vect

◆ idx_record_containert

typedef boost::multi_index_container< idx_record, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(idx_record, expr2tc, idx)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(idx_record, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::idx_record_containert

◆ index_map_containert

typedef boost::multi_index_container< index_map_rect, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(index_map_rect, expr2tc, idx)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(index_map_rect, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::index_map_containert

◆ index_map_rect

typedef struct index_map_rec array_convt::index_map_rect

◆ initial_readert

typedef std::function<smt_astt(const expr2tc &idx)> array_convt::initial_readert

Gives the initial value of an array at an index, as a function of that index.

◆ touched_array_sett

typedef boost::multi_index_container< touched_arrayt, boost::multi_index::indexed_by< boost::multi_index::ordered_unique< BOOST_MULTI_INDEX_MEMBER(touched_arrayt, unsigned int, array_id), std::greater<unsigned int> >, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(touched_arrayt, unsigned int, ctx_level), std::greater<unsigned int> > > > array_convt::touched_array_sett

◆ touched_arrayt

typedef struct touched_array array_convt::touched_arrayt

Constructor & Destructor Documentation

◆ array_convt()

array_convt::array_convt ( smt_solver_baset * _ctx )

◆ ~array_convt()

array_convt::~array_convt ( )

default

Member Function Documentation

◆ add_array_constraints_for_solving()

void array_convt::add_array_constraints_for_solving ( )

overridevirtual

Reimplemented from array_iface.

◆ add_array_equalities()

void array_convt::add_array_equalities ( )

◆ add_array_equality()

void array_convt::add_array_equality	(	unsigned int	arr1_id,
		unsigned int	arr2_id,
		unsigned int	arr1_update,
		unsigned int	arr2_update,
		smt_astt &	result,
		unsigned int	start_pos = 0 )

◆ add_initial_ackerman_constraints()

void array_convt::add_initial_ackerman_constraints	(	const ast_vect &	vals,
		const index_map_containert &	idx_map,
		unsigned int	start_point )

◆ add_new_indexes()

void array_convt::add_new_indexes ( )

◆ apply_new_selects()

void array_convt::apply_new_selects ( )

◆ array_ite()

smt_astt array_convt::array_ite	(	smt_astt	cond,
		const array_ast *	true_arr,
		const array_ast *	false_arr,
		const smt_sort *	thesort )

◆ collate_array_values()

void array_convt::collate_array_values	(	ast_vect &	vals,
		unsigned int	base_array_id,
		unsigned int	array_update_no,
		const smt_sort *	subtype,
		unsigned int	start_point,
		smt_astt	init_val = nullptr,
		const initial_readert *	reader = nullptr )

◆ convert_array_assign()

void array_convt::convert_array_assign	(	const array_ast *	src,
		smt_astt	sym )

◆ convert_array_of()

smt_astt array_convt::convert_array_of	(	smt_astt	init_val,
		unsigned long	domain_width )

overridevirtual

Create an array with a single initializer.

This may be a small, fixed size array, or it may be a nondeterministically sized array with a word-sized domain. Default implementation is to repeatedly store into the array for as many elements as necessary; subclassing class should override if it has a more efficient method. Nondeterministically sized memory with an initializer is very rare; the only real users of this are fixed-sized (but large) static arrays that are zero initialized, or some infinite-domain modelling arrays used in ESBMC.

Parameters

init_val	The value to initialize each element with.
domain_width	The size of the array to create, in domain bits.

Returns: An AST representing the created constant array.

Implements array_iface.

◆ convert_array_of_wsort()

smt_astt array_convt::convert_array_of_wsort	(	smt_astt	init_val,
		unsigned long	domain_width,
		smt_sortt	arr_sort )

virtual

◆ encode_array_equality()

smt_astt array_convt::encode_array_equality	(	const array_ast *	a1,
		const array_ast *	a2 )

◆ execute_array_ite()

void array_convt::execute_array_ite	(	ast_vect &	dest,
		const ast_vect &	true_vals,
		const ast_vect &	false_vals,
		const index_map_containert &	idx_map,
		smt_astt	cond,
		unsigned int	start_point )

◆ execute_array_joining_ite()

void array_convt::execute_array_joining_ite	(	ast_vect &	dest,
		unsigned int	cur_id,
		const array_ast *	true_arr_ast,
		const array_ast *	false_arr_ast,
		const index_map_containert &	idx_map,
		smt_astt	cond,
		smt_sortt	subtype,
		unsigned int	start_point )

◆ execute_array_trans()

void array_convt::execute_array_trans	(	array_update_vect &	data,
		unsigned int	arr,
		unsigned int	idx,
		const smt_sort *	subtype,
		unsigned int	start_point )

◆ execute_array_update()

void array_convt::execute_array_update	(	ast_vect &	dest_data,
		ast_vect &	src_data,
		const index_map_containert &	idx_map,
		const expr2tc &	idx,
		smt_astt	val,
		unsigned int	start_point )

◆ execute_new_updates()

void array_convt::execute_new_updates ( )

◆ get_array_elem()

expr2tc array_convt::get_array_elem	(	smt_astt	a,
		uint64_t	idx,
		const type2tc &	subtype )

overridevirtual

Extract an element from the model of an array, at an explicit index.

Parameters

array	AST representing the array we are extracting from
index	The index of the element we wish to expect
subtype	The type of the element we are extracting, i.e., array range

Returns: Expression representation of the element

Implements array_iface.

◆ get_array_update()

const array_with & array_convt::get_array_update	(	unsigned int	id,
		unsigned int	up )

inline

◆ join_array_indexes()

void array_convt::join_array_indexes ( )

◆ mk_array_symbol()

smt_astt array_convt::mk_array_symbol	(	const std::string &	name,
		const smt_sort *	ms,
		smt_sortt	subtype )

override

◆ mk_bounded_array_equality()

smt_astt array_convt::mk_bounded_array_equality	(	const array_ast *	a1,
		const array_ast *	a2 )

◆ mk_select()

smt_astt array_convt::mk_select	(	const array_ast *	array,
		const expr2tc &	idx,
		const smt_sort *	ressort )

◆ mk_store()

smt_astt array_convt::mk_store	(	const array_ast *	array,
		const expr2tc &	idx,
		smt_astt	value,
		const smt_sort *	ressort )

virtual

◆ mk_unbounded_select()

smt_astt array_convt::mk_unbounded_select	(	const array_ast *	array,
		const expr2tc &	idx,
		const smt_sort *	ressort )

◆ mk_unbounded_store()

smt_astt array_convt::mk_unbounded_store	(	const array_ast *	array,
		const expr2tc &	idx,
		smt_astt	value,
		const smt_sort *	ressort )

◆ new_array_id()

unsigned int array_convt::new_array_id ( )

◆ new_ast() [1/2]

array_ast * array_convt::new_ast ( smt_sortt _s )

inline

◆ new_ast() [2/2]

array_ast * array_convt::new_ast	(	smt_sortt	_s,
		const std::vector< smt_astt > &	_a )

inline

◆ pop_array_ctx()

void array_convt::pop_array_ctx ( )

overridevirtual

Reimplemented from array_iface.

◆ push_array_ctx()

void array_convt::push_array_ctx ( )

overridevirtual

Reimplemented from array_iface.

◆ set_initial_reader()

void array_convt::set_initial_reader	(	smt_astt	array,
		initial_readert	reader )

Makes reader the source of array's initial value at each index it is accessed at, in place of a free variable.

◆ unbounded_array_ite()

smt_astt array_convt::unbounded_array_ite	(	smt_astt	cond,
		const array_ast *	true_arr,
		const array_ast *	false_arr,
		const smt_sort *	thesort )

Member Data Documentation

◆ array_equalities

std::multimap<unsigned int, struct array_equality> array_convt::array_equalities

◆ array_indexes

std::vector<idx_record_containert> array_convt::array_indexes

◆ array_of_vals

array_of_val_containert array_convt::array_of_vals

◆ array_relations

std::vector<touched_array_sett> array_convt::array_relations

◆ array_selects

std::vector<array_select_containert> array_convt::array_selects

◆ array_subtypes

std::vector<smt_sortt> array_convt::array_subtypes

◆ array_updates

std::vector<array_update_containert> array_convt::array_updates

◆ array_valuation

std::vector<std::vector<std::vector<smt_astt> > > array_convt::array_valuation

◆ ctx

smt_solver_baset* array_convt::ctx

◆ expr_index_map

std::vector<index_map_containert> array_convt::expr_index_map

◆ initial_readers

std::map<unsigned int, initial_readert> array_convt::initial_readers

◆ num_arrays_history

std::vector<unsigned int> array_convt::num_arrays_history

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

src/solvers/smt/array_conv.h
src/solvers/smt/array_conv.cpp

Classes

Public Types

Public Member Functions

Public Attributes

Member Typedef Documentation

◆ array_of_val_containert

◆ array_of_val_rect

◆ array_select_containert

◆ array_selectt

◆ array_update_containert

◆ array_update_vect

◆ array_witht

◆ ast_vect

◆ idx_record_containert

◆ index_map_containert

◆ index_map_rect

◆ initial_readert

◆ touched_array_sett

◆ touched_arrayt

Constructor & Destructor Documentation

◆ array_convt()

◆ ~array_convt()

Member Function Documentation

◆ add_array_constraints_for_solving()

◆ add_array_equalities()

◆ add_array_equality()

◆ add_initial_ackerman_constraints()

◆ add_new_indexes()

◆ apply_new_selects()

◆ array_ite()

◆ collate_array_values()

◆ convert_array_assign()

◆ convert_array_of()

◆ convert_array_of_wsort()

◆ encode_array_equality()

◆ execute_array_ite()

◆ execute_array_joining_ite()

◆ execute_array_trans()

◆ execute_array_update()

◆ execute_new_updates()

◆ get_array_elem()

◆ get_array_update()

◆ join_array_indexes()

◆ mk_array_symbol()

◆ mk_bounded_array_equality()

◆ mk_select()

◆ mk_store()

◆ mk_unbounded_select()

◆ mk_unbounded_store()

◆ new_array_id()

◆ new_ast() [1/2]

◆ new_ast() [2/2]

◆ pop_array_ctx()

◆ push_array_ctx()

◆ set_initial_reader()

◆ unbounded_array_ite()

Member Data Documentation

◆ array_equalities

◆ array_indexes

◆ array_of_vals

◆ array_relations

◆ array_selects

◆ array_subtypes

◆ array_updates

◆ array_valuation

◆ ctx

◆ expr_index_map

◆ initial_readers

◆ num_arrays_history