Package io.github.cvc5

Class Solver

  • public class Solver
extends java.lang.Object
    A cvc5 solver.

    • Field Detail

      • pointer

        protected long pointer

    • Constructor Detail

      • Solver

        @Deprecated
public Solver()
        Deprecated.
        This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
        Create solver instance.

      • Solver

        public Solver​(TermManager d_tm)
        Create solver instance.
        Parameters:
        d_tm - The associated term manager.

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • toString

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

      • equals

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

      • getTermManager

        public TermManager getTermManager()
        Get the associated term manager instance
        Returns:
        The term manager.

      • getBooleanSort

        @Deprecated
public Sort getBooleanSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.
        Get the Boolean sort.
        Returns:
        Sort Boolean.

      • getIntegerSort

        @Deprecated
public Sort getIntegerSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.
        Get the integer sort.
        Returns:
        Sort Integer.

      • getRealSort

        @Deprecated
public Sort getRealSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.
        Get the real sort.
        Returns:
        Sort Real.

      • getRegExpSort

        @Deprecated
public Sort getRegExpSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.
        Get the regular expression sort.
        Returns:
        Sort RegExp.

      • getStringSort

        @Deprecated
public Sort getStringSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.getStringSort(). It will be removed in a future release.
        Get the string sort.
        Returns:
        Sort String.

      • mkArraySort

        @Deprecated
public Sort mkArraySort​(Sort indexSort,
                        Sort elemSort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkArraySort(Sort, Sort). It will be removed in a future release.
        Create an array sort.
        Parameters:
        indexSort - The array index sort.
        elemSort - The array element sort.
        Returns:
        The array sort.

      • mkBitVectorSort

        @Deprecated
public Sort mkBitVectorSort​(int size)
                     throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBitVectorSort(int). It will be removed in a future release.
        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

        @Deprecated
public Sort mkFiniteFieldSort​(java.lang.String size,
                              int base)
                       throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.
        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

        @Deprecated
public Sort mkFloatingPointSort​(int exp,
                                int sig)
                         throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.
        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

      • mkDatatypeSorts

        @Deprecated
public Sort[] mkDatatypeSorts​(DatatypeDecl[] dtypedecls)
                       throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeSorts(DatatypeDecl[]). It will be removed in a future release.
        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

        @Deprecated
public Sort mkFunctionSort​(Sort domain,
                           Sort codomain)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFunctionSort(Sort, Sort). It will be removed in a future release.
        Create function sort.
        Parameters:
        domain - The sort of the fuction argument.
        codomain - The sort of the function return value.
        Returns:
        The function sort.

      • mkFunctionSort

        @Deprecated
public Sort mkFunctionSort​(Sort[] sorts,
                           Sort codomain)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFunctionSort(Sort[], Sort). It will be removed in a future release.
        Create function sort.
        Parameters:
        sorts - The sort of the function arguments.
        codomain - The sort of the function return value.
        Returns:
        The function sort.

      • mkParamSort

        @Deprecated
public Sort mkParamSort​(java.lang.String symbol)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.
        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

        @Deprecated
public Sort mkParamSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkParamSort(). It will be removed in a future release.
        Create a sort parameter.
        Returns:
        The sort parameter.
        Note:
        This method is experimental and may change in future versions.

      • mkPredicateSort

        @Deprecated
public Sort mkPredicateSort​(Sort[] sorts)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.
        Create a predicate sort.
        Parameters:
        sorts - The list of sorts of the predicate.
        Returns:
        The predicate sort.

      • mkRecordSort

        @Deprecated
public Sort mkRecordSort​(Pair<java.lang.String,​Sort>[] fields)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.
        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

        @Deprecated
public Sort mkSetSort​(Sort elemSort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.
        Create a set sort.
        Parameters:
        elemSort - The sort of the set elements.
        Returns:
        The set sort.

      • mkBagSort

        @Deprecated
public Sort mkBagSort​(Sort elemSort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.
        Create a bag sort.
        Parameters:
        elemSort - The sort of the bag elements.
        Returns:
        The bag sort.

      • mkSequenceSort

        @Deprecated
public Sort mkSequenceSort​(Sort elemSort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.
        Create a sequence sort.
        Parameters:
        elemSort - The sort of the sequence elements.
        Returns:
        The sequence sort.

      • mkAbstractSort

        @Deprecated
public Sort mkAbstractSort​(SortKind kind)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.
        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

        @Deprecated
public Sort mkUninterpretedSort​(java.lang.String symbol)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.
        Create an uninterpreted sort.
        Parameters:
        symbol - The name of the sort.
        Returns:
        The uninterpreted sort.

      • mkUninterpretedSort

        @Deprecated
public Sort mkUninterpretedSort()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUninterpretedSort(). It will be removed in a future release.
        Create an uninterpreted sort.
        Returns:
        The uninterpreted sort.

      • mkUnresolvedDatatypeSort

        @Deprecated
public Sort mkUnresolvedDatatypeSort​(java.lang.String symbol,
                                     int arity)
                              throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.
        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

        @Deprecated
public Sort mkUnresolvedDatatypeSort​(java.lang.String symbol)
                              throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). It will be removed in a future release.
        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

        @Deprecated
public Sort mkUninterpretedSortConstructorSort​(int arity,
                                               java.lang.String symbol)
                                        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.
        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

        @Deprecated
public Sort mkUninterpretedSortConstructorSort​(int arity)
                                        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). It will be removed in a future release.
        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

        @Deprecated
public Sort mkTupleSort​(Sort[] sorts)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.
        Create a tuple sort.
        Parameters:
        sorts - Of the elements of the tuple.
        Returns:
        The tuple sort.

      • mkNullableSort

        @Deprecated
public Sort mkNullableSort​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.
        Create a nullable sort.
        Parameters:
        sort - The sort of the element of the nullable.
        Returns:
        The nullable sort.

      • mkTerm

        @Deprecated
public Term mkTerm​(Kind kind)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.
        Create 0-ary term of given kind.
        Parameters:
        kind - The kind of the term.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Kind kind,
                   Term child)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.
        Create a unary term of given kind.
        Parameters:
        kind - The kind of the term.
        child - The child of the term.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Kind kind,
                   Term child1,
                   Term child2)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.
        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

        @Deprecated
