Package io.github.cvc5

Class TermManager

  • public class TermManager
extends java.lang.Object
    A cvc5 term manager.

    • Field Detail

      • pointer

        protected long pointer

    • Constructor Detail

      • TermManager

        public TermManager()
        Create a term manager instance.

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • toString

        protected java.lang.String toString​(long pointer)

      • equals

        public boolean equals​(java.lang.Object o)
        Overrides:
        equals in class java.lang.Object

      • getStatistics

        public Statistics getStatistics()
        Get a snapshot of the current state of the statistic values of this term manager. Term manager statistics are independent from any solver instance. The returned object is completely decoupled from the term manager and will not change when the solver is used again.
        Returns:
        A snapshot of the current state of the statistic values.

      • getBooleanSort

        public Sort getBooleanSort()
        Get the Boolean sort.
        Returns:
        Sort Boolean.

      • getIntegerSort

        public Sort getIntegerSort()
        Get the integer sort.
        Returns:
        Sort Integer.

      • getIntegerSort

        public long getIntegerSort​(long pointer)

      • getRealSort

        public Sort getRealSort()
        Get the real sort.
        Returns:
        Sort Real.

      • getRegExpSort

        public Sort getRegExpSort()
        Get the regular expression sort.
        Returns:
        Sort RegExp.

      • getRoundingModeSort

        public Sort getRoundingModeSort()
                         throws CVC5ApiException
        Get the floating-point rounding mode sort.
        Returns:
        Sort RoundingMode.
        Throws:
        CVC5ApiException - on error

      • getStringSort

        public Sort getStringSort()
        Get the string sort.
        Returns:
        Sort String.

      • mkArraySort

        public Sort mkArraySort​(Sort indexSort,
                        Sort elemSort)
        Create an array sort.
        Parameters:
        indexSort - The array index sort.
        elemSort - The array element sort.
        Returns:
        The array sort.

      • mkBitVectorSort

        public Sort mkBitVectorSort​(int size)
                     throws CVC5ApiException
        Create a bit-vector sort.
        Parameters:
        size - The bit-width of the bit-vector sort.
        Returns:
        The bit-vector sort.
        Throws:
        CVC5ApiException - on error

      • mkFiniteFieldSort

        public Sort mkFiniteFieldSort​(java.lang.String size,
                              int base)
                       throws CVC5ApiException
        Create a finite field sort.
        Parameters:
        size - The size of the finite field sort.
        base - The base of the string representation.
        Returns:
        The finite field sort.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPointSort

        public Sort mkFloatingPointSort​(int exp,
                                int sig)
                         throws CVC5ApiException
        Create a floating-point sort.
        Parameters:
        exp - The bit-width of the exponent of the floating-point sort.
        sig - The bit-width of the significand of the floating-point sort.
        Returns:
        The floating-point sort.
        Throws:
        CVC5ApiException - on error

      • mkDatatypeSort

        public Sort mkDatatypeSort​(DatatypeDecl dtypedecl)
                    throws CVC5ApiException
        Create a datatype sort.
        Parameters:
        dtypedecl - The datatype declaration from which the sort is created.
        Returns:
        The datatype sort.
        Throws:
        CVC5ApiException - on error

      • mkDatatypeSorts

        public Sort[] mkDatatypeSorts​(DatatypeDecl[] dtypedecls)
                       throws CVC5ApiException
        Create a vector of datatype sorts. The names of the datatype declarations must be distinct.
        Parameters:
        dtypedecls - The datatype declarations from which the sort is created.
        Returns:
        The datatype sorts.
        Throws:
        CVC5ApiException - on error

      • mkFunctionSort

        public Sort mkFunctionSort​(Sort domain,
                           Sort codomain)
        Create function sort.
        Parameters:
        domain - The sort of the fuction argument.
        codomain - The sort of the function return value.
        Returns:
        The function sort.

      • mkFunctionSort

        public Sort mkFunctionSort​(Sort[] sorts,
                           Sort codomain)
        Create function sort.
        Parameters:
        sorts - The sort of the function arguments.
        codomain - The sort of the function return value.
        Returns:
        The function sort.

      • mkParamSort

        public Sort mkParamSort​(java.lang.String symbol)
        Create a sort parameter.
        Parameters:
        symbol - The name of the sort.
        Returns:
        The sort parameter.
        Note:
        This method is experimental and may change in future versions.

      • mkParamSort

        public Sort mkParamSort()
        Create a sort parameter.
        Returns:
        The sort parameter.
        Note:
        This method is experimental and may change in future versions.

      • mkSkolem

        public Term mkSkolem​(SkolemId skolemId,
                     Term[] indices)
        Create a skolem
        Parameters:
        skolemId - The id of the skolem.
        indices - The indices of the skolem.
        Returns:
        The skolem.
        Note:
        This method is experimental and may change in future versions.

      • getNumIndicesForSkolemId

        public int getNumIndicesForSkolemId​(SkolemId id)
        Get the number of indices for a given skolem id.
        Parameters:
        id - The skolem id.
        Returns:
        The number of indices for the given skolem id.
        Note:
        This method is experimental and may change in future versions.

      • mkPredicateSort

        public Sort mkPredicateSort​(Sort[] sorts)
        Create a predicate sort.
        Parameters:
        sorts - The list of sorts of the predicate.
        Returns:
        The predicate sort.

      • mkRecordSort

        public Sort mkRecordSort​(Pair<java.lang.String,​Sort>[] fields)
        Create a record sort
        Parameters:
        fields - The list of fields of the record.
        Returns:
        The record sort.
        Note:
        This method is experimental and may change in future versions.

      • mkSetSort

        public Sort mkSetSort​(Sort elemSort)
        Create a set sort.
        Parameters:
        elemSort - The sort of the set elements.
        Returns:
        The set sort.

      • mkBagSort

        public Sort mkBagSort​(Sort elemSort)
        Create a bag sort.
        Parameters:
        elemSort - The sort of the bag elements.
        Returns:
        The bag sort.

      • mkSequenceSort

        public Sort mkSequenceSort​(Sort elemSort)
        Create a sequence sort.
        Parameters:
        elemSort - The sort of the sequence elements.
        Returns:
        The sequence sort.

      • mkAbstractSort

        public Sort mkAbstractSort​(SortKind kind)
        Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified. The SortKind k must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, SortKind.ARRAY_SORT and SortKind.BITVECTOR_SORT can be passed as the SortKind k to this method, while SortKind.INTEGER_SORT and SortKind.STRING_SORT cannot.
        Parameters:
        kind - The kind of the abstract sort
        Returns:
        The abstract sort.
        Note:
        Providing the kind SortKind.ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, often denoted ?., Providing a kind k that has no indices and a fixed arity of argument sorts will return the sort of SortKind k whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is SortKind.ABSTRACT_SORT., This method is experimental and may change in future versions.

      • mkUninterpretedSort

        public Sort mkUninterpretedSort​(java.lang.String symbol)
        Create an uninterpreted sort.
        Parameters:
        symbol - The name of the sort.
        Returns:
        The uninterpreted sort.

      • mkUninterpretedSort

        public Sort mkUninterpretedSort()
        Create an uninterpreted sort.
        Returns:
        The uninterpreted sort.

      • mkUnresolvedDatatypeSort

        public Sort mkUnresolvedDatatypeSort​(java.lang.String symbol,
                                     int arity)
                              throws CVC5ApiException
        Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.
        Parameters:
        symbol - The symbol of the sort.
        arity - The number of sort parameters of the sort.
        Returns:
        The unresolved sort.
        Throws:
        CVC5ApiException - on error

      • mkUnresolvedDatatypeSort

        public Sort mkUnresolvedDatatypeSort​(java.lang.String symbol)
                              throws CVC5ApiException
        Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive datatypes without sort parameters.
        Parameters:
        symbol - The symbol of the sort.
        Returns:
        The unresolved sort.
        Throws:
        CVC5ApiException - on error

      • mkUninterpretedSortConstructorSort

        public Sort mkUninterpretedSortConstructorSort​(int arity,
                                               java.lang.String symbol)
                                        throws CVC5ApiException
        Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
        Parameters:
        arity - The arity of the sort (must be > 0)
        symbol - The symbol of the sort.
        Returns:
        The sort constructor sort.
        Throws:
        CVC5ApiException - on error

      • mkUninterpretedSortConstructorSort

        public Sort mkUninterpretedSortConstructorSort​(int arity)
                                        throws CVC5ApiException
        Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
        Parameters:
        arity - The arity of the sort (must be > 0)
        Returns:
        The sort constructor sort.
        Throws:
        CVC5ApiException - on error

      • mkTupleSort

        public Sort mkTupleSort​(Sort[] sorts)
        Create a tuple sort.
        Parameters:
        sorts - Of the elements of the tuple.
        Returns:
        The tuple sort.

      • mkNullableSort

        public Sort mkNullableSort​(Sort sort)
        Create a nullable sort.
        Parameters:
        sort - The sort of the element of the nullable.
        Returns:
        The nullable sort.

      • mkTerm

        public Term mkTerm​(Kind kind)
        Create 0-ary term of given kind.
        Parameters:
        kind - The kind of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Kind kind,
                   Term child)
        Create a unary term of given kind.
        Parameters:
        kind - The kind of the term.
        child - The child of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Kind kind,
                   Term child1,
                   Term child2)
        Create binary term of given kind.
        Parameters:
        kind - The kind of the term.
        child1 - The first child of the term.
        child2 - The second child of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Kind kind,
                   Term child1,
                   Term child2,
                   Term child3)
        Create ternary term of given kind.
        Parameters:
        kind - The kind of the term.
        child1 - The first child of the term.
        child2 - The second child of the term.
        child3 - The third child of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Kind kind,
                   Term[] children)
        Create n-ary term of given kind.
        Parameters:
        kind - The kind of the term.
        children - The children of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Op op,
                   Term child1,
                   Term child2)
        Create binary term of given kind from a given operator. Create operators with mkOp(Kind), mkOp(Kind, String), mkOp(Kind, int[]).
        Parameters:
        op - The operator.
        child1 - The first child of the term.
        child2 - The second child of the term.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Op op,
                   Term child1,
                   Term child2,
                   Term child3)
        Create ternary term of given kind from a given operator. Create operators with mkOp(Kind), mkOp(Kind, String), mkOp(Kind, int[]).
        Parameters:
        op - The operator.
        child1 - The first child of the term.
        child2 - The second child of the term.
        child3 - The third child of the term.
        Returns:
        The Term.

      • mkTuple

        public Term mkTuple​(Term[] terms)
        Create a tuple term. Terms are automatically converted if sorts are compatible.
        Parameters:
        terms - The elements in the tuple.
        Returns:
        The tuple Term.

      • mkNullableSome

        public Term mkNullableSome​(Term term)
        Create a nullable some term.
        Parameters:
        term - The element value.
        Returns:
        the Element value wrapped in some constructor.

      • mkNullableVal

        public Term mkNullableVal​(Term term)
        Create a selector for nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        The element value of the nullable term.

      • mkNullableIsNull

        public Term mkNullableIsNull​(Term term)
        Create a null tester for a nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        A tester whether term is null.

      • mkNullableIsSome

        public Term mkNullableIsSome​(Term term)
        Create a some tester for a nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        A tester whether term is some.

      • mkNullableNull

        public Term mkNullableNull​(Sort sort)
        Create a constant representing a null value of the given sort.
        Parameters:
        sort - The sort of the Nullable element.
        Returns:
        The null constant.

      • mkNullableLift

        public Term mkNullableLift​(Kind kind,
                           Term[] args)
        Create a term that lifts kind to nullable terms. Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)
        Parameters:
        kind - The lifted operator.
        args - The arguments of the lifted operator.
        Returns:
        A term of Kind NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.

      • mkOp

        public Op mkOp​(Kind kind)
        Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).
        Parameters:
        kind - The kind to wrap.
        Returns:
        The operator.
        Note:
        In this case, the Op simply wraps the Kind. The Kind can be used in mkTerm directly without creating an op first.

      • mkOp

        public Op mkOp​(Kind kind,
               java.lang.String arg)
        Create operator of kind: See enum Kind for a description of the parameters.
        Parameters:
        kind - The kind of the operator.
        arg - The string argument to this operator.
        Returns:
        The operator.

      • mkOp

        public Op mkOp​(Kind kind,
               int arg)
        throws CVC5ApiException
        Create operator of kind:
        • DIVISIBLE
        • BITVECTOR_REPEAT
        • BITVECTOR_ZERO_EXTEND
        • BITVECTOR_SIGN_EXTEND
        • BITVECTOR_ROTATE_LEFT
        • BITVECTOR_ROTATE_RIGHT
        • INT_TO_BITVECTOR
        • FLOATINGPOINT_TO_UBV
        • FLOATINGPOINT_TO_UBV_TOTAL
        • FLOATINGPOINT_TO_SBV
        • FLOATINGPOINT_TO_SBV_TOTAL
        • TUPLE_UPDATE
        See enum Kind for a description of the parameters.
        Parameters:
        kind - The kind of the operator.
        arg - The unsigned int argument to this operator.
        Returns:
        The operator.
        Throws:
        CVC5ApiException - on error

      • mkOp

        public Op mkOp​(Kind kind,
               int arg1,
               int arg2)
        throws CVC5ApiException
        Create operator of Kind:
        • BITVECTOR_EXTRACT
        • FLOATINGPOINT_TO_FP_FROM_IEEE_BV
        • FLOATINGPOINT_TO_FP_FROM_FP
        • FLOATINGPOINT_TO_FP_FROM_REAL
        • FLOATINGPOINT_TO_FP_FROM_SBV
        • FLOATINGPOINT_TO_FP_FROM_UBV
        See enum Kind for a description of the parameters.
        Parameters:
        kind - The kind of the operator.
        arg1 - The first unsigned int argument to this operator.
        arg2 - The second unsigned int argument to this operator.
        Returns:
        The operator.
        Throws:
        CVC5ApiException - on error

      • mkOp

        public Op mkOp​(Kind kind,
               int[] args)
        throws CVC5ApiException
        Create operator of Kind:
        • TUPLE_PROJECT
        See enum Kind for a description of the parameters.
        Parameters:
        kind - The kind of the operator.
        args - The arguments (indices) of the operator.
        Returns:
        The operator.
        Throws:
        CVC5ApiException - on error

      • mkTrue

        public Term mkTrue()
        Create a Boolean true constant.
        Returns:
        The true constant.

      • mkFalse

        public Term mkFalse()
        Create a Boolean false constant.
        Returns:
        The false constant.

      • mkBoolean

        public Term mkBoolean​(boolean val)
        Create a Boolean constant.
        Parameters:
        val - The value of the constant.
        Returns:
        The Boolean constant.

      • mkPi

        public Term mkPi()
        Create a constant representing the number Pi.
        Returns:
        A constant representing Pi.

      • mkInteger

        public Term mkInteger​(java.lang.String s)
               throws CVC5ApiException
        Create an integer constant from a string.
        Parameters:
        s - The string representation of the constant, may represent an. integer (e.g., "123").
        Returns:
        A constant of sort Integer assuming s represents an integer).
        Throws:
        CVC5ApiException - on error

      • mkInteger

        public Term mkInteger​(long val)
        Create an integer constant from a C++ int.
        Parameters:
        val - The value of the constant.
        Returns:
        A constant of sort Integer.

      • mkReal

        public Term mkReal​(java.lang.String s)
            throws CVC5ApiException
        Create a real constant from a string.
        Parameters:
        s - The string representation of the constant, may represent an. integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
        Returns:
        A constant of sort Real.
        Throws:
        CVC5ApiException - on error

      • mkReal

        public Term mkReal​(long val)
        Create a real constant from an integer.
        Parameters:
        val - The value of the constant.
        Returns:
        A constant of sort Integer.

      • mkReal

        public Term mkReal​(long num,
                   long den)
        Create a real constant from a rational.
        Parameters:
        num - The value of the numerator.
        den - The value of the denominator.
        Returns:
        A constant of sort Real.

      • mkRegexpNone

        public Term mkRegexpNone()
        Create a regular expression none (re.none) term.
        Returns:
        The none term.

      • mkRegexpAll

        public Term mkRegexpAll()
        Create a regular expression all (re.all) term.
        Returns:
        The all term.

      • mkRegexpAllchar

        public Term mkRegexpAllchar()
        Create a regular expression allchar (re.allchar) term.
        Returns:
        The allchar term.

      • mkEmptySet

        public Term mkEmptySet​(Sort sort)
        Create a constant representing an empty set of the given sort.
        Parameters:
        sort - The sort of the set elements.
        Returns:
        The empty set constant.

      • mkEmptyBag

        public Term mkEmptyBag​(Sort sort)
        Create a constant representing an empty bag of the given sort.
        Parameters:
        sort - The sort of the bag elements.
        Returns:
        The empty bag constant.

      • mkSepEmp

        public Term mkSepEmp()
        Create a separation logic empty term.
        Returns:
        The separation logic empty term.
        Note:
        This method is experimental and may change in future versions.

      • mkSepNil

        public Term mkSepNil​(Sort sort)
        Create a separation logic nil term.
        Parameters:
        sort - The sort of the nil term.
        Returns:
        The separation logic nil term.
        Note:
        This method is experimental and may change in future versions.

      • mkString

        public Term mkString​(java.lang.String s)
        Create a String constant.
        Parameters:
        s - The string this constant represents.
        Returns:
        The String constant.

      • mkString

        public Term mkString​(java.lang.String s,
                     boolean useEscSequences)
        Create a String constant.
        Parameters:
        s - The string this constant represents.
        useEscSequences - Determines whether escape sequences in s should be converted to the corresponding unicode character.
        Returns:
        The String constant.

      • mkString

        public Term mkString​(int[] s)
              throws CVC5ApiException
        Create a String constant.
        Parameters:
        s - A list of unsigned (unicode) values this constant represents as string.
        Returns:
        The String constant.
        Throws:
        CVC5ApiException - on error

      • mkEmptySequence

        public Term mkEmptySequence​(Sort sort)
        Create an empty sequence of the given element sort.
        Parameters:
        sort - The element sort of the sequence.
        Returns:
        The empty sequence with given element sort.

      • mkUniverseSet

        public Term mkUniverseSet​(Sort sort)
        Create a universe set of the given sort.
        Parameters:
        sort - The sort of the set elements.
        Returns:
        The universe set constant.

      • mkBitVector

        public Term mkBitVector​(int size)
                 throws CVC5ApiException
        Create a bit-vector constant of given size and value = 0.
        Parameters:
        size - The bit-width of the bit-vector sort.
        Returns:
        The bit-vector constant.
        Throws:
        CVC5ApiException - on error

      • mkBitVector

        public Term mkBitVector​(int size,
                        long val)
                 throws CVC5ApiException
        Create a bit-vector constant of given size and value.
        Parameters:
        size - The bit-width of the bit-vector sort.
        val - The value of the constant.
        Returns:
        The bit-vector constant.
        Throws:
        CVC5ApiException - on error
        Note:
        The given value must fit into a bit-vector of the given size.

      • mkBitVector

        public Term mkBitVector​(int size,
                        java.lang.String s,
                        int base)
                 throws CVC5ApiException
        Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
        Parameters:
        size - The bit-width of the constant.
        s - The string representation of the constant.
        base - The base of the string representation (2, 10, or 16)
        Returns:
        The bit-vector constant.
        Throws:
        CVC5ApiException - on error
        Note:
        The given value must fit into a bit-vector of the given size.

      • mkFiniteFieldElem

        public Term mkFiniteFieldElem​(java.lang.String val,
                              Sort sort,
                              int base)
                       throws CVC5ApiException
        Create a finite field constant in a given field and for a given value.
        Parameters:
        val - The value of the constant.
        sort - The sort of the finite field.
        base - The base of the string representation.
        Returns:
        The finite field constant.
        Throws:
        CVC5ApiException - on error
        Note:
        The given value must fit into a the given finite field.

      • mkConstArray

        public Term mkConstArray​(Sort sort,
                         Term val)
        Create a constant array with the provided constant value stored at every index
        Parameters:
        sort - The sort of the constant array (must be an array sort)
        val - The constant value to store (must match the sort's element sort).
        Returns:
        The constant array term.

      • mkFloatingPointPosInf

        public Term mkFloatingPointPosInf​(int exp,
                                  int sig)
                           throws CVC5ApiException
        Create a positive infinity floating-point constant (SMT-LIB: +oo).
        Parameters:
        exp - Number of bits in the exponent.
        sig - Number of bits in the significand.
        Returns:
        The floating-point constant.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPointNegInf

        public Term mkFloatingPointNegInf​(int exp,
                                  int sig)
                           throws CVC5ApiException
        Create a negative infinity floating-point constant (SMT-LIB: -oo).
        Parameters:
        exp - Number of bits in the exponent.
        sig - Number of bits in the significand.
        Returns:
        The floating-point constant.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPointNaN

        public Term mkFloatingPointNaN​(int exp,
                               int sig)
                        throws CVC5ApiException
        Create a not-a-number floating-point constant (SMT-LIB: NaN).
        Parameters:
        exp - Number of bits in the exponent.
        sig - Number of bits in the significand.
        Returns:
        The floating-point constant.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPointPosZero

        public Term mkFloatingPointPosZero​(int exp,
                                   int sig)
                            throws CVC5ApiException
        Create a positive zero floating-point constant (SMT-LIB: +zero).
        Parameters:
        exp - Number of bits in the exponent.
        sig - Number of bits in the significand.
        Returns:
        The floating-point constant.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPointNegZero

        public Term mkFloatingPointNegZero​(int exp,
                                   int sig)
                            throws CVC5ApiException
        Create a negative zero floating-point constant (SMT-LIB: -zero).
        Parameters:
        exp - Number of bits in the exponent.
        sig - Number of bits in the significand.
        Returns:
        The floating-point constant.
        Throws:
        CVC5ApiException - on error

      • mkRoundingMode

        public Term mkRoundingMode​(RoundingMode rm)
        Create a rounding mode constant.
        Parameters:
        rm - The floating point rounding mode this constant represents.
        Returns:
        The rounding mode.

      • mkFloatingPoint

        public Term mkFloatingPoint​(int exp,
                            int sig,
                            Term val)
                     throws CVC5ApiException
        Create a floating-point value from a bit-vector given in IEEE-754 format.
        Parameters:
        exp - Size of the exponent.
        sig - Size of the significand.
        val - Value of the floating-point constant as a bit-vector term.
        Returns:
        The floating-point value.
        Throws:
        CVC5ApiException - on error

      • mkFloatingPoint

        public Term mkFloatingPoint​(Term sign,
                            Term exp,
                            Term sig)
                     throws CVC5ApiException
        Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
        Parameters:
        sign - The sign bit.
        exp - The bit-vector representing the exponent.
        sig - The bit-vector representing the significand.
        Returns:
        The floating-point value.
        Throws:
        CVC5ApiException - on error

      • mkCardinalityConstraint

        public Term mkCardinalityConstraint​(Sort sort,
                                    int upperBound)
                             throws CVC5ApiException
        Create a cardinality constraint for an uninterpreted sort.
        Parameters:
        sort - The sort the cardinality constraint is for.
        upperBound - The upper bound on the cardinality of the sort.
        Returns:
        The cardinality constraint.
        Throws:
        CVC5ApiException - on error
        Note:
        This method is experimental and may change in future versions.

      • mkConst

        public Term mkConst​(Sort sort,
                    java.lang.String symbol)
        Create a free constant. SMT-LIB: ( declare-const <symbol> <sort> ) ( declare-fun <symbol> ( ) <sort> )
        Parameters:
        sort - The sort of the constant.
        symbol - The name of the constant.
        Returns:
        The first-order constant.

      • mkConst

        public Term mkConst​(Sort sort)
        Create a free constant with a default symbol name.
        Parameters:
        sort - The sort of the constant.
        Returns:
        The first-order constant.

      • mkVar

        public Term mkVar​(Sort sort)
        Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
        Parameters:
        sort - The sort of the variable.
        Returns:
        The variable.

      • mkVar

        public Term mkVar​(Sort sort,
                  java.lang.String symbol)
        Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
        Parameters:
        sort - The sort of the variable.
        symbol - The name of the variable.
        Returns:
        The variable.

      • mkDatatypeConstructorDecl

        public DatatypeConstructorDecl mkDatatypeConstructorDecl​(java.lang.String name)
        Create a datatype constructor declaration.
        Parameters:
        name - The name of the datatype constructor.
        Returns:
        The DatatypeConstructorDecl.

      • mkDatatypeDecl

        public DatatypeDecl mkDatatypeDecl​(java.lang.String name)
        Create a datatype declaration.
        Parameters:
        name - The name of the datatype.
        Returns:
        The DatatypeDecl.

      • mkDatatypeDecl

        public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   boolean isCoDatatype)
        Create a datatype declaration.
        Parameters:
        name - The name of the datatype.
        isCoDatatype - True if a codatatype is to be constructed.
        Returns:
        The DatatypeDecl.

      • mkDatatypeDecl

        public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   Sort[] params)
        Create a datatype declaration. Create sorts parameter with Solver.mkParamSort(String).
        Parameters:
        name - The name of the datatype.
        params - A list of sort parameters.
        Returns:
        The DatatypeDecl.
        Note:
        This method is experimental and may change in future versions.

      • mkDatatypeDecl

        public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   Sort[] params,
                                   boolean isCoDatatype)
        Create a datatype declaration. Create sorts parameter with Solver.mkParamSort(String).
        Parameters:
        name - The name of the datatype.
        params - A list of sort parameters.
        isCoDatatype - True if a codatatype is to be constructed.
        Returns:
        The DatatypeDecl.

      • getPointer

        public long getPointer()

      • deletePointer

        public void deletePointer()

      • toString

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