Modifier and Type | Class and Description |
---|---|
class |
Term.ConstIterator |
Modifier and Type | Field and Description |
---|---|
protected long |
pointer |
Constructor and Description |
---|
Term()
Null term
|
Modifier and Type | Method and 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.
|
protected void deletePointer(long pointer)
public boolean equals(java.lang.Object t)
equals
in class java.lang.Object
t
- The term to compare to for equality.public int compareTo(Term t)
compareTo
in interface java.lang.Comparable<Term>
t
- The term to compare to.public int getNumChildren()
public Term getChild(int index) throws CVC5ApiException
index
- The index of the child term to return.CVC5ApiException
- on errorpublic long getId()
public Kind getKind() throws CVC5ApiException
CVC5ApiException
- on errorpublic Sort getSort()
public Term substitute(Term term, Term replacement)
term
with replacement
in this term.term
- The term to replace.replacement
- The term to replace it with.term
with replacement
in
this term.public Term substitute(Term[] terms, Term[] replacements)
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)
.terms
- The terms to replace.replacements
- The replacement terms.terms
with
replacements
in this term.public boolean hasOp()
public Op getOp()
hasOp()
returns true.public boolean hasSymbol()
public java.lang.String getSymbol()
public boolean isNull()
public Term notTerm()
public Term andTerm(Term t)
t
- A Boolean term.public Term orTerm(Term t)
t
- A Boolean term.public Term xorTerm(Term t)
t
- A Boolean term.public Term eqTerm(Term t)
t
- A Boolean term.public Term impTerm(Term t)
t
- A Boolean term.public Term iteTerm(Term thenTerm, Term elseTerm)
thenTerm
- The 'then' term.elseTerm
- The 'else' term.protected java.lang.String toString(long pointer)
public int getRealOrIntegerValueSign()
public boolean isIntegerValue()
public java.math.BigInteger getIntegerValue()
public boolean isStringValue()
public java.lang.String getStringValue()
AbstractPointer.toString()
)
which returns the term in some string representation, whatever
data it may hold.public boolean isRealValue()
public Pair<java.math.BigInteger,java.math.BigInteger> getRealValue()
public boolean isConstArray()
public Term getConstArrayBase()
public boolean isBooleanValue()
public boolean getBooleanValue()
public boolean isBitVectorValue()
public java.lang.String getBitVectorValue() throws CVC5ApiException
CVC5ApiException
- on errorpublic java.lang.String getBitVectorValue(int base) throws CVC5ApiException
base
are 2
(bit string), 10
(decimal string) or 16
(hexadecimal string).base
- 2
for binary, 10
for decimal, and 16
for hexadecimal.CVC5ApiException
- on errorTerm#isBitVectorValue()
.public boolean isFiniteFieldValue()
public java.lang.String getFiniteFieldValue() throws CVC5ApiException
CVC5ApiException
- on errorTerm#isFiniteFieldValue()
.public boolean isUninterpretedSortValue()
public java.lang.String getUninterpretedSortValue()
public boolean isRoundingModeValue()
public RoundingMode getRoundingModeValue() throws CVC5ApiException
CVC5ApiException
- on errorpublic boolean isTupleValue()
public Term[] getTupleValue()
public boolean isFloatingPointPosZero()
public boolean isFloatingPointNegZero()
public boolean isFloatingPointPosInf()
public boolean isFloatingPointNegInf()
public boolean isFloatingPointNaN()
public boolean isFloatingPointValue()
public Triplet<java.lang.Long,java.lang.Long,Term> getFloatingPointValue()
public boolean isSetValue()
public java.util.Set<Term> getSetValue()
public boolean isSequenceValue()
public Term[] getSequenceValue()
Solver.simplify(Term)
to turn a sequence that is
constructed by, e.g., concatenation of unit sequences, into a
sequence value.public boolean isCardinalityConstraint()
public Pair<Sort,java.math.BigInteger> getCardinalityConstraint()
public boolean isRealAlgebraicNumber()
public Term getRealAlgebraicNumberDefiningPolynomial(Term v)
v
- The variable over which to express the polynomial.public Term getRealAlgebraicNumberLowerBound()
public Term getRealAlgebraicNumberUpperBound()
public boolean isSkolem()
public SkolemId getSkolemId() throws CVC5ApiException
CVC5ApiException
- on errorpublic Term[] getSkolemIndices() throws CVC5ApiException
SkolemId.ARRAY_DEQ_DIFF
is indexed by two arrays.CVC5ApiException
- on errorpublic java.util.Iterator<Term> iterator()
iterator
in interface java.lang.Iterable<Term>
public int hashCode()
hashCode
in class java.lang.Object
public long getPointer()
public void deletePointer()
public java.lang.String toString()
toString
in class java.lang.Object