array_iface Class Reference

#include <smt_array.h>

Inheritance diagram for array_iface:

Public Member Functions
	array_iface (bool _b, bool inf)
virtual smt_astt	mk_array_symbol (const std::string &name, smt_sortt sort, smt_sortt subtype)=0
virtual expr2tc	get_array_elem (smt_astt a, uint64_t idx, const type2tc &subtype)=0
	Extract an element from the model of an array, at an explicit index.
virtual smt_astt	convert_array_of (smt_astt init_val, unsigned long domain_width)=0
	Create an array with a single initializer.
smt_astt	default_convert_array_of (smt_astt init_val, unsigned long domain_width, smt_solver_baset *ctx)
virtual void	add_array_constraints_for_solving ()
virtual void	push_array_ctx ()
virtual void	pop_array_ctx ()

Public Attributes
bool	supports_bools_in_arrays
bool	can_init_infinite_arrays

Constructor & Destructor Documentation

array_iface()

array_iface::array_iface ( bool _b, bool inf )

inline

Member Function Documentation

add_array_constraints_for_solving()

virtual void array_iface::add_array_constraints_for_solving ( )

inlinevirtual

Reimplemented in array_convt.

convert_array_of()

virtual smt_astt array_iface::convert_array_of ( smt_astt init_val, unsigned long domain_width )

pure virtual

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.

Implemented in array_convt, bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

default_convert_array_of()

smt_astt array_iface::default_convert_array_of	(	smt_astt	init_val,
		unsigned long	domain_width,
		smt_solver_baset *	ctx )

get_array_elem()

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

pure virtual

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

Implemented in array_convt, bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_array_symbol()

virtual smt_astt array_iface::mk_array_symbol ( const std::string & name, smt_sortt sort, smt_sortt subtype )

pure virtual

pop_array_ctx()

virtual void array_iface::pop_array_ctx ( )

inlinevirtual

Reimplemented in array_convt.

push_array_ctx()

virtual void array_iface::push_array_ctx ( )

inlinevirtual

Reimplemented in array_convt.

Member Data Documentation

can_init_infinite_arrays

bool array_iface::can_init_infinite_arrays

supports_bools_in_arrays

bool array_iface::supports_bools_in_arrays

---

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

• src/solvers/smt/smt_array.h
• src/solvers/smt/smt_solver.cpp