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 sub-terms), 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 bit-vector 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 floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.

getId()

Returns:: The id of this term.

getIntegerValue()

Note

Asserts isIntegerValue().

Returns:: The integer term as a native python integer.

getKind()

Returns:: The Kind of this term.

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 floating-point 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 future

versions.

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.

getSort()

Returns:: The Sort of this term.

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 bit-vector 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 floating-point value for not a number.

isFloatingPointNegInf()

Returns:: True iff the term is the floating-point value for negative infinity.

isFloatingPointNegZero()

Returns:: True iff the term is the floating-point value for negative zero.

isFloatingPointPosInf()

Returns:: True iff the term is the floating-point value for positive infinity.

isFloatingPointPosZero()

Returns:: True iff the term is the floating-point value for positive zero.

isFloatingPointValue()

Returns:: True iff this term is a floating-point 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 floating-point 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_{n-1}) (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()

If-then-else with this term as the Boolean condition.

Parameters:

then_t – The then term.
else_t – The else term.

Returns:

The if-then-else 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 in term_or_list_2 in this term.

Note

This replacement is applied during a pre-order 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) with

term_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.