Package io.github.cvc5

Class Solver

  • All Implemented Interfaces:
    java.lang.AutoCloseable
    public class Solver
extends java.lang.Object
implements java.lang.AutoCloseable
    A cvc5 solver.

    • Constructor Detail

      • Solver

        public Solver()

    • Method Detail

      • getPointer

        public long getPointer()

      • deletePointer

        public void deletePointer()

      • close

        public void close()
        Specified by:
        close in interface java.lang.AutoCloseable

      • getNullSort

        public Sort getNullSort()
        Returns:
        Sort null.

      • getBooleanSort

        public Sort getBooleanSort()
        Returns:
        Sort Boolean.

      • getIntegerSort

        public Sort getIntegerSort()
        Returns:
        Sort Integer.

      • getIntegerSort

        public long getIntegerSort​(long pointer)

      • getRealSort

        public Sort getRealSort()
        Returns:
        Sort Real.

      • getRegExpSort

        public Sort getRegExpSort()
        Returns:
        Sort RegExp.

      • getStringSort

        public Sort getStringSort()
        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

      • 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.
        Throws:
        CVC5ApiException

      • 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

      • 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

      • 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.

      • 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.

      • 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

      • 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

      • 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

      • 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

      • mkTupleSort

        public Sort mkTupleSort​(Sort[] sorts)
        Create a tuple sort.
        Parameters:
        sorts - Of the elements of the tuple.
        Returns:
        The tuple 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)
        Create nullary term of given kind from a given operator. Create operators with mkOp().
        Parameters:
        op - The operator.
        Returns:
        The Term.

      • mkTerm

        public Term mkTerm​(Op op,
                   Term child)
        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

        public Term mkTerm​(Op op,
                   Term child1,
                   Term child2)
        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

        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().
        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

        public Term mkTerm​(Op op,
                   Term[] children)
        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

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

      • 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.
        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.

      • 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.
        Throws:
        CVC5ApiException

      • 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.
        Throws:
        CVC5ApiException

      • 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.
        Throws:
        CVC5ApiException

      • 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

      • 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

      • 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

      • 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

      • 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
        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
        Note:
        The given value must fit into a bit-vector of the given size.

      • 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

      • 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

      • 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

      • 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

      • 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

      • mkRoundingMode

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

      • mkFloatingPoint

        public Term mkFloatingPoint​(int exp,
                            int sig,
                            Term val)
                     throws CVC5ApiException
        Create a floating-point constant.
        Parameters:
        exp - Size of the exponent.
        sig - Size of the significand.
        val - Value of the floating-point constant as a bit-vector term.
        Throws:
        CVC5ApiException

      • 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
        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 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 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 formula without doing "much" work. Does not involve the SAT Engine in the simplification, but uses the current definitions, assertions, and the current partial model, if one has been constructed. It also involves theory normalization.
        Parameters:
        t - The formula to simplify.
        Returns:
        The simplified formula.
        Note:
        This method 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.

      • 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
        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​(io.github.cvc5.modes.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> )
        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.
        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.

      • 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.

      • getProof

        public java.lang.String getProof()
        Get refutation proof for the most recent call to checkSat. SMT-LIB: ( get-proof ) Requires to enable option produce-proofs.
        Returns:
        A string representing the proof. This is impacted by the value of proof-format-mode.
        Note:
        This method is experimental and may change in future versions.

      • getProof

        public java.lang.String getProof​(io.github.cvc5.modes.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 string representing the proof. This is equivalent to getProof when c is PROOF_COMPONENT_FULL.
        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.
        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.

      • 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

      • 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​(io.github.cvc5.modes.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 or NOT_ENTAILED query. SMT-LIB: ( block-model-values ( <terms>+ ) ) Requires enabling option produce-models.
        Note:
        This method is experimental and may change in future versions.

      • getInstantiations

        public java.lang.String getInstantiations()
        Return a string that contains information about all instantiations made by the quantifiers module.
        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

      • 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

      • 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

      • 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.

      • synthInv

        public Term synthInv​(java.lang.String symbol,
                     Term[] boundVars)
        Synthesize invariant. SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) )
        Parameters:
        symbol - The name of the invariant.
        boundVars - The parameters to this invariant.
        Returns:
        The invariant.

      • synthInv

        public Term synthInv​(java.lang.String symbol,
                     Term[] boundVars,
                     Grammar grammar)
        Synthesize invariant following specified syntactic constraints. SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) <g> )
        Parameters:
        symbol - The name of the invariant.
        boundVars - The parameters to this invariant.
        grammar - The syntactic constraints.
        Returns:
        The invariant.

      • 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.

      • 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.

      • 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.

      • getStatistics

        public Statistics getStatistics()
        Returns 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.

      • getNullTerm

        public Term getNullTerm()
        Returns:
        Null term.

      • getNullResult

        public Result getNullResult()
        Returns:
        Null result.

      • getNullSynthResult

        public SynthResult getNullSynthResult()
        Returns:
        Null synth result.

      • getNullOp

        public Op getNullOp()
        Returns:
        Null op.

      • getNullDatatypeDecl

        public DatatypeDecl getNullDatatypeDecl()
        Returns:
        Null op.