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
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.
Note
Both terms must belong to the same node manager.
 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.
Note
Both terms must belong to the same node manager.
 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. Note that this method will return true for integer constants and real constants that have integer value.

int32_t
getInt32Value
(
)
const
¶

Get the
int32_t
representation of this integral 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. Note that this method will return true for integer constants and real constants that have integral value.

uint32_t
getUInt32Value
(
)
const
¶

Get the
uint32_t
representation of this integral 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. Note that this method will return true for integer constants and real constants that have integral value.

int64_t
getInt64Value
(
)
const
¶

Get the
int64_t
representation of this integral 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. Note that this method will return true for integer constants and real constants that have integral value.

uint64_t
getUInt64Value
(
)
const
¶

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

This integer value as a
uint64_t
.

bool
isIntegerValue
(
)
const
¶

 Returns :

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

std
::
string
getIntegerValue
(
)
const
¶

Note
Asserts isIntegerValue() .
 Returns :

The integral 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 :


nm – The associated node 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
(
)
¶