tuple_node_smt_ast Class Reference

Function app representing a tuple sorted value. More...

#include <smt_tuple_node_ast.h>

Inheritance diagram for tuple_node_smt_ast:

Public Member Functions
	tuple_node_smt_ast (smt_tuple_node_flattener &f, smt_solver_baset *ctx, smt_sortt s, std::string _name)
	Primary constructor.
	~tuple_node_smt_ast () override=default
smt_astt	ite (smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const override
smt_astt	eq (smt_solver_baset *ctx, smt_astt other) const override
	Abstractly produce an equality.
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	project (smt_solver_baset *ctx, unsigned int elem) const override
	Project a member from a structure, or an field-array from a struct array.
void	dump () const override
void	make_free (smt_solver_baset *ctx)
void	pre_ite (smt_solver_baset *ctx, smt_astt cond, smt_astt falseop)
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.

Public Attributes
const std::string	name
	The symbol prefix of the variables representing this tuples value, as a string (i.e., no associated type).
smt_tuple_node_flattener &	flat
std::vector< smt_astt >	elements
const unsigned int	creation_ctx_level
	Context level this AST was created at.
Public Attributes inherited from smt_ast
smt_sortt	sort
	The sort of this function application.
const smt_solver_baset *	context
	The solver context.

Detailed Description

Function app representing a tuple sorted value.

This AST represents any kind of SMT function that results in something of a tuple sort. As documented in smt_tuple.c, the result of any kind of tuple operation that gets flattened is a symbol prefix, which is what this ast actually stores.

This AST should only be used in smt_tuple.c, if you're using it elsewhere think very hard about what you're trying to do. Its creation should also only occur if there is no tuple support in the solver being used, and a tuple creating method has been called.

See also

smt_tuple.c

Constructor & Destructor Documentation

tuple_node_smt_ast()

tuple_node_smt_ast::tuple_node_smt_ast ( smt_tuple_node_flattener & f, smt_solver_baset * ctx, smt_sortt s, std::string _name )

inline

Primary constructor.

Parameters

s	The sort of the tuple, of type tuple_smt_sort.
_name	The symbol prefix of the variables representing this tuples value.

~tuple_node_smt_ast()

tuple_node_smt_ast::~tuple_node_smt_ast ( )

overridedefault

Member Function Documentation

assign()

void tuple_node_smt_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 tuple_node_smt_ast::dump ( ) const

inlineoverridevirtual

Reimplemented from smt_ast.

eq()

smt_astt tuple_node_smt_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.

ite()

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

overridevirtual

Reimplemented from smt_ast.

make_free()

void tuple_node_smt_ast::make_free

(

smt_solver_baset *

ctx

)

pre_ite()

void tuple_node_smt_ast::pre_ite	(	smt_solver_baset *	ctx,
		smt_astt	cond,
		smt_astt	falseop )

project()

smt_astt tuple_node_smt_ast::project ( smt_solver_baset * ctx, unsigned int elem ) const

overridevirtual

Project a member from a structure, or an field-array from a struct array.

Parameters

ctx	SMT context to produce this in.
elem	Struct index to project.

Returns

AST representing the chosen element / element-array

Reimplemented from smt_ast.

select()

smt_astt tuple_node_smt_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 tuple_node_smt_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

creation_ctx_level

const unsigned int tuple_node_smt_ast::creation_ctx_level

Context level this AST was created at.

elements are allocated lazily, so they can belong to a deeper level than the AST itself; those outlive their contents unless the flattener clears them on the way back down (issue #6831).

elements

std::vector<smt_astt> tuple_node_smt_ast::elements

flat

smt_tuple_node_flattener& tuple_node_smt_ast::flat

name

const std::string tuple_node_smt_ast::name

The symbol prefix of the variables representing this tuples value, as a string (i.e., no associated type).

---

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

• src/solvers/smt/tuple/smt_tuple_node_ast.h
• src/solvers/smt/tuple/smt_tuple_node_ast.cpp