smt_terms::SymSet< sym_entry > Class Template Reference

symbolic Set class More...

#include <data_structures.hpp>

Public Member Functions
	SymSet ()
	SymSet (const cvc5::Term &term, Solver *s, TermType type=TermType::SymSet)
	SymSet (const cvc5::Sort &entry_sort, TermType entry_type, Solver *s, const std::string &name="")
	Construct a new empty Symbolic Set object.
	SymSet (const std::vector< sym_entry > &entries, const std::string &name="")
	Construct a new Symbolic Set object.
void	insert (const sym_entry &entry)
void	contains (const sym_entry &entry) const
	Create an inclusion constraint.
void	not_contains (const sym_entry &entry) const
	Create an inclusion constraint.
	operator std::string () const
	operator cvc5::Term () const
void	print_trace () const
	SymSet (const SymSet &other)=default
	SymSet (SymSet &&other)=default
SymSet &	operator= (const SymSet &right)=default
SymSet &	operator= (SymSet &&right)=default
	~SymSet ()=default

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

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

Detailed Description

template<ConstructibleFromTerm sym_entry>
class smt_terms::SymSet< sym_entry >

symbolic Set class

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

Definition at line 289 of file data_structures.hpp.

Constructor & Destructor Documentation

SymSet() [1/6]

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::SymSet ( )

inline

Definition at line 298 of file data_structures.hpp.

SymSet() [2/6]

template<ConstructibleFromTerm sym_entry>

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

inline

Definition at line 303 of file data_structures.hpp.

SymSet() [3/6]

template<ConstructibleFromTerm sym_entry>

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

inline

Construct a new empty Symbolic Set object.

Parameters

entry_sort	cvc5 sort
entry_type	Symbolic term type
s	pointer to solver
name	name of the resulting symbolic variable, defaults to var_{i}

Definition at line 316 of file data_structures.hpp.

SymSet() [4/6]

template<ConstructibleFromTerm sym_entry>

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

inline

Construct a new Symbolic Set object.

Parameters

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

Definition at line 338 of file data_structures.hpp.

SymSet() [5/6]

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::SymSet ( const SymSet< sym_entry > &  other )

default

SymSet() [6/6]

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::SymSet ( SymSet< sym_entry > &&  other )

default

~SymSet()

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::~SymSet ( )

default

Member Function Documentation

contains()

template<ConstructibleFromTerm sym_entry>

void smt_terms::SymSet< sym_entry >::contains ( const sym_entry &  entry ) const

inline

Create an inclusion constraint.

Parameters

entry

entry to be checked

Todo:

(alex) maybe it should return the term value, for bool comaptibility

Definition at line 379 of file data_structures.hpp.

insert()

template<ConstructibleFromTerm sym_entry>

void smt_terms::SymSet< sym_entry >::insert ( const sym_entry &  entry )

inline

Definition at line 368 of file data_structures.hpp.

not_contains()

template<ConstructibleFromTerm sym_entry>

void smt_terms::SymSet< sym_entry >::not_contains ( const sym_entry &  entry ) const

inline

Create an inclusion constraint.

Parameters

entry

entry to be checked

Definition at line 393 of file data_structures.hpp.

operator cvc5::Term()

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::operator cvc5::Term ( ) const

inline

Definition at line 404 of file data_structures.hpp.

operator std::string()

template<ConstructibleFromTerm sym_entry>

smt_terms::SymSet< sym_entry >::operator std::string ( ) const

inline

Definition at line 403 of file data_structures.hpp.

operator=() [1/2]

template<ConstructibleFromTerm sym_entry>

SymSet & smt_terms::SymSet< sym_entry >::operator= ( const SymSet< sym_entry > &  right )

default

operator=() [2/2]

template<ConstructibleFromTerm sym_entry>

SymSet & smt_terms::SymSet< sym_entry >::operator= ( SymSet< sym_entry > &&  right )

default

print_trace()

template<ConstructibleFromTerm sym_entry>

void smt_terms::SymSet< sym_entry >::print_trace ( ) const

inline

Definition at line 406 of file data_structures.hpp.

Friends And Related Symbol Documentation

operator<<

template<ConstructibleFromTerm sym_entry>

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

friend

Definition at line 408 of file data_structures.hpp.

Member Data Documentation

entry_type

template<ConstructibleFromTerm sym_entry>

TermType smt_terms::SymSet< sym_entry >::entry_type

Definition at line 296 of file data_structures.hpp.

solver

template<ConstructibleFromTerm sym_entry>

Solver* smt_terms::SymSet< sym_entry >::solver

Definition at line 292 of file data_structures.hpp.

term

template<ConstructibleFromTerm sym_entry>

cvc5::Term smt_terms::SymSet< sym_entry >::term

Definition at line 293 of file data_structures.hpp.

type

template<ConstructibleFromTerm sym_entry>

TermType smt_terms::SymSet< sym_entry >::type = TermType::SymSet

Definition at line 295 of file data_structures.hpp.

---

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

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