Class TermManager

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 o)

  Overrides:

  equals in class Object

• getStatistics

  public Statistics getStatistics()

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

  Returns:

  A snapshot of the current state of the statistic values.

• getBooleanSort

  public Sort getBooleanSort()

  Get the Boolean sort.

  Returns:

  Sort Boolean.

• getIntegerSort

  public Sort getIntegerSort()

  Get the integer sort.

  Returns:

  Sort Integer.

• getRealSort

  public Sort getRealSort()

  Get the real sort.

  Returns:

  Sort Real.

• getRegExpSort

  public Sort getRegExpSort()

  Get the regular expression sort.

  Returns:

  Sort RegExp.

• getRoundingModeSort

  public Sort getRoundingModeSort() throws CVC5ApiException

  Get the floating-point rounding mode sort.

  Returns:

  Sort RoundingMode.

  Throws:

  CVC5ApiException - on error

• getStringSort

  public Sort getStringSort()

  Get the string sort.

  Returns:

  Sort String.

• mkArraySort

  public Sort mkArraySort(Sort indexSort, Sort elemSort)

  Create an array sort.

  Parameters:

  indexSort - The array index sort.

  elemSort - The array element sort.

  Returns:

  The array sort.

• mkBitVectorSort

  public Sort mkBitVectorSort(int size) throws CVC5ApiException

  Create a bit-vector sort.

  Parameters:

  size - The bit-width of the bit-vector sort.

  Returns:

  The bit-vector sort.

  Throws:

  CVC5ApiException - on error

• mkFiniteFieldSort

  public Sort mkFiniteFieldSort(String size, int base) throws CVC5ApiException

  Create a finite field sort.

  Parameters:

  size - The size of the finite field sort.

  base - The base of the string representation.

  Returns:

  The finite field sort.

  Throws:

  CVC5ApiException - on error

• mkFloatingPointSort

  public Sort mkFloatingPointSort(int exp, int sig) throws CVC5ApiException

  Create a floating-point sort.

  Parameters:

  exp - The bit-width of the exponent of the floating-point sort.

  sig - The bit-width of the significand of the floating-point sort.

  Returns:

  The floating-point sort.

  Throws:

  CVC5ApiException - on error

• mkDatatypeSort

  public Sort mkDatatypeSort(DatatypeDecl dtypedecl) throws CVC5ApiException

  Create a datatype sort.

  Parameters:

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

  Returns:

  The datatype sort.

  Throws:

  CVC5ApiException - on error

• mkDatatypeSorts

  public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls) throws CVC5ApiException

  Create a vector of datatype sorts. The names of the datatype declarations must be distinct.

  Parameters:

  dtypedecls - The datatype declarations from which the sort is created.

  Returns:

  The datatype sorts.

  Throws:

  CVC5ApiException - on error

• mkFunctionSort

  public Sort mkFunctionSort(Sort domain, Sort codomain)

  Create function sort.

  Parameters:

  domain - The sort of the fuction argument.

  codomain - The sort of the function return value.

  Returns:

  The function sort.

• mkFunctionSort

  public Sort mkFunctionSort(Sort[] sorts, Sort codomain)

  Create function sort.

  Parameters:

  sorts - The sort of the function arguments.

  codomain - The sort of the function return value.

  Returns:

  The function sort.

• mkParamSort

  public Sort mkParamSort(String symbol)

  Create a sort parameter.

  Parameters:

  symbol - The name of the sort.

  Returns:

  The sort parameter.

  Note:

  This method is experimental and may change in future versions.

• mkParamSort

  public Sort mkParamSort()

  Create a sort parameter.

  Returns:

  The sort parameter.

  Note:

  This method is experimental and may change in future versions.

• mkSkolem

  public Term mkSkolem(SkolemId skolemId, Term[] indices)

  Create a skolem

  Parameters:

  skolemId - The id of the skolem.

  indices - The indices of the skolem.

  Returns:

  The skolem.

  Note:

  This method is experimental and may change in future versions.

• getNumIndicesForSkolemId

  public int getNumIndicesForSkolemId(SkolemId id)

  Get the number of indices for a given skolem id.

  Parameters:

  id - The skolem id.

  Returns:

  The number of indices for the given skolem id.

  Note:

  This method is experimental and may change in future versions.

• mkPredicateSort

  public Sort mkPredicateSort(Sort[] sorts)

  Create a predicate sort.

  Parameters:

  sorts - The list of sorts of the predicate.

  Returns:

  The predicate sort.

• mkRecordSort

  public Sort mkRecordSort(Pair<String,Sort>[] fields)

  Create a record sort

  Parameters:

  fields - The list of fields of the record.

  Returns:

  The record sort.

  Note:

  This method is experimental and may change in future versions.

• mkSetSort

  public Sort mkSetSort(Sort elemSort)

  Create a set sort.

  Parameters:

  elemSort - The sort of the set elements.

  Returns:

  The set sort.

• mkBagSort

  public Sort mkBagSort(Sort elemSort)

  Create a bag sort.

  Parameters:

  elemSort - The sort of the bag elements.

  Returns:

  The bag sort.

• mkSequenceSort

  public Sort mkSequenceSort(Sort elemSort)

  Create a sequence sort.

  Parameters:

  elemSort - The sort of the sequence elements.

  Returns:

  The sequence sort.

• mkAbstractSort

  public Sort mkAbstractSort(SortKind kind)

  Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified. The SortKind k must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, SortKind.ARRAY_SORT and SortKind.BITVECTOR_SORT can be passed as the SortKind k to this method, while SortKind.INTEGER_SORT and SortKind.STRING_SORT cannot.

  Parameters:

  kind - The kind of the abstract sort

  Returns:

  The abstract sort.

  Note:

  Providing the kind SortKind.ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, often denoted ?., Providing a kind k that has no indices and a fixed arity of argument sorts will return the sort of SortKind k whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is SortKind.ABSTRACT_SORT., This method is experimental and may change in future versions.

• mkUninterpretedSort

  public Sort mkUninterpretedSort(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(String symbol, int arity) throws CVC5ApiException

  Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.

  Parameters:

  symbol - The symbol of the sort.

  arity - The number of sort parameters of the sort.

  Returns:

  The unresolved sort.

  Throws:

  CVC5ApiException - on error

• mkUnresolvedDatatypeSort

  public Sort mkUnresolvedDatatypeSort(String symbol) throws CVC5ApiException

  Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive datatypes without sort parameters.

  Parameters:

  symbol - The symbol of the sort.

  Returns:

  The unresolved sort.

  Throws:

  CVC5ApiException - on error

• mkUninterpretedSortConstructorSort

  public Sort mkUninterpretedSortConstructorSort(int arity, String symbol) throws CVC5ApiException

  Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.

  Parameters:

  arity - The arity of the sort (must be > 0)

  symbol - The symbol of the sort.

  Returns:

  The sort constructor sort.

  Throws:

  CVC5ApiException - on error

• mkUninterpretedSortConstructorSort

  public Sort mkUninterpretedSortConstructorSort(int arity) throws CVC5ApiException

  Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.

  Parameters:

  arity - The arity of the sort (must be > 0)

  Returns:

  The sort constructor sort.

  Throws:

  CVC5ApiException - on error

• mkTupleSort

  public Sort mkTupleSort(Sort[] sorts)

  Create a tuple sort.

  Parameters:

  sorts - Of the elements of the tuple.

  Returns:

  The tuple sort.

• mkNullableSort

  public Sort mkNullableSort(Sort sort)

  Create a nullable sort.

  Parameters:

  sort - The sort of the element of the nullable.

  Returns:

  The nullable sort.

• mkTerm

  public Term mkTerm(Kind kind)

  Create 0-ary term of given kind.

  Parameters:

  kind - The kind of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Kind kind, Term child)

  Create a unary term of given kind.

  Parameters:

  kind - The kind of the term.

  child - The child of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Kind kind, Term child1, Term child2)

  Create binary term of given kind.

  Parameters:

  kind - The kind of the term.

  child1 - The first child of the term.

  child2 - The second child of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Kind kind, Term child1, Term child2, Term child3)

  Create ternary term of given kind.

  Parameters:

  kind - The kind of the term.

  child1 - The first child of the term.

  child2 - The second child of the term.

  child3 - The third child of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Kind kind, Term[] children)

  Create n-ary term of given kind.

  Parameters:

  kind - The kind of the term.

  children - The children of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Op op)

  Create nullary term of given kind from a given operator. Create operators with mkOp(Kind), mkOp(Kind, String), mkOp(Kind, int[]).

  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(Kind), mkOp(Kind, String), mkOp(Kind, int[]).

  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(Kind), mkOp(Kind, String), mkOp(Kind, int[]).

  Parameters:

  op - The operator.

  child1 - The first child of the term.

  child2 - The second child of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Op op, Term child1, Term child2, Term child3)

  Create ternary term of given kind from a given operator. Create operators with mkOp(Kind), mkOp(Kind, String), mkOp(Kind, int[]).

  Parameters:

  op - The operator.

  child1 - The first child of the term.

  child2 - The second child of the term.

  child3 - The third child of the term.

  Returns:

  The Term.

• mkTerm

  public Term mkTerm(Op op, Term[] children)

  Create n-ary term of given kind from a given operator. Create operators with mkOp(Kind), mkOp(Kind, String), mkOp(Kind, int[]).

  Parameters:

  op - The operator.

  children - The children of the term.

  Returns:

  The Term.

• mkTuple

  public Term mkTuple(Term[] terms)

  Create a tuple term. Terms are automatically converted if sorts are compatible.

  Parameters:

  terms - The elements in the tuple.

  Returns:

  The tuple Term.

• mkNullableSome

  public Term mkNullableSome(Term term)

  Create a nullable some term.

  Parameters:

  term - The element value.

  Returns:

  the Element value wrapped in some constructor.

• mkNullableVal

  public Term mkNullableVal(Term term)

  Create a selector for nullable term.

  Parameters:

  term - A nullable term.

  Returns:

  The element value of the nullable term.

• mkNullableIsNull

  public Term mkNullableIsNull(Term term)

  Create a null tester for a nullable term.

  Parameters:

  term - A nullable term.

  Returns:

  A tester whether term is null.

• mkNullableIsSome

  public Term mkNullableIsSome(Term term)

  Create a some tester for a nullable term.

  Parameters:

  term - A nullable term.

  Returns:

  A tester whether term is some.

• mkNullableNull

  public Term mkNullableNull(Sort sort)

  Create a constant representing a null value of the given sort.

  Parameters:

  sort - The sort of the Nullable element.

  Returns:

  The null constant.

• mkNullableLift

  public Term mkNullableLift(Kind kind, Term[] args)

  Create a term that lifts kind to nullable terms. Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)

  Parameters:

  kind - The lifted operator.

  args - The arguments of the lifted operator.

  Returns:

  A term of Kind NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.

• mkOp

  public Op mkOp(Kind kind)

  Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).

  Parameters:

  kind - The kind to wrap.

  Returns:

  The operator.

  Note:

  In this case, the Op simply wraps the Kind. The Kind can be used in mkTerm directly without creating an op first.

• mkOp

  public Op mkOp(Kind kind, String arg)

  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

  public Op mkOp(Kind kind, int arg) throws CVC5ApiException

  Create operator of kind:

  • DIVISIBLE
  • BITVECTOR_REPEAT
  • BITVECTOR_ZERO_EXTEND
  • BITVECTOR_SIGN_EXTEND
  • BITVECTOR_ROTATE_LEFT
  • BITVECTOR_ROTATE_RIGHT
  • INT_TO_BITVECTOR
  • FLOATINGPOINT_TO_UBV
  • FLOATINGPOINT_TO_UBV_TOTAL
  • FLOATINGPOINT_TO_SBV
  • FLOATINGPOINT_TO_SBV_TOTAL
  • TUPLE_UPDATE

  See enum Kind for a description of the parameters.

  Parameters:

  kind - The kind of the operator.

  arg - The unsigned int argument to this operator.

  Returns:

  The operator.

  Throws:

  CVC5ApiException - on error

• mkOp

  public Op mkOp(Kind kind, int arg1, int arg2) throws CVC5ApiException

  Create operator of Kind:

  • BITVECTOR_EXTRACT
  • FLOATINGPOINT_TO_FP_FROM_IEEE_BV
  • FLOATINGPOINT_TO_FP_FROM_FP
  • FLOATINGPOINT_TO_FP_FROM_REAL
  • FLOATINGPOINT_TO_FP_FROM_SBV
  • FLOATINGPOINT_TO_FP_FROM_UBV

  See enum Kind for a description of the parameters.

  Parameters:

  kind - The kind of the operator.

  arg1 - The first unsigned int argument to this operator.

  arg2 - The second unsigned int argument to this operator.

  Returns:

  The operator.

  Throws:

  CVC5ApiException - on error

• mkOp

  public Op mkOp(Kind kind, int[] args) throws CVC5ApiException

  Create operator of Kind:

  • TUPLE_PROJECT

  See enum Kind for a description of the parameters.

  Parameters:

  kind - The kind of the operator.

  args - The arguments (indices) of the operator.

  Returns:

  The operator.

  Throws:

  CVC5ApiException - on error

• mkTrue

  public Term mkTrue()

  Create a Boolean true constant.

  Returns:

  The true constant.

• mkFalse

  public Term mkFalse()

  Create a Boolean false constant.

  Returns:

  The false constant.

• mkBoolean

  public Term mkBoolean(boolean val)

  Create a Boolean constant.

  Parameters:

  val - The value of the constant.

  Returns:

  The Boolean constant.

• mkPi

  public Term mkPi()

  Create a constant representing the number Pi.

  Returns:

  A constant representing Pi.

• mkInteger

  public Term mkInteger(String s) throws CVC5ApiException

  Create an integer constant from a string.

  Parameters:

  s - The string representation of the constant, may represent an. integer (e.g., "123").

  Returns:

  A constant of sort Integer assuming s represents an integer).

  Throws:

  CVC5ApiException - on error

• mkInteger

  public Term mkInteger(long val)

  Create an integer constant from a C++ int.

  Parameters:

  val - The value of the constant.

  Returns:

  A constant of sort Integer.

• mkReal

  public Term mkReal(String s) throws CVC5ApiException

  Create a real constant from a string.

  Parameters:

  s - The string representation of the constant, may represent an. integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").

  Returns:

  A constant of sort Real.

  Throws:

  CVC5ApiException - on error

• mkReal

  public Term mkReal(long val)

  Create a real constant from an integer.

  Parameters:

  val - The value of the constant.

  Returns:

  A constant of sort Integer.

• mkReal

  public Term mkReal(long num, long den)

  Create a real constant from a rational.

  Parameters:

  num - The value of the numerator.

  den - The value of the denominator.

  Returns:

  A constant of sort Real.

• mkRegexpNone

  public Term mkRegexpNone()

  Create a regular expression none (re.none) term.

  Returns:

  The none term.

• mkRegexpAll

  public Term mkRegexpAll()

  Create a regular expression all (re.all) term.

  Returns:

  The all term.

• mkRegexpAllchar

  public Term mkRegexpAllchar()

  Create a regular expression allchar (re.allchar) term.

  Returns:

  The allchar term.

• mkEmptySet

  public Term mkEmptySet(Sort sort)

  Create a constant representing an empty set of the given sort.

  Parameters:

  sort - The sort of the set elements.

  Returns:

  The empty set constant.

• mkEmptyBag

  public Term mkEmptyBag(Sort sort)

  Create a constant representing an empty bag of the given sort.

  Parameters:

  sort - The sort of the bag elements.

  Returns:

  The empty bag constant.

• mkSepEmp

  public Term mkSepEmp()

  Create a separation logic empty term.

  Returns:

  The separation logic empty term.

  Note:

  This method is experimental and may change in future versions.

• mkSepNil

  public Term mkSepNil(Sort sort)

  Create a separation logic nil term.

  Parameters:

  sort - The sort of the nil term.

  Returns:

  The separation logic nil term.

  Note:

  This method is experimental and may change in future versions.

• mkString

  public Term mkString(String s)

  Create a String constant.

  Parameters:

  s - The string this constant represents.

  Returns:

  The String constant.

• mkString

  public Term mkString(String s, boolean useEscSequences)

  Create a String constant.

  Parameters:

  s - The string this constant represents.

  useEscSequences - Determines whether escape sequences in s should be converted to the corresponding unicode character.

  Returns:

  The String constant.

• mkString

  public Term mkString(int[] s) throws CVC5ApiException

  Create a String constant.

  Parameters:

  s - A list of unsigned (unicode) values this constant represents as string.

  Returns:

  The String constant.

  Throws:

  CVC5ApiException - on error

• mkEmptySequence

  public Term mkEmptySequence(Sort sort)

  Create an empty sequence of the given element sort.

  Parameters:

  sort - The element sort of the sequence.

  Returns:

  The empty sequence with given element sort.

• mkUniverseSet

  public Term mkUniverseSet(Sort sort)

  Create a universe set of the given sort.

  Parameters:

  sort - The sort of the set elements.

  Returns:

  The universe set constant.

• mkBitVector

  public Term mkBitVector(int size) throws CVC5ApiException

  Create a bit-vector constant of given size and value = 0.

  Parameters:

  size - The bit-width of the bit-vector sort.

  Returns:

  The bit-vector constant.

  Throws:

  CVC5ApiException - on error

• mkBitVector

  public Term mkBitVector(int size, long val) throws CVC5ApiException

  Create a bit-vector constant of given size and value.

  Parameters:

  size - The bit-width of the bit-vector sort.

  val - The value of the constant.

  Returns:

  The bit-vector constant.

  Throws:

  CVC5ApiException - on error

  Note:

  The given value must fit into a bit-vector of the given size.

• mkBitVector

  public Term mkBitVector(int size, String s, int base) throws CVC5ApiException

  Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

  Parameters:

  size - The bit-width of the constant.

  s - The string representation of the constant.

  base - The base of the string representation (2, 10, or 16)

  Returns:

  The bit-vector constant.

  Throws:

  CVC5ApiException - on error

  Note:

  The given value must fit into a bit-vector of the given size.

• mkFiniteFieldElem

  public Term mkFiniteFieldElem(String val, Sort sort, int base) throws CVC5ApiException

  Create a finite field constant in a given field and for a given value.

  Parameters:

  val - The value of the constant.

  sort - The sort of the finite field.

  base - The base of the string representation.

  Returns:

  The finite field constant.

  Throws:

  CVC5ApiException - on error

  Note:

  The given value must fit into a the given finite field.

• mkConstArray

  public Term mkConstArray(Sort sort, Term val)

  Create a constant array with the provided constant value stored at every index

  Parameters:

  sort - The sort of the constant array (must be an array sort)

  val - The constant value to store (must match the sort's element sort).

  Returns:

  The constant array term.

• mkFloatingPointPosInf

  public Term mkFloatingPointPosInf(int exp, int sig) throws CVC5ApiException

  Create a positive infinity floating-point constant (SMT-LIB: +oo).

  Parameters:

  exp - Number of bits in the exponent.

  sig - Number of bits in the significand.

  Returns:

  The floating-point constant.

  Throws:

  CVC5ApiException - on error

• mkFloatingPointNegInf

  public Term mkFloatingPointNegInf(int exp, int sig) throws CVC5ApiException

  Create a negative infinity floating-point constant (SMT-LIB: -oo).

  Parameters:

  exp - Number of bits in the exponent.

  sig - Number of bits in the significand.

  Returns:

  The floating-point constant.

  Throws:

  CVC5ApiException - on error

• mkFloatingPointNaN

  public Term mkFloatingPointNaN(int exp, int sig) throws CVC5ApiException

  Create a not-a-number floating-point constant (SMT-LIB: NaN).

  Parameters:

  exp - Number of bits in the exponent.

  sig - Number of bits in the significand.

  Returns:

  The floating-point constant.

  Throws:

  CVC5ApiException - on error

• mkFloatingPointPosZero

  public Term mkFloatingPointPosZero(int exp, int sig) throws CVC5ApiException

  Create a positive zero floating-point constant (SMT-LIB: +zero).

  Parameters:

  exp - Number of bits in the exponent.

  sig - Number of bits in the significand.

  Returns:

  The floating-point constant.

  Throws:

  CVC5ApiException - on error

• mkFloatingPointNegZero

  public Term mkFloatingPointNegZero(int exp, int sig) throws CVC5ApiException

  Create a negative zero floating-point constant (SMT-LIB: -zero).

  Parameters:

  exp - Number of bits in the exponent.

  sig - Number of bits in the significand.

  Returns:

  The floating-point constant.

  Throws:

  CVC5ApiException - on error

• mkRoundingMode

  public Term mkRoundingMode(RoundingMode rm)

  Create a rounding mode constant.

  Parameters:

  rm - The floating point rounding mode this constant represents.

  Returns:

  The rounding mode.

• mkFloatingPoint

  public Term mkFloatingPoint(int exp, int sig, Term val) throws CVC5ApiException

  Create a floating-point value from a bit-vector given in IEEE-754 format.

  Parameters:

  exp - Size of the exponent.

  sig - Size of the significand.

  val - Value of the floating-point constant as a bit-vector term.

  Returns:

  The floating-point value.

  Throws:

  CVC5ApiException - on error

• mkFloatingPoint

  public Term mkFloatingPoint(Term sign, Term exp, Term sig) throws CVC5ApiException

  Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).

  Parameters:

  sign - The sign bit.

  exp - The bit-vector representing the exponent.

  sig - The bit-vector representing the significand.

  Returns:

  The floating-point value.

  Throws:

  CVC5ApiException - on error

• mkCardinalityConstraint

  public Term mkCardinalityConstraint(Sort sort, int upperBound) throws CVC5ApiException

  Create a cardinality constraint for an uninterpreted sort.

  Parameters:

  sort - The sort the cardinality constraint is for.

  upperBound - The upper bound on the cardinality of the sort.

  Returns:

  The cardinality constraint.

  Throws:

  CVC5ApiException - on error

  Note:

  This method is experimental and may change in future versions.

• mkConst

  public Term mkConst(Sort sort, 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, 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(String name)

  Create a datatype constructor declaration.

  Parameters:

  name - The name of the datatype constructor.

  Returns:

  The DatatypeConstructorDecl.

• mkDatatypeDecl

  public DatatypeDecl mkDatatypeDecl(String name)

  Create a datatype declaration.

  Parameters:

  name - The name of the datatype.

  Returns:

  The DatatypeDecl.

• mkDatatypeDecl

  public DatatypeDecl mkDatatypeDecl(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(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(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.

• 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