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 Python offers).
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

A cvc5 Term.
Wrapper class for
cvc5::Term
. __getitem__ ( )

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

Iterate over all child terms.
 andTerm ( )

Boolean and.
 Parameters :

t – A Boolean term.
 Returns :

The conjunction of this term and the given term.
 eqTerm ( )

Equality
 Parameters :

t – A Boolean term.
 Returns :

The Boolean equivalence of this term and the given term.
 getBitVectorValue ( )

Note
Asserts
isBitVectorValue()
.Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexdecimal string).
 Returns :

The representation of a bitvector value in string representation.
 getBooleanValue ( )

Note
Asserts
isBooleanValue()
 Returns :

The representation of a Boolean value as a native Boolean value.
 getCardinalityConstraint ( )

Note
Asserts
isCardinalityConstraint()
. Returns :

The sort the cardinality constraint is for and its upper bound.
Warning
This function is experimental and may change in future versions.
 getConstArrayBase ( )

Note
Asserts
isConstArray()
. Returns :

The base (element stored at all indicies) of this constant array.
 getFiniteFieldValue ( )

Note
Asserts
isFiniteFieldValue()
.Note
Uses the integer representative of smallest absolute value.
 Returns :

The representation of a finite field value as an integer.
 getFloatingPointValue ( )

Note
Asserts
isFloatingPointValue()
. Returns :

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

 Returns :

The id of this term.
 getIntegerValue ( )

Note
Asserts
isIntegerValue()
. Returns :

The integer term as a native python integer.
 getNumChildren ( )

 Returns :

The number of children of this term.
 getOp ( )

 Returns :

The
Op
used to create this Term.
Note
This is safe to call when
hasOp()
returns True.
 getRealAlgebraicNumberDefiningPolynomial ( )

Note
Asserts
isRealAlgebraicNumber()
. Parameters :

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

The defining polynomial for the real algebraic number, expressed in terms of the given variable.
 getRealAlgebraicNumberLowerBound ( )

Note
Asserts
isRealAlgebraicNumber()
. Returns :

The lower bound for the value of the real algebraic number.
 getRealAlgebraicNumberUpperBound ( )

Note
Asserts
isRealAlgebraicNumber()
. Returns :

The upper bound for the value of the real algebraic number.
 getRealOrIntegerValueSign ( )

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

Note
Asserts
isRealValue()
. Returns :

The representation of a rational value as a python Fraction.
 getRoundingModeValue ( )

Note
Asserts
isRoundingModeValue()
. Returns :

The floatingpoint rounding mode value held by the term.
 getSequenceValue ( )

Note
Asserts
isSequenceValue()
.Note
It is usually necessary for sequences to call
Solver.simplify()
to turn a sequence that is constructed by, e.g., concatenation of unit sequences, into a sequence value. Returns :

The representation of a sequence value as a vector of terms.
 getSetValue ( )

Note
Asserts
isSetValue()
. Returns :

The representation of a set value as a set of terms.
 getSkolemId ( )

Get skolem identifier of this term. .. note:: Asserts
isSkolem()
. .. warning:: This function is experimental and may change in futureversions.
 Returns :

The skolem identifier of this term.
 getSkolemIndices ( )

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

Note
Asserts
isStringValue()
.Note
This function is not to be confused with
__str__()
which returns the term in some string representation, whatever data it may hold. Returns :

The string term as a native string value.
 getSymbol ( )

..note:: Asserts
hasSymbol()
. Returns :

The raw symbol of the term.
 getTupleValue ( )

Note
Asserts
isTupleValue()
. Returns :

The representation of a tuple value as a vector of terms.
 getUninterpretedSortValue ( )

Note
Asserts
isUninterpretedSortValue()
. Returns :

The representation of an uninterpreted value as a pair of its sort and its index.
 hasOp ( )

 Returns :

True iff this term has an operator.
 hasSymbol ( )

 Returns :

True iff this term has a symbol.
 impTerm ( )

Boolean Implication.
 Parameters :

t – A Boolean term.
 Returns :

The implication of this term and the given term.
 isBitVectorValue ( )

 Returns :

True iff this term is a bitvector value.
 isBooleanValue ( )

 Returns :

True iff this term is a Boolean value.
 isCardinalityConstraint ( )

 Returns :

True if the term is a cardinality constraint.
Warning
This function is experimental and may change in future versions.
 isConstArray ( )

 Returns :

True iff this term is a constant array.
 isFiniteFieldValue ( )

 Returns :

True iff this term is a finite field value.
 isFloatingPointNaN ( )

 Returns :

True iff the term is the floatingpoint value for not a number.
 isFloatingPointNegInf ( )

 Returns :

True iff the term is the floatingpoint value for negative infinity.
 isFloatingPointNegZero ( )

 Returns :

True iff the term is the floatingpoint value for negative zero.
 isFloatingPointPosInf ( )

 Returns :

True iff the term is the floatingpoint value for positive infinity.
 isFloatingPointPosZero ( )

 Returns :

True iff the term is the floatingpoint value for positive zero.
 isFloatingPointValue ( )

 Returns :

True iff this term is a floatingpoint value.
 isIntegerValue ( )

 Returns :

True iff this term is an integer value.
 isNull ( )

 Returns :

True iff this term is a null term.
 isRealAlgebraicNumber ( )

 Returns :

True if the term is a real algebraic number.
Warning
This function is experimental and may change in future versions.
 isRealValue ( )

 Returns :

True iff this term is a rational value.
Note
A term of kind
PI
is not considered to be a real value.
 isRoundingModeValue ( )

 Returns :

True if the term is a floatingpoint rounding mode value.
 isSequenceValue ( )

 Returns :

True iff this term is a sequence value.
 isSetValue ( )

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:
(set.union (set.singleton c1) ... (set.union (set.singleton c_{n1}) (set.singleton c_n))))
where \(c_1 \dots c_n\) are values ordered by id such that \(c_1 > \cdots > c_n\) .
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.
 isSkolem ( )

 Returns :

True if the term is a skolem.
Warning
This function is experimental and may change in future versions.
 isStringValue ( )

 Returns :

True iff this term is a string value.
 isTupleValue ( )

 Returns :

True iff this term is a tuple value.
 isUninterpretedSortValue ( )

 Returns :

True iff this term is a value from an uninterpreted sort.
 iteTerm ( )

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

Boolean negation.
 Returns :

The Boolean negation of this term.
 orTerm ( )

Boolean or.
 Parameters :

t – A Boolean term.
 Returns :

The disjunction of this term and the given term.
 substitute ( )

 Returns :

The result of simultaneously replacing the term(s) stored in
term_or_list_1
by the term(s) stored interm_or_list_2
in this term.
Note
This replacement is applied during a preorder traversal and only once to the term. It is not run until fix point. In the case that terms contains duplicates, the replacement earliest in the list takes priority. For example, calling substitute on
f(x,y)
withterm_or_list_1 = [ x, z ], term_or_list_2 = [ g(z), w ]
results in the term
f(g(z),y)
.
 toPythonObj ( )

Converts a constant value Term to a Python object.
Currently supports:

Boolean: Returns a Python bool

Int : Returns a Python int

Real : Returns a Python Fraction

BV : Returns a Python int (treats BV as unsigned)

FF : Returns a Python int (gives the FF integer representative of smallest absolute value)

String : Returns a Python Unicode string

Array : Returns a Python dict mapping indices to values. The constant base is returned as the default value.

 xorTerm ( )

Boolean exclusive or.
 Parameters :

t – A Boolean term.
 Returns :

The exclusive disjunction of this term and the given term.