Term
The
Term
class represents arbitrary expressions that
are Boolean or from some of the supported theories. The list of all supported
types (or kinds) is given by the
Kind
enum.
The
Term
class provides methods for general
inspection (e.g., comparison, retrieve the kind and sort, access subterms),
but also methods to 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
Solver
class
provides factory functions for all other terms, e.g.,
Solver::mkTerm()
for generic terms and
Solver::mk<Type>()
for constant values of a given type.

class
cvc5
::
Term

A cvc5 Term .
Public Functions

Term
(
)

Constructor for a null term.

~Term
(
)

Destructor.

bool
operator
==
(
const
Term
&
t
)
const

Syntactic equality operator. Return true if both terms are syntactically identical. Both terms must belong to the same solver object.
 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. Return true if both terms differ syntactically. Both terms must belong to the same solver object.
 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

 Returns

The number of children of this term

Term
operator
[]
(
size_t
index
)
const

Get the child term at a given index.
 Parameters

index – The index of the child term to return.
 Returns

The child term with the given index.

uint64_t
getId
(
)
const

 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).
 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 on
f(x,y)
withterms = { x, z }
,replacements = { g(z), w }
results in the termf(g(z),y)
.Note
This replacement is applied during a preorder traversal and only once (it is not run until fixed point).
 Returns

The result of simultaneously replacing
terms
withreplacements
in this term.

bool
hasOp
(
)
const

 Returns

True iff this term has an operator.

Op
getOp
(
)
const

Note
This is safe to call when hasOp() returns true.
 Returns

The Op used to create this term.

bool
hasSymbol
(
)
const

Does the term have a symbol, i.e., 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 Solver::mkConst() or Solver::mkVar() .
Note
Asserts hasSymbol() .
 Returns

The raw symbol of the 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

The Boolean 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
&
then_t
,
const
Term
&
else_t
)
const

Ifthenelse with this term as the Boolean condition.
 Parameters


then_t – The ‘then’ term.

else_t – 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 integer or real value sign. Must be called on integer or real values, or otherwise an exception is thrown.
 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

 Returns

True if the term is an integer value that fits within int32_t.

int32_t
getInt32Value
(
)
const

Get the
int32_t
representation of this integer value.Note
Asserts isInt32Value() .
 Returns

This integer value as a
int32_t
.

bool
isUInt32Value
(
)
const

 Returns

True if the term is an integer value that fits within uint32_t.

uint32_t
getUInt32Value
(
)
const

Get the
uint32_t
representation of this integer value.Note
Asserts isUInt32Value() .
 Returns

This integer value as a
uint32_t
.

bool
isInt64Value
(
)
const

 Returns

True if the term is an integer value that fits within int64_t.

int64_t
getInt64Value
(
)
const

Get the
int64_t
representation of this integer value.Note
Asserts isInt64Value() .
 Returns

This integer value as a
int64_t
.

bool
isUInt64Value
(
)
const

 Returns

True if the term is an integer value that fits within uint64_t.

uint64_t
getUInt64Value
(
)
const

Get the
uint64_t
representation of this integer value.Note
Asserts isUInt64Value() .
 Returns

This integer value as a
uint64_t
.

bool
isIntegerValue
(
)
const

 Returns

True if the term is an integer value.

std
::
string
getIntegerValue
(
)
const

Note
Asserts isIntegerValue() .
 Returns

The integer term in (decimal) string representation.

bool
isStringValue
(
)
const

 Returns

True if the term is a string value.

std
::
wstring
getStringValue
(
)
const

Note
Asserts isStringValue() .
Note
This method 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

 Returns

True if the term is a rational value whose numerator and denominator fit within int32_t and uint32_t, respectively.

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

Note
Asserts isReal32Value() .
 Returns

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

bool
isReal64Value
(
)
const

 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

Note
Asserts isReal64Value() .
 Returns

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

bool
isRealValue
(
)
const

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

Note
Asserts isRealValue() .
 Returns

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

bool
isConstArray
(
)
const

 Returns

True if the term is a constant array.

Term
getConstArrayBase
(
)
const

Note
Asserts isConstArray() .
 Returns

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

bool
isBooleanValue
(
)
const

 Returns

True if the term is a Boolean value.

bool
getBooleanValue
(
)
const

Note
Asserts isBooleanValue() .
 Returns

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

bool
isBitVectorValue
(
)
const

 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.
Supported values for
base
are2
(bit string),10
(decimal string) or16
(hexadecimal string).Note
Asserts isBitVectorValue() .
 Returns

The string representation of a bitvector value.

bool
isUninterpretedSortValue
(
)
const

 Returns

True if the term is an abstract value.

std
::
string
getUninterpretedSortValue
(
)
const

Note
Asserts isUninterpretedSortValue() .
 Returns

The representation of an uninterpreted sort value as a string.

bool
isTupleValue
(
)
const

 Returns

True if the term is a tuple value.

std
::
vector
<
Term
>
getTupleValue
(
)
const

Note
Asserts isTupleValue() .
 Returns

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

bool
isRoundingModeValue
(
)
const

 Returns

True if the term is a floatingpoint rounding mode value.

RoundingMode
getRoundingModeValue
(
)
const

Note
Asserts isRoundingModeValue() .
 Returns

The floatingpoint rounding mode value held by the term.

bool
isFloatingPointPosZero
(
)
const

 Returns

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

bool
isFloatingPointNegZero
(
)
const

 Returns

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

bool
isFloatingPointPosInf
(
)
const

 Returns

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

bool
isFloatingPointNegInf
(
)
const

 Returns

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

bool
isFloatingPointNaN
(
)
const

 Returns

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

bool
isFloatingPointValue
(
)
const

 Returns

True if the term is a floatingpoint value.

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

Note
Asserts isFloatingPointValue() .
 Returns

The representation of a floatingpoint value as a tuple of the exponent width, the significand width and a bitvector value.

bool
isSetValue
(
)
const

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

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

Note
Asserts isSequenceValue() .
 Returns

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

bool
isCardinalityConstraint
(
)
const

 Returns

True if the term is a cardinality constraint.

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

Note
Asserts isCardinalityConstraint() .
 Returns

The sort the cardinality constraint is for and its upper bound.
Friends
 friend class cvc5::Command
 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


slv – The associated solver object.

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
(
)