smt_terms::SymArray< sym_index, sym_entry > Class Template Reference

symbolic Array class More...

#include <data_structures.hpp>

Public Member Functions
	SymArray ()
	SymArray (const cvc5::Term &term, Solver *s, TermType type=TermType::SymArray)
	SymArray (const cvc5::Sort &index_sort, const TermType &index_type, const cvc5::Sort &entry_sort, const TermType &entry_type, Solver *s, const std::string &name="")
	Construct an empty Symbolic Array object.
	SymArray (const std::vector< sym_index > &indicies, const std::vector< sym_entry > &entries, const std::string &name="")
	Construct a new Symbolic Array object.
	SymArray (const std::vector< sym_entry > &entries, const STerm &index_base, const std::string &name="")
	Construct a new Symbolic Array object.
sym_entry	get (const sym_index &ind) const
sym_entry	operator[] (const sym_index &ind) const
void	put (const sym_index &ind, const sym_entry &entry)
	operator std::string () const
	operator cvc5::Term () const
void	print_trace () const
	SymArray (const SymArray &other)=default
	SymArray (SymArray &&other)=default
SymArray &	operator= (const SymArray &right)=default
SymArray &	operator= (SymArray &&right)=default
	~SymArray ()=default

Public Attributes
Solver *	solver
cvc5::Term	term
TermType	type = TermType::SymArray
TermType	ind_type
TermType	entry_type

Friends
std::ostream &	operator<< (std::ostream &out, const SymArray &term)

Detailed Description

template<typename sym_index, ConstructibleFromTerm sym_entry>
class smt_terms::SymArray< sym_index, sym_entry >

symbolic Array class

allows to group separate STerms in one place and perform operations over sym indicies Compatible parameters: STerm Bool STuple SymArray SymSet

Definition at line 108 of file data_structures.hpp.

Constructor & Destructor Documentation

SymArray() [1/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( )

inline

Definition at line 118 of file data_structures.hpp.

SymArray() [2/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( const cvc5::Term &  term, Solver *  s, TermType  type = TermType::SymArray< sym_index, sym_entry >  )

inline

Definition at line 124 of file data_structures.hpp.

SymArray() [3/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( const cvc5::Sort &  index_sort, const TermType &  index_type, const cvc5::Sort &  entry_sort, const TermType &  entry_type, Solver *  s, const std::string &  name = ""  )

inline

Construct an empty Symbolic Array object.

Parameters

index_sort	cvc5 Sort of an index
index_type	type of index Symbolic Term
entry_sort	cvc5 Sort of an entry
entry_type	type of entry Symbolic Term
s	pointer to solver
name	name of the resulting symbolic variable, defaults to var_{i}

Definition at line 144 of file data_structures.hpp.

SymArray() [4/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( const std::vector< sym_index > &  indicies, const std::vector< sym_entry > &  entries, const std::string &  name = ""  )

inline

Construct a new Symbolic Array object.

Parameters

indicies	vector of symbolic objects
entries	vector of symbolic objects
name	name of the resulting symbolic variable, defaults to var_{i}

Definition at line 173 of file data_structures.hpp.

SymArray() [5/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( const std::vector< sym_entry > &  entries, const STerm &  index_base, const std::string &  name = ""  )

inline

Construct a new Symbolic Array object.

Creates a vector-like array with constant integer indicies

Parameters

entries	vector of symbolic entries
index_base	example of an index. Needed to extract the sort out of STerm
name	name of the resulting symbolic variable, defaults to var_{i}

Definition at line 218 of file data_structures.hpp.

SymArray() [6/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( const SymArray< sym_index, sym_entry > &  other )

default

SymArray() [7/7]

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::SymArray ( SymArray< sym_index, sym_entry > &&  other )

default

~SymArray()

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::~SymArray ( )

default

Member Function Documentation

get()

template<typename sym_index , ConstructibleFromTerm sym_entry>

sym_entry smt_terms::SymArray< sym_index, sym_entry >::get ( const sym_index &  ind ) const

inline

Definition at line 247 of file data_structures.hpp.

operator cvc5::Term()

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::operator cvc5::Term ( ) const

inline

Definition at line 261 of file data_structures.hpp.

operator std::string()

template<typename sym_index , ConstructibleFromTerm sym_entry>

smt_terms::SymArray< sym_index, sym_entry >::operator std::string ( ) const

inline

Definition at line 260 of file data_structures.hpp.

operator=() [1/2]

template<typename sym_index , ConstructibleFromTerm sym_entry>

SymArray & smt_terms::SymArray< sym_index, sym_entry >::operator= ( const SymArray< sym_index, sym_entry > &  right )

default

operator=() [2/2]

template<typename sym_index , ConstructibleFromTerm sym_entry>

SymArray & smt_terms::SymArray< sym_index, sym_entry >::operator= ( SymArray< sym_index, sym_entry > &&  right )

default

operator[]()

template<typename sym_index , ConstructibleFromTerm sym_entry>

sym_entry smt_terms::SymArray< sym_index, sym_entry >::operator[] ( const sym_index &  ind ) const

inline

Definition at line 253 of file data_structures.hpp.

print_trace()

template<typename sym_index , ConstructibleFromTerm sym_entry>

void smt_terms::SymArray< sym_index, sym_entry >::print_trace ( ) const

inline

Definition at line 263 of file data_structures.hpp.

put()

template<typename sym_index , ConstructibleFromTerm sym_entry>

void smt_terms::SymArray< sym_index, sym_entry >::put ( const sym_index &  ind, const sym_entry &  entry  )

inline

Definition at line 255 of file data_structures.hpp.

Friends And Related Symbol Documentation

operator<<

template<typename sym_index , ConstructibleFromTerm sym_entry>

std::ostream & operator<< ( std::ostream &  out, const SymArray< sym_index, sym_entry > &  term  )

friend

Definition at line 265 of file data_structures.hpp.

Member Data Documentation

entry_type

template<typename sym_index , ConstructibleFromTerm sym_entry>

TermType smt_terms::SymArray< sym_index, sym_entry >::entry_type

Definition at line 116 of file data_structures.hpp.

ind_type

template<typename sym_index , ConstructibleFromTerm sym_entry>

TermType smt_terms::SymArray< sym_index, sym_entry >::ind_type

Definition at line 115 of file data_structures.hpp.

solver

template<typename sym_index , ConstructibleFromTerm sym_entry>

Solver* smt_terms::SymArray< sym_index, sym_entry >::solver

Definition at line 111 of file data_structures.hpp.

term

template<typename sym_index , ConstructibleFromTerm sym_entry>

cvc5::Term smt_terms::SymArray< sym_index, sym_entry >::term

Definition at line 112 of file data_structures.hpp.

type

template<typename sym_index , ConstructibleFromTerm sym_entry>

TermType smt_terms::SymArray< sym_index, sym_entry >::type = TermType::SymArray

Definition at line 114 of file data_structures.hpp.

---

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

• src/barretenberg/smt_verification/terms/data_structures.hpp