Term 

The Term class represents an arbitrary expression of any of the supported sorts. The list of all supported kinds of terms is given by the Kind enum. The Term class provides functions for general inspection (e.g., comparison, retrieving the kind and sort, accessing sub-terms), but also functions for retrieving constant values for the supported theories (i.e., is<Type>Value() and get<Type>Value() , which returns the constant values in the best type standard C++ offers).

Additionally, a Term can be hashed (using std::hash<cvc5::Term> ) and given to output streams, including terms within standard containers like std::map , std::set , or std::vector .

The Term only offers the default constructor to create a null term. Instead, the TermManager class provides factory functions to create terms, e.g., TermManager::mkTerm() for generic terms and TermManager::mk<Type>() for constants, variables and values of a given type.

class cvc5::Term
std::ostream& cvc5::operator<< (std::ostream& out, const Term& t)
std::ostream& cvc5::operator<< (std::ostream& out, const std::vector<Term>& vector)
std::ostream& cvc5::operator<< (std::ostream& out, const std::set<Term>& set)
std::ostream& cvc5::operator<< (std::ostream& out, const std::unordered_set<Term>& set)
template<typename V> std::ostream& cvc5::operator<< (std::ostream& out, const std::map<Term, V>& map)
template<typename V> std::ostream& cvc5::operator<< (std::ostream& out, const std::unordered_map<Term, V>& map)
std::hash<cvc5::Term>

class Term 

A cvc5 Term .

Public Functions

Term ( ) : Constructor for a null term.

~Term ( ) : Destructor.

bool operator == ( const Term & t ) const 

Syntactic equality operator.

Parameters :: t – The term to compare to for equality.
Returns :: True if the terms are equal.

bool operator != ( const Term & t ) const 

Syntactic disequality operator.

Parameters :: t – The term to compare to for disequality.
Returns :: True if terms are disequal.

bool operator < ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is less than t.

bool operator > ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is greater than t.

bool operator <= ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is less than or equal to t.

bool operator >= ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is greater than or equal to t.

size_t getNumChildren ( ) const 

Get the number of children of this term.

Returns :: The number of children of this term.

Term operator [] ( size_t index ) const 

Get the child term of this term at a given index.

Parameters :: index – The index of the child.
Returns :: The child term at the given index.

uint64_t getId ( ) const 

Get the id of this term.

Returns :: The id of this term.

Kind getKind ( ) const 

Get the kind of this term.

Returns :: The kind of this term.

Sort getSort ( ) const 

Get the sort of this term.

Returns :: The sort of this term.

Term substitute ( const Term & term , const Term & replacement ) const 

Replace term with replacement in this term.

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Parameters :

term – The term to replace.
replacement – The term to replace it with.

Returns :

The result of replacing term with replacement in this term.

Term substitute ( const std :: vector < Term > & terms , const std :: vector < Term > & replacements ) const 

Simultaneously replace terms with replacements in this term.

In the case that terms contains duplicates, the replacement earliest in the vector takes priority. For example, calling substitute on f(x,y) with terms = { x, z } , replacements = { g(z), w } results in the term f(g(z),y) .

Note

Requires that terms and replacements are of equal size (they are interpreted as 1 : 1 mapping).

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Parameters :

terms – The terms to replace.
replacements – The replacement terms.

Returns :

The result of simultaneously replacing terms with replacements in this term.

bool hasOp ( ) const 

Determine if this term has an operator.

Returns :: True iff this term has an operator.

Op getOp ( ) const 

Get the operator of a term with an operator.

Note

Requires that this term has an operator (see hasOp() ).

Returns :: The Op used to create this term.

bool hasSymbol ( ) const 

Determine if this term has a symbol (a name).

For example, free constants and variables have symbols.

Returns :: True if the term has a symbol.

std :: string getSymbol ( ) const 

Get the symbol of this Term .

The symbol of the term is the string that was provided when constructing it via TermManager::mkConst() or TermManager::mkVar() .

Note

