array_ast Class Reference

#include <array_conv.h>

Inheritance diagram for array_ast:

Public Member Functions
	array_ast (array_convt *actx, smt_solver_baset *ctx, const smt_sort *_s)
	array_ast (array_convt *actx, smt_solver_baset *ctx, const smt_sort *_s, std::vector< smt_astt > _a)
	~array_ast () override=default
smt_astt	eq (smt_solver_baset *ctx, smt_astt other) const override
	Abstractly produce an equality.
smt_astt	ite (smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const override
void	assign (smt_solver_baset *ctx, smt_astt sym) const override
	Abstractly produce an assign.
smt_astt	update (smt_solver_baset *ctx, smt_astt value, unsigned int idx, const expr2tc &idx_expr=expr2tc()) const override
	Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.
smt_astt	select (smt_solver_baset *ctx, const expr2tc &idx) const override
	Select a value from an array, for both normal arrays and tuple arrays.
smt_astt	eq_fixedsize (smt_solver_baset *ctx, const array_ast *other) const
void	dump () const override
Public Member Functions inherited from smt_ast
	smt_ast (smt_solver_baset *ctx, smt_sortt s)
virtual	~smt_ast ()=default
virtual smt_astt	with_sort (smt_solver_baset *ctx, smt_sortt s) const
	The same solver term under a different sort.
virtual smt_astt	project (smt_solver_baset *ctx, unsigned int elem) const
	Project a member from a structure, or an field-array from a struct array.

Public Attributes
std::string	symname
std::vector< smt_astt >	array_fields
unsigned int	base_array_id
unsigned int	array_update_num
array_convt *	array_ctx
Public Attributes inherited from smt_ast
smt_sortt	sort
	The sort of this function application.
const smt_solver_baset *	context
	The solver context.

Constructor & Destructor Documentation

array_ast() [1/2]

array_ast::array_ast ( array_convt * actx, smt_solver_baset * ctx, const smt_sort * _s )

inline

array_ast() [2/2]

array_ast::array_ast ( array_convt * actx, smt_solver_baset * ctx, const smt_sort * _s, std::vector< smt_astt > _a )

inline

~array_ast()

array_ast::~array_ast ( )

overridedefault

Member Function Documentation

assign()

void array_ast::assign ( smt_solver_baset * ctx, smt_astt sym ) const

overridevirtual

Abstractly produce an assign.

Defaults to being an equality, however for some special cases up to the backend, there may be optimizations made for array or tuple assigns, and so forth.

Parameters

ctx	SMT context to do the assignment in.
sym	Symbol to assign to

Reimplemented from smt_ast.

dump()

void array_ast::dump ( ) const

inlineoverridevirtual

Reimplemented from smt_ast.

eq()

smt_astt array_ast::eq ( smt_solver_baset * ctx, smt_astt other ) const

overridevirtual

Abstractly produce an equality.

Does the right thing (TM) whether it's a normal piece of AST or a tuple / array.

Parameters

ctx	SMT context to produce the equality in.
other	Piece of AST to compare 'this' with.

Returns

Boolean typed AST representing an equality

Reimplemented from smt_ast.

eq_fixedsize()

smt_astt array_ast::eq_fixedsize	(	smt_solver_baset *	ctx,
		const array_ast *	other ) const

ite()

smt_astt array_ast::ite ( smt_solver_baset * ctx, smt_astt cond, smt_astt falseop ) const

overridevirtual

Reimplemented from smt_ast.

select()

smt_astt array_ast::select ( smt_solver_baset * ctx, const expr2tc & idx ) const

overridevirtual

Select a value from an array, for both normal arrays and tuple arrays.

Parameters

ctx	SMT context to produce this in.
idx	Index to select the value from.

Returns

AST of the array's range sort representing the selected item

Reimplemented from smt_ast.

update()

smt_astt array_ast::update ( smt_solver_baset * ctx, smt_astt value, unsigned int idx, const expr2tc & idx_expr = expr2tc() ) const

overridevirtual

Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.

Parameters

ctx	SMT context to make this update in.
value	Value to insert into the updated field
idx	Array index or tuple field
idx_expr	If an array, expression representing the index

Returns

AST of this type, representing the update

Reimplemented from smt_ast.

Member Data Documentation

array_ctx

array_convt* array_ast::array_ctx

array_fields

std::vector<smt_astt> array_ast::array_fields

array_update_num

unsigned int array_ast::array_update_num

base_array_id

unsigned int array_ast::base_array_id

symname

std::string array_ast::symname

---

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

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