java.lang.Object
- io.github.cvc5.Term

All Implemented Interfaces:: java.lang.Comparable<Term>, java.lang.Iterable<Term>

public class Term
extends java.lang.Object
implements java.lang.Comparable<Term>, java.lang.Iterable<Term>

A cvc5 Term.

Nested Class Summary

Nested Classes
Modifier and Type Class Description

class Term.ConstIterator

Field Summary

Fields
Modifier and Type Field Description

protected long pointer

Constructor Summary

Constructors
Constructor Description

Term()
Null term

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`Term`	`andTerm(Term t)`	Boolean and.
`int`	`compareTo(Term t)`	Comparison for ordering on terms.
`void`	`deletePointer()`
`protected void`	`deletePointer(long pointer)`
`Term`	`eqTerm(Term t)`	Equality.
`boolean`	`equals(java.lang.Object t)`	Syntactic equality operator.
`java.lang.String`	`getBitVectorValue()`	Asserts isBitVectorValue().
`java.lang.String`	`getBitVectorValue(int base)`	Get the string representation of a bit-vector value.
`boolean`	`getBooleanValue()`	Asserts isBooleanValue().
`Pair<Sort,java.math.BigInteger>`	`getCardinalityConstraint()`	Asserts isCardinalityConstraint().
`Term`	`getChild(int index)`	Get the child term at a given index.
`Term`	`getConstArrayBase()`	Asserts isConstArray().
`java.lang.String`	`getFiniteFieldValue()`	Get the string representation of a finite field value.
`Triplet<java.lang.Long,java.lang.Long,Term>`	`getFloatingPointValue()`	Asserts isFloatingPointValue().
`long`	`getId()`
`java.math.BigInteger`	`getIntegerValue()`	Asserts isIntegerValue().
`Kind`	`getKind()`
`int`	`getNumChildren()`
`Op`	`getOp()`
`long`	`getPointer()`
`Term`	`getRealAlgebraicNumberDefiningPolynomial(Term v)`	Asserts isRealAlgebraicNumber().
`Term`	`getRealAlgebraicNumberLowerBound()`	Asserts isRealAlgebraicNumber().
`Term`	`getRealAlgebraicNumberUpperBound()`	Asserts isRealAlgebraicNumber().
`int`	`getRealOrIntegerValueSign()`	Get integer or real value sign.
`Pair<java.math.BigInteger,java.math.BigInteger>`	`getRealValue()`	Asserts isRealValue().
`RoundingMode`	`getRoundingModeValue()`	Asserts isRoundingModeValue().
`Term[]`	`getSequenceValue()`	Asserts isSequenceValue().
`java.util.Set<Term>`	`getSetValue()`	Asserts isSetValue().
`SkolemId`	`getSkolemId()`	Get skolem identifier of this term.
`Term[]`	`getSkolemIndices()`	Get the skolem indices of this term.
`Sort`	`getSort()`
`java.lang.String`	`getStringValue()`
`java.lang.String`	`getSymbol()`	Asserts hasSymbol().
`Term[]`	`getTupleValue()`	Asserts isTupleValue().
`java.lang.String`	`getUninterpretedSortValue()`	Asserts isUninterpretedSortValue().
`int`	`hashCode()`	Get the hash value of a term.
`boolean`	`hasOp()`
`boolean`	`hasSymbol()`
`Term`	`impTerm(Term t)`	Boolean implication.
`boolean`	`isBitVectorValue()`
`boolean`	`isBooleanValue()`
`boolean`	`isCardinalityConstraint()`
`boolean`	`isConstArray()`
`boolean`	`isFiniteFieldValue()`
`boolean`	`isFloatingPointNaN()`
`boolean`	`isFloatingPointNegInf()`
`boolean`	`isFloatingPointNegZero()`
`boolean`	`isFloatingPointPosInf()`
`boolean`	`isFloatingPointPosZero()`
`boolean`	`isFloatingPointValue()`
`boolean`	`isIntegerValue()`
`boolean`	`isNull()`
`boolean`	`isRealAlgebraicNumber()`
`boolean`	`isRealValue()`
`boolean`	`isRoundingModeValue()`
`boolean`	`isSequenceValue()`
`boolean`	`isSetValue()`
`boolean`	`isSkolem()`
`boolean`	`isStringValue()`
`boolean`	`isTupleValue()`
`boolean`	`isUninterpretedSortValue()`
`java.util.Iterator<Term>`	`iterator()`
`Term`	`iteTerm(Term thenTerm, Term elseTerm)`	If-then-else with this term as the Boolean condition.
`Term`	`notTerm()`	Boolean negation.
`Term`	`orTerm(Term t)`	Boolean or.
`Term`	`substitute(Term[] terms, Term[] replacements)`	Simultaneously replace `terms` with `replacements` in this term.
`Term`	`substitute(Term term, Term replacement)`	Replace `term` with `replacement` in this term.
`java.lang.String`	`toString()`
`protected java.lang.String`	`toString(long pointer)`
`Term`	`xorTerm(Term t)`	Boolean exclusive or.

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable
forEach, spliterator

- Field Detail
  - pointer
```
protected long pointer
```
- Constructor Detail
  - Term
```
public Term()
```
    Null term
- Method Detail
  - deletePointer
```
protected void deletePointer(long pointer)
```
  - equals
```
public boolean equals(java.lang.Object t)
```
    Syntactic equality operator. Return true if both terms are syntactically identical.
    
    Overrides:
    
    equals in class java.lang.Object
    
    Parameters:
    
    t - The term to compare to for equality.
    
    Returns:
    
    True if the terms are equal.
  - compareTo
```
public int compareTo(Term t)
```
    Comparison for ordering on terms.
    
    Specified by:
    
    compareTo in interface java.lang.Comparable<Term>
    
    Parameters:
    
    t - The term to compare to.
    
    Returns:
    
    A negative integer, zero, or a positive integer as this term. is less than, equal to, or greater than the specified term.
  - getNumChildren
```
public int getNumChildren()
```
    Returns:
    
    The number of children of this term.
  - getChild
```
public Term getChild(int index)
              throws CVC5ApiException
```
    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.
    
    Throws:
    
    CVC5ApiException - on error
  - getId
```
public long getId()
```
    Returns:
    
    The id of this term.
  - getKind
```
public Kind getKind()
             throws CVC5ApiException
```
    Returns:
    
    The kind of this term.
    
    Throws:
    
    CVC5ApiException - on error
  - getSort
```
public Sort getSort()
```
    Returns:
    
    The sort of this term.
  - substitute
```
public Term substitute(Term term,
                       Term replacement)
```
    Replace term with replacement in this term.
    
    Parameters:
    
    term - The term to replace.
    
    replacement - The term to replace it with.
    
    Returns:
    
    The result of replacing term with replacement in this term.
    
    Note:
    
    This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).
  - substitute
```
public Term substitute(Term[] terms,
                       Term[] replacements)
```
    Simultaneously replace terms with replacements 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) with terms = { x, z }, replacements = { g(z), w } results in the term f(g(z),y).
    
    Parameters:
    
    terms - The terms to replace.
    
    replacements - The replacement terms.
    
    Returns:
    
    The result of simultaneously replacing terms with replacements in this term.
    
    Note:
    
    This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).
  - hasOp
```
public boolean hasOp()
```
    Returns:
    
    True iff this term has an operator.
  - getOp
```
public Op getOp()
```
    Returns:
    
    The Op used to create this term.
    
    Note:
    
    This is safe to call when hasOp() returns true.
  - hasSymbol
```
public boolean hasSymbol()
```
    Returns:
    
    True if the term has a symbol.
  - getSymbol
```
public java.lang.String getSymbol()
```
    Asserts hasSymbol().
    
    Returns:
    
    The raw symbol of the term.
  - isNull
```
public boolean isNull()
```
    Returns:
    
    True if this Term is a null term.
  - notTerm
```
public Term notTerm()
```
    Boolean negation.
    
    Returns:
    
    The Boolean negation of this term.
  - andTerm
```
public Term andTerm(Term t)
```
    Boolean and.
    
    Parameters:
    
    t - A Boolean term.
    
    Returns:
    
    The conjunction of this term and the given term.
  - orTerm
```
public Term orTerm(Term t)
```
    Boolean or.
    
    Parameters:
    
    t - A Boolean term.
    
    Returns:
    
    The disjunction of this term and the given term.
  - xorTerm
```
public Term xorTerm(Term t)
```
    Boolean exclusive or.
    
    Parameters:
    
    t - A Boolean term.
    
    Returns:
    
    The exclusive disjunction of this term and the given term.
  - eqTerm
```
public Term eqTerm(Term t)
```
    Equality.
    
    Parameters:
    
    t - A Boolean term.
    
    Returns:
    
    The Boolean equivalence of this term and the given term.
  - impTerm
```
public Term impTerm(Term t)
```
    Boolean implication.
    
    Parameters:
    
    t - A Boolean term.
    
    Returns:
    
    The implication of this term and the given term.
  - iteTerm
```
public Term iteTerm(Term thenTerm,
                    Term elseTerm)
```
    If-then-else with this term as the Boolean condition.
    
    Parameters:
    
    thenTerm - The 'then' term.
    
    elseTerm - The 'else' term.
    
    Returns:
    
    The if-then-else term with this term as the Boolean condition.
  - toString
