Package io.github.cvc5

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

    • Field Detail

      • pointer

        protected long pointer

    • Constructor Detail

      • Term

        public Term()
        Null term

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • getPointer

        public long getPointer()

      • equals

        public boolean equals​(java.lang.Object t)
        Syntactic equality operator. Return true if both terms are syntactically identical. Both terms must belong to the same solver object.
        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

      • getId

        public long getId()
        Returns:
        The id of this term.

      • 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.
        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).
        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

      • 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).
        Returns:
        The string representation of a bit-vector value.
        Throws:
        CVC5ApiException
        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
        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.

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

      • iterator

        public java.util.Iterator<Term> iterator()
        Specified by:
        iterator in interface java.lang.Iterable<Term>

      • deletePointer

        public void deletePointer()

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object