TermManager

java.lang.Object
- io.github.cvc5.TermManager

public class TermManager
extends java.lang.Object

A cvc5 term manager.

Field Summary

Fields
Modifier and Type Field and Description

protected long pointer

Fields
Modifier and Type	Field and Description
`protected long`	`pointer`

Constructor Summary

Constructors
Constructor and Description

TermManager()
Create a term manager instance.

Constructors
Constructor and Description
`TermManager()` Create a term manager instance.

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`deletePointer()`
`protected void`	`deletePointer(long pointer)`
`boolean`	`equals(java.lang.Object o)`
`Sort`	`getBooleanSort()` Get the Boolean sort.
`Sort`	`getIntegerSort()` Get the integer sort.
`long`	`getIntegerSort(long pointer)`
`int`	`getNumIndicesForSkolemId(SkolemId id)` Get the number of indices for a given skolem id.
`long`	`getPointer()`
`Sort`	`getRealSort()` Get the real sort.
`Sort`	`getRegExpSort()` Get the regular expression sort.
`Sort`	`getRoundingModeSort()` Get the floating-point rounding mode sort.
`Statistics`	`getStatistics()` Get a snapshot of the current state of the statistic values of this term manager.
`Sort`	`getStringSort()` Get the string sort.
`Sort`	`mkAbstractSort(SortKind kind)` Create an abstract sort.
`Sort`	`mkArraySort(Sort indexSort, Sort elemSort)` Create an array sort.
`Sort`	`mkBagSort(Sort elemSort)` Create a bag sort.
`Term`	`mkBitVector(int size)` Create a bit-vector constant of given size and value = 0.
`Term`	`mkBitVector(int size, long val)` Create a bit-vector constant of given size and value.
`Term`	`mkBitVector(int size, java.lang.String s, int base)` Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
`Sort`	`mkBitVectorSort(int size)` Create a bit-vector sort.
`Term`	`mkBoolean(boolean val)` Create a Boolean constant.
`Term`	`mkCardinalityConstraint(Sort sort, int upperBound)` Create a cardinality constraint for an uninterpreted sort.
`Term`	`mkConst(Sort sort)` Create a free constant with a default symbol name.
`Term`	`mkConst(Sort sort, java.lang.String symbol)` Create a free constant.
`Term`	`mkConstArray(Sort sort, Term val)` Create a constant array with the provided constant value stored at every index
`DatatypeConstructorDecl`	`mkDatatypeConstructorDecl(java.lang.String name)` Create a datatype constructor declaration.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name)` Create a datatype declaration.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, boolean isCoDatatype)` Create a datatype declaration.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, Sort[] params)` Create a datatype declaration.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, Sort[] params, boolean isCoDatatype)` Create a datatype declaration.
`Sort`	`mkDatatypeSort(DatatypeDecl dtypedecl)` Create a datatype sort.
`Sort[]`	`mkDatatypeSorts(DatatypeDecl[] dtypedecls)` Create a vector of datatype sorts.
`Term`	`mkEmptyBag(Sort sort)` Create a constant representing an empty bag of the given sort.
`Term`	`mkEmptySequence(Sort sort)` Create an empty sequence of the given element sort.
`Term`	`mkEmptySet(Sort sort)` Create a constant representing an empty set of the given sort.
`Term`	`mkFalse()` Create a Boolean `false` constant.
`Term`	`mkFiniteFieldElem(java.lang.String val, Sort sort, int base)` Create a finite field constant in a given field and for a given value.
`Sort`	`mkFiniteFieldSort(java.lang.String size, int base)` Create a finite field sort.
`Term`	`mkFloatingPoint(int exp, int sig, Term val)` Create a floating-point value from a bit-vector given in IEEE-754 format.
`Term`	`mkFloatingPoint(Term sign, Term exp, Term sig)` Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
`Term`	`mkFloatingPointNaN(int exp, int sig)` Create a not-a-number floating-point constant (SMT-LIB: `NaN`).
`Term`	`mkFloatingPointNegInf(int exp, int sig)` Create a negative infinity floating-point constant (SMT-LIB: `-oo`).
`Term`	`mkFloatingPointNegZero(int exp, int sig)` Create a negative zero floating-point constant (SMT-LIB: `-zero`).
`Term`	`mkFloatingPointPosInf(int exp, int sig)` Create a positive infinity floating-point constant (SMT-LIB: `+oo`).
`Term`	`mkFloatingPointPosZero(int exp, int sig)` Create a positive zero floating-point constant (SMT-LIB: `+zero`).
`Sort`	`mkFloatingPointSort(int exp, int sig)` Create a floating-point sort.
`Sort`	`mkFunctionSort(Sort[] sorts, Sort codomain)` Create function sort.
`Sort`	`mkFunctionSort(Sort domain, Sort codomain)` Create function sort.
`Term`	`mkInteger(long val)` Create an integer constant from a C++ `int`.
`Term`	`mkInteger(java.lang.String s)` Create an integer constant from a string.
`Term`	`mkNullableIsNull(Term term)` Create a null tester for a nullable term.
`Term`	`mkNullableIsSome(Term term)` Create a some tester for a nullable term.
`Term`	`mkNullableLift(Kind kind, Term[] args)` Create a term that lifts kind to nullable terms.
`Term`	`mkNullableNull(Sort sort)` Create a constant representing a null value of the given sort.
`Term`	`mkNullableSome(Term term)` Create a nullable some term.
`Sort`	`mkNullableSort(Sort sort)` Create a nullable sort.
`Term`	`mkNullableVal(Term term)` Create a selector for nullable term.
`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`).
`Op`	`mkOp(Kind kind, int arg)` 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.
`Op`	`mkOp(Kind kind, int[] args)` Create operator of Kind: TUPLE_PROJECT See enum `Kind` for a description of the parameters.
`Op`	`mkOp(Kind kind, int arg1, int arg2)` 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.
`Op`	`mkOp(Kind kind, java.lang.String arg)` Create operator of kind: `Kind.DIVISIBLE` (to support arbitrary precision integers) See enum `Kind` for a description of the parameters.
`Sort`	`mkParamSort()` Create a sort parameter.
`Sort`	`mkParamSort(java.lang.String symbol)` Create a sort parameter.
`Term`	`mkPi()` Create a constant representing the number Pi.
`Sort`	`mkPredicateSort(Sort[] sorts)` Create a predicate sort.
`Term`	`mkReal(long val)` Create a real constant from an integer.
`Term`	`mkReal(long num, long den)` Create a real constant from a rational.
`Term`	`mkReal(java.lang.String s)` Create a real constant from a string.
`Sort`	`mkRecordSort(Pair<java.lang.String,Sort>[] fields)` Create a record sort
`Term`	`mkRegexpAll()` Create a regular expression all (`re.all`) term.
`Term`	`mkRegexpAllchar()` Create a regular expression allchar (`re.allchar`) term.
`Term`	`mkRegexpNone()` Create a regular expression none (`re.none`) term.
`Term`	`mkRoundingMode(RoundingMode rm)` Create a rounding mode constant.
`Term`	`mkSepEmp()` Create a separation logic empty term.
`Term`	`mkSepNil(Sort sort)` Create a separation logic nil term.
`Sort`	`mkSequenceSort(Sort elemSort)` Create a sequence sort.
`Sort`	`mkSetSort(Sort elemSort)` Create a set sort.
`Term`	`mkSkolem(SkolemId skolemId, Term[] indices)` Create a skolem
`Term`	`mkString(int[] s)` Create a String constant.
`Term`	`mkString(java.lang.String s)` Create a String constant.
`Term`	`mkString(java.lang.String s, boolean useEscSequences)` Create a String constant.
`Term`	`mkTerm(Kind kind)` Create 0-ary term of given kind.
`Term`	`mkTerm(Kind kind, Term child)` Create a unary term of given kind.
`Term`	`mkTerm(Kind kind, Term[] children)` Create n-ary term of given kind.
`Term`	`mkTerm(Kind kind, Term child1, Term child2)` Create binary term of given kind.
`Term`	`mkTerm(Kind kind, Term child1, Term child2, Term child3)` Create ternary term of given kind.
`Term`	`mkTerm(Op op)` Create nullary term of given kind from a given operator.
`Term`	`mkTerm(Op op, Term child)` Create unary term of given kind from a given operator.
`Term`	`mkTerm(Op op, Term[] children)` Create n-ary term of given kind from a given operator.
`Term`	`mkTerm(Op op, Term child1, Term child2)` Create binary term of given kind from a given operator.
`Term`	`mkTerm(Op op, Term child1, Term child2, Term child3)` Create ternary term of given kind from a given operator.
`Term`	`mkTrue()` Create a Boolean `true` constant.
`Term`	`mkTuple(Term[] terms)` Create a tuple term.
`Sort`	`mkTupleSort(Sort[] sorts)` Create a tuple sort.
`Sort`	`mkUninterpretedSort()` Create an uninterpreted sort.
`Sort`	`mkUninterpretedSort(java.lang.String symbol)` Create an uninterpreted sort.
`Sort`	`mkUninterpretedSortConstructorSort(int arity)` Create a sort constructor sort.
`Sort`	`mkUninterpretedSortConstructorSort(int arity, java.lang.String symbol)` Create a sort constructor sort.
`Term`	`mkUniverseSet(Sort sort)` Create a universe set of the given sort.
`Sort`	`mkUnresolvedDatatypeSort(java.lang.String symbol)` Create an unresolved datatype sort.
`Sort`	`mkUnresolvedDatatypeSort(java.lang.String symbol, int arity)` Create an unresolved datatype sort.
`Term`	`mkVar(Sort sort)` Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
`Term`	`mkVar(Sort sort, java.lang.String symbol)` Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
`java.lang.String`	`toString()`
`protected java.lang.String`	`toString(long pointer)`

