public class DatatypeDecl extends Object
Datatype), but a specification for creating a datatype sort.
The interface for a datatype declaration coincides with the syntax for the
SMT-LIB 2.6 command declare-datatype, or a single datatype within the
declare-datatypes command.
Datatype sorts can be constructed from DatatypeDecl using the methods:
- Solver.mkDatatypeSort(DatatypeDecl)
- Solver.mkDatatypeSorts(DatatypeDecl[])| Modifier and Type | Field and Description |
|---|---|
protected long |
pointer |
| Constructor and Description |
|---|
DatatypeDecl()
Null datatypeDecl
|
| Modifier and Type | Method and Description |
|---|---|
void |
addConstructor(DatatypeConstructorDecl ctor)
Add datatype constructor declaration.
|
void |
deletePointer() |
protected void |
deletePointer(long pointer) |
boolean |
equals(Object d)
Syntactic equality operator.
|
String |
getName() |
int |
getNumConstructors()
Get the number of constructors (so far) for this Datatype declaration.
|
long |
getPointer() |
int |
hashCode()
Get the hash value of a datatype declaration.
|
boolean |
isNull() |
boolean |
isParametric()
Determine if this datatype declaration is parametric.
|
String |
toString() |
protected String |
toString(long pointer) |
protected void deletePointer(long pointer)
public boolean equals(Object d)
public void addConstructor(DatatypeConstructorDecl ctor)
ctor - The datatype constructor declaration to add.public int getNumConstructors()
public boolean isParametric()
public boolean isNull()
protected String toString(long pointer)
public String getName()
public int hashCode()
public long getPointer()
public void deletePointer()