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

getId ( self ) ¶

Returns :: The id of this term.

getIntegerValue ( self ) ¶

Note

Asserts isIntegerValue() .

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

getKind ( self ) ¶

Returns :: The Kind of this term.

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

getSort ( self ) ¶

Returns :: The Sort of this term.

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

isFloatingPointNegInf ( self ) ¶

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

isFloatingPointNegZero ( self ) ¶

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

isFloatingPointPosInf ( self ) ¶

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

isFloatingPointPosZero ( self ) ¶

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

isFloatingPointValue ( self ) ¶

Returns :: True iff this term is a floating-point 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 floating-point 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_{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.

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

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