public Term mkTerm​(Kind kind,
                   Term child1,
                   Term child2,
                   Term child3)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.
        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

        @Deprecated
public Term mkTerm​(Kind kind,
                   Term[] children)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.
        Create n-ary term of given kind.
        Parameters:
        kind - The kind of the term.
        children - The children of the term.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Op op)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Op). It will be removed in a future release.
        Create nullary term of given kind from a given operator. Create operators with mkOp().
        Parameters:
        op - The operator.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Op op,
                   Term child)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.
        Create unary term of given kind from a given operator. Create operators with mkOp().
        Parameters:
        op - The operator.
        child - The child of the term.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Op op,
                   Term child1,
                   Term child2)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.
        Create binary term of given kind from a given operator. Create operators with mkOp().
        Parameters:
        op - The operator.
        child1 - The first child of the term.
        child2 - The second child of the term.
        Returns:
        The Term.

      • mkTerm

        @Deprecated
public Term mkTerm​(Op op,
                   Term child1,
                   Term child2,
                   Term child3)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). It will be removed in a future release.
        Create ternary term of given kind from a given operator. Create operators with mkOp().
        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.

      • mkTerm

        @Deprecated
public Term mkTerm​(Op op,
                   Term[] children)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.
        Create n-ary term of given kind from a given operator. Create operators with mkOp().
        Parameters:
        op - The operator.
        children - The children of the term.
        Returns:
        The Term.

      • mkTuple

        @Deprecated
public Term mkTuple​(Term[] terms)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.
        Create a tuple term. Terms are automatically converted if sorts are compatible.
        Parameters:
        terms - The elements in the tuple.
        Returns:
        The tuple Term.

      • mkNullableSome

        @Deprecated
public Term mkNullableSome​(Term term)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.
        Create a nullable some term.
        Parameters:
        term - The element value.
        Returns:
        the Element value wrapped in some constructor.

      • mkNullableVal

        @Deprecated
public Term mkNullableVal​(Term term)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.
        Create a selector for nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        The element value of the nullable term.

      • mkNullableIsNull

        @Deprecated
public Term mkNullableIsNull​(Term term)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.
        Create a null tester for a nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        A tester whether term is null.

      • mkNullableIsSome

        @Deprecated
public Term mkNullableIsSome​(Term term)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.
        Create a some tester for a nullable term.
        Parameters:
        term - A nullable term.
        Returns:
        A tester whether term is some.

      • mkNullableNull

        @Deprecated
public Term mkNullableNull​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.
        Create a constant representing a null value of the given sort.
        Parameters:
        sort - The sort of the Nullable element.
        Returns:
        The null constant.

      • mkNullableLift

        @Deprecated
public Term mkNullableLift​(Kind kind,
                           Term[] args)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.
        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

        @Deprecated
public Op mkOp​(Kind kind)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.
        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

        @Deprecated
public Op mkOp​(Kind kind,
               java.lang.String arg)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.
        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

        @Deprecated
public Op mkOp​(Kind kind,
               int arg)
        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkOp(Kind, int). It will be removed in a future release.
        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

        @Deprecated
public Op mkOp​(Kind kind,
               int arg1,
               int arg2)
        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkOp(Kind, int, int). It will be removed in a future release.
        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

        @Deprecated
public Op mkOp​(Kind kind,
               int[] args)
        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkOp(Kind, int[]). It will be removed in a future release.
        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

        @Deprecated
public Term mkTrue()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkTrue(). It will be removed in a future release.
        Create a Boolean true constant.
        Returns:
        The true constant.

      • mkFalse

        @Deprecated
public Term mkFalse()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFalse(). It will be removed in a future release.
        Create a Boolean false constant.
        Returns:
        The false constant.

      • mkBoolean

        @Deprecated
public Term mkBoolean​(boolean val)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBoolean(boolean). It will be removed in a future release.
        Create a Boolean constant.
        Parameters:
        val - The value of the constant.
        Returns:
        The Boolean constant.

      • mkPi

        @Deprecated
public Term mkPi()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkPi(). It will be removed in a future release.
        Create a constant representing the number Pi.
        Returns:
        A constant representing Pi.

      • mkInteger

        @Deprecated
public Term mkInteger​(java.lang.String s)
               throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.
        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

        @Deprecated
public Term mkInteger​(long val)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkInteger(long). It will be removed in a future release.
        Create an integer constant from a C++ int.
        Parameters:
        val - The value of the constant.
        Returns:
        A constant of sort Integer.

      • mkReal

        @Deprecated
public Term mkReal​(java.lang.String s)
            throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.
        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

        @Deprecated
public Term mkReal​(long val)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkReal(long). It will be removed in a future release.
        Create a real constant from an integer.
        Parameters:
        val - The value of the constant.
        Returns:
        A constant of sort Integer.

      • mkReal

        @Deprecated
public Term mkReal​(long num,
                   long den)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkReal(long, long). It will be removed in a future release.
        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

        @Deprecated
public Term mkRegexpNone()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.
        Create a regular expression none (re.none) term.
        Returns:
        The none term.

      • mkRegexpAll

        @Deprecated
public Term mkRegexpAll()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.
        Create a regular expression all (re.all) term.
        Returns:
        The all term.

      • mkRegexpAllchar

        @Deprecated
public Term mkRegexpAllchar()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.
        Create a regular expression allchar (re.allchar) term.
        Returns:
        The allchar term.

      • mkEmptySet

        @Deprecated
public Term mkEmptySet​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.
        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

        @Deprecated
public Term mkEmptyBag​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.
        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

        @Deprecated
public Term mkSepEmp()
        Deprecated.
        This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.
        Create a separation logic empty term.
        Returns:
        The separation logic empty term.
        Note:
        This method is experimental and may change in future versions.

      • mkSepNil

        @Deprecated
public Term mkSepNil​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.
        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

        @Deprecated
public Term mkString​(java.lang.String s)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.
        Create a String constant.
        Parameters:
        s - The string this constant represents.
        Returns:
        The String constant.

      • mkString

        @Deprecated
public Term mkString​(java.lang.String s,
                     boolean useEscSequences)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkString(String, boolean). It will be removed in a future release.
        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

        @Deprecated
public Term mkString​(int[] s)
              throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkString(int[]). It will be removed in a future release.
        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

        @Deprecated
public Term mkEmptySequence​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.
        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

        @Deprecated
public Term mkUniverseSet​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.
        Create a universe set of the given sort.
        Parameters:
        sort - The sort of the set elements.
        Returns:
        The universe set constant.

      • mkBitVector

        @Deprecated
public Term mkBitVector​(int size)
                 throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.
        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

        @Deprecated
public Term mkBitVector​(int size,
                        long val)
                 throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.
        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

        @Deprecated
public Term mkBitVector​(int size,
                        java.lang.String s,
                        int base)
                 throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkBitVector(int, String, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkFiniteFieldElem​(java.lang.String val,
                              Sort sort,
                              int base)
                       throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkConstArray​(Sort sort,
                         Term val)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPointPosInf​(int exp,
                                  int sig)
                           throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPointNegInf​(int exp,
                                  int sig)
                           throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPointNaN​(int exp,
                               int sig)
                        throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPointPosZero​(int exp,
                                   int sig)
                            throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPointNegZero​(int exp,
                                   int sig)
                            throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkRoundingMode​(RoundingMode rm)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.
        Create a rounding mode constant.
        Parameters:
        rm - The floating point rounding mode this constant represents.
        Returns:
        The rounding mode.

      • mkFloatingPoint

        @Deprecated
public Term mkFloatingPoint​(int exp,
                            int sig,
                            Term val)
                     throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.
        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

        @Deprecated
public Term mkFloatingPoint​(Term sign,
                            Term exp,
                            Term sig)
                     throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, Term). It will be removed in a future release.
        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

        @Deprecated
public Term mkCardinalityConstraint​(Sort sort,
                                    int upperBound)
                             throws CVC5ApiException
        Deprecated.
        This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.
        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

        @Deprecated
public Term mkConst​(Sort sort,
                    java.lang.String symbol)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.
        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

        @Deprecated
public Term mkConst​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkConst(Sort). It will be removed in a future release.
        Create a free constant with a default symbol name.
        Parameters:
        sort - The sort of the constant.
        Returns:
        The first-order constant.

      • mkVar

        @Deprecated
public Term mkVar​(Sort sort)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.
        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

        @Deprecated
public Term mkVar​(Sort sort,
                  java.lang.String symbol)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.
        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

        @Deprecated
public DatatypeConstructorDecl mkDatatypeConstructorDecl​(java.lang.String name)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.
        Create a datatype constructor declaration.
        Parameters:
        name - The name of the datatype constructor.
        Returns:
        The DatatypeConstructorDecl.

      • mkDatatypeDecl

        @Deprecated
public DatatypeDecl mkDatatypeDecl​(java.lang.String name)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.
        Create a datatype declaration.
        Parameters:
        name - The name of the datatype.
        Returns:
        The DatatypeDecl.

      • mkDatatypeDecl

        @Deprecated
public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   boolean isCoDatatype)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.
        Create a datatype declaration.
        Parameters:
        name - The name of the datatype.
        isCoDatatype - True if a codatatype is to be constructed.
        Returns:
        The DatatypeDecl.

      • mkDatatypeDecl

        @Deprecated
public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   Sort[] params)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
        Create a datatype declaration. Create sorts parameter with 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

        @Deprecated
public DatatypeDecl mkDatatypeDecl​(java.lang.String name,
                                   Sort[] params,
                                   boolean isCoDatatype)
        Deprecated.
        This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
        Create a datatype declaration. Create sorts parameter with 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.

      • simplify

        public Term simplify​(Term t)
        Simplify a term or formula based on rewriting.
        Parameters:
        t - The term to simplify.
        Returns:
        The simplified term.
        Note:
        This function is experimental and may change in future versions.

      • simplify

        public Term simplify​(Term t,
                     boolean applySubs)
        Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables. If applySubs is true, then for example, if `(= x 0)` was asserted to this solver, this method may replace occurrences of `x` with `0`.
        Parameters:
        t - The term to simplify.
        applySubs - Whether to apply substitutions for solved variables.
        Returns:
        The simplified term.
        Note:
        This function is experimental and may change in future versions.

      • assertFormula

        public void assertFormula​(Term term)
        Assert a formula. SMT-LIB: ( assert <term> )
        Parameters:
        term - The formula to assert.

      • checkSat

        public Result checkSat()
        Check satisfiability. SMT-LIB: ( check-sat )
        Returns:
        The result of the satisfiability check.

      • checkSatAssuming

        public Result checkSatAssuming​(Term assumption)
        Check satisfiability assuming the given formula. SMT-LIB: ( check-sat-assuming ( <prop_literal> ) )
        Parameters:
        assumption - The formula to assume.
        Returns:
        The result of the satisfiability check.

      • checkSatAssuming

        public Result checkSatAssuming​(Term[] assumptions)
        Check satisfiability assuming the given formulas. SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) )
        Parameters:
        assumptions - The formulas to assume.
        Returns:
        The result of the satisfiability check.

      • declareDatatype

        public Sort declareDatatype​(java.lang.String symbol,
                            DatatypeConstructorDecl[] ctors)
        Create datatype sort. SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
        Parameters:
        symbol - The name of the datatype sort.
        ctors - The constructor declarations of the datatype sort.
        Returns:
        The datatype sort.

      • declareFun

        public Term declareFun​(java.lang.String symbol,
                       Sort[] sorts,
                       Sort sort)
        Declare n-ary function symbol. SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
        Parameters:
        symbol - The name of the function.
        sorts - The sorts of the parameters to this function.
        sort - The sort of the return value of this function.
        Returns:
        The function.

      • declareFun

        public Term declareFun​(java.lang.String symbol,
                       Sort[] sorts,
                       Sort sort,
                       boolean fresh)
        Declare n-ary function symbol. SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
        Parameters:
        symbol - The name of the function.
        sorts - The sorts of the parameters to this function.
        sort - The sort of the return value of this function.
        fresh - If true, then this method always returns a new Term. Otherwise, this method will always return the same Term for each call with the given sorts and symbol where fresh is false.
        Returns:
        The function.

      • declareSort

        public Sort declareSort​(java.lang.String symbol,
                        int arity)
                 throws CVC5ApiException
        Declare uninterpreted sort. SMT-LIB: ( declare-sort <symbol> <numeral> )
        Parameters:
        symbol - The name of the sort.
        arity - The arity of the sort.
        Returns:
        The sort.
        Throws:
        CVC5ApiException - on error
        Note:
        This corresponds to mkUninterpretedSort() const if arity = 0, and to mkUninterpretedSortConstructorSort() const if arity > 0.

      • declareSort

        public Sort declareSort​(java.lang.String symbol,
                        int arity,
                        boolean fresh)
                 throws CVC5ApiException
        Declare uninterpreted sort. SMT-LIB: ( declare-sort <symbol> <numeral> )
        Parameters:
        symbol - The name of the sort.
        arity - The arity of the sort.
        fresh - If true, then this method always returns a new Sort. Otherwise, this method will always return the same Sort for each call with the given arity and symbol where fresh is false.
        Returns:
        The sort.
        Throws:
        CVC5ApiException - on error
        Note:
        This corresponds to mkUninterpretedSort() const if arity = 0, and to mkUninterpretedSortConstructorSort() const if arity > 0.

      • defineFun

        public Term defineFun​(java.lang.String symbol,
                      Term[] boundVars,
                      Sort sort,
                      Term term)
        Define n-ary function in the current context. SMT-LIB: ( define-fun <function_def> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        term - The function body.
        Returns:
        The function.

      • defineFun

        public Term defineFun​(java.lang.String symbol,
                      Term[] boundVars,
                      Sort sort,
                      Term term,
                      boolean global)
        Define n-ary function. SMT-LIB: ( define-fun <function_def> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        term - The function body.
        global - Determines whether this definition is global (i.e., persists when popping the context).
        Returns:
        The function.

      • defineFunRec

        public Term defineFunRec​(java.lang.String symbol,
                         Term[] boundVars,
                         Sort sort,
                         Term term)
        Define recursive function in the current context. SMT-LIB: ( define-fun-rec <function_def> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        term - The function body.
        Returns:
        The function.

      • defineFunRec

        public Term defineFunRec​(java.lang.String symbol,
                         Term[] boundVars,
                         Sort sort,
                         Term term,
                         boolean global)
        Define recursive function. SMT-LIB: ( define-fun-rec <function_def> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        term - The function body.
        global - Determines whether this definition is global (i.e., persists when popping the context).
        Returns:
        The function.

      • defineFunRec

        public Term defineFunRec​(Term fun,
                         Term[] boundVars,
                         Term term)
        Define recursive function in the current context. SMT-LIB: ( define-fun-rec <function_def> ) Create parameter fun with mkConst(Sort).
        Parameters:
        fun - The sorted function.
        boundVars - The parameters to this function.
        term - The function body.
        Returns:
        The function.

      • defineFunRec

        public Term defineFunRec​(Term fun,
                         Term[] boundVars,
                         Term term,
                         boolean global)
        Define recursive function. SMT-LIB: ( define-fun-rec <function_def> ) Create parameter fun with mkConst(Sort).
        Parameters:
        fun - The sorted function.
        boundVars - The parameters to this function.
        term - The function body.
        global - Determines whether this definition is global (i.e., persists when popping the context).
        Returns:
        The function.

      • defineFunsRec

        public void defineFunsRec​(Term[] funs,
                          Term[][] boundVars,
                          Term[] terms)
        Define recursive functions in the current context. SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) Create elements of parameter funs with mkConst(Sort).
        Parameters:
        funs - The sorted functions.
        boundVars - The list of parameters to the functions.
        terms - The list of function bodies of the functions.

      • defineFunsRec

        public void defineFunsRec​(Term[] funs,
                          Term[][] boundVars,
                          Term[] terms,
                          boolean global)
        Define recursive functions. SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) Create elements of parameter funs with mkConst(Sort).
        Parameters:
        funs - The sorted functions.
        boundVars - The list of parameters to the functions.
        terms - The list of function bodies of the functions.
        global - Determines whether this definition is global (i.e., persists when popping the context).

      • getLearnedLiterals

        public Term[] getLearnedLiterals()
        Get a list of input literals that are entailed by the current set of assertions. SMT-LIB: ( get-learned-literals )
        Returns:
        The list of learned literals.
        Note:
        This method is experimental and may change in future versions.

      • getLearnedLiterals

        public Term[] getLearnedLiterals​(LearnedLitType type)
        Get a list of literals that are entailed by the current set of assertions. SMT-LIB: ( get-learned-literals :type )
        Parameters:
        type - The type of learned literals to return
        Returns:
        The list of learned literals.
        Note:
        This method is experimental and may change in future versions.

      • getAssertions

        public Term[] getAssertions()
        Get the list of asserted formulas. SMT-LIB: ( get-assertions )
        Returns:
        The list of asserted formulas.

      • getInfo

        public java.lang.String getInfo​(java.lang.String flag)
        Get info from the solver. SMT-LIB: ( get-info <info_flag> )
        Parameters:
        flag - The get-info flag.
        Returns:
        The info.

      • getOption

        public java.lang.String getOption​(java.lang.String option)
        Get the value of a given option. SMT-LIB: ( get-option <keyword> )
        Parameters:
        option - The option for which the value is queried.
        Returns:
        A string representation of the option value.

      • getOptionInfo

        public OptionInfo getOptionInfo​(java.lang.String option)
        Get some information about the given option. Check the OptionInfo class for more details on which information is available.
        Parameters:
        option - The name of the option.
        Returns:
        Information about the given option.

      • getUnsatAssumptions

        public Term[] getUnsatAssumptions()
        Get the set of unsat ("failed") assumptions. SMT-LIB: ( get-unsat-assumptions ) Requires to enable option produce-unsat-assumptions.
        Returns:
        The set of unsat assumptions.

      • getUnsatCore

        public Term[] getUnsatCore()
        Get the unsatisfiable core. SMT-LIB: (get-unsat-core) Requires to enable option produce-unsat-cores.
        Returns:
        A set of terms representing the unsatisfiable core.
        Note:
        In contrast to SMT-LIB, cvc5's API does not distinguish between named and unnamed assertions when producing an unsatisfiable core. Additionally, the API allows this option to be called after a check with assumptions. A subset of those assumptions may be included in the unsatisfiable core returned by this method.

      • getUnsatCoreLemmas

        public Term[] getUnsatCoreLemmas()
        Get the lemmas used to derive unsatisfiability. SMT-LIB: (get-unsat-core-lemmas) Requires the SAT proof unsat core mode, so to enable option unsat-core-mode=sat-proof
        Returns:
        A set of terms representing the lemmas used to derive unsatisfiability.
        Note:
        This method is experimental and may change in future versions.

      • getDifficulty

        public java.util.Map<Term,​Term> getDifficulty()
        Get a difficulty estimate for an asserted formula. This method is intended to be called immediately after any response to a checkSat.
        Returns:
        A map from (a subset of) the input assertions to a real value that. is an estimate of how difficult each assertion was to solve. Unmentioned assertions can be assumed to have zero difficulty.
        Note:
        This method is experimental and may change in future versions.

      • getTimeoutCore

        public Pair<Result,​Term[]> getTimeoutCore()
        Get a timeout core, which computes a subset of the current assertions that cause a timeout. Note it does not require being proceeded by a call to checkSat. SMT-LIB: (get-timeout-core)
        Returns:
        The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of the current assertions that cause a timeout in the specified time timeout-core-timeout. If the result is unsat, then the list of formulas correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the current assertions are satisfiable, and the list of formulas is empty. This method may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.
        Note:
        This method is experimental and may change in future versions.

      • getTimeoutCoreAssuming

        public Pair<Result,​Term[]> getTimeoutCoreAssuming​(Term[] assumptions)
        Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions. Note it does not require being proceeded by a call to checkSat. SMT-LIB: (get-timeout-core)
        Parameters:
        assumptions - The formulas to assume.
        Returns:
        The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of assumptions that cause a timeout when added to the current assertions in the specified time timeout-core-timeout. If the result is unsat, then the list of formulas plus the current assertions correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the given assumptions plus the current assertions are satisfiable, and the list of formulas is empty. This method may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.
        Note:
        This method is experimental and may change in future versions.

      • getProof

        public Proof[] getProof()
        Get refutation proof for the most recent call to checkSat. SMT-LIB: ( get-proof ) Requires to enable option produce-proofs.
        Returns:
        A vector of proof nodes. This is equivalent to getProof when c is FULL.
        Note:
        This method is experimental and may change in future versions.

      • getProof

        public Proof[] getProof​(ProofComponent c)
        Get a proof associated with the most recent call to checkSat. SMT-LIB: ( get-proof :c) Requires to enable option produce-proofs.
        Parameters:
        c - The component of the proof to return
        Returns:
        A vector of proof nodes.
        Note:
        This method is experimental and may change in future versions.

      • proofToString

        public java.lang.String proofToString​(Proof proof)
        Prints a proof into a string with a slected proof format mode. Other aspects of printing are taken from the solver options.
        Parameters:
        proof - A proof.
        Returns:
        The proof printed in the current format.
        Note:
        This method is experimental and may change in future versions.

      • proofToString

        public java.lang.String proofToString​(Proof proof,
                                      ProofFormat format)
        Prints a proof into a string with a slected proof format mode. Other aspects of printing are taken from the solver options.
        Parameters:
        proof - A proof.
        format - The proof format used to print the proof. Must be `PROOF_FORMAT_NONE` if the proof is from a component other than `PROOF_COMPONENT_FULL`.
        Returns:
        The proof printed in the current format.
        Note:
        This method is experimental and may change in future versions.

      • getValue

        public Term getValue​(Term term)
        Get the value of the given term in the current model. SMT-LIB: ( get-value ( <term> ) )
        Parameters:
        term - The term for which the value is queried.
        Returns:
        The value of the given term.

      • getValue

        public Term[] getValue​(Term[] terms)
        Get the values of the given terms in the current model. SMT-LIB: ( get-value ( <term>+ ) )
        Parameters:
        terms - The terms for which the value is queried.
        Returns:
        The values of the given terms.

      • getModelDomainElements

        public Term[] getModelDomainElements​(Sort s)
        Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this method.
        Parameters:
        s - The uninterpreted sort in question.
        Returns:
        The domain elements of s in the current model.

      • isModelCoreSymbol

        public boolean isModelCoreSymbol​(Term v)
        This returns false if the model value of free constant v was not essential for showing the satisfiability of the last call to checkSat() using the current model. This method will only return false (for any v) if the option model-cores has been set.
        Parameters:
        v - The term in question.
        Returns:
        True if v is a model core symbol.
        Note:
        This method is experimental and may change in future versions.

      • getModel

        public java.lang.String getModel​(Sort[] sorts,
                                 Term[] vars)
        Get the model SMT-LIB: ( get-model ) Requires to enable option produce-models.
        Parameters:
        sorts - The list of uninterpreted sorts that should be printed in the. model.
        vars - The list of free constants that should be printed in the. model. A subset of these may be printed based on isModelCoreSymbol(Term).
        Returns:
        A string representing the model.
        Note:
        This method is experimental and may change in future versions.

      • getQuantifierElimination

        public Term getQuantifierElimination​(Term q)
        Do quantifier elimination. SMT-LIB: ( get-qe <q> ) Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.
        Parameters:
        q - A quantified formula of the form: Q x1...xn. P( x1...xn, y1...yn ) where P( x1...xn, y1...yn ) is a quantifier-free formula.
        Returns:
        A formula ret such that, given the current set of formulas A asserted to this solver: - ( A && q ) and ( A && ret ) are equivalent - ret is quantifier-free formula containing only free variables in y1...yn.
        Note:
        This method is experimental and may change in future versions.

      • getQuantifierEliminationDisjunct

        public Term getQuantifierEliminationDisjunct​(Term q)
        Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination. SMT-LIB: ( get-qe-disjunct <q> ) Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.
        Parameters:
        q - A quantified formula of the form: Q x1...xn. P( x1...xn, y1...yn ) where P( x1...xn, y1...yn ) is a quantifier-free formula.
        Returns:
        A formula ret such that, given the current set of formulas A asserted to this solver: - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is exists, - ret is quantifier-free formula containing only free variables in y1...yn, - If Q is exists, let A && Q_n be the formula A && ~(ret && Q_1) && ... && ~(ret && Q_n) where for each i=1,...n, formula ret && Q_i is the result of calling getQuantifierEliminationDisjunct(Term) for q with the set of assertions A && Q_{i-1}. Similarly, if Q is forall, then let A && Q_n be A && (ret && Q_1) && ... && (ret&& Q_n) where ret && Q_i is the same as above. In either case, we have that ret && Q_j will eventually be true or false, for some finite j.
        Note:
        This method is experimental and may change in future versions.

      • declareSepHeap

        public void declareSepHeap​(Sort locSort,
                           Sort dataSort)
        When using separation logic, this sets the location sort and the datatype sort to the given ones. This method should be invoked exactly once, before any separation logic constraints are provided.
        Parameters:
        locSort - The location sort of the heap.
        dataSort - The data sort of the heap.
        Note:
        This method is experimental and may change in future versions.

      • getValueSepHeap

        public Term getValueSepHeap()
        When using separation logic, obtain the term for the heap.
        Returns:
        The term for the heap.
        Note:
        This method is experimental and may change in future versions.

      • getValueSepNil

        public Term getValueSepNil()
        When using separation logic, obtain the term for nil.
        Returns:
        The term for nil.
        Note:
        This method is experimental and may change in future versions.

      • declarePool

        public Term declarePool​(java.lang.String symbol,
                        Sort sort,
                        Term[] initValue)
        Declare a symbolic pool of terms with the given initial value. SMT-LIB: ( declare-pool <symbol> <sort> ( <term>* ) )
        Parameters:
        symbol - The name of the pool.
        sort - The sort of the elements of the pool.
        initValue - The initial value of the pool.
        Returns:
        The pool.
        Note:
        This method is experimental and may change in future versions.

      • declareOracleFun

        public Term declareOracleFun​(java.lang.String symbol,
                             Sort[] sorts,
                             Sort sort,
                             IOracle oracle)
        Declare an oracle function with reference to an implementation. Oracle functions have a different semantics with respect to ordinary declared functions. In particular, for an input to be satisfiable, its oracle functions are implicitly universally quantified. This method is used in part for implementing this command: (declare-oracle-fun <sym> (<sort>*) <sort> <sym>) In particular, the above command is implemented by constructing a function over terms that wraps a call to binary sym via a text interface.
        Parameters:
        symbol - The name of the oracle
        sorts - The sorts of the parameters to this function
        sort - The sort of the return value of this function
        oracle - An object that implements the oracle interface.
        Returns:
        The oracle function
        Note:
        This method is experimental and may change in future versions.

      • addPlugin

        public void addPlugin​(AbstractPlugin p)
        Add plugin to this solver. Its callbacks will be called throughout the lifetime of this solver.
        Parameters:
        p - The plugin to add to this solver.

      • pop

        public void pop​(int nscopes)
         throws CVC5ApiException
        Pop (a) level(s) from the assertion stack. SMT-LIB: ( pop <numeral> )
        Parameters:
        nscopes - The number of levels to pop.
        Throws:
        CVC5ApiException - on error

      • getInterpolant

        public Term getInterpolant​(Term conj)
        Get an interpolant SMT-LIB: ( get-interpolant <conj> ) Requires option produce-interpolants to be set to a mode different from none.
        Parameters:
        conj - The conjecture term.
        Returns:
        A Term I such that A->I and I->B are valid, where A is the current set of assertions and B is given in the input by conj, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • getInterpolant

        public Term getInterpolant​(Term conj,
                           Grammar grammar)
        Get an interpolant SMT-LIB: ( get-interpolant <conj> <g> ) Requires option produce-interpolants to be set to a mode different from none.
        Parameters:
        conj - The conjecture term.
        grammar - The grammar for the interpolant I.
        Returns:
        A Term I such that A->I and I->B are valid, where A is the current set of assertions and B is given in the input by conj, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • getInterpolantNext

        public Term getInterpolantNext()
        Get the next interpolant. Can only be called immediately after a successful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful. SMT-LIB: (get-interpolant-next) Requires to enable incremental mode, and option produce-interpolants to be set to a mode different from none.
        Returns:
        A Term I such that A->I and I->B are valid, where A is the current set of assertions and B is given in the input by conj on the last call to getInterpolant, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • getAbduct

        public Term getAbduct​(Term conj)
        Get an abduct. SMT-LIB: ( get-abduct <conj> ) Requires enabling option produce-abducts.
        Parameters:
        conj - The conjecture term.
        Returns:
        A term C such that A && C is satisfiable, and A && ~B && C is unsatisfiable, where A is the current set of assertions and B is given in the input by conj, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • getAbduct

        public Term getAbduct​(Term conj,
                      Grammar grammar)
        Get an abduct. SMT-LIB: ( get-abduct <conj> <g> ) Requires enabling option produce-abducts.
        Parameters:
        conj - The conjecture term.
        grammar - The grammar for the abduct C.
        Returns:
        A term C such that A && C is satisfiable, and A && ~B && C is unsatisfiable, where A is the current set of assertions and B is given in the input by conj, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • getAbductNext

        public Term getAbductNext()
        Get the next abduct. Can only be called immediately after a successful call to get-abduct or get-abduct-next. Is guaranteed to produce a syntactically different abduct wrt the last returned abduct if successful. SMT-LIB: ( get-abduct-next ) Requires enabling incremental mode and option produce-abducts.
        Returns:
        A term C such that A^C is satisfiable, and A^~B^C is. unsatisfiable, where A is the current set of assertions and B is given in the input by conj in the last call to getAbduct, or the null term if such a term cannot be found.
        Note:
        This method is experimental and may change in future versions.

      • blockModel

        public void blockModel​(BlockModelsMode mode)
        Block the current model. Can be called only if immediately preceded by a SAT or INVALID query. SMT-LIB: ( block-model ) Requires enabling option produce-models.
        Parameters:
        mode - The mode to use for blocking.
        Note:
        This method is experimental and may change in future versions.

      • blockModelValues

        public void blockModelValues​(Term[] terms)
        Block the current model values of (at least) the values in terms. Can be called only if immediately preceded by a SAT query. SMT-LIB: ( block-model-values ( <terms>+ ) ) Requires enabling option produce-models.
        Parameters:
        terms - The model values to block.
        Note:
        This method is experimental and may change in future versions.

      • getInstantiations

        public java.lang.String getInstantiations()
        Get a string that contains information about all instantiations made by the quantifiers module.
        Returns:
        The string representing the information about all instantiations.
        Note:
        This method is experimental and may change in future versions.

      • push

        public void push​(int nscopes)
          throws CVC5ApiException
        Push (a) level(s) to the assertion stack. SMT-LIB: ( push <numeral> )
        Parameters:
        nscopes - The number of levels to push.
        Throws:
        CVC5ApiException - on error

      • resetAssertions

        public void resetAssertions()
        Remove all assertions. SMT-LIB: ( reset-assertions )

      • setInfo

        public void setInfo​(java.lang.String keyword,
                    java.lang.String value)
             throws CVC5ApiException
        Set info. SMT-LIB: ( set-info <attribute> )
        Parameters:
        keyword - The info flag.
        value - The value of the info flag.
        Throws:
        CVC5ApiException - on error

      • setLogic

        public void setLogic​(java.lang.String logic)
              throws CVC5ApiException
        Set logic. SMT-LIB: ( set-logic <symbol> )
        Parameters:
        logic - The logic to set.
        Throws:
        CVC5ApiException - on error

      • isLogicSet

        public boolean isLogicSet()
        Is logic set? Returns whether we called setLogic yet for this solver.
        Returns:
        whether we called setLogic yet for this solver.

      • getLogic

        public java.lang.String getLogic()
                          throws CVC5ApiException
        Get the logic set the solver.
        Returns:
        The logic used by the solver.
        Throws:
        CVC5ApiException - on error
        Note:
        Asserts isLogicSet().

      • setOption

        public void setOption​(java.lang.String option,
                      java.lang.String value)
        Set option. SMT-LIB: ( set-option <option> )
        Parameters:
        option - The option name.
        value - The option value.

      • declareSygusVar

        public Term declareSygusVar​(java.lang.String symbol,
                            Sort sort)
        Append symbol to the current list of universal variables. SyGuS v2: ( declare-var <symbol> <sort> )
        Parameters:
        sort - The sort of the universal variable.
        symbol - The name of the universal variable.
        Returns:
        The universal variable.

      • mkGrammar

        public Grammar mkGrammar​(Term[] boundVars,
                         Term[] ntSymbols)
        Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.
        Parameters:
        boundVars - The parameters to corresponding synth-fun/synth-inv.
        ntSymbols - The pre-declaration of the non-terminal symbols.
        Returns:
        The grammar.

      • synthFun

        public Term synthFun​(java.lang.String symbol,
                     Term[] boundVars,
                     Sort sort)
        Synthesize n-ary function. SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        Returns:
        The function.

      • synthFun

        public Term synthFun​(java.lang.String symbol,
                     Term[] boundVars,
                     Sort sort,
                     Grammar grammar)
        Synthesize n-ary function following specified syntactic constraints. SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
        Parameters:
        symbol - The name of the function.
        boundVars - The parameters to this function.
        sort - The sort of the return value of this function.
        grammar - The syntactic constraints.
        Returns:
        The function.

      • addSygusConstraint

        public void addSygusConstraint​(Term term)
        Add a forumla to the set of Sygus constraints. SyGuS v2: ( constraint <term> )
        Parameters:
        term - The formula to add as a constraint.

      • getSygusConstraints

        public Term[] getSygusConstraints()
        Get the list of sygus constraints.
        Returns:
        The list of sygus constraints.

      • addSygusAssume

        public void addSygusAssume​(Term term)
        Add a forumla to the set of Sygus assumptions. SyGuS v2: ( assume <term> )
        Parameters:
        term - The formula to add as an assumption.

      • getSygusAssumptions

        public Term[] getSygusAssumptions()
        Get the list of sygus assumptions.
        Returns:
        The list of sygus assumptions.

      • addSygusInvConstraint

        public void addSygusInvConstraint​(Term inv,
                                  Term pre,
                                  Term trans,
                                  Term post)
        Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem. SyGuS v2: ( inv-constraint <inv> <pre> <trans> <post> )
        Parameters:
        inv - The function-to-synthesize.
        pre - The pre-condition.
        trans - The transition relation.
        post - The post-condition.

      • checkSynth

        public SynthResult checkSynth()
        Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. SyGuS v2: ( check-synth )
        Returns:
        The result of the check, which is "solution" if the check found a. solution in which case solutions are available via getSynthSolutions, "no solution" if it was determined there is no solution, or "unknown" otherwise.

      • checkSynthNext

        public SynthResult checkSynthNext()
        Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next.
        Returns:
        The result of the check, which is "solution" if the check found a solution in which case solutions are available via getSynthSolutions, "no solution" if it was determined there is no solution, or "unknown" otherwise.
        Note:
        Requires incremental mode. SyGuS v2: ( check-synth-next )

      • getSynthSolution

        public Term getSynthSolution​(Term term)
        Get the synthesis solution of the given term. This method should be called immediately after the solver answers unsat for sygus input.
        Parameters:
        term - The term for which the synthesis solution is queried.
        Returns:
        The synthesis solution of the given term.

      • getSynthSolutions

        public Term[] getSynthSolutions​(Term[] terms)
        Get the synthesis solutions of the given terms. This method should be called immediately after the solver answers unsat for sygus input.
        Parameters:
        terms - The terms for which the synthesis solutions is queried.
        Returns:
        The synthesis solutions of the given terms.

      • findSynth

        public Term findSynth​(FindSynthTarget fst)
        Find a target term of interest using sygus enumeration, with no provided grammar. The solver will infer which grammar to use in this call, which by default will be the grammars specified by the function(s)-to-synthesize in the current context. SyGuS v2: (find-synth :target)
        Parameters:
        fst - The identifier specifying what kind of term to find
        Returns:
        The result of the find, which is the null term if this call failed.
        Note:
        This method is experimental and may change in future versions.

      • findSynth

        public Term findSynth​(FindSynthTarget fst,
                      Grammar grammar)
        Find a target term of interest using sygus enumeration with a provided grammar. SyGuS v2: (find-synth :target G)
        Parameters:
        fst - The identifier specifying what kind of term to find
        grammar - The grammar for the term
        Returns:
        The result of the find, which is the null term if this call failed.
        Note:
        This method is experimental and may change in future versions.

      • findSynthNext

        public Term findSynthNext()
        Try to find a next target term of interest using sygus enumeration. Must be called immediately after a successful call to find-synth or find-synth-next. SyGuS v2: (find-synth-next)
        Returns:
        The result of the find, which is the null term if this call failed.
        Note:
        This method is experimental and may change in future versions.

      • getStatistics

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

      • getVersion

        public java.lang.String getVersion()
        Get a string representation of the version of this solver.
        Returns:
        The version string.

      • getPointer

        public long getPointer()

      • deletePointer

        public void deletePointer()

      • toString

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