```
protected java.lang.String toString(long pointer)
```
    Returns:
    
    A string representation of this term.
  - getRealOrIntegerValueSign
```
public int 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.
  - isIntegerValue
```
public boolean isIntegerValue()
```
    Returns:
    
    True if the term is an integer value.
  - getIntegerValue
```
public java.math.BigInteger getIntegerValue()
```
    Asserts isIntegerValue().
    
    Returns:
    
    The integer represented by this term.
  - isStringValue
```
public boolean isStringValue()
```
    Returns:
    
    True if the term is a string constant.
  - getStringValue
```
public java.lang.String getStringValue()
```
    Returns:
    
    The stored string constant. Asserts isString().
    
    Note:
    
    This method is not to be confused with Object.toString()) which returns the term in some string representation, whatever data it may hold.
  - isRealValue
```
public boolean isRealValue()
```
    Returns:
    
    True if the term is a rational value.
  - getRealValue
```
public Pair<java.math.BigInteger,java.math.BigInteger> getRealValue()
```
    Asserts isRealValue().
    
    Returns:
    
    The representation of a rational value as a pair of its numerator. and denominator.
  - isConstArray
```
public boolean isConstArray()
```
    Returns:
    
    True if the term is a constant array.
  - getConstArrayBase
```
public Term getConstArrayBase()
```
    Asserts isConstArray().
    
    Returns:
    
    The base (element stored at all indices) of a constant array.
  - isBooleanValue
```
public boolean isBooleanValue()
```
    Returns:
    
    True if the term is a Boolean value.
  - getBooleanValue
```
public boolean getBooleanValue()
```
    Asserts isBooleanValue().
    
    Returns:
    
    The representation of a Boolean value as a native Boolean value.
  - isBitVectorValue
```
public boolean isBitVectorValue()
```
    Returns:
    
    True if the term is a bit-vector value.
  - getBitVectorValue
```
public java.lang.String getBitVectorValue()
                                   throws CVC5ApiException
```
    Asserts isBitVectorValue().
    
    Returns:
    
    The representation of a bit-vector value in bit string representation.
    
    Throws:
    
    CVC5ApiException - on error
  - getBitVectorValue
```
public java.lang.String getBitVectorValue(int base)
                                   throws CVC5ApiException
```
    Get the string representation of a bit-vector value. Supported values for base are 2 (bit string), 10 (decimal string) or 16 (hexadecimal string).
    
    Parameters:
    
    base - 2 for binary, 10 for decimal, and 16 for hexadecimal.
    
    Returns:
    
    The string representation of a bit-vector value.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    Asserts Term#isBitVectorValue().
  - isFiniteFieldValue
```
public boolean isFiniteFieldValue()
```
    Returns:
    
    True if the term is a finite field value.
  - getFiniteFieldValue
```
public java.lang.String getFiniteFieldValue()
                                     throws CVC5ApiException
```
    Get the string representation of a finite field value.
    
    Returns:
    
    The string representation of a finite field value.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    Asserts Term#isFiniteFieldValue().
  - isUninterpretedSortValue
```
public boolean isUninterpretedSortValue()
```
    Returns:
    
    True if the term is an uninterpreted sort value.
  - getUninterpretedSortValue
```
public java.lang.String getUninterpretedSortValue()
```
    Asserts isUninterpretedSortValue().
    
    Returns:
    
    The representation of an uninterpreted sort value as a string.
  - isRoundingModeValue
```
public boolean isRoundingModeValue()
```
    Returns:
    
    True if the term is a floating-point rounding mode value.
  - getRoundingModeValue
```
public RoundingMode getRoundingModeValue()
                                  throws CVC5ApiException