Requires that this term has a symbol (see hasSymbol() ).

Returns :: The raw symbol of the term.

bool isNull ( ) const 

Determine if this term is nullary.

Returns :: True if this Term is a null term.

Term notTerm ( ) const 

Boolean negation.

Returns :: The Boolean negation of this term.

Term andTerm ( const Term & t ) const 

Boolean and.

Parameters :: t – A Boolean term.
Returns :: The conjunction of this term and the given term.

Term orTerm ( const Term & t ) const 

Boolean or.

Parameters :: t – A Boolean term.
Returns :: The disjunction of this term and the given term.

Term xorTerm ( const Term & t ) const 

Boolean exclusive or.

Parameters :: t – A Boolean term.
Returns :: The exclusive disjunction of this term and the given term.

Term eqTerm ( const Term & t ) const 

Equality.

Parameters :: t – A Boolean term.
Returns :: A Boolean term representing equivalence of this term and the given term.

Term impTerm ( const Term & t ) const 

Boolean implication.

Parameters :: t – A Boolean term.
Returns :: The implication of this term and the given term.

Term iteTerm ( const Term & t , const Term & e ) const 

If-then-else with this term as the Boolean condition.

Parameters :

t – The ‘then’ term.
e – The ‘else’ term.

Returns :

The if-then-else term with this term as the Boolean condition.

std :: string toString ( ) const 

Returns :: A string representation of this term.

const_iterator begin ( ) const 

Returns :: An iterator to the first child of this Term .

const_iterator end ( ) const 

Returns :: An iterator to one-off-the-last child of this Term .

int32_t getRealOrIntegerValueSign ( ) const 

Get the sign of an integer or real value.

Note

Requires that this term is an integer or real value.

Returns :: 0 if this term is zero, -1 if this term is a negative real or integer value, 1 if this term is a positive real or integer value.

bool isInt32Value ( ) const 

Determine if this term is an int32 value.

Note

This will return true for integer constants and real constants that have integer value.

Returns :: True if the term is an integral value that fits within int32_t.

int32_t getInt32Value ( ) const 

Get the int32_t representation of this integral value.

Note

Requires that this term is an int32 value (see isInt32Value() ).

Returns :: This integral value as int32_t value.

bool isUInt32Value ( ) const 

Determine if this term is a uint32 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns :: True if the term is an integral value and fits within uint32_t.

uint32_t getUInt32Value ( ) const 

Get the uint32_t representation of this integral value.

Note

Requires that this term is a uint32 value (see isUInt32Value() ).

Returns :: This integral value as a uint32_t .

bool isInt64Value ( ) const 

Determine if this term is an int64 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns :: True if the term is an integral value and fits within int64_t.

int64_t getInt64Value ( ) const 

Get the int64_t representation of this integral value.

Note

Requires that this term is an int64 value (see isInt64Value() ).

Returns :: This integral value as a int64_t .

bool isUInt64Value ( ) const 

Determine if this term is a uint64 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns :: True if the term is an integral value that fits within uint64_t.

uint64_t getUInt64Value ( ) const 

Get the uint64_t representation of this integral value.

Note

Requires that this term is an uint64 value (see isUInt64Value() ).

Returns :: This integral value as a uint64_t .

bool isIntegerValue ( ) const 

Determine if this term is an integral value.

Returns :: True if the term is an integer constant or a real constant that has an integral value.

std :: string getIntegerValue ( ) const 

Get a string representation of this integral value.

Note

Requires that this term is an integral value (see isIntegerValue() ).

Returns :: The integral term in (decimal) string representation.

bool isStringValue ( ) const 

Determine if this term is a string value.

Returns :: True if the term is a string value.

std :: wstring getStringValue ( ) const 

Get the native string representation of a string value.

Note

Requires that this term is a string value (see isStringValue() ).

Note

This is not to be confused with toString() , which returns some string representation of the term, whatever data it may hold.

Returns :: The string term as a native string value.

bool isReal32Value ( ) const 

