smt_terms::STuple Class Reference

sym Tuple class More...

#include <data_structures.hpp>

Public Member Functions
	STuple ()
	STuple (const cvc5::Term &term, Solver *s, TermType type=TermType::STuple)
	STuple (const std::vector< STerm > &terms)
	Construct a new STuple object.
void	operator== (const STuple &other) const
void	operator!= (const STuple &other) const
cvc5::Sort	get_sort () const
	Get the obtained tuple sort.
	operator std::string () const
	operator cvc5::Term () const
	STuple (const STuple &other)=default
	STuple (STuple &&other)=default
STuple &	operator= (const STuple &right)=default
STuple &	operator= (STuple &&right)=default
	~STuple ()=default

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

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

Detailed Description

sym Tuple class

allows to group separate STerms in one place

Definition at line 16 of file data_structures.hpp.

Constructor & Destructor Documentation

STuple() [1/5]

smt_terms::STuple::STuple ( )

inline

Definition at line 22 of file data_structures.hpp.

STuple() [2/5]

smt_terms::STuple::STuple ( const cvc5::Term &  term, Solver *  s, TermType  type = TermType::STuple  )

inline

Definition at line 26 of file data_structures.hpp.

STuple() [3/5]

smt_terms::STuple::STuple ( const std::vector< STerm > &  terms )

inline

Construct a new STuple object.

Parameters

terms

vector of terms to store in tuple

Definition at line 36 of file data_structures.hpp.

STuple() [4/5]

smt_terms::STuple::STuple ( const STuple &  other )

default

STuple() [5/5]

smt_terms::STuple::STuple ( STuple &&  other )

default

~STuple()

smt_terms::STuple::~STuple ( )

default

Member Function Documentation

get_sort()

cvc5::Sort smt_terms::STuple::get_sort ( ) const

inline

Get the obtained tuple sort.

Returns

cvc5::Sort

Definition at line 76 of file data_structures.hpp.

operator cvc5::Term()

smt_terms::STuple::operator cvc5::Term ( ) const

inline

Definition at line 79 of file data_structures.hpp.

operator std::string()

smt_terms::STuple::operator std::string ( ) const

inline

Definition at line 78 of file data_structures.hpp.

operator!=()

void smt_terms::STuple::operator!= ( const STuple &  other ) const

inline

Create an inequality constraint between two symbolic tuples of the same type

Definition at line 64 of file data_structures.hpp.

operator=() [1/2]

STuple & smt_terms::STuple::operator= ( const STuple &  right )

default

operator=() [2/2]

STuple & smt_terms::STuple::operator= ( STuple &&  right )

default

operator==()

void smt_terms::STuple::operator== ( const STuple &  other ) const

inline

Create an equality constraint between two symbolic tuples of the same type

Definition at line 54 of file data_structures.hpp.

Friends And Related Symbol Documentation

operator<<

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

friend

Definition at line 81 of file data_structures.hpp.

Member Data Documentation

solver

Solver* smt_terms::STuple::solver

Definition at line 18 of file data_structures.hpp.

term

cvc5::Term smt_terms::STuple::term

Definition at line 19 of file data_structures.hpp.

type

TermType smt_terms::STuple::type = TermType::STuple

Definition at line 20 of file data_structures.hpp.

---

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

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