```
    Asserts isRoundingModeValue().
    
    Returns:
    
    The floating-point rounding mode value held by the term.
    
    Throws:
    
    CVC5ApiException - on error
  - isTupleValue
```
public boolean isTupleValue()
```
    Returns:
    
    True if the term is a tuple value.
  - getTupleValue
```
public Term[] getTupleValue()
```
    Asserts isTupleValue().
    
    Returns:
    
    The representation of a tuple value as a vector of terms.
  - isFloatingPointPosZero
```
public boolean isFloatingPointPosZero()
```
    Returns:
    
    True if the term is the floating-point value for positive zero.
  - isFloatingPointNegZero
```
public boolean isFloatingPointNegZero()
```
    Returns:
    
    True if the term is the floating-point value for negative zero.
  - isFloatingPointPosInf
```
public boolean isFloatingPointPosInf()
```
    Returns:
    
    True if the term is the floating-point value for positive. infinity.
  - isFloatingPointNegInf
```
public boolean isFloatingPointNegInf()
```
    Returns:
    
    True if the term is the floating-point value for negative. infinity.
  - isFloatingPointNaN
```
public boolean isFloatingPointNaN()
```
    Returns:
    
    True if the term is the floating-point value for not a number.
  - isFloatingPointValue
```
public boolean isFloatingPointValue()
```
    Returns:
    
    True if the term is a floating-point value.
  - getFloatingPointValue
```
public Triplet<java.lang.Long,java.lang.Long,Term> getFloatingPointValue()
```
    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.
  - isSetValue
```
public boolean isSetValue()
```
    Returns:
    
    True if the term is a set value.
  - getSetValue
```
public java.util.Set<Term> getSetValue()
```
    Asserts isSetValue().
    
    Returns:
    
    The representation of a set value as a set of terms.
  - isSequenceValue
```
public boolean isSequenceValue()
```
    Returns:
    
    True if the term is a sequence value.
  - getSequenceValue
```
public Term[] getSequenceValue()
```
    Asserts isSequenceValue().
    
    Returns:
    
    The representation of a sequence value as a vector of terms.
    
    Note:
    
    It is usually necessary for sequences to call Solver.simplify(Term) to turn a sequence that is constructed by, e.g., concatenation of unit sequences, into a sequence value.
  - isCardinalityConstraint
```
public boolean isCardinalityConstraint()
```
    Returns:
    
    True if the term is a cardinality constraint.
  - getCardinalityConstraint
```
public Pair<Sort,java.math.BigInteger> getCardinalityConstraint()
```
    Asserts isCardinalityConstraint().
    
    Returns:
    
    The sort the cardinality constraint is for and its upper bound.
  - isRealAlgebraicNumber
```
public boolean isRealAlgebraicNumber()
```
    Returns:
    
    True if the term is a real algebraic number.
  - getRealAlgebraicNumberDefiningPolynomial
```
public Term getRealAlgebraicNumberDefiningPolynomial(Term v)
```
    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
```
public Term getRealAlgebraicNumberLowerBound()
```
    Asserts isRealAlgebraicNumber().
    
    Returns:
    
    The lower bound for the value of the real algebraic number.
  - getRealAlgebraicNumberUpperBound
```
public Term getRealAlgebraicNumberUpperBound()
```
    Asserts isRealAlgebraicNumber().
    
    Returns:
    
    The upper bound for the value of the real algebraic number.
  - isSkolem
```
public boolean isSkolem()
```
    Returns:
    
    True if this term is a skolem function.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getSkolemId
```
public SkolemId getSkolemId()
                     throws CVC5ApiException
```
    Get skolem identifier of this term.
    
    Returns:
    
    The skolem identifier of this term.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    Asserts isSkolem()., This method is experimental and may change in future versions.
  - getSkolemIndices
```
public Term[] getSkolemIndices()
                        throws CVC5ApiException
```
    Get the skolem indices of this term.
    
    Returns:
    
    The skolem indices of this term. This a 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.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    Asserts isSkolem()., This method is experimental and may change in future versions.
  - iterator
```
public java.util.Iterator<Term> iterator()
```
    Specified by:
    
    iterator in interface java.lang.Iterable<Term>
  - hashCode
```
public int hashCode()
```
    Get the hash value of a term.
    
    Overrides:
    
    hashCode in class java.lang.Object
    
    Returns:
    
    The hash value.
  - getPointer
```
public long getPointer()
```
  - deletePointer
```
public void deletePointer()
```
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object

Class Term

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface java.lang.Iterable

Field Detail

pointer

Constructor Detail

Term

Method Detail

deletePointer

equals

compareTo

getNumChildren

getChild

getId

getKind

getSort

substitute

substitute

hasOp

getOp

hasSymbol

getSymbol

isNull

notTerm

andTerm

orTerm

xorTerm

eqTerm

impTerm

iteTerm

toString

getRealOrIntegerValueSign

isIntegerValue

getIntegerValue

isStringValue

getStringValue

isRealValue

getRealValue

isConstArray

getConstArrayBase

isBooleanValue

getBooleanValue

isBitVectorValue

getBitVectorValue

getBitVectorValue

isFiniteFieldValue

getFiniteFieldValue

isUninterpretedSortValue

getUninterpretedSortValue

isRoundingModeValue

getRoundingModeValue

isTupleValue

getTupleValue

isFloatingPointPosZero

isFloatingPointNegZero

isFloatingPointPosInf

isFloatingPointNegInf

isFloatingPointNaN

isFloatingPointValue

getFloatingPointValue

isSetValue

getSetValue

isSequenceValue

getSequenceValue

isCardinalityConstraint

getCardinalityConstraint

isRealAlgebraicNumber

getRealAlgebraicNumberDefiningPolynomial

getRealAlgebraicNumberLowerBound

getRealAlgebraicNumberUpperBound

isSkolem

getSkolemId

getSkolemIndices

iterator

hashCode

getPointer