Determine if this term is a rational value whose numerator fits into an int32 value and its denominator fits into a uint32 value.

Returns :: True if the term is a rational and its numerator and denominator fit into 32 bit integer values.

std :: pair < int32_t , uint32_t > getReal32Value ( ) const 

Get the 32 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that this term is a rational value and its numerator and denominator fit into 32 bit integer values (see isReal32Value() ).

Returns :: The representation of a rational value as a pair of its numerator and denominator as integer values.

bool isReal64Value ( ) const 

Determine if this term is a rational value whose numerator fits into an int64 value and its denominator fits into a uint64 value.

Returns :: True if the term is a rational value whose numerator and denominator fit within int64_t and uint64_t, respectively.

std :: pair < int64_t , uint64_t > getReal64Value ( ) const 

Get the 64 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that this term is a rational value and its numerator and denominator fit into 64 bit integer values (see isReal64Value() ).

Returns :: The representation of a rational value as a pair of its numerator and denominator.

bool isRealValue ( ) const 

Determine if this term is a rational value.

Note

A term of kind PI is not considered to be a real value.

Returns :: True if the term is a rational value.

std :: string getRealValue ( ) const 

Get a string representation of this rational value.

Note

Requires that this term is a rational value (see isRealValue() ).

Returns :: The representation of a rational value as a (rational) string.

bool isConstArray ( ) const 

Determine if this term is a constant array.

Returns :: True if the term is a constant array.

Term getConstArrayBase ( ) const 

Determine the base (element stored at all indices) of a constant array.

Note

Requires that this term is a constant array (see isConstArray() ).

Returns :: The base term.

bool isBooleanValue ( ) const 

Determine if this term is a Boolean value.

Returns :: True if the term is a Boolean value.

bool getBooleanValue ( ) const 

Get the value of a Boolean term as a native Boolean value.

Note

Asserts isBooleanValue() .

Returns :: The representation of a Boolean value as a native Boolean value.

bool isBitVectorValue ( ) const 

Determine if this term is a bit-vector value.

Returns :: True if the term is a bit-vector value.

std :: string getBitVectorValue ( uint32_t base = 2 ) const 

Get the string representation of a bit-vector value.

Note

Asserts isBitVectorValue() .

Parameters :: base – 2 for binary, 10 for decimal, and 16 for hexadecimal.
Returns :: The string representation of a bit-vector value.

bool isFiniteFieldValue ( ) const 

Determine if this term is a finite field value.

Returns :: True if the term is a finite field value.

std :: string getFiniteFieldValue ( ) const 

Get the string representation of a finite field value (base 10).

Note

Asserts isFiniteFieldValue() .

Note

Uses the integer representative of smallest absolute value.

Returns :: The string representation of the integer representation of this finite field value.

bool isUninterpretedSortValue ( ) const 

Determine if this term is an uninterpreted sort value.

Returns :: True if the term is an abstract value.

std :: string getUninterpretedSortValue ( ) const 

Get a string representation of an uninterpreted sort value.

Note

Asserts isUninterpretedSortValue() .

Returns :: The representation of an uninterpreted sort value as a string.

bool isTupleValue ( ) const 

Determine if this term is a tuple value.

Returns :: True if the term is a tuple value.

std :: vector < Term > getTupleValue ( ) const 

Get a tuple value as a vector of terms.

Note

Asserts isTupleValue() .

Returns :: The representation of a tuple value as a vector of terms.

bool isRoundingModeValue ( ) const 

Determine if this term is a floating-point rounding mode value.

Returns :: True if the term is a rounding mode value.

RoundingMode getRoundingModeValue ( ) const 

Get the RoundingMode value of a given rounding-mode value term.

Note

Asserts isRoundingModeValue() .

Returns :: The floating-point rounding mode value of the term.

bool isFloatingPointPosZero ( ) const 

Determine if this term is a floating-point positive zero value (+zero).

Returns :: True if the term is the floating-point value for positive zero.

bool isFloatingPointNegZero ( ) const 