Methods inherited from class java.lang.Object
clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - pointer
```
protected long pointer
```
- Constructor Detail
  - TermManager
```
public TermManager()
```
    Create a term manager instance.
- Method Detail
  - deletePointer
```
protected void deletePointer(long pointer)
```
  - toString
```
protected java.lang.String toString(long pointer)
```
  - equals
```
public boolean equals(java.lang.Object o)
```
    Overrides:
    
    equals in class java.lang.Object
  - getStatistics
```
public Statistics getStatistics()
```
    Get a snapshot of the current state of the statistic values of this term manager. Term manager statistics are independent from any solver instance. The returned object is completely decoupled from the term manager and will not change when the solver is used again.
    
    Returns:
    
    A snapshot of the current state of the statistic values.
  - getBooleanSort
```
public Sort getBooleanSort()
```
    Get the Boolean sort.
    
    Returns:
    
    Sort Boolean.
  - getIntegerSort
```
public Sort getIntegerSort()
```
    Get the integer sort.
    
    Returns:
    
    Sort Integer.
  - getIntegerSort
```
public long getIntegerSort(long pointer)
```
  - getRealSort
```
public Sort getRealSort()
```
    Get the real sort.
    
    Returns:
    
    Sort Real.
  - getRegExpSort
```
public Sort getRegExpSort()
```
    Get the regular expression sort.
    
    Returns:
    
    Sort RegExp.
  - getRoundingModeSort
```
public Sort getRoundingModeSort()
                         throws CVC5ApiException
```
    Get the floating-point rounding mode sort.
    
    Returns:
    
    Sort RoundingMode.
    
    Throws:
    
    CVC5ApiException - on error
  - getStringSort
```
public Sort getStringSort()
```
    Get the string sort.
    
    Returns:
    
    Sort String.
  - mkArraySort
```
public Sort mkArraySort(Sort indexSort,
                        Sort elemSort)
```
    Create an array sort.
    
    Parameters:
    
    indexSort - The array index sort.
    
    elemSort - The array element sort.
    
    Returns:
    
    The array sort.
  - mkBitVectorSort
```
public Sort mkBitVectorSort(int size)
                     throws CVC5ApiException
```
    Create a bit-vector sort.
    
    Parameters:
    
    size - The bit-width of the bit-vector sort.
    
    Returns:
    
    The bit-vector sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFiniteFieldSort
```
public Sort mkFiniteFieldSort(java.lang.String size,
                              int base)
                       throws CVC5ApiException
```
    Create a finite field sort.
    
    Parameters:
    
    size - The size of the finite field sort.
    
    base - The base of the string representation.
    
    Returns:
    
    The finite field sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointSort
```
public Sort mkFloatingPointSort(int exp,
                                int sig)
                         throws CVC5ApiException
```
    Create a floating-point sort.
    
    Parameters:
    
    exp - The bit-width of the exponent of the floating-point sort.
    
    sig - The bit-width of the significand of the floating-point sort.
    
    Returns:
    
    The floating-point sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkDatatypeSort
```
public Sort mkDatatypeSort(DatatypeDecl dtypedecl)
                    throws CVC5ApiException
```
    Create a datatype sort.
    
    Parameters:
    
    dtypedecl - The datatype declaration from which the sort is created.
    
    Returns:
    
    The datatype sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkDatatypeSorts
```
public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls)
                       throws CVC5ApiException
```
    Create a vector of datatype sorts. The names of the datatype declarations must be distinct.
    
    Parameters:
    
    dtypedecls - The datatype declarations from which the sort is created.
    
    Returns:
    
    The datatype sorts.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFunctionSort
```
public Sort mkFunctionSort(Sort domain,
                           Sort codomain)
```
    Create function sort.
    
    Parameters:
    
    domain - The sort of the fuction argument.
    
    codomain - The sort of the function return value.
    
    Returns:
    
    The function sort.
  - mkFunctionSort
```
public Sort mkFunctionSort(Sort[] sorts,
                           Sort codomain)
```
    Create function sort.
    
    Parameters:
    
    sorts - The sort of the function arguments.
    
    codomain - The sort of the function return value.
    
    Returns:
    
    The function sort.
  - mkParamSort
```
public Sort mkParamSort(java.lang.String symbol)
```
    Create a sort parameter.
    
    Parameters:
    
    symbol - The name of the sort.
    
    Returns:
    
    The sort parameter.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkParamSort
```
public Sort mkParamSort()
```
    Create a sort parameter.
    
    Returns:
    
    The sort parameter.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkSkolem
```
public Term mkSkolem(SkolemId skolemId,
                     Term[] indices)
```
    Create a skolem
    
    Parameters:
    
    skolemId - The id of the skolem.
    
    indices - The indices of the skolem.
    
    Returns:
    
    The skolem.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getNumIndicesForSkolemId
```
public int getNumIndicesForSkolemId(SkolemId id)
```
    Get the number of indices for a given skolem id.
    
    Parameters:
    
    id - The skolem id.
    
    Returns:
    
    The number of indices for the given skolem id.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkPredicateSort
```
public Sort mkPredicateSort(Sort[] sorts)
```
    Create a predicate sort.
    
    Parameters:
    
    sorts - The list of sorts of the predicate.
    
    Returns:
    
    The predicate sort.
  - mkRecordSort
```
public Sort mkRecordSort(Pair<java.lang.String,Sort>[] fields)
```
    Create a record sort
    
    Parameters:
    
    fields - The list of fields of the record.
    
    Returns:
    
    The record sort.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkSetSort
```
public Sort mkSetSort(Sort elemSort)
```
    Create a set sort.
    
    Parameters:
    
    elemSort - The sort of the set elements.
    
    Returns:
    
    The set sort.
  - mkBagSort
```
public Sort mkBagSort(Sort elemSort)
```
    Create a bag sort.
    
    Parameters:
    
    elemSort - The sort of the bag elements.
    
    Returns:
    
    The bag sort.
  - mkSequenceSort
```
public Sort mkSequenceSort(Sort elemSort)
```
    Create a sequence sort.
    
    Parameters:
    
    elemSort - The sort of the sequence elements.
    
    Returns:
    
    The sequence sort.
  - mkAbstractSort
```
public Sort mkAbstractSort(SortKind kind)
```
    Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified. The SortKind k must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, SortKind.ARRAY_SORT and SortKind.BITVECTOR_SORT can be passed as the SortKind k to this method, while SortKind.INTEGER_SORT and SortKind.STRING_SORT cannot.
    
    Parameters:
    
    kind - The kind of the abstract sort
    
    Returns:
    
    The abstract sort.
    
    Note:
    
    Providing the kind SortKind.ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, often denoted ?., Providing a kind k that has no indices and a fixed arity of argument sorts will return the sort of SortKind k whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is SortKind.ABSTRACT_SORT., This method is experimental and may change in future versions.
  - mkUninterpretedSort
```
public Sort mkUninterpretedSort(java.lang.String symbol)
```
    Create an uninterpreted sort.
    
    Parameters:
    
    symbol - The name of the sort.
    
    Returns:
    
    The uninterpreted sort.
  - mkUninterpretedSort
```
public Sort mkUninterpretedSort()
```
    Create an uninterpreted sort.
    
    Returns:
    
    The uninterpreted sort.
  - mkUnresolvedDatatypeSort
```
public Sort mkUnresolvedDatatypeSort(java.lang.String symbol,
                                     int arity)
                              throws CVC5ApiException
```
    Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.
    
    Parameters:
    
    symbol - The symbol of the sort.
    
    arity - The number of sort parameters of the sort.
    
    Returns:
    
    The unresolved sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUnresolvedDatatypeSort
```
public Sort mkUnresolvedDatatypeSort(java.lang.String symbol)
                              throws CVC5ApiException
```
    Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive datatypes without sort parameters.
    
    Parameters:
    
    symbol - The symbol of the sort.
    
    Returns:
    
    The unresolved sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUninterpretedSortConstructorSort
```
public Sort mkUninterpretedSortConstructorSort(int arity,
                                               java.lang.String symbol)
                                        throws CVC5ApiException
```
    Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
    
    Parameters:
    
    arity - The arity of the sort (must be > 0)
    
    symbol - The symbol of the sort.
    
    Returns:
    
    The sort constructor sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUninterpretedSortConstructorSort
```
public Sort mkUninterpretedSortConstructorSort(int arity)
                                        throws CVC5ApiException
```
    Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
    
    Parameters:
    
    arity - The arity of the sort (must be > 0)
    
    Returns:
    
    The sort constructor sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkTupleSort
```
public Sort mkTupleSort(Sort[] sorts)
```
    Create a tuple sort.
    
    Parameters:
    
    sorts - Of the elements of the tuple.
    
    Returns:
    
    The tuple sort.
  - mkNullableSort
```
public Sort mkNullableSort(Sort sort)
```
    Create a nullable sort.
    
    Parameters:
    
    sort - The sort of the element of the nullable.
    
    Returns:
    
    The nullable sort.
  - mkTerm
```
public Term mkTerm(Kind kind)
```
    Create 0-ary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
public Term mkTerm(Kind kind,
                   Term child)
```
    Create a unary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child - The child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
public Term mkTerm(Kind kind,
                   Term child1,
                   Term child2)
```
    Create binary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
public Term mkTerm(Kind kind,
                   Term child1,
                   Term child2,
                   Term child3)
```
    Create ternary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    child3 - The third child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
public Term mkTerm(Kind kind,
                   Term[] children)
```
    Create n-ary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    children - The children of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
