tuple_iface Class Reference

#include <smt_tuple.h>

Inheritance diagram for tuple_iface:

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

Constructor & Destructor Documentation

~tuple_iface()

virtual tuple_iface::~tuple_iface ( )

virtualdefault

Member Function Documentation

add_tuple_constraints_for_solving()

virtual void tuple_iface::add_tuple_constraints_for_solving ( )

inlinevirtual

Reimplemented in smt_tuple_node_flattener.

mk_struct_sort()

virtual smt_sortt tuple_iface::mk_struct_sort ( const type2tc & type )

pure virtual

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.

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

mk_tuple_array_symbol()

virtual smt_astt tuple_iface::mk_tuple_array_symbol ( const expr2tc & expr )

pure virtual

Like mk_tuple_symbol, but for arrays.

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

mk_tuple_symbol()

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

pure virtual

Convert a symbol to a tuple_smt_ast.

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

pop_tuple_ctx()

virtual void tuple_iface::pop_tuple_ctx ( )

inlinevirtual

Reimplemented in smt_tuple_node_flattener.

push_tuple_ctx()

virtual void tuple_iface::push_tuple_ctx ( )

inlinevirtual

Reimplemented in smt_tuple_node_flattener.

tuple_array_create()

virtual smt_astt tuple_iface::tuple_array_create ( const type2tc & array_type, smt_astt * inputargs, bool const_array, smt_sortt domain )

pure virtual

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, and yices_convt.

tuple_array_of()

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

pure virtual

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.

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

tuple_create()

virtual smt_astt tuple_iface::tuple_create ( const expr2tc & structdef )

pure virtual

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

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

tuple_fresh()

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

pure virtual

Create a fresh tuple, with freely valued fields.

Parameters

s	Sort of the tuple to create

Returns

AST representing the created tuple

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, and yices_convt.

tuple_get() [1/2]

virtual expr2tc tuple_iface::tuple_get ( const expr2tc & expr )

pure virtual

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

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

tuple_get() [2/2]

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

pure virtual

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

tuple_get_array_elem()

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

pure virtual

Implemented in smt_tuple_node_flattener, smt_tuple_sym_flattener, yices_convt, and z3_convt.

---

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

• src/solvers/smt/tuple/smt_tuple.h