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
subterms),
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)

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.

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

Replace
term
withreplacement
in this term.Note
This replacement is applied during a preorder 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
withreplacement
in this term.

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

Simultaneously replace
terms
withreplacements
in this term.In the case that
terms
contains duplicates, the replacement earliest in the vector takes priority. For example, calling substitute onf(x,y)
withterms = { x, z }
,replacements = { g(z), w }
results in the termf(g(z),y)
.Note
Requires that
terms
andreplacements
are of equal size (they are interpreted as 1 : 1 mapping).Note
This replacement is applied during a preorder 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
withreplacements
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
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

Ifthenelse with this term as the Boolean condition.
 Parameters :


t – The ‘then’ term.

e – The ‘else’ term.

 Returns :

The ifthenelse 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 oneoffthelast 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 bitvector value.
 Returns :

True if the term is a bitvector value.

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

Get the string representation of a bitvector value.
Note
Asserts isBitVectorValue() .
 Parameters :

base –
2
for binary,10
for decimal, and16
for hexadecimal.  Returns :

The string representation of a bitvector 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 floatingpoint rounding mode value.
 Returns :

True if the term is a rounding mode value.

RoundingMode
getRoundingModeValue
(
)
const

Get the RoundingMode value of a given roundingmode value term.
Note
Asserts isRoundingModeValue() .
 Returns :

The floatingpoint rounding mode value of the term.

bool
isFloatingPointPosZero
(
)
const

Determine if this term is a floatingpoint positive zero value (+zero).
 Returns :

True if the term is the floatingpoint value for positive zero.

bool
isFloatingPointNegZero
(
)
const

Determine if this term is a floatingpoint negative zero value (zero).
 Returns :

True if the term is the floatingpoint value for negative zero.

bool
isFloatingPointPosInf
(
)
const

Determine if this term is a floatingpoint positive infinity value (+oo).
 Returns :

True if the term is the floatingpoint value for positive. infinity.

bool
isFloatingPointNegInf
(
)
const

Determine if this term is a floatingpoint negative infinity value (oo).
 Returns :

True if the term is the floatingpoint value for negative. infinity.

bool
isFloatingPointNaN
(
)
const

Determine if a given term is a floatingpoint NaN value.
 Returns :

True if the term is the floatingpoint value for not a number.

bool
isFloatingPointValue
(
)
const

Determine if a given term is a floatingpoint value.
 Returns :

True if the term is a floatingpoint value.

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

Get the representation of a floatingpoint value as a tuple of its exponent width, significand width and a bitvector value term.
Note
Asserts isFloatingPointValue() .
 Returns :

The floatingpoint 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_{n1}) (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 KindAPPLY_UF
and three children:f
,x
, andy
Public Types

using
iterator_category
=
std
::
forward_iterator_tag

Iterator tag

using
difference_type
=
std
::
ptrdiff_t

The type returned when two iterators are subtracted
Public Functions

const_iterator
(
)

Null Constructor.

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.

using
iterator_category
=
std
::
forward_iterator_tag

Term
(
)

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.