public Term mkTerm(Op op)
```
    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,
               java.lang.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(java.lang.String s)
               throws CVC5ApiException
```
    Create an integer constant from a string.
    
    Parameters:
    
    s - The string representation of the constant, may represent an. integer (e.g., "123").
    
    Returns:
    
    A constant of sort Integer assuming s represents an integer).
    
    Throws:
    
    CVC5ApiException - on error
  - mkInteger
```
public Term mkInteger(long val)
```
    Create an integer constant from a C++ int.
    
    Parameters:
    
    val - The value of the constant.
    
    Returns:
    
    A constant of sort Integer.
  - mkReal
```
public Term mkReal(java.lang.String s)
            throws CVC5ApiException
```
    Create a real constant from a string.
    
    Parameters:
    
    s - The string representation of the constant, may represent an. integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
    
    Returns:
    
    A constant of sort Real.
    
    Throws:
    
    CVC5ApiException - on error
  - mkReal
```
public Term mkReal(long val)
```
    Create a real constant from an integer.
    
    Parameters:
    
    val - The value of the constant.
    
    Returns:
    
    A constant of sort Integer.
  - mkReal
```
public Term mkReal(long num,
                   long den)
```
    Create a real constant from a rational.
    
    Parameters:
    
    num - The value of the numerator.
    
    den - The value of the denominator.
    
    Returns:
    
    A constant of sort Real.
  - mkRegexpNone
```
public Term mkRegexpNone()
```
    Create a regular expression none (re.none) term.
    
    Returns:
    
    The none term.
  - mkRegexpAll
```
public Term mkRegexpAll()
```
    Create a regular expression all (re.all) term.
    
    Returns:
    
    The all term.
  - mkRegexpAllchar
```
public Term mkRegexpAllchar()
```
    Create a regular expression allchar (re.allchar) term.
    
    Returns:
    
    The allchar term.
  - mkEmptySet
```
public Term mkEmptySet(Sort sort)
```
    Create a constant representing an empty set of the given sort.
    
    Parameters:
    
    sort - The sort of the set elements.
    
    Returns:
    
    The empty set constant.
  - mkEmptyBag
```
public Term mkEmptyBag(Sort sort)
```
    Create a constant representing an empty bag of the given sort.
    
    Parameters:
    
    sort - The sort of the bag elements.
    
    Returns:
    
    The empty bag constant.
  - mkSepEmp
```
public Term mkSepEmp()
```
    Create a separation logic empty term.
    
    Returns:
    
    The separation logic empty term.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkSepNil
```
public Term mkSepNil(Sort sort)
```
    Create a separation logic nil term.
    
    Parameters:
    
    sort - The sort of the nil term.
    
    Returns:
    
    The separation logic nil term.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkString
```
public Term mkString(java.lang.String s)
```
    Create a String constant.
    
    Parameters:
    
    s - The string this constant represents.
    
    Returns:
    
    The String constant.
  - mkString
```
public Term mkString(java.lang.String s,
                     boolean useEscSequences)
```
    Create a String constant.
    
    Parameters:
    
    s - The string this constant represents.
    
    useEscSequences - Determines whether escape sequences in s should be converted to the corresponding unicode character.
    
    Returns:
    
    The String constant.
  - mkString
```
public Term mkString(int[] s)
              throws CVC5ApiException
```
    Create a String constant.
    
    Parameters:
    
    s - A list of unsigned (unicode) values this constant represents as string.
    
    Returns:
    
    The String constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkEmptySequence
```
public Term mkEmptySequence(Sort sort)
```
    Create an empty sequence of the given element sort.
    
    Parameters:
    
    sort - The element sort of the sequence.
    
    Returns:
    
    The empty sequence with given element sort.
  - mkUniverseSet
```
public Term mkUniverseSet(Sort sort)
```
    Create a universe set of the given sort.
    
    Parameters:
    
    sort - The sort of the set elements.
    
    Returns:
    
    The universe set constant.
  - mkBitVector
