Term
 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 ( self , Term t )

Boolean and.
 Parameters

t – A Boolean term.
 Returns

The conjunction of this term and the given term.
 eqTerm ( self , Term t )

Equality
 Parameters

t – A Boolean term.
 Returns

The Boolean equivalence of this term and the given term.
 getBitVectorValue ( self , base = 2 )

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

Note
Asserts
isBooleanValue()
 Returns

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

 Returns

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

Note
Asserts
isConstArray()
. Returns

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

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

 Returns

The id of this term.
 getIntegerValue ( self )

Note
Asserts
isIntegerValue()
. Returns

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

 Returns

The number of children of this term.
 getOp ( self )

 Returns

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

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

Note
Asserts
isRealValue()
. Returns

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

Note
Asserts
isRoundingModeValue()
. Returns

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

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

Note
Asserts
isSetValue()
. Returns

The representation of a set value as a set of terms.
 getStringValue ( self )

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

..note:: Asserts
hasSymbol()
. Returns

The raw symbol of the term.
 getTupleValue ( self )

Note
Asserts
isTupleValue()
. Returns

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

Note
Asserts
isUninterpretedSortValue()
. Returns

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

 Returns

True iff this term has an operator.
 hasSymbol ( self )

 Returns

True iff this term has a symbol.
 impTerm ( self , Term t )

Boolean Implication.
 Parameters

t – A Boolean term.
 Returns

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

 Returns

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

 Returns

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

 Returns

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

 Returns

True iff this term is a constant array.
 isFloatingPointNaN ( self )

 Returns

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

 Returns

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

 Returns

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

 Returns

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

 Returns

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

 Returns

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

 Returns

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

 Returns

True iff this term is a null term.
 isRealValue ( self )

 Returns

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

 Returns

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

 Returns

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

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.
 isStringValue ( self )

 Returns

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

 Returns

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

 Returns

True iff this term is a value from an uninterpreted sort.
 iteTerm ( self , Term then_t , Term else_t )

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

Boolean negation.
 Returns

The Boolean negation of this term.
 orTerm ( self , Term t )

Boolean or.
 Parameters

t – A Boolean term.
 Returns

The disjunction of this term and the given term.
 substitute ( self , term_or_list_1 , term_or_list_2 )

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

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)

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 ( self , Term t )

Boolean exclusive or.
 Parameters

t – A Boolean term.
 Returns

The exclusive disjunction of this term and the given term.