Package io.github.cvc5
Class DatatypeConstructor
- java.lang.Object
-
- io.github.cvc5.DatatypeConstructor
-
- All Implemented Interfaces:
java.lang.Iterable<DatatypeSelector>
public class DatatypeConstructor extends java.lang.Object implements java.lang.Iterable<DatatypeSelector>
A cvc5 datatype constructor.
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description class
DatatypeConstructor.ConstIterator
-
Field Summary
Fields Modifier and Type Field Description protected long
pointer
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method 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 isretSort
.java.lang.String
getName()
int
getNumSelectors()
long
getPointer()
DatatypeSelector
getSelector(int index)
Get the DatatypeSelector at the given indexDatatypeSelector
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)
-
-
-
Method Detail
-
deletePointer
protected void deletePointer(long pointer)
-
equals
public boolean equals(java.lang.Object c)
Syntactic equality operator.- Overrides:
equals
in classjava.lang.Object
- Parameters:
c
- The datatype constructor to compare to for equality.- Returns:
- True if the datatype constructors are equal.
-
getName
public java.lang.String getName()
- Returns:
- The name of this Datatype constructor.
-
getTerm
public Term getTerm()
Get the constructor term of this datatype constructor. Datatype constructors are a special class of function-like terms whose sort is datatype constructor (Sort.isDatatypeConstructor()
). All datatype constructors, including nullary ones, should be used as the first argument to Terms whose kind isKind.APPLY_CONSTRUCTOR
. For example, the nil list is represented by the term(APPLY_CONSTRUCTOR nil)
, wherenil
is the term returned by this method.- Returns:
- The constructor term.
- Note:
- This method should not be used for parametric datatypes. Instead,
use method
getInstantiatedTerm(Sort)
below.
-
getInstantiatedTerm
public Term getInstantiatedTerm(Sort retSort)
Get the constructor term of this datatype constructor whose return type isretSort
. 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 tonil
, andretSort
is(List Int)
.- Parameters:
retSort
- The desired return sort of the constructor.- Returns:
- The constructor term.
- Note:
- The returned constructor term
t
is used to construct the above (nullary) application ofnil
withSolver.mkTerm(APPLY_CONSTRUCTOR, new Term[] {t})
., This method is experimental and may change in future versions.
-
getTesterTerm
public Term getTesterTerm()
Get the tester term of this datatype constructor. Similar to constructors, testers are a class of function-like terms of tester sort (Sort.isDatatypeTester()
), and should be used as the first argument of Terms of kindKind.APPLY_TESTER
.- Returns:
- The tester term.
-
getNumSelectors
public int getNumSelectors()
- Returns:
- The number of selectors (so far) of this Datatype constructor.
-
getSelector
public DatatypeSelector getSelector(int index)
Get the DatatypeSelector at the given index- Parameters:
index
- The given index i.- Returns:
- The i^th DatatypeSelector.
-
getSelector
public DatatypeSelector getSelector(java.lang.String name)
Get the datatype selector with the given name. This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.- Parameters:
name
- The name of the datatype selector.- Returns:
- The first datatype selector with the given name.
-
isNull
public boolean isNull()
- Returns:
- True if this DatatypeConstructor is a null object.
-
toString
protected java.lang.String toString(long pointer)
- Returns:
- A string representation of this datatype constructor.
-
iterator
public java.util.Iterator<DatatypeSelector> iterator()
- Specified by:
iterator
in interfacejava.lang.Iterable<DatatypeSelector>
-
hashCode
public int hashCode()
Get the hash value of a datatype constructor.- Overrides:
hashCode
in classjava.lang.Object
- Returns:
- The hash value.
-
getPointer
public long getPointer()
-
deletePointer
public void deletePointer()
-
toString
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
-