```
public Term mkBitVector(int size)
                 throws CVC5ApiException
```
    Create a bit-vector constant of given size and value = 0.
    
    Parameters:
    
    size - The bit-width of the bit-vector sort.
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkBitVector
```
public Term mkBitVector(int size,
                        long val)
                 throws CVC5ApiException
```
    Create a bit-vector constant of given size and value.
    
    Parameters:
    
    size - The bit-width of the bit-vector sort.
    
    val - The value of the constant.
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a bit-vector of the given size.
  - mkBitVector
```
public Term mkBitVector(int size,
                        java.lang.String s,
                        int base)
                 throws CVC5ApiException
```
    Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
    
    Parameters:
    
    size - The bit-width of the constant.
    
    s - The string representation of the constant.
    
    base - The base of the string representation (2, 10, or 16)
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a bit-vector of the given size.
  - mkFiniteFieldElem
```
public Term mkFiniteFieldElem(java.lang.String val,
                              Sort sort,
                              int base)
                       throws CVC5ApiException
```
    Create a finite field constant in a given field and for a given value.
    
    Parameters:
    
    val - The value of the constant.
    
    sort - The sort of the finite field.
    
    base - The base of the string representation.
    
    Returns:
    
    The finite field constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a the given finite field.
  - mkConstArray
```
public Term mkConstArray(Sort sort,
                         Term val)
```
    Create a constant array with the provided constant value stored at every index
    
    Parameters:
    
    sort - The sort of the constant array (must be an array sort)
    
    val - The constant value to store (must match the sort's element sort).
    
    Returns:
    
    The constant array term.
  - mkFloatingPointPosInf
```
public Term mkFloatingPointPosInf(int exp,
                                  int sig)
                           throws CVC5ApiException
```
    Create a positive infinity floating-point constant (SMT-LIB: +oo).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNegInf
```
public Term mkFloatingPointNegInf(int exp,
                                  int sig)
                           throws CVC5ApiException
```
    Create a negative infinity floating-point constant (SMT-LIB: -oo).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNaN
```
public Term mkFloatingPointNaN(int exp,
                               int sig)
                        throws CVC5ApiException
```
    Create a not-a-number floating-point constant (SMT-LIB: NaN).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointPosZero
```
public Term mkFloatingPointPosZero(int exp,
                                   int sig)
                            throws CVC5ApiException
```
    Create a positive zero floating-point constant (SMT-LIB: +zero).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNegZero
```
public Term mkFloatingPointNegZero(int exp,
                                   int sig)
                            throws CVC5ApiException
```
    Create a negative zero floating-point constant (SMT-LIB: -zero).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkRoundingMode
```
public Term mkRoundingMode(RoundingMode rm)
```
    Create a rounding mode constant.
    
    Parameters:
    
    rm - The floating point rounding mode this constant represents.
    
    Returns:
    
    The rounding mode.
  - mkFloatingPoint
```
public Term mkFloatingPoint(int exp,
                            int sig,
                            Term val)
                     throws CVC5ApiException
```
    Create a floating-point value from a bit-vector given in IEEE-754 format.
    
    Parameters:
    
    exp - Size of the exponent.
    
    sig - Size of the significand.
    
    val - Value of the floating-point constant as a bit-vector term.
    
    Returns:
    
    The floating-point value.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPoint
```
public Term mkFloatingPoint(Term sign,
                            Term exp,
                            Term sig)
                     throws CVC5ApiException
```
    Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
    
    Parameters:
    
    sign - The sign bit.
    
    exp - The bit-vector representing the exponent.
    
    sig - The bit-vector representing the significand.
    
    Returns:
    
    The floating-point value.
    
    Throws:
    
    CVC5ApiException - on error
  - mkCardinalityConstraint
```
public Term mkCardinalityConstraint(Sort sort,
                                    int upperBound)
                             throws CVC5ApiException
```
    Create a cardinality constraint for an uninterpreted sort.
    
    Parameters:
    
    sort - The sort the cardinality constraint is for.
    
    upperBound - The upper bound on the cardinality of the sort.
    
    Returns:
    
    The cardinality constraint.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkConst
```
public Term mkConst(Sort sort,
                    java.lang.String symbol)
```
    Create a free constant. SMT-LIB: ( declare-const <symbol> <sort> ) ( declare-fun <symbol> ( ) <sort> )
    
    Parameters:
    
    sort - The sort of the constant.
    
    symbol - The name of the constant.
    
    Returns:
    
    The first-order constant.
  - mkConst
```
public Term mkConst(Sort sort)
```
    Create a free constant with a default symbol name.
    
    Parameters:
    
    sort - The sort of the constant.
    
    Returns:
    
    The first-order constant.
  - mkVar
```
public Term mkVar(Sort sort)
```
    Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
    
    Parameters:
    
    sort - The sort of the variable.
    
    Returns:
    
    The variable.
  - mkVar
```
public Term mkVar(Sort sort,
                  java.lang.String symbol)
```
    Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
    
    Parameters:
    
    sort - The sort of the variable.
    
    symbol - The name of the variable.
    
    Returns:
    
    The variable.
  - mkDatatypeConstructorDecl
```
public DatatypeConstructorDecl mkDatatypeConstructorDecl(java.lang.String name)
```
    Create a datatype constructor declaration.
    
    Parameters:
    
    name - The name of the datatype constructor.
    
    Returns:
    
    The DatatypeConstructorDecl.
  - mkDatatypeDecl
```
public DatatypeDecl mkDatatypeDecl(java.lang.String name)
```
    Create a datatype declaration.
    
    Parameters:
    
    name - The name of the datatype.
    
    Returns:
    
    The DatatypeDecl.
  - mkDatatypeDecl
```
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                   boolean isCoDatatype)
```
    Create a datatype declaration.
    
    Parameters:
    
    name - The name of the datatype.
    
    isCoDatatype - True if a codatatype is to be constructed.
    
    Returns:
    
    The DatatypeDecl.
  - mkDatatypeDecl
```
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                   Sort[] params)
```
    Create a datatype declaration. Create sorts parameter with Solver.mkParamSort(String).
    
    Parameters:
    
    name - The name of the datatype.
    
    params - A list of sort parameters.
    
    Returns:
    
    The DatatypeDecl.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkDatatypeDecl
```
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                   Sort[] params,
                                   boolean isCoDatatype)
```
    Create a datatype declaration. Create sorts parameter with Solver.mkParamSort(String).
    
    Parameters:
    
    name - The name of the datatype.
    
    params - A list of sort parameters.
    
    isCoDatatype - True if a codatatype is to be constructed.
    
    Returns:
    
    The DatatypeDecl.
  - getPointer
```
public long getPointer()
```
  - deletePointer
```
public void deletePointer()
```
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object

Class TermManager

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

pointer

Constructor Detail

TermManager

Method Detail

deletePointer

toString

equals

getStatistics

getBooleanSort

getIntegerSort

getIntegerSort

getRealSort

getRegExpSort

getRoundingModeSort

getStringSort

mkArraySort

mkBitVectorSort

mkFiniteFieldSort

mkFloatingPointSort

mkDatatypeSort

mkDatatypeSorts

mkFunctionSort

mkFunctionSort

mkParamSort

mkParamSort

mkSkolem

getNumIndicesForSkolemId

mkPredicateSort

mkRecordSort

mkSetSort

mkBagSort

mkSequenceSort

mkAbstractSort

mkUninterpretedSort

mkUninterpretedSort

mkUnresolvedDatatypeSort

mkUnresolvedDatatypeSort

mkUninterpretedSortConstructorSort

mkUninterpretedSortConstructorSort

mkTupleSort

mkNullableSort

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTerm

mkTuple

mkNullableSome

mkNullableVal

mkNullableIsNull

mkNullableIsSome

mkNullableNull

mkNullableLift

mkOp

mkOp

mkOp

mkOp

mkOp

mkTrue

mkFalse

mkBoolean

mkPi

mkInteger

mkInteger

mkReal

mkReal

mkReal

mkRegexpNone

mkRegexpAll