Determine if this term is a floating-point negative zero value (-zero).

Returns :: True if the term is the floating-point value for negative zero.

bool isFloatingPointPosInf ( ) const 

Determine if this term is a floating-point positive infinity value (+oo).

Returns :: True if the term is the floating-point value for positive. infinity.

bool isFloatingPointNegInf ( ) const 

Determine if this term is a floating-point negative infinity value (-oo).

Returns :: True if the term is the floating-point value for negative. infinity.

bool isFloatingPointNaN ( ) const 

Determine if a given term is a floating-point NaN value.

Returns :: True if the term is the floating-point value for not a number.

bool isFloatingPointValue ( ) const 

Determine if a given term is a floating-point value.

Returns :: True if the term is a floating-point value.

std :: tuple < uint32_t , uint32_t , Term > getFloatingPointValue ( ) const 

Get the representation of a floating-point value as a tuple of its exponent width, significand width and a bit-vector value term.

Note

Asserts isFloatingPointValue() .

Returns :: The floating-point value representation.

bool isSetValue ( ) const 

Determine if this term is a set value.

A term is a set value if it is considered to be a (canonical) constant set value. A canonical set value is one whose AST is:

                (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))

               

where \(c_1 ... c_n\) are values ordered by id such that \(c_1 > ... > c_n\) (see Term::operator>(const Term&) const ).

Note

A universe set term (kind SET_UNIVERSE ) is not considered to be a set value.

Returns :: True if the term is a set value.

std :: set < Term > getSetValue ( ) const 

Get a set value as a set of terms.

Note

Asserts isSetValue() .

Returns :: The representation of a set value as a set of terms.

bool isSequenceValue ( ) const 

Determine if this term is a sequence value.

A term is a sequence value if it has kind #CONST_SEQUENCE. In contrast to values for the set sort (as described in isSetValue() ), a sequence value is represented as a Term with no children.

Semantically, a sequence value is a concatenation of unit sequences whose elements are themselves values. For example:

                (seq.++ (seq.unit 0) (seq.unit 1))

               

The above term has two representations in Term . One is as the sequence concatenation term:

                (SEQ_CONCAT (SEQ_UNIT 0) (SEQ_UNIT 1))

               

where 0 and 1 are the terms corresponding to the integer constants 0 and 1.

Alternatively, the above term is represented as the constant sequence value:

CONST_SEQUENCE_{0,1}

where calling getSequenceValue() on the latter returns the vector {0, 1} .

The former term is not a sequence value, but the latter term is.

Constant sequences cannot be constructed directly via the API. They are returned in response to API calls such Solver::getValue() and Solver::simplify() .

Returns :: True if the term is a sequence value.

std :: vector < Term > getSequenceValue ( ) const 

Get a sequence value as a vector of terms.

Note

Asserts isSequenceValue() .

Returns :: The representation of a sequence value as a vector of terms.

bool isCardinalityConstraint ( ) const 

Determine if this term is a cardinality constraint.

Returns :: True if the term is a cardinality constraint.

std :: pair < Sort , uint32_t > getCardinalityConstraint ( ) const 

Get a cardinality constraint as a pair of its sort and upper bound.

Note

Asserts isCardinalityConstraint() .

Returns :: The sort the cardinality constraint is for and its upper bound.

bool isRealAlgebraicNumber ( ) const 

Determine if this term is a real algebraic number.

Returns :: True if the term is a real algebraic number.

Term getRealAlgebraicNumberDefiningPolynomial ( const Term & v ) const 

Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.

Note

Asserts isRealAlgebraicNumber() .

Parameters :: v – The variable over which to express the polynomial.
Returns :: The defining polynomial.

Term getRealAlgebraicNumberLowerBound ( ) const 

Get the lower bound for a real algebraic number value.

Note

Asserts isRealAlgebraicNumber() .

Returns :: The lower bound.

Term getRealAlgebraicNumberUpperBound ( ) const 

Get the upper bound for a real algebraic number value.

Note

Asserts isRealAlgebraicNumber() .

Returns :: The upper bound.

bool isSkolem ( ) const 

Is this term a skolem?

Warning

This function is experimental and may change in future versions.

Returns :: True if this term is a skolem function.

SkolemId getSkolemId ( ) const 

Get skolem identifier of this term.

Note

Asserts isSkolem() .

Warning

This function is experimental and may change in future versions.

Returns :: The skolem identifier of this term.

std :: vector < Term > getSkolemIndices ( ) const 

Get the skolem indices of this term.

Note

Asserts isSkolem() .

Warning

This function is experimental and may change in future versions.

Returns :: The skolem indices of this term. This is list of terms that the skolem function is indexed by. For example, the array diff skolem SkolemId::ARRAY_DEQ_DIFF is indexed by two arrays.

Friends

friend class parser::Cmd

friend struct std::hash< Term >

class const_iterator 

Iterator for the children of a Term .

Note

This treats uninterpreted functions as Term just like any other term for example, the term f(x, y) will have Kind APPLY_UF and three children: f , x , and y

Public Types

using iterator_category = std :: forward_iterator_tag : Iterator tag

using value_type = Term : The type of the item

using pointer = const Term * : The pointer type of the item

using reference = const Term & : The reference type of the item

using difference_type = std :: ptrdiff_t : The type returned when two iterators are subtracted

Public Functions

const_iterator ( ) : Null Constructor.

const_iterator ( TermManager * tm , const std :: shared_ptr < internal :: Node > & e , uint32_t p ) 

Constructor

Parameters :

tm – The associated term manager.
e – A std::shared pointer to the node that we’re iterating over.
p – The position of the iterator (e.g. which child it’s on).

const_iterator ( const const_iterator & it ) : Copy constructor.

const_iterator & operator = ( const const_iterator & it ) 

Assignment operator.

Parameters :: it – The iterator to assign to.
Returns :: The reference to the iterator after assignment.

bool operator == ( const const_iterator & it ) const 

Equality operator.

Parameters :: it – The iterator to compare to for equality.
Returns :: True if the iterators are equal.

bool operator != ( const const_iterator & it ) const 

Disequality operator.

Parameters :: it – The iterator to compare to for disequality.
Returns :: True if the iterators are disequal.

const_iterator & operator ++ ( ) 

Increment operator (prefix).

Returns :: A reference to the iterator after incrementing by one.

const_iterator operator ++ ( int ) 

Increment operator (postfix).

Returns :: A reference to the iterator after incrementing by one.

Term operator * ( ) const 

Dereference operator.

Returns :: The term this iterator points to.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const Term & t ) 

Serialize a term to given stream.

Parameters :

out – The output stream.
t – The term to be serialized to the given output stream.

Returns :

The output stream.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: vector < Term > & vector ) 

Serialize a vector of terms to given stream.

Parameters :

out – The output stream.
vector – The vector of terms to be serialized to the given stream.

Returns :

The output stream.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: set < Term > & set ) 

Serialize a set of terms to the given stream.

Parameters :

out – The output stream.
set – The set of terms to be serialized to the given stream.

Returns :

The output stream.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: unordered_set < Term > & unordered_set ) 

Serialize an unordered_set of terms to the given stream.

Parameters :

out – The output stream.
unordered_set – The set of terms to be serialized to the given stream.

Returns :

The output stream.

template < typename V > std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: map < Term , V > & map ) 

Serialize a map of terms to the given stream.

Parameters :

out – The output stream.
map – The map of terms to be serialized to the given stream.

Returns :

The output stream.

template < typename V > std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: unordered_map < Term , V > & unordered_map ) 

Serialize an unordered_map of terms to the given stream.

Parameters :

out – The output stream.
unordered_map – The map of terms to be serialized to the given stream.

Returns :

The output stream.

template < > struct hash < cvc5 :: Term > 

Hash function for Terms.

Public Functions

size_t operator () ( const cvc5 :: Term & t ) const 