Package io.github.cvc5

Class DatatypeConstructor

  • All Implemented Interfaces:
    java.lang.Iterable<DatatypeSelector>
    public class DatatypeConstructor
extends java.lang.Object
implements java.lang.Iterable<DatatypeSelector>
    A cvc5 datatype constructor.

    • Field Detail

      • solver

        protected final Solver solver

      • pointer

        protected long pointer

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • getPointer

        public long getPointer()

      • 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 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.
        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 is 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).
        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 of nil with Solver.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 kind Kind.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.

      • getSolver

        public Solver getSolver()

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object