Class Solver

Method Details

• deletePointer

  protected void deletePointer(long pointer)

  Delete the native resource associated with the specified pointer.

  Subclasses must implement this method to provide resource-specific cleanup logic.

  Parameters:

  pointer - the native pointer to delete

• toString

  protected String toString(long pointer)

  Return a string representation of the specified native pointer.

  Subclasses must implement this method to convert the native pointer into a meaningful string.

  Parameters:

  pointer - the native pointer

  Returns:

  a string representation of the pointer

• equals

  public boolean equals(Object s)

  Overrides:

  equals in class 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.

• getRoundingModeSort

  @Deprecated public Sort getRoundingModeSort() throws CVC5ApiException

  Deprecated.

  This function is deprecated and replaced by TermManager.getRoundingModeSort(). It will be removed in a future release.

  Get the floating-point rounding mode sort.

  Returns:

  Sort RoundingMode.

  Throws:

  CVC5ApiException - on error

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

• mkDatatypeSort

  @Deprecated public Sort mkDatatypeSort(DatatypeDecl dtypedecl) throws CVC5ApiException

  Deprecated.

  This function is deprecated and replaced by TermManager.mkDatatypeSort(DatatypeDecl). It will be removed in a future release.

  Create a datatype sort.

  Parameters:

  dtypedecl - The datatype declaration from which the sort is created.

  Returns:

  The datatype 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(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<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(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(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(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, 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, 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:

  • Kind.DIVISIBLE (to support arbitrary precision integers)

  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(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(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(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(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, 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(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, 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, 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(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(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(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(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 TermManager.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(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 TermManager.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(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(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(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(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(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(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(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(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(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 TermManager.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 TermManager.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 TermManager.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 TermManager.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 String getInfo(String flag)

  Get info from the solver. SMT-LIB: ( get-info <info_flag> )

  Parameters:

  flag - The get-info flag.

  Returns:

  The info.

• getOption

  public String getOption(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.

• getOptionNames

  public String[] getOptionNames()

  Get all option names that can be used with setOption(String, String), getOption(String) and getOptionInfo(String).

  Returns:

  All option names.

• getOptionInfo

  public OptionInfo getOptionInfo(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 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 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 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.

• proofToString

  public String proofToString(Proof proof, ProofFormat format, Map assertionNames)

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

  assertionNames - Mapping between assertions and names, if they were given by the user. This is used by the Alethe proof format.

  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 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(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(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() throws CVC5ApiException

  Pop a level from the assertion stack. SMT-LIB: ( pop <numeral> )

  Throws:

  CVC5ApiException - on error

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

  Given that A->B is valid, this function determines a term I over the shared variables of A and B, such that A->I and I->B are valid. A is the current set of assertions and B is the conjecture, given as conj.

  SMT-LIB: ( get-interpolant <symbol> <conj> )

  Parameters:

  conj - The conjecture term.

  Returns:

  The interpolant, if an interpolant exists, else the null term.

  Note:

  In SMT-LIB, <symbol> assigns a symbol to the interpolant., Requires option produce-interpolants to be set to a mode different from none., This method is experimental and may change in future versions.

• getInterpolant

  public Term getInterpolant(Term conj, Grammar grammar)

  Get an interpolant.

  Given that A->B is valid, this function determines a term I, over the shared variables of A and B, with respect to a given grammar, such that A->I and I->B are valid, if such a term exits. A is the current set of assertions and B is the conjecture, given as conj.

  SMT-LIB: ( get-interpolant <symbol> <conj> <g> )

  Parameters:

  conj - The conjecture term.

  grammar - The grammar for the interpolant I.

  Returns:

  The interpolant, if an interpolant exists, else the null term.

  Note:

  In SMT-LIB, <symbol> assigns a symbol to the interpolant., Requires option produce-interpolants to be set to a mode different from none., 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 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() throws CVC5ApiException

  Push a level to the assertion stack. SMT-LIB: ( push <numeral> )

  Throws:

  CVC5ApiException - on error

• 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(String keyword, 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(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 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(String option, String value)

  Set option. SMT-LIB: ( set-option <option> )

  Parameters:

  option - The option name.

  value - The option value.

• declareSygusVar

  public Term declareSygusVar(String symbol, Sort sort)

  Append symbol to the current list of universal variables. SyGuS v2: ( declare-var <symbol> <sort> )

  Parameters:

  symbol - The name of the universal variable.

  sort - The sort 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(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(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 String getVersion()

  Get a string representation of the version of this solver.

  Returns:

  The version string.

• getPointer

  public long getPointer()

  Return the raw native pointer.

  Returns:

  the pointer value

• deletePointer

  public void deletePointer()

  Free the native resource associated with this pointer.

  This method should be called to explicitly clean up the underlying native resource. It removes this instance from the Context, then invokes the subclass-defined deletePointer(long) method to perform the actual cleanup.

• toString

  public String toString()

  Return a string representation of the pointer.

  Overrides:

  toString in class Object

  Returns:

  a string representation of the pointer