Package io.github.cvc5

Class Term

java.lang.Object
io.github.cvc5.Term
All Implemented Interfaces:
Comparable<Term>, Iterable<Term>
public class Term extends Object implements Comparable<Term>, Iterable<Term>
A cvc5 Term.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • Term

      public Term()
      Null term

  • Method Details

    • deletePointer

      protected void deletePointer(long pointer)
      Delete the native resource associated with the specified pointer.

      Subclasses must implement this method to provide resource-specific cleanup logic.

      Parameters:
      pointer - the native pointer to delete

    • equals

      public boolean equals(Object t)
      Syntactic equality operator. Return true if both terms are syntactically identical.
      Overrides:
      equals in class 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 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()
      Get the number of children of this term.
      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()
      Get the id of this term.
      Returns:
      The id of this term.

    • getKind

      public Kind getKind() throws CVC5ApiException
      Get the kind of this term.
      Returns:
      The kind of this term.
      Throws:
      CVC5ApiException - on error

    • getSort

      public Sort getSort()
      Get the sort of this term.
      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()
      Determine if this term has an operator.
      Returns:
      True iff this term has an operator.

    • getOp

      public Op getOp()
      Get the Op used to create this term.
      Returns:
      The Op used to create this term.
      Note:
      This is safe to call when hasOp() returns true.

    • hasSymbol

      public boolean hasSymbol()
      Determine if the term has a symbol.
      Returns:
      True if the term has a symbol.

    • getSymbol

      public String getSymbol()
      Asserts hasSymbol().
      Returns:
      The raw symbol of the term.

    • isNull

      public boolean isNull()
      Determine if this term is a null term.
      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 String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native 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()
      Determine if the term is an integer value.
      Returns:
      True if the term is an integer value.

    • getIntegerValue

      public BigInteger getIntegerValue()
      Asserts isIntegerValue().
      Returns:
      The integer represented by this term.

    • isStringValue

      public boolean isStringValue()
      Determine if the term is a string constant.
      Returns:
      True if the term is a string constant.

    • getStringValue

      public String getStringValue()
      Get the stored string constant.
      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()
      Determine if the term is a rational value.
      Returns:
      True if the term is a rational value.

    • getRealValue

      public Pair<BigInteger,BigInteger> getRealValue()
      Asserts isRealValue().
      Returns:
      The representation of a rational value as a pair of its numerator. and denominator.

    • isConstArray

      public boolean isConstArray()
      Determine if the term is a constant array.
      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()
      Determine if the term is a Boolean value.
      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()
      Determine if the term is a bit-vector value.
      Returns:
      True if the term is a bit-vector value.

    • getBitVectorValue

      public String getBitVectorValue() throws CVC5ApiException
      Asserts isBitVectorValue().
      Returns:
      The representation of a bit-vector value in bit string representation.
      Throws:
      CVC5ApiException - on error

    • getBitVectorValue

      public 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()
      Determine if the term is a finite field value.
      Returns:
      True if the term is a finite field value.

    • getFiniteFieldValue

      public 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()
      Determine if the term is an uninterpreted sort value.
      Returns:
      True if the term is an uninterpreted sort value.

    • getUninterpretedSortValue

      public String getUninterpretedSortValue()
      Asserts isUninterpretedSortValue().
      Returns:
      The representation of an uninterpreted sort value as a string.

    • isRoundingModeValue

      public boolean isRoundingModeValue()
      Determine if the term is a floating-point rounding mode value.
      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()
      Determine if the term is a tuple value.
      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()
      Determine if the term is the floating-point value for positive zero.
      Returns:
      True if the term is the floating-point value for positive zero.

    • isFloatingPointNegZero

      public boolean isFloatingPointNegZero()
      Determine if the term is the floating-point value for negative zero.
      Returns:
      True if the term is the floating-point value for negative zero.

    • isFloatingPointPosInf

      public boolean isFloatingPointPosInf()
      Determine if the term is the floating-point value for positive.
      Returns:
      True if the term is the floating-point value for positive. infinity.

    • isFloatingPointNegInf

      public boolean isFloatingPointNegInf()
      Determine if the term is the floating-point value for negative. infinity.
      Returns:
      True if the term is the floating-point value for negative. infinity.

    • isFloatingPointNaN

      public boolean isFloatingPointNaN()
      Determine if the term is the floating-point value for not a number.
      Returns:
      True if the term is the floating-point value for not a number.

    • isFloatingPointValue

      public boolean isFloatingPointValue()
      Determine if the term is a floating-point value.
      Returns:
      True if the term is a floating-point value.

    • getFloatingPointValue

      public Triplet<Long,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()
      Determine if the term is a set value.
      Returns:
      True if the term is a set value.

    • getSetValue

      public Set<Term> getSetValue()
      Asserts isSetValue().
      Returns:
      The representation of a set value as a set of terms.

    • isSequenceValue

      public boolean isSequenceValue()
      Determine if the term is a sequence value.
      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()
      Determine if the term is a cardinality constraint.
      Returns:
      True if the term is a cardinality constraint.

    • getCardinalityConstraint

      public Pair<Sort,BigInteger> getCardinalityConstraint()
      Asserts isCardinalityConstraint().
      Returns:
      The sort the cardinality constraint is for and its upper bound.

    • isRealAlgebraicNumber

      public boolean isRealAlgebraicNumber()
      Determine if the term is a real algebraic number.
      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()
      Determine if this term is a skolem function.
      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 Iterator<Term> iterator()
      Specified by:
      iterator in interface Iterable<Term>

    • hashCode

      public int hashCode()
      Get the hash value of a term.
      Overrides:
      hashCode in class Object
      Returns:
      The hash value.

    • getPointer

      public long getPointer()
      Return the raw native pointer.
      Returns:
      the pointer value

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      This method should be called to explicitly clean up the underlying native resource. It removes this instance from the Context, then invokes the subclass-defined deletePointer(long) method to perform the actual cleanup.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer