smt_tuple_sym_flattener Class Reference

#include <smt_tuple_sym.h>

Inheritance diagram for smt_tuple_sym_flattener:

Public Member Functions
	smt_tuple_sym_flattener (smt_solver_baset *_ctx, const namespacet &_ns)
virtual	~smt_tuple_sym_flattener ()=default
smt_sortt	mk_struct_sort (const type2tc &type) override
	Create a sort representing a struct.
smt_astt	tuple_create (const expr2tc &structdef) override
	Create a new tuple from a struct definition.
smt_astt	tuple_fresh (smt_sortt s, std::string name="") override
	Create a fresh tuple, with freely valued fields.
smt_astt	tuple_array_of (const expr2tc &init_value, unsigned long domain_width) override
	Create a potentially /large/ array of tuples.
smt_astt	mk_tuple_symbol (const std::string &name, smt_sortt s) override
	Convert a symbol to a tuple_smt_ast.
smt_astt	mk_tuple_array_symbol (const expr2tc &expr) override
	Like mk_tuple_symbol, but for arrays.
expr2tc	tuple_get (const expr2tc &expr) override
	Extract the assignment to a tuple-typed symbol from the SMT solvers model.
expr2tc	tuple_get (const type2tc &type, smt_astt a) override
expr2tc	tuple_get_array_elem (smt_astt array, uint64_t index, const type2tc &subtype) override
expr2tc	tuple_get_rec (tuple_sym_smt_astt tuple)
smt_astt	tuple_array_create (const type2tc &array_type, smt_astt *input_args, bool const_array, smt_sortt domain) override
Public Member Functions inherited from tuple_iface
virtual void	add_tuple_constraints_for_solving ()
virtual void	push_tuple_ctx ()
virtual void	pop_tuple_ctx ()
virtual	~tuple_iface ()=default

Public Attributes
smt_solver_baset *	ctx
const namespacet &	ns

Constructor & Destructor Documentation

smt_tuple_sym_flattener()

smt_tuple_sym_flattener::smt_tuple_sym_flattener ( smt_solver_baset * _ctx, const namespacet & _ns )

inline

~smt_tuple_sym_flattener()

virtual smt_tuple_sym_flattener::~smt_tuple_sym_flattener ( )

virtualdefault

Member Function Documentation

mk_struct_sort()

smt_sortt smt_tuple_sym_flattener::mk_struct_sort ( const type2tc & type )

overridevirtual

Create a sort representing a struct.

i.e., a tuple. Ideally this should actually be part of the overridden tuple api, but due to history it isn't yet. If solvers don't support tuples, implement this to abort.

Parameters

type	The struct type to create a tuple representation of.

Returns

The tuple representation of the type, wrapped in an smt_sort.

Implements tuple_iface.

mk_tuple_array_symbol()

smt_astt smt_tuple_sym_flattener::mk_tuple_array_symbol ( const expr2tc & expr )

overridevirtual

Like mk_tuple_symbol, but for arrays.

Implements tuple_iface.

mk_tuple_symbol()

smt_astt smt_tuple_sym_flattener::mk_tuple_symbol ( const std::string & name, smt_sortt s )

overridevirtual

Convert a symbol to a tuple_smt_ast.

Implements tuple_iface.

tuple_array_create()

smt_astt smt_tuple_sym_flattener::tuple_array_create ( const type2tc & array_type, smt_astt * input_args, bool const_array, smt_sortt domain )

overridevirtual

Implements tuple_iface.

tuple_array_of()

smt_astt smt_tuple_sym_flattener::tuple_array_of ( const expr2tc & init_value, unsigned long domain_width )

overridevirtual

Create a potentially /large/ array of tuples.

This is called when we encounter an array_of operation, with a very large array size, of tuple sort.

Parameters

Expression	of tuple value to populate this array with.
domain_width	The size of array to create, in domain bits.

Returns

An AST representing an array of the tuple value, init_value.

Implements tuple_iface.

tuple_create()

smt_astt smt_tuple_sym_flattener::tuple_create ( const expr2tc & structdef )

overridevirtual

Create a new tuple from a struct definition.

Parameters

structdef

A constant_struct2tc, describing all the members of the tuple to create.

Returns

AST representing the created tuple

Implements tuple_iface.

tuple_fresh()

smt_astt smt_tuple_sym_flattener::tuple_fresh ( smt_sortt s, std::string name = "" )

overridevirtual

Create a fresh tuple, with freely valued fields.

Parameters

s	Sort of the tuple to create

Returns

AST representing the created tuple

Implements tuple_iface.

tuple_get() [1/2]

expr2tc smt_tuple_sym_flattener::tuple_get ( const expr2tc & expr )

overridevirtual

Extract the assignment to a tuple-typed symbol from the SMT solvers model.

Implements tuple_iface.

tuple_get() [2/2]

expr2tc smt_tuple_sym_flattener::tuple_get ( const type2tc & type, smt_astt a )

overridevirtual

Implements tuple_iface.

tuple_get_array_elem()

expr2tc smt_tuple_sym_flattener::tuple_get_array_elem ( smt_astt array, uint64_t index, const type2tc & subtype )

overridevirtual

Implements tuple_iface.

tuple_get_rec()

expr2tc smt_tuple_sym_flattener::tuple_get_rec

(

tuple_sym_smt_astt

tuple

)

Member Data Documentation

ctx

smt_solver_baset* smt_tuple_sym_flattener::ctx

ns

const namespacet& smt_tuple_sym_flattener::ns

---

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

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