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

Public Member Functions

Public Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ SymArray() [1/7]

◆ SymArray() [2/7]

◆ SymArray() [3/7]

◆ SymArray() [4/7]

◆ SymArray() [5/7]

◆ SymArray() [6/7]

◆ SymArray() [7/7]

◆ ~SymArray()

Member Function Documentation

◆ get()

◆ operator cvc5::Term()

◆ operator std::string()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]()

◆ print_trace()

◆ put()

Friends And Related Symbol Documentation

◆ operator<<

Member Data Documentation

◆ entry_type

◆ ind_type

◆ solver

◆ term

◆ type