public class DatatypeConstructor extends java.lang.Object implements java.lang.Iterable<DatatypeSelector>
Modifier and Type | Class and Description |
---|---|
class |
DatatypeConstructor.ConstIterator |
Modifier and Type | Field and Description |
---|---|
protected long |
pointer |
Modifier and Type | Method and Description |
---|---|
void |
deletePointer() |
protected void |
deletePointer(long pointer) |
boolean |
equals(java.lang.Object c)
Syntactic equality operator.
|
Term |
getInstantiatedTerm(Sort retSort)
Get the constructor term of this datatype constructor whose return
type is
retSort . |
java.lang.String |
getName() |
int |
getNumSelectors() |
long |
getPointer() |
DatatypeSelector |
getSelector(int index)
Get the DatatypeSelector at the given index
|
DatatypeSelector |
getSelector(java.lang.String name)
Get the datatype selector with the given name.
|
Term |
getTerm()
Get the constructor term of this datatype constructor.
|
Term |
getTesterTerm()
Get the tester term of this datatype constructor.
|
int |
hashCode()
Get the hash value of a datatype constructor.
|
boolean |
isNull() |
java.util.Iterator<DatatypeSelector> |
iterator() |
java.lang.String |
toString() |
protected java.lang.String |
toString(long pointer) |
protected void deletePointer(long pointer)
public boolean equals(java.lang.Object c)
equals
in class java.lang.Object
c
- The datatype constructor to compare to for equality.public java.lang.String getName()
public Term getTerm()
Sort.isDatatypeConstructor()
). All
datatype constructors, including nullary ones, should be used as the
first argument to Terms whose kind is Kind.APPLY_CONSTRUCTOR
.
For example, the nil list is represented by the term
(APPLY_CONSTRUCTOR nil)
, where nil
is the term returned by
this method.getInstantiatedTerm(Sort)
below.public Term getInstantiatedTerm(Sort retSort)
retSort
.
This method is intended to be used on constructors of parametric datatypes
and can be seen as returning the constructor term that has been explicitly
cast to the given sort.
This method is required for constructors of parametric datatypes whose
return type cannot be determined by type inference. For example, given:
(declare-datatype List (par (T) ((nil) (cons (head T)
(tail (List T))))))
The type of nil terms need to be provided by the user. In SMT version 2.6,
this is done via the syntax for qualified identifiers:
(as nil (List Int))
This method is equivalent of applying the above, where this
DatatypeConstructor is the one corresponding to nil
, and
retSort
is (List Int)
.retSort
- The desired return sort of the constructor.t
is used to construct the
above (nullary) application of nil
with
Solver.mkTerm(APPLY_CONSTRUCTOR, new Term[] {t})
., This method is experimental and may change in future versions.public Term getTesterTerm()
Sort.isDatatypeTester()
), and should be used as the
first argument of Terms of kind Kind.APPLY_TESTER
.public int getNumSelectors()
public DatatypeSelector getSelector(int index)
index
- The given index i.public DatatypeSelector getSelector(java.lang.String name)
name
- The name of the datatype selector.public boolean isNull()
protected java.lang.String toString(long pointer)
public java.util.Iterator<DatatypeSelector> iterator()
iterator
in interface java.lang.Iterable<DatatypeSelector>
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