Package io.github.cvc5

Class Datatype

java.lang.Object
io.github.cvc5.Datatype
All Implemented Interfaces:
Iterable<DatatypeConstructor>
public class Datatype extends Object implements Iterable<DatatypeConstructor>
A cvc5 datatype.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Method Details

    • equals

      public boolean equals(Object dt)
      Syntactic equality operator.
      Overrides:
      equals in class Object
      Parameters:
      dt - The datatype to compare to for equality.
      Returns:
      True if the datatypes are equal.

    • getConstructor

      public DatatypeConstructor getConstructor(int idx)
      Get the datatype constructor at a given index.
      Parameters:
      idx - The index of the datatype constructor to return.
      Returns:
      The datatype constructor with the given index.

    • getConstructor

      public DatatypeConstructor getConstructor(String name)
      Get the datatype constructor with the given name. This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.
      Parameters:
      name - The name of the datatype constructor.
      Returns:
      The datatype constructor with the given name.

    • getSelector

      public DatatypeSelector getSelector(String name)
      Get the datatype constructor with the given name. This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned.
      Parameters:
      name - The name of the datatype selector.
      Returns:
      The datatype selector with the given name.

    • getName

      public String getName()
      Get the name of this Datatype.
      Returns:
      The name of this Datatype.

    • getNumConstructors

      public int getNumConstructors()
      Get the number of constructors for this Datatype.
      Returns:
      The number of constructors for this Datatype.

    • getParameters

      public Sort[] getParameters()
      Get the parameters of this datatype.
      Returns:
      The parameters of this datatype, if it is parametric. An exception. is thrown if this datatype is not parametric.
      Note:
      This method is experimental and may change in future versions.

    • isParametric

      public boolean isParametric()
      Determine if this datatype is parametric.
      Returns:
      True if this datatype is parametric.
      Note:
      This method is experimental and may change in future versions.

    • isCodatatype

      public boolean isCodatatype()
      Determine if this datatype corresponds to a co-datatype.
      Returns:
      True if this datatype corresponds to a co-datatype.

    • isTuple

      public boolean isTuple()
      Determine if this datatype corresponds to a tuple.
      Returns:
      True if this datatype corresponds to a tuple.

    • isRecord

      public boolean isRecord()
      Determine if this datatype corresponds to a record.
      Returns:
      True if this datatype corresponds to a record.
      Note:
      This method is experimental and may change in future versions.

    • isFinite

      public boolean isFinite()
      Determine if this datatype is finite.
      Returns:
      True if this datatype is finite

    • isWellFounded

      public boolean isWellFounded()
      Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
      Returns:
      True if this datatype is well-founded.

    • isNull

      public boolean isNull()
      Determine if this Datatype is a null object.
      Returns:
      True if this Datatype is a null object.

    • toString

      protected String toString(long pointer)
      Provide a string representation of the native datatype.
      Parameters:
      pointer - The native memory address pointing to the datatype.
      Returns:
      A string representation of this datatype.

    • iterator

      public Iterator<DatatypeConstructor> iterator()
      Specified by:
      iterator in interface Iterable<DatatypeConstructor>

    • hashCode

      public int hashCode()
      Get the hash value of a datatype.
      Overrides:
      hashCode in class Object
      Returns:
      The hash value.

    • getPointer

      public long getPointer()
      Return the raw native pointer.

      Every native call obtains the pointers of the objects it uses through this method, so that using an object after its native resource has been released raises an exception instead of crashing the JVM.

      Returns:
      the pointer value
      Throws:
      IllegalStateException - if the native resource of this object has been released, e.g., via deletePointer()

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      Native resources are freed automatically once the Java object is no longer reachable. This method frees the native resource immediately instead; afterwards, using the object raises an IllegalStateException. It must be called from the thread that is using the associated term manager. Calling it more than once has no further effect.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer