Solver

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

public class Solver
extends java.lang.Object

A cvc5 solver.

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
`Solver()` Deprecated. This function is deprecated and replaced by `Solver(TermManager)`. It will be removed in a future release.
`Solver(TermManager d_tm)` Create solver instance.

Method Summary

All Methods Instance Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`void`	`addPlugin(AbstractPlugin p)` Add plugin to this solver.
`void`	`addSygusAssume(Term term)` Add a forumla to the set of Sygus assumptions.
`void`	`addSygusConstraint(Term term)` Add a forumla to the set of Sygus constraints.
`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.
`void`	`assertFormula(Term term)` Assert a formula.
`void`	`blockModel(BlockModelsMode mode)` Block the current model.
`void`	`blockModelValues(Term[] terms)` Block the current model values of (at least) the values in terms.
`Result`	`checkSat()` Check satisfiability.
`Result`	`checkSatAssuming(Term assumption)` Check satisfiability assuming the given formula.
`Result`	`checkSatAssuming(Term[] assumptions)` Check satisfiability assuming the given formulas.
`SynthResult`	`checkSynth()` Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
`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.
`Sort`	`declareDatatype(java.lang.String symbol, DatatypeConstructorDecl[] ctors)` Create datatype sort.
`Term`	`declareFun(java.lang.String symbol, Sort[] sorts, Sort sort)` Declare n-ary function symbol.
`Term`	`declareFun(java.lang.String symbol, Sort[] sorts, Sort sort, boolean fresh)` Declare n-ary function symbol.
`Term`	`declareOracleFun(java.lang.String symbol, Sort[] sorts, Sort sort, IOracle oracle)` Declare an oracle function with reference to an implementation.
`Term`	`declarePool(java.lang.String symbol, Sort sort, Term[] initValue)` Declare a symbolic pool of terms with the given initial value.
`void`	`declareSepHeap(Sort locSort, Sort dataSort)` When using separation logic, this sets the location sort and the datatype sort to the given ones.
`Sort`	`declareSort(java.lang.String symbol, int arity)` Declare uninterpreted sort.
`Sort`	`declareSort(java.lang.String symbol, int arity, boolean fresh)` Declare uninterpreted sort.
`Term`	`declareSygusVar(java.lang.String symbol, Sort sort)` Append `symbol` to the current list of universal variables.
`Term`	`defineFun(java.lang.String symbol, Term[] boundVars, Sort sort, Term term)` Define n-ary function in the current context.
`Term`	`defineFun(java.lang.String symbol, Term[] boundVars, Sort sort, Term term, boolean global)` Define n-ary function.
`Term`	`defineFunRec(java.lang.String symbol, Term[] boundVars, Sort sort, Term term)` Define recursive function in the current context.
`Term`	`defineFunRec(java.lang.String symbol, Term[] boundVars, Sort sort, Term term, boolean global)` Define recursive function.
`Term`	`defineFunRec(Term fun, Term[] boundVars, Term term)` Define recursive function in the current context.
`Term`	`defineFunRec(Term fun, Term[] boundVars, Term term, boolean global)` Define recursive function.
`void`	`defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms)` Define recursive functions in the current context.
`void`	`defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms, boolean global)` Define recursive functions.
`void`	`deletePointer()`
`protected void`	`deletePointer(long pointer)`
`boolean`	`equals(java.lang.Object s)`
`Term`	`findSynth(FindSynthTarget fst)` Find a target term of interest using sygus enumeration, with no provided grammar.
`Term`	`findSynth(FindSynthTarget fst, Grammar grammar)` Find a target term of interest using sygus enumeration with a provided grammar.
`Term`	`findSynthNext()` Try to find a next target term of interest using sygus enumeration.
`Term`	`getAbduct(Term conj)` Get an abduct.
`Term`	`getAbduct(Term conj, Grammar grammar)` Get an abduct.
`Term`	`getAbductNext()` Get the next abduct.
`Term[]`	`getAssertions()` Get the list of asserted formulas.
`Sort`	`getBooleanSort()` Deprecated. This function is deprecated and replaced by `TermManager.getBooleanSort()`. It will be removed in a future release.
`java.util.Map<Term,Term>`	`getDifficulty()` Get a difficulty estimate for an asserted formula.
`java.lang.String`	`getInfo(java.lang.String flag)` Get info from the solver.
`java.lang.String`	`getInstantiations()` Get a string that contains information about all instantiations made by the quantifiers module.
`Sort`	`getIntegerSort()` Deprecated. This function is deprecated and replaced by `TermManager.getIntegerSort()`. It will be removed in a future release.
`Term`	`getInterpolant(Term conj)` Get an interpolant.
`Term`	`getInterpolant(Term conj, Grammar grammar)` Get an interpolant.
`Term`	`getInterpolantNext()` Get the next interpolant.
`Term[]`	`getLearnedLiterals()` Get a list of input literals that are entailed by the current set of assertions.
`Term[]`	`getLearnedLiterals(LearnedLitType type)` Get a list of literals that are entailed by the current set of assertions.
`java.lang.String`	`getLogic()` Get the logic set the solver.
`java.lang.String`	`getModel(Sort[] sorts, Term[] vars)` Get the model SMT-LIB: `( get-model )` Requires to enable option `produce-models`.
`Term[]`	`getModelDomainElements(Sort s)` Get the domain elements of uninterpreted sort s in the current model.
`java.lang.String`	`getOption(java.lang.String option)` Get the value of a given option.
`OptionInfo`	`getOptionInfo(java.lang.String option)` Get some information about the given option.
`java.lang.String[]`	`getOptionNames()` Get all option names that can be used with `setOption(String, String)`, `getOption(String)` and `getOptionInfo(String)`.
`long`	`getPointer()`
`Proof[]`	`getProof()` Get refutation proof for the most recent call to checkSat.
`Proof[]`	`getProof(ProofComponent c)` Get a proof associated with the most recent call to checkSat.
`Term`	`getQuantifierElimination(Term q)` Do quantifier elimination.
`Term`	`getQuantifierEliminationDisjunct(Term q)` Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.
`Sort`	`getRealSort()` Deprecated. This function is deprecated and replaced by `TermManager.getRealSort()`. It will be removed in a future release.
`Sort`	`getRegExpSort()` Deprecated. This function is deprecated and replaced by `TermManager.getRegExpSort()`. It will be removed in a future release.
`Sort`	`getRoundingModeSort()` Deprecated. This function is deprecated and replaced by `TermManager.getRoundingModeSort()`. It will be removed in a future release.
`Statistics`	`getStatistics()` Get a snapshot of the current state of the statistic values of this solver.
`Sort`	`getStringSort()` Deprecated. This function is deprecated and replaced by `TermManager.getStringSort()`. It will be removed in a future release.
`Term[]`	`getSygusAssumptions()` Get the list of sygus assumptions.
`Term[]`	`getSygusConstraints()` Get the list of sygus constraints.
`Term`	`getSynthSolution(Term term)` Get the synthesis solution of the given term.
`Term[]`	`getSynthSolutions(Term[] terms)` Get the synthesis solutions of the given terms.
`TermManager`	`getTermManager()` Get the associated term manager instance
`Pair<Result,Term[]>`	`getTimeoutCore()` Get a timeout core, which computes a subset of the current assertions that cause a timeout.
`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.
`Term[]`	`getUnsatAssumptions()` Get the set of unsat ("failed") assumptions.
`Term[]`	`getUnsatCore()` Get the unsatisfiable core.
`Term[]`	`getUnsatCoreLemmas()` Get the lemmas used to derive unsatisfiability.
`Term`	`getValue(Term term)` Get the value of the given term in the current model.
`Term[]`	`getValue(Term[] terms)` Get the values of the given terms in the current model.
`Term`	`getValueSepHeap()` When using separation logic, obtain the term for the heap.
`Term`	`getValueSepNil()` When using separation logic, obtain the term for nil.
`java.lang.String`	`getVersion()` Get a string representation of the version of this solver.
`boolean`	`isLogicSet()` Is logic set? Returns whether we called setLogic yet for this solver.
`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.
`Sort`	`mkAbstractSort(SortKind kind)` Deprecated. This function is deprecated and replaced by `TermManager.mkAbstractSort(SortKind)`. It will be removed in a future release.
`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.
`Sort`	`mkBagSort(Sort elemSort)` Deprecated. This function is deprecated and replaced by `TermManager.mkBagSort(Sort)`. It will be removed in a future release.
`Term`	`mkBitVector(int size)` Deprecated. This function is deprecated and replaced by `TermManager.mkBitVector(int)`. It will be removed in a future release.
`Term`	`mkBitVector(int size, long val)` Deprecated. This function is deprecated and replaced by `TermManager.mkBitVector(int, long)`. It will be removed in a future release.
`Term`	`mkBitVector(int size, java.lang.String s, int base)` Deprecated. This function is deprecated and replaced by `TermManager.mkBitVector(int, String, int)`. It will be removed in a future release.
`Sort`	`mkBitVectorSort(int size)` Deprecated. This function is deprecated and replaced by `TermManager.mkBitVectorSort(int)`. It will be removed in a future release.
`Term`	`mkBoolean(boolean val)` Deprecated. This function is deprecated and replaced by `TermManager.mkBoolean(boolean)`. It will be removed in a future release.
`Term`	`mkCardinalityConstraint(Sort sort, int upperBound)` Deprecated. This function is deprecated and replaced by `TermManager.mkCardinalityConstraint(Sort, int)`. It will be removed in a future release.
`Term`	`mkConst(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkConst(Sort)`. It will be removed in a future release.
`Term`	`mkConst(Sort sort, java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkConst(Sort, String)`. It will be removed in a future release.
`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.
`DatatypeConstructorDecl`	`mkDatatypeConstructorDecl(java.lang.String name)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeConstructorDecl(String)`. It will be removed in a future release.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeDecl(String)`. It will be removed in a future release.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, boolean isCoDatatype)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeDecl(String, boolean)`. It will be removed in a future release.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, Sort[] params)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeDecl(String, Sort[])`. It will be removed in a future release.
`DatatypeDecl`	`mkDatatypeDecl(java.lang.String name, Sort[] params, boolean isCoDatatype)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeDecl(String, Sort[])`. It will be removed in a future release.
`Sort`	`mkDatatypeSort(DatatypeDecl dtypedecl)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeSort(DatatypeDecl)`. It will be removed in a future release.
`Sort[]`	`mkDatatypeSorts(DatatypeDecl[] dtypedecls)` Deprecated. This function is deprecated and replaced by `TermManager.mkDatatypeSorts(DatatypeDecl[])`. It will be removed in a future release.
`Term`	`mkEmptyBag(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkEmptyBag(Sort)`. It will be removed in a future release.
`Term`	`mkEmptySequence(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkEmptySequence(Sort)`. It will be removed in a future release.
`Term`	`mkEmptySet(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkEmptySet(Sort)`. It will be removed in a future release.
`Term`	`mkFalse()` Deprecated. This function is deprecated and replaced by `TermManager.mkFalse()`. It will be removed in a future release.
`Term`	`mkFiniteFieldElem(java.lang.String val, Sort sort, int base)` Deprecated. This function is deprecated and replaced by `TermManager.mkFiniteFieldElem(String, Sort, int)`. It will be removed in a future release.
`Sort`	`mkFiniteFieldSort(java.lang.String size, int base)` Deprecated. This function is deprecated and replaced by `TermManager.mkFiniteFieldSort(String, int)`. It will be removed in a future release.
`Term`	`mkFloatingPoint(int exp, int sig, Term val)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPoint(int, int, Term)`. It will be removed in a future release.
`Term`	`mkFloatingPoint(Term sign, Term exp, Term sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPoint(Term, Term, Term)`. It will be removed in a future release.
`Term`	`mkFloatingPointNaN(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointNaN(int, int)`. It will be removed in a future release.
`Term`	`mkFloatingPointNegInf(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointNegInf(int, int)`. It will be removed in a future release.
`Term`	`mkFloatingPointNegZero(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointNegZero(int, int)`. It will be removed in a future release.
`Term`	`mkFloatingPointPosInf(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointPosInf(int, int)`. It will be removed in a future release.
`Term`	`mkFloatingPointPosZero(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointPosZero(int, int)`. It will be removed in a future release.
`Sort`	`mkFloatingPointSort(int exp, int sig)` Deprecated. This function is deprecated and replaced by `TermManager.mkFloatingPointSort(int, int)`. It will be removed in a future release.
`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.
`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.
`Grammar`	`mkGrammar(Term[] boundVars, Term[] ntSymbols)` Create a Sygus grammar.
`Term`	`mkInteger(long val)` Deprecated. This function is deprecated and replaced by `TermManager.mkInteger(long)`. It will be removed in a future release.
`Term`	`mkInteger(java.lang.String s)` Deprecated. This function is deprecated and replaced by `TermManager.mkInteger(String)`. It will be removed in a future release.
`Term`	`mkNullableIsNull(Term term)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableIsNull(Term)`. It will be removed in a future release.
`Term`	`mkNullableIsSome(Term term)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableIsSome(Term)`. It will be removed in a future release.
`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.
`Term`	`mkNullableNull(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableNull(Sort)`. It will be removed in a future release.
`Term`	`mkNullableSome(Term term)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableSome(Term)`. It will be removed in a future release.
`Sort`	`mkNullableSort(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableSort(Sort)`. It will be removed in a future release.
`Term`	`mkNullableVal(Term term)` Deprecated. This function is deprecated and replaced by `TermManager.mkNullableVal(Term)`. It will be removed in a future release.
`Op`	`mkOp(Kind kind)` Deprecated. This function is deprecated and replaced by `TermManager.mkOp(Kind)`. It will be removed in a future release.
`Op`	`mkOp(Kind kind, int arg)` Deprecated. This function is deprecated and replaced by `TermManager.mkOp(Kind, int)`. It will be removed in a future release.
`Op`	`mkOp(Kind kind, int[] args)` Deprecated. This function is deprecated and replaced by `TermManager.mkOp(Kind, int[])`. It will be removed in a future release.
`Op`	`mkOp(Kind kind, int arg1, int arg2)` Deprecated. This function is deprecated and replaced by `TermManager.mkOp(Kind, int, int)`. It will be removed in a future release.
`Op`	`mkOp(Kind kind, java.lang.String arg)` Deprecated. This function is deprecated and replaced by `TermManager.mkOp(Kind, String)`. It will be removed in a future release.
`Sort`	`mkParamSort()` Deprecated. This function is deprecated and replaced by `TermManager.mkParamSort()`. It will be removed in a future release.
`Sort`	`mkParamSort(java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkParamSort(String)`. It will be removed in a future release.
`Term`	`mkPi()` Deprecated. This function is deprecated and replaced by `TermManager.mkPi()`. It will be removed in a future release.
`Sort`	`mkPredicateSort(Sort[] sorts)` Deprecated. This function is deprecated and replaced by `TermManager.mkPredicateSort(Sort[])`. It will be removed in a future release.
`Term`	`mkReal(long val)` Deprecated. This function is deprecated and replaced by `TermManager.mkReal(long)`. It will be removed in a future release.
`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.
`Term`	`mkReal(java.lang.String s)` Deprecated. This function is deprecated and replaced by `TermManager.mkReal(String)`. It will be removed in a future release.
`Sort`	`mkRecordSort(Pair<java.lang.String,Sort>[] fields)` Deprecated. This function is deprecated and replaced by `TermManager.mkRecordSort(Pair[])`. It will be removed in a future release.
`Term`	`mkRegexpAll()` Deprecated. This function is deprecated and replaced by `TermManager.mkRegexpAll()`. It will be removed in a future release.
`Term`	`mkRegexpAllchar()` Deprecated. This function is deprecated and replaced by `TermManager.mkRegexpAllchar()`. It will be removed in a future release.
`Term`	`mkRegexpNone()` Deprecated. This function is deprecated and replaced by `TermManager.mkRegexpNone()`. It will be removed in a future release.
`Term`	`mkRoundingMode(RoundingMode rm)` Deprecated. This function is deprecated and replaced by `TermManager.mkRoundingMode(RoundingMode)`. It will be removed in a future release.
`Term`	`mkSepEmp()` Deprecated. This function is deprecated and replaced by `TermManager.mkSepEmp()`. It will be removed in a future release.
`Term`	`mkSepNil(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkSepNil(Sort)`. It will be removed in a future release.
`Sort`	`mkSequenceSort(Sort elemSort)` Deprecated. This function is deprecated and replaced by `TermManager.mkSequenceSort(Sort)`. It will be removed in a future release.
`Sort`	`mkSetSort(Sort elemSort)` Deprecated. This function is deprecated and replaced by `TermManager.mkSetSort(Sort)`. It will be removed in a future release.
`Term`	`mkString(int[] s)` Deprecated. This function is deprecated and replaced by `TermManager.mkString(int[])`. It will be removed in a future release.
`Term`	`mkString(java.lang.String s)` Deprecated. This function is deprecated and replaced by `TermManager.mkString(String)`. It will be removed in a future release.
`Term`	`mkString(java.lang.String s, boolean useEscSequences)` Deprecated. This function is deprecated and replaced by `TermManager.mkString(String, boolean)`. It will be removed in a future release.
`Term`	`mkTerm(Kind kind)` Deprecated. This function is deprecated and replaced by `TermManager.mkTerm(Kind)`. It will be removed in a future release.
`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.
`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.
`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.
`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.
`Term`	`mkTerm(Op op)` Deprecated. This function is deprecated and replaced by `TermManager.mkTerm(Op)`. It will be removed in a future release.
`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.
`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.
`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.
`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.
`Term`	`mkTrue()` Deprecated. This function is deprecated and replaced by `TermManager.mkTrue()`. It will be removed in a future release.
`Term`	`mkTuple(Term[] terms)` Deprecated. This function is deprecated and replaced by `TermManager.mkTuple(Term[])`. It will be removed in a future release.
`Sort`	`mkTupleSort(Sort[] sorts)` Deprecated. This function is deprecated and replaced by `TermManager.mkTupleSort(Sort[])`. It will be removed in a future release.
`Sort`	`mkUninterpretedSort()` Deprecated. This function is deprecated and replaced by `TermManager.mkUninterpretedSort()`. It will be removed in a future release.
`Sort`	`mkUninterpretedSort(java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkUninterpretedSort(String)`. It will be removed in a future release.
`Sort`	`mkUninterpretedSortConstructorSort(int arity)` Deprecated. This function is deprecated and replaced by `TermManager.mkUninterpretedSortConstructorSort(int)`. It will be removed in a future release.
`Sort`	`mkUninterpretedSortConstructorSort(int arity, java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkUninterpretedSortConstructorSort(int, String)`. It will be removed in a future release.
`Term`	`mkUniverseSet(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkUniverseSet(Sort)`. It will be removed in a future release.
`Sort`	`mkUnresolvedDatatypeSort(java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkUnresolvedDatatypeSort(String)`. It will be removed in a future release.
`Sort`	`mkUnresolvedDatatypeSort(java.lang.String symbol, int arity)` Deprecated. This function is deprecated and replaced by `TermManager.mkUnresolvedDatatypeSort(String, int)`. It will be removed in a future release.
`Term`	`mkVar(Sort sort)` Deprecated. This function is deprecated and replaced by `TermManager.mkVar(Sort)`. It will be removed in a future release.
`Term`	`mkVar(Sort sort, java.lang.String symbol)` Deprecated. This function is deprecated and replaced by `TermManager.mkVar(Sort, String)`. It will be removed in a future release.
`void`	`pop()` Pop a level from the assertion stack.
`void`	`pop(int nscopes)` Pop (a) level(s) from the assertion stack.
`java.lang.String`	`proofToString(Proof proof)` Prints a proof into a string with a slected proof format mode.
`java.lang.String`	`proofToString(Proof proof, ProofFormat format)` Prints a proof into a string with a slected proof format mode.
`java.lang.String`	`proofToString(Proof proof, ProofFormat format, java.util.Map assertionNames)` Prints a proof into a string with a slected proof format mode.
`void`	`push()` Push a level to the assertion stack.
`void`	`push(int nscopes)` Push (a) level(s) to the assertion stack.
`void`	`resetAssertions()` Remove all assertions.
`void`	`setInfo(java.lang.String keyword, java.lang.String value)` Set info.
`void`	`setLogic(java.lang.String logic)` Set logic.
`void`	`setOption(java.lang.String option, java.lang.String value)` Set option.
`Term`	`simplify(Term t)` Simplify a term or formula based on rewriting.
`Term`	`simplify(Term t, boolean applySubs)` Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.
`Term`	`synthFun(java.lang.String symbol, Term[] boundVars, Sort sort)` Synthesize n-ary function.
`Term`	`synthFun(java.lang.String symbol, Term[] boundVars, Sort sort, Grammar grammar)` Synthesize n-ary function following specified syntactic constraints.
`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
  - Solver
```
@Deprecated
public Solver()
```
    Deprecated. This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
    
    Create solver instance.
  - Solver
```
public Solver(TermManager d_tm)
```
    Create solver instance.
    
    Parameters:
    
    d_tm - The associated term manager.
- Method Detail
  - deletePointer
```
protected void deletePointer(long pointer)
```
  - toString
```
protected java.lang.String toString(long pointer)
```
  - equals
```
public boolean equals(java.lang.Object s)
```
    Overrides:
    
    equals in class java.lang.Object
  - getTermManager
```
public TermManager getTermManager()
```
    Get the associated term manager instance
    
    Returns:
    
    The term manager.
  - getBooleanSort
```
@Deprecated
public Sort getBooleanSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.
    
    Get the Boolean sort.
    
    Returns:
    
    Sort Boolean.
  - getIntegerSort
```
@Deprecated
public Sort getIntegerSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.
    
    Get the integer sort.
    
    Returns:
    
    Sort Integer.
  - getRealSort
```
@Deprecated
public Sort getRealSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.
    
    Get the real sort.
    
    Returns:
    
    Sort Real.
  - getRegExpSort
```
@Deprecated
public Sort getRegExpSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.
    
    Get the regular expression sort.
    
    Returns:
    
    Sort RegExp.
  - 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(java.lang.String size,
                                          int base)
                                   throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.
    
    Create a finite field sort.
    
    Parameters:
    
    size - The size of the finite field sort.
    
    base - The base of the string representation.
    
    Returns:
    
    The finite field sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointSort
```
@Deprecated
public Sort mkFloatingPointSort(int exp,
                                            int sig)
                                     throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.
    
    Create a floating-point sort.
    
    Parameters:
    
    exp - The bit-width of the exponent of the floating-point sort.
    
    sig - The bit-width of the significand of the floating-point sort.
    
    Returns:
    
    The floating-point sort.
    
    Throws:
    
    CVC5ApiException - on error
  - 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(java.lang.String symbol)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.
    
    Create a sort parameter.
    
    Parameters:
    
    symbol - The name of the sort.
    
    Returns:
    
    The sort parameter.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkParamSort
```
@Deprecated
public Sort mkParamSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkParamSort(). It will be removed in a future release.
    
    Create a sort parameter.
    
    Returns:
    
    The sort parameter.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkPredicateSort
```
@Deprecated
public Sort mkPredicateSort(Sort[] sorts)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.
    
    Create a predicate sort.
    
    Parameters:
    
    sorts - The list of sorts of the predicate.
    
    Returns:
    
    The predicate sort.
  - mkRecordSort
```
@Deprecated
public Sort mkRecordSort(Pair<java.lang.String,Sort>[] fields)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.
    
    Create a record sort
    
    Parameters:
    
    fields - The list of fields of the record.
    
    Returns:
    
    The record sort.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkSetSort
```
@Deprecated
public Sort mkSetSort(Sort elemSort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.
    
    Create a set sort.
    
    Parameters:
    
    elemSort - The sort of the set elements.
    
    Returns:
    
    The set sort.
  - mkBagSort
```
@Deprecated
public Sort mkBagSort(Sort elemSort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.
    
    Create a bag sort.
    
    Parameters:
    
    elemSort - The sort of the bag elements.
    
    Returns:
    
    The bag sort.
  - mkSequenceSort
```
@Deprecated
public Sort mkSequenceSort(Sort elemSort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.
    
    Create a sequence sort.
    
    Parameters:
    
    elemSort - The sort of the sequence elements.
    
    Returns:
    
    The sequence sort.
  - mkAbstractSort
```
@Deprecated
public Sort mkAbstractSort(SortKind kind)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.
    
    Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified. The SortKind k must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, SortKind.ARRAY_SORT and SortKind.BITVECTOR_SORT can be passed as the SortKind k to this method, while SortKind.INTEGER_SORT and SortKind.STRING_SORT cannot.
    
    Parameters:
    
    kind - The kind of the abstract sort
    
    Returns:
    
    The abstract sort.
    
    Note:
    
    Providing the kind SortKind.ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, often denoted ?., Providing a kind k that has no indices and a fixed arity of argument sorts will return the sort of SortKind k whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is SortKind.ABSTRACT_SORT., This method is experimental and may change in future versions.
  - mkUninterpretedSort
```
@Deprecated
public Sort mkUninterpretedSort(java.lang.String symbol)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.
    
    Create an uninterpreted sort.
    
    Parameters:
    
    symbol - The name of the sort.
    
    Returns:
    
    The uninterpreted sort.
  - mkUninterpretedSort
```
@Deprecated
public Sort mkUninterpretedSort()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUninterpretedSort(). It will be removed in a future release.
    
    Create an uninterpreted sort.
    
    Returns:
    
    The uninterpreted sort.
  - mkUnresolvedDatatypeSort
```
@Deprecated
public Sort mkUnresolvedDatatypeSort(java.lang.String symbol,
                                                 int arity)
                                          throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.
    
    Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.
    
    Parameters:
    
    symbol - The symbol of the sort.
    
    arity - The number of sort parameters of the sort.
    
    Returns:
    
    The unresolved sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUnresolvedDatatypeSort
```
@Deprecated
public Sort mkUnresolvedDatatypeSort(java.lang.String symbol)
                                          throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). It will be removed in a future release.
    
    Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive datatypes without sort parameters.
    
    Parameters:
    
    symbol - The symbol of the sort.
    
    Returns:
    
    The unresolved sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUninterpretedSortConstructorSort
```
@Deprecated
public Sort mkUninterpretedSortConstructorSort(int arity,
                                                           java.lang.String symbol)
                                                    throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.
    
    Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
    
    Parameters:
    
    arity - The arity of the sort (must be > 0)
    
    symbol - The symbol of the sort.
    
    Returns:
    
    The sort constructor sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkUninterpretedSortConstructorSort
```
@Deprecated
public Sort mkUninterpretedSortConstructorSort(int arity)
                                                    throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). It will be removed in a future release.
    
    Create a sort constructor sort. An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
    
    Parameters:
    
    arity - The arity of the sort (must be > 0)
    
    Returns:
    
    The sort constructor sort.
    
    Throws:
    
    CVC5ApiException - on error
  - mkTupleSort
```
@Deprecated
public Sort mkTupleSort(Sort[] sorts)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.
    
    Create a tuple sort.
    
    Parameters:
    
    sorts - Of the elements of the tuple.
    
    Returns:
    
    The tuple sort.
  - mkNullableSort
```
@Deprecated
public Sort mkNullableSort(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.
    
    Create a nullable sort.
    
    Parameters:
    
    sort - The sort of the element of the nullable.
    
    Returns:
    
    The nullable sort.
  - mkTerm
```
@Deprecated
public Term mkTerm(Kind kind)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.
    
    Create 0-ary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Kind kind,
                               Term child)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.
    
    Create a unary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child - The child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Kind kind,
                               Term child1,
                               Term child2)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.
    
    Create binary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Kind kind,
                               Term child1,
                               Term child2,
                               Term child3)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.
    
    Create ternary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    child3 - The third child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Kind kind,
                               Term[] children)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.
    
    Create n-ary term of given kind.
    
    Parameters:
    
    kind - The kind of the term.
    
    children - The children of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Op op)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Op). It will be removed in a future release.
    
    Create nullary term of given kind from a given operator. Create operators with mkOp().
    
    Parameters:
    
    op - The operator.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Op op,
                               Term child)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.
    
    Create unary term of given kind from a given operator. Create operators with mkOp().
    
    Parameters:
    
    op - The operator.
    
    child - The child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Op op,
                               Term child1,
                               Term child2)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.
    
    Create binary term of given kind from a given operator. Create operators with mkOp().
    
    Parameters:
    
    op - The operator.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Op op,
                               Term child1,
                               Term child2,
                               Term child3)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). It will be removed in a future release.
    
    Create ternary term of given kind from a given operator. Create operators with mkOp().
    
    Parameters:
    
    op - The operator.
    
    child1 - The first child of the term.
    
    child2 - The second child of the term.
    
    child3 - The third child of the term.
    
    Returns:
    
    The Term.
  - mkTerm
```
@Deprecated
public Term mkTerm(Op op,
                               Term[] children)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.
    
    Create n-ary term of given kind from a given operator. Create operators with mkOp().
    
    Parameters:
    
    op - The operator.
    
    children - The children of the term.
    
    Returns:
    
    The Term.
  - mkTuple
```
@Deprecated
public Term mkTuple(Term[] terms)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.
    
    Create a tuple term. Terms are automatically converted if sorts are compatible.
    
    Parameters:
    
    terms - The elements in the tuple.
    
    Returns:
    
    The tuple Term.
  - mkNullableSome
```
@Deprecated
public Term mkNullableSome(Term term)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.
    
    Create a nullable some term.
    
    Parameters:
    
    term - The element value.
    
    Returns:
    
    the Element value wrapped in some constructor.
  - mkNullableVal
```
@Deprecated
public Term mkNullableVal(Term term)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.
    
    Create a selector for nullable term.
    
    Parameters:
    
    term - A nullable term.
    
    Returns:
    
    The element value of the nullable term.
  - mkNullableIsNull
```
@Deprecated
public Term mkNullableIsNull(Term term)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.
    
    Create a null tester for a nullable term.
    
    Parameters:
    
    term - A nullable term.
    
    Returns:
    
    A tester whether term is null.
  - mkNullableIsSome
```
@Deprecated
public Term mkNullableIsSome(Term term)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.
    
    Create a some tester for a nullable term.
    
    Parameters:
    
    term - A nullable term.
    
    Returns:
    
    A tester whether term is some.
  - mkNullableNull
```
@Deprecated
public Term mkNullableNull(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.
    
    Create a constant representing a null value of the given sort.
    
    Parameters:
    
    sort - The sort of the Nullable element.
    
    Returns:
    
    The null constant.
  - mkNullableLift
```
@Deprecated
public Term mkNullableLift(Kind kind,
                                       Term[] args)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.
    
    Create a term that lifts kind to nullable terms. Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)
    
    Parameters:
    
    kind - The lifted operator.
    
    args - The arguments of the lifted operator.
    
    Returns:
    
    A term of Kind NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.
  - mkOp
```
@Deprecated
public Op mkOp(Kind kind)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.
    
    Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).
    
    Parameters:
    
    kind - The kind to wrap.
    
    Returns:
    
    The operator.
    
    Note:
    
    In this case, the Op simply wraps the Kind. The Kind can be used in mkTerm directly without creating an op first.
  - mkOp
```
@Deprecated
public Op mkOp(Kind kind,
                           java.lang.String arg)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.
    Create operator of kind:
    - 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(java.lang.String s)
                           throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.
    
    Create an integer constant from a string.
    
    Parameters:
    
    s - The string representation of the constant, may represent an. integer (e.g., "123").
    
    Returns:
    
    A constant of sort Integer assuming s represents an integer).
    
    Throws:
    
    CVC5ApiException - on error
  - mkInteger
```
@Deprecated
public Term mkInteger(long val)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkInteger(long). It will be removed in a future release.
    
    Create an integer constant from a C++ int.
    
    Parameters:
    
    val - The value of the constant.
    
    Returns:
    
    A constant of sort Integer.
  - mkReal
```
@Deprecated
public Term mkReal(java.lang.String s)
                        throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.
    
    Create a real constant from a string.
    
    Parameters:
    
    s - The string representation of the constant, may represent an. integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
    
    Returns:
    
    A constant of sort Real.
    
    Throws:
    
    CVC5ApiException - on error
  - mkReal
```
@Deprecated
public Term mkReal(long val)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkReal(long). It will be removed in a future release.
    
    Create a real constant from an integer.
    
    Parameters:
    
    val - The value of the constant.
    
    Returns:
    
    A constant of sort Integer.
  - mkReal
```
@Deprecated
public Term mkReal(long num,
                               long den)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkReal(long, long). It will be removed in a future release.
    
    Create a real constant from a rational.
    
    Parameters:
    
    num - The value of the numerator.
    
    den - The value of the denominator.
    
    Returns:
    
    A constant of sort Real.
  - mkRegexpNone
```
@Deprecated
public Term mkRegexpNone()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.
    
    Create a regular expression none (re.none) term.
    
    Returns:
    
    The none term.
  - mkRegexpAll
```
@Deprecated
public Term mkRegexpAll()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.
    
    Create a regular expression all (re.all) term.
    
    Returns:
    
    The all term.
  - mkRegexpAllchar
```
@Deprecated
public Term mkRegexpAllchar()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.
    
    Create a regular expression allchar (re.allchar) term.
    
    Returns:
    
    The allchar term.
  - mkEmptySet
```
@Deprecated
public Term mkEmptySet(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.
    
    Create a constant representing an empty set of the given sort.
    
    Parameters:
    
    sort - The sort of the set elements.
    
    Returns:
    
    The empty set constant.
  - mkEmptyBag
```
@Deprecated
public Term mkEmptyBag(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.
    
    Create a constant representing an empty bag of the given sort.
    
    Parameters:
    
    sort - The sort of the bag elements.
    
    Returns:
    
    The empty bag constant.
  - mkSepEmp
```
@Deprecated
public Term mkSepEmp()
```
    Deprecated. This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.
    
    Create a separation logic empty term.
    
    Returns:
    
    The separation logic empty term.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkSepNil
```
@Deprecated
public Term mkSepNil(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.
    
    Create a separation logic nil term.
    
    Parameters:
    
    sort - The sort of the nil term.
    
    Returns:
    
    The separation logic nil term.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkString
```
@Deprecated
public Term mkString(java.lang.String s)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.
    
    Create a String constant.
    
    Parameters:
    
    s - The string this constant represents.
    
    Returns:
    
    The String constant.
  - mkString
```
@Deprecated
public Term mkString(java.lang.String s,
                                 boolean useEscSequences)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkString(String, boolean). It will be removed in a future release.
    
    Create a String constant.
    
    Parameters:
    
    s - The string this constant represents.
    
    useEscSequences - Determines whether escape sequences in s should be converted to the corresponding unicode character.
    
    Returns:
    
    The String constant.
  - mkString
```
@Deprecated
public Term mkString(int[] s)
                          throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkString(int[]). It will be removed in a future release.
    
    Create a String constant.
    
    Parameters:
    
    s - A list of unsigned (unicode) values this constant represents as string.
    
    Returns:
    
    The String constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkEmptySequence
```
@Deprecated
public Term mkEmptySequence(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.
    
    Create an empty sequence of the given element sort.
    
    Parameters:
    
    sort - The element sort of the sequence.
    
    Returns:
    
    The empty sequence with given element sort.
  - mkUniverseSet
```
@Deprecated
public Term mkUniverseSet(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.
    
    Create a universe set of the given sort.
    
    Parameters:
    
    sort - The sort of the set elements.
    
    Returns:
    
    The universe set constant.
  - mkBitVector
```
@Deprecated
public Term mkBitVector(int size)
                             throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.
    
    Create a bit-vector constant of given size and value = 0.
    
    Parameters:
    
    size - The bit-width of the bit-vector sort.
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkBitVector
```
@Deprecated
public Term mkBitVector(int size,
                                    long val)
                             throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.
    
    Create a bit-vector constant of given size and value.
    
    Parameters:
    
    size - The bit-width of the bit-vector sort.
    
    val - The value of the constant.
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a bit-vector of the given size.
  - mkBitVector
```
@Deprecated
public Term mkBitVector(int size,
                                    java.lang.String s,
                                    int base)
                             throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkBitVector(int, String, int). It will be removed in a future release.
    
    Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
    
    Parameters:
    
    size - The bit-width of the constant.
    
    s - The string representation of the constant.
    
    base - The base of the string representation (2, 10, or 16)
    
    Returns:
    
    The bit-vector constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a bit-vector of the given size.
  - mkFiniteFieldElem
```
@Deprecated
public Term mkFiniteFieldElem(java.lang.String val,
                                          Sort sort,
                                          int base)
                                   throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.
    
    Create a finite field constant in a given field and for a given value.
    
    Parameters:
    
    val - The value of the constant.
    
    sort - The sort of the finite field.
    
    base - The base of the string representation.
    
    Returns:
    
    The finite field constant.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    The given value must fit into a the given finite field.
  - mkConstArray
```
@Deprecated
public Term mkConstArray(Sort sort,
                                     Term val)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.
    
    Create a constant array with the provided constant value stored at every index
    
    Parameters:
    
    sort - The sort of the constant array (must be an array sort)
    
    val - The constant value to store (must match the sort's element sort).
    
    Returns:
    
    The constant array term.
  - mkFloatingPointPosInf
```
@Deprecated
public Term mkFloatingPointPosInf(int exp,
                                              int sig)
                                       throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.
    
    Create a positive infinity floating-point constant (SMT-LIB: +oo).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNegInf
```
@Deprecated
public Term mkFloatingPointNegInf(int exp,
                                              int sig)
                                       throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.
    
    Create a negative infinity floating-point constant (SMT-LIB: -oo).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNaN
```
@Deprecated
public Term mkFloatingPointNaN(int exp,
                                           int sig)
                                    throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.
    
    Create a not-a-number floating-point constant (SMT-LIB: NaN).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointPosZero
```
@Deprecated
public Term mkFloatingPointPosZero(int exp,
                                               int sig)
                                        throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.
    
    Create a positive zero floating-point constant (SMT-LIB: +zero).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPointNegZero
```
@Deprecated
public Term mkFloatingPointNegZero(int exp,
                                               int sig)
                                        throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.
    
    Create a negative zero floating-point constant (SMT-LIB: -zero).
    
    Parameters:
    
    exp - Number of bits in the exponent.
    
    sig - Number of bits in the significand.
    
    Returns:
    
    The floating-point constant.
    
    Throws:
    
    CVC5ApiException - on error
  - mkRoundingMode
```
@Deprecated
public Term mkRoundingMode(RoundingMode rm)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.
    
    Create a rounding mode constant.
    
    Parameters:
    
    rm - The floating point rounding mode this constant represents.
    
    Returns:
    
    The rounding mode.
  - mkFloatingPoint
```
@Deprecated
public Term mkFloatingPoint(int exp,
                                        int sig,
                                        Term val)
                                 throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.
    
    Create a floating-point value from a bit-vector given in IEEE-754 format.
    
    Parameters:
    
    exp - Size of the exponent.
    
    sig - Size of the significand.
    
    val - Value of the floating-point constant as a bit-vector term.
    
    Returns:
    
    The floating-point value.
    
    Throws:
    
    CVC5ApiException - on error
  - mkFloatingPoint
```
@Deprecated
public Term mkFloatingPoint(Term sign,
                                        Term exp,
                                        Term sig)
                                 throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, Term). It will be removed in a future release.
    
    Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
    
    Parameters:
    
    sign - The sign bit.
    
    exp - The bit-vector representing the exponent.
    
    sig - The bit-vector representing the significand.
    
    Returns:
    
    The floating-point value.
    
    Throws:
    
    CVC5ApiException - on error
  - mkCardinalityConstraint
```
@Deprecated
public Term mkCardinalityConstraint(Sort sort,
                                                int upperBound)
                                         throws CVC5ApiException
```
    Deprecated. This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.
    
    Create a cardinality constraint for an uninterpreted sort.
    
    Parameters:
    
    sort - The sort the cardinality constraint is for.
    
    upperBound - The upper bound on the cardinality of the sort.
    
    Returns:
    
    The cardinality constraint.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkConst
```
@Deprecated
public Term mkConst(Sort sort,
                                java.lang.String symbol)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.
    
    Create a free constant. SMT-LIB: ( declare-const <symbol> <sort> ) ( declare-fun <symbol> ( ) <sort> )
    
    Parameters:
    
    sort - The sort of the constant.
    
    symbol - The name of the constant.
    
    Returns:
    
    The first-order constant.
  - mkConst
```
@Deprecated
public Term mkConst(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkConst(Sort). It will be removed in a future release.
    
    Create a free constant with a default symbol name.
    
    Parameters:
    
    sort - The sort of the constant.
    
    Returns:
    
    The first-order constant.
  - mkVar
```
@Deprecated
public Term mkVar(Sort sort)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.
    
    Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
    
    Parameters:
    
    sort - The sort of the variable.
    
    Returns:
    
    The variable.
  - mkVar
```
@Deprecated
public Term mkVar(Sort sort,
                              java.lang.String symbol)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.
    
    Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
    
    Parameters:
    
    sort - The sort of the variable.
    
    symbol - The name of the variable.
    
    Returns:
    
    The variable.
  - mkDatatypeConstructorDecl
```
@Deprecated
public DatatypeConstructorDecl mkDatatypeConstructorDecl(java.lang.String name)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.
    
    Create a datatype constructor declaration.
    
    Parameters:
    
    name - The name of the datatype constructor.
    
    Returns:
    
    The DatatypeConstructorDecl.
  - mkDatatypeDecl
```
@Deprecated
public DatatypeDecl mkDatatypeDecl(java.lang.String name)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.
    
    Create a datatype declaration.
    
    Parameters:
    
    name - The name of the datatype.
    
    Returns:
    
    The DatatypeDecl.
  - mkDatatypeDecl
```
@Deprecated
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                               boolean isCoDatatype)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.
    
    Create a datatype declaration.
    
    Parameters:
    
    name - The name of the datatype.
    
    isCoDatatype - True if a codatatype is to be constructed.
    
    Returns:
    
    The DatatypeDecl.
  - mkDatatypeDecl
```
@Deprecated
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                               Sort[] params)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
    
    Create a datatype declaration. Create sorts parameter with mkParamSort(String).
    
    Parameters:
    
    name - The name of the datatype.
    
    params - A list of sort parameters.
    
    Returns:
    
    The DatatypeDecl.
    
    Note:
    
    This method is experimental and may change in future versions.
  - mkDatatypeDecl
```
@Deprecated
public DatatypeDecl mkDatatypeDecl(java.lang.String name,
                                               Sort[] params,
                                               boolean isCoDatatype)
```
    Deprecated. This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
    
    Create a datatype declaration. Create sorts parameter with mkParamSort(String).
    
    Parameters:
    
    name - The name of the datatype.
    
    params - A list of sort parameters.
    
    isCoDatatype - True if a codatatype is to be constructed.
    
    Returns:
    
    The DatatypeDecl.
  - simplify
```
public Term simplify(Term t)
```
    Simplify a term or formula based on rewriting.
    
    Parameters:
    
    t - The term to simplify.
    
    Returns:
    
    The simplified term.
    
    Note:
    
    This function is experimental and may change in future versions.
  - simplify
```
public Term simplify(Term t,
                     boolean applySubs)
```
    Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables. If applySubs is true, then for example, if `(= x 0)` was asserted to this solver, this method may replace occurrences of `x` with `0`.
    
    Parameters:
    
    t - The term to simplify.
    
    applySubs - Whether to apply substitutions for solved variables.
    
    Returns:
    
    The simplified term.
    
    Note:
    
    This function is experimental and may change in future versions.
  - assertFormula
```
public void assertFormula(Term term)
```
    Assert a formula. SMT-LIB: ( assert <term> )
    
    Parameters:
    
    term - The formula to assert.
  - checkSat
```
public Result checkSat()
```
    Check satisfiability. SMT-LIB: ( check-sat )
    
    Returns:
    
    The result of the satisfiability check.
  - checkSatAssuming
```
public Result checkSatAssuming(Term assumption)
```
    Check satisfiability assuming the given formula. SMT-LIB: ( check-sat-assuming ( <prop_literal> ) )
    
    Parameters:
    
    assumption - The formula to assume.
    
    Returns:
    
    The result of the satisfiability check.
  - checkSatAssuming
```
public Result checkSatAssuming(Term[] assumptions)
```
    Check satisfiability assuming the given formulas. SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) )
    
    Parameters:
    
    assumptions - The formulas to assume.
    
    Returns:
    
    The result of the satisfiability check.
  - declareDatatype
```
public Sort declareDatatype(java.lang.String symbol,
                            DatatypeConstructorDecl[] ctors)
```
    Create datatype sort. SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
    
    Parameters:
    
    symbol - The name of the datatype sort.
    
    ctors - The constructor declarations of the datatype sort.
    
    Returns:
    
    The datatype sort.
  - declareFun
```
public Term declareFun(java.lang.String symbol,
                       Sort[] sorts,
                       Sort sort)
```
    Declare n-ary function symbol. SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
    
    Parameters:
    
    symbol - The name of the function.
    
    sorts - The sorts of the parameters to this function.
    
    sort - The sort of the return value of this function.
    
    Returns:
    
    The function.
  - declareFun
```
public Term declareFun(java.lang.String symbol,
                       Sort[] sorts,
                       Sort sort,
                       boolean fresh)
```
    Declare n-ary function symbol. SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
    
    Parameters:
    
    symbol - The name of the function.
    
    sorts - The sorts of the parameters to this function.
    
    sort - The sort of the return value of this function.
    
    fresh - If true, then this method always returns a new Term. Otherwise, this method will always return the same Term for each call with the given sorts and symbol where fresh is false.
    
    Returns:
    
    The function.
  - declareSort
```
public Sort declareSort(java.lang.String symbol,
                        int arity)
                 throws CVC5ApiException
```
    Declare uninterpreted sort. SMT-LIB: ( declare-sort <symbol> <numeral> )
    
    Parameters:
    
    symbol - The name of the sort.
    
    arity - The arity of the sort.
    
    Returns:
    
    The sort.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This corresponds to mkUninterpretedSort() const if arity = 0, and to mkUninterpretedSortConstructorSort() const if arity > 0.
  - declareSort
```
public Sort declareSort(java.lang.String symbol,
                        int arity,
                        boolean fresh)
                 throws CVC5ApiException
```
    Declare uninterpreted sort. SMT-LIB: ( declare-sort <symbol> <numeral> )
    
    Parameters:
    
    symbol - The name of the sort.
    
    arity - The arity of the sort.
    
    fresh - If true, then this method always returns a new Sort. Otherwise, this method will always return the same Sort for each call with the given arity and symbol where fresh is false.
    
    Returns:
    
    The sort.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This corresponds to mkUninterpretedSort() const if arity = 0, and to mkUninterpretedSortConstructorSort() const if arity > 0.
  - defineFun
```
public Term defineFun(java.lang.String symbol,
                      Term[] boundVars,
                      Sort sort,
                      Term term)
```
    Define n-ary function in the current context. SMT-LIB: ( define-fun <function_def> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    term - The function body.
    
    Returns:
    
    The function.
  - defineFun
```
public Term defineFun(java.lang.String symbol,
                      Term[] boundVars,
                      Sort sort,
                      Term term,
                      boolean global)
```
    Define n-ary function. SMT-LIB: ( define-fun <function_def> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    term - The function body.
    
    global - Determines whether this definition is global (i.e., persists when popping the context).
    
    Returns:
    
    The function.
  - defineFunRec
```
public Term defineFunRec(java.lang.String symbol,
                         Term[] boundVars,
                         Sort sort,
                         Term term)
```
    Define recursive function in the current context. SMT-LIB: ( define-fun-rec <function_def> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    term - The function body.
    
    Returns:
    
    The function.
  - defineFunRec
```
public Term defineFunRec(java.lang.String symbol,
                         Term[] boundVars,
                         Sort sort,
                         Term term,
                         boolean global)
```
    Define recursive function. SMT-LIB: ( define-fun-rec <function_def> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    term - The function body.
    
    global - Determines whether this definition is global (i.e., persists when popping the context).
    
    Returns:
    
    The function.
  - defineFunRec
```
public Term defineFunRec(Term fun,
                         Term[] boundVars,
                         Term term)
```
    Define recursive function in the current context. SMT-LIB: ( define-fun-rec <function_def> ) Create parameter fun with mkConst(Sort).
    
    Parameters:
    
    fun - The sorted function.
    
    boundVars - The parameters to this function.
    
    term - The function body.
    
    Returns:
    
    The function.
  - defineFunRec
```
public Term defineFunRec(Term fun,
                         Term[] boundVars,
                         Term term,
                         boolean global)
```
    Define recursive function. SMT-LIB: ( define-fun-rec <function_def> ) Create parameter fun with mkConst(Sort).
    
    Parameters:
    
    fun - The sorted function.
    
    boundVars - The parameters to this function.
    
    term - The function body.
    
    global - Determines whether this definition is global (i.e., persists when popping the context).
    
    Returns:
    
    The function.
  - defineFunsRec
```
public void defineFunsRec(Term[] funs,
                          Term[][] boundVars,
                          Term[] terms)
```
    Define recursive functions in the current context. SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) Create elements of parameter funs with mkConst(Sort).
    
    Parameters:
    
    funs - The sorted functions.
    
    boundVars - The list of parameters to the functions.
    
    terms - The list of function bodies of the functions.
  - defineFunsRec
```
public void defineFunsRec(Term[] funs,
                          Term[][] boundVars,
                          Term[] terms,
                          boolean global)
```
    Define recursive functions. SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) Create elements of parameter funs with mkConst(Sort).
    
    Parameters:
    
    funs - The sorted functions.
    
    boundVars - The list of parameters to the functions.
    
    terms - The list of function bodies of the functions.
    
    global - Determines whether this definition is global (i.e., persists when popping the context).
  - getLearnedLiterals
```
public Term[] getLearnedLiterals()
```
    Get a list of input literals that are entailed by the current set of assertions. SMT-LIB: ( get-learned-literals )
    
    Returns:
    
    The list of learned literals.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getLearnedLiterals
```
public Term[] getLearnedLiterals(LearnedLitType type)
```
    Get a list of literals that are entailed by the current set of assertions. SMT-LIB: ( get-learned-literals :type )
    
    Parameters:
    
    type - The type of learned literals to return
    
    Returns:
    
    The list of learned literals.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getAssertions
```
public Term[] getAssertions()
```
    Get the list of asserted formulas. SMT-LIB: ( get-assertions )
    
    Returns:
    
    The list of asserted formulas.
  - getInfo
```
public java.lang.String getInfo(java.lang.String flag)
```
    Get info from the solver. SMT-LIB: ( get-info <info_flag> )
    
    Parameters:
    
    flag - The get-info flag.
    
    Returns:
    
    The info.
  - getOption
```
public java.lang.String getOption(java.lang.String option)
```
    Get the value of a given option. SMT-LIB: ( get-option <keyword> )
    
    Parameters:
    
    option - The option for which the value is queried.
    
    Returns:
    
    A string representation of the option value.
  - getOptionNames
```
public java.lang.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(java.lang.String option)
```
    Get some information about the given option. Check the OptionInfo class for more details on which information is available.
    
    Parameters:
    
    option - The name of the option.
    
    Returns:
    
    Information about the given option.
  - getUnsatAssumptions
```
public Term[] getUnsatAssumptions()
```
    Get the set of unsat ("failed") assumptions. SMT-LIB: ( get-unsat-assumptions ) Requires to enable option produce-unsat-assumptions.
    
    Returns:
    
    The set of unsat assumptions.
  - getUnsatCore
```
public Term[] getUnsatCore()
```
    Get the unsatisfiable core. SMT-LIB: (get-unsat-core) Requires to enable option produce-unsat-cores.
    
    Returns:
    
    A set of terms representing the unsatisfiable core.
    
    Note:
    
    In contrast to SMT-LIB, cvc5's API does not distinguish between named and unnamed assertions when producing an unsatisfiable core. Additionally, the API allows this option to be called after a check with assumptions. A subset of those assumptions may be included in the unsatisfiable core returned by this method.
  - getUnsatCoreLemmas
```
public Term[] getUnsatCoreLemmas()
```
    Get the lemmas used to derive unsatisfiability. SMT-LIB: (get-unsat-core-lemmas) Requires the SAT proof unsat core mode, so to enable option unsat-core-mode=sat-proof
    
    Returns:
    
    A set of terms representing the lemmas used to derive unsatisfiability.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getDifficulty
```
public java.util.Map<Term,Term> getDifficulty()
```
    Get a difficulty estimate for an asserted formula. This method is intended to be called immediately after any response to a checkSat.
    
    Returns:
    
    A map from (a subset of) the input assertions to a real value that. is an estimate of how difficult each assertion was to solve. Unmentioned assertions can be assumed to have zero difficulty.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getTimeoutCore
```
public Pair<Result,Term[]> getTimeoutCore()
```
    Get a timeout core, which computes a subset of the current assertions that cause a timeout. Note it does not require being proceeded by a call to checkSat. SMT-LIB: (get-timeout-core)
    
    Returns:
    
    The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of the current assertions that cause a timeout in the specified time timeout-core-timeout. If the result is unsat, then the list of formulas correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the current assertions are satisfiable, and the list of formulas is empty. This method may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getTimeoutCoreAssuming
```
public Pair<Result,Term[]> getTimeoutCoreAssuming(Term[] assumptions)
```
    Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions. Note it does not require being proceeded by a call to checkSat. SMT-LIB: (get-timeout-core)
    
    Parameters:
    
    assumptions - The formulas to assume.
    
    Returns:
    
    The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of assumptions that cause a timeout when added to the current assertions in the specified time timeout-core-timeout. If the result is unsat, then the list of formulas plus the current assertions correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the given assumptions plus the current assertions are satisfiable, and the list of formulas is empty. This method may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getProof
```
public Proof[] getProof()
```
    Get refutation proof for the most recent call to checkSat. SMT-LIB: ( get-proof ) Requires to enable option produce-proofs.
    
    Returns:
    
    A vector of proof nodes. This is equivalent to getProof when c is FULL.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getProof
```
public Proof[] getProof(ProofComponent c)
```
    Get a proof associated with the most recent call to checkSat. SMT-LIB: ( get-proof :c) Requires to enable option produce-proofs.
    
    Parameters:
    
    c - The component of the proof to return
    
    Returns:
    
    A vector of proof nodes.
    
    Note:
    
    This method is experimental and may change in future versions.
  - proofToString
```
public java.lang.String proofToString(Proof proof)
```
    Prints a proof into a string with a slected proof format mode. Other aspects of printing are taken from the solver options.
    
    Parameters:
    
    proof - A proof.
    
    Returns:
    
    The proof printed in the current format.
    
    Note:
    
    This method is experimental and may change in future versions.
  - proofToString
```
public java.lang.String proofToString(Proof proof,
                                      ProofFormat format)
```
    Prints a proof into a string with a slected proof format mode. Other aspects of printing are taken from the solver options.
    
    Parameters:
    
    proof - A proof.
    
    format - The proof format used to print the proof. Must be `PROOF_FORMAT_NONE` if the proof is from a component other than `PROOF_COMPONENT_FULL`.
    
    Returns:
    
    The proof printed in the current format.
    
    Note:
    
    This method is experimental and may change in future versions.
  - proofToString
```
public java.lang.String proofToString(Proof proof,
                                      ProofFormat format,
                                      java.util.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 java.lang.String getModel(Sort[] sorts,
                                 Term[] vars)
```
    Get the model SMT-LIB: ( get-model ) Requires to enable option produce-models.
    
    Parameters:
    
    sorts - The list of uninterpreted sorts that should be printed in the. model.
    
    vars - The list of free constants that should be printed in the. model. A subset of these may be printed based on isModelCoreSymbol(Term).
    
    Returns:
    
    A string representing the model.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getQuantifierElimination
```
public Term getQuantifierElimination(Term q)
```
    Do quantifier elimination. SMT-LIB: ( get-qe <q> ) Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.
    
    Parameters:
    
    q - A quantified formula of the form: Q x1...xn. P( x1...xn, y1...yn ) where P( x1...xn, y1...yn ) is a quantifier-free formula.
    
    Returns:
    
    A formula ret such that, given the current set of formulas A asserted to this solver: - ( A && q ) and ( A && ret ) are equivalent - ret is quantifier-free formula containing only free variables in y1...yn.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getQuantifierEliminationDisjunct
```
public Term getQuantifierEliminationDisjunct(Term q)
```
    Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination. SMT-LIB: ( get-qe-disjunct <q> ) Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.
    
    Parameters:
    
    q - A quantified formula of the form: Q x1...xn. P( x1...xn, y1...yn ) where P( x1...xn, y1...yn ) is a quantifier-free formula.
    
    Returns:
    
    A formula ret such that, given the current set of formulas A asserted to this solver: - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is exists, - ret is quantifier-free formula containing only free variables in y1...yn, - If Q is exists, let A && Q_n be the formula A && ~(ret && Q_1) && ... && ~(ret && Q_n) where for each i=1,...n, formula ret && Q_i is the result of calling getQuantifierEliminationDisjunct(Term) for q with the set of assertions A && Q_{i-1}. Similarly, if Q is forall, then let A && Q_n be A && (ret && Q_1) && ... && (ret&& Q_n) where ret && Q_i is the same as above. In either case, we have that ret && Q_j will eventually be true or false, for some finite j.
    
    Note:
    
    This method is experimental and may change in future versions.
  - declareSepHeap
```
public void declareSepHeap(Sort locSort,
                           Sort dataSort)
```
    When using separation logic, this sets the location sort and the datatype sort to the given ones. This method should be invoked exactly once, before any separation logic constraints are provided.
    
    Parameters:
    
    locSort - The location sort of the heap.
    
    dataSort - The data sort of the heap.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getValueSepHeap
```
public Term getValueSepHeap()
```
    When using separation logic, obtain the term for the heap.
    
    Returns:
    
    The term for the heap.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getValueSepNil
```
public Term getValueSepNil()
```
    When using separation logic, obtain the term for nil.
    
    Returns:
    
    The term for nil.
    
    Note:
    
    This method is experimental and may change in future versions.
  - declarePool
```
public Term declarePool(java.lang.String symbol,
                        Sort sort,
                        Term[] initValue)
```
    Declare a symbolic pool of terms with the given initial value. SMT-LIB: ( declare-pool <symbol> <sort> ( <term>* ) )
    
    Parameters:
    
    symbol - The name of the pool.
    
    sort - The sort of the elements of the pool.
    
    initValue - The initial value of the pool.
    
    Returns:
    
    The pool.
    
    Note:
    
    This method is experimental and may change in future versions.
  - declareOracleFun
```
public Term declareOracleFun(java.lang.String symbol,
                             Sort[] sorts,
                             Sort sort,
                             IOracle oracle)
```
    Declare an oracle function with reference to an implementation. Oracle functions have a different semantics with respect to ordinary declared functions. In particular, for an input to be satisfiable, its oracle functions are implicitly universally quantified. This method is used in part for implementing this command: (declare-oracle-fun <sym> (<sort>*) <sort> <sym>) In particular, the above command is implemented by constructing a function over terms that wraps a call to binary sym via a text interface.
    
    Parameters:
    
    symbol - The name of the oracle
    
    sorts - The sorts of the parameters to this function
    
    sort - The sort of the return value of this function
    
    oracle - An object that implements the oracle interface.
    
    Returns:
    
    The oracle function
    
    Note:
    
    This method is experimental and may change in future versions.
  - addPlugin
```
public void addPlugin(AbstractPlugin p)
```
    Add plugin to this solver. Its callbacks will be called throughout the lifetime of this solver.
    
    Parameters:
    
    p - The plugin to add to this solver.
  - pop
```
public void pop()
         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 java.lang.String getInstantiations()
```
    Get a string that contains information about all instantiations made by the quantifiers module.
    
    Returns:
    
    The string representing the information about all instantiations.
    
    Note:
    
    This method is experimental and may change in future versions.
  - push
```
public void push()
          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(java.lang.String keyword,
                    java.lang.String value)
             throws CVC5ApiException
```
    Set info. SMT-LIB: ( set-info <attribute> )
    
    Parameters:
    
    keyword - The info flag.
    
    value - The value of the info flag.
    
    Throws:
    
    CVC5ApiException - on error
  - setLogic
```
public void setLogic(java.lang.String logic)
              throws CVC5ApiException
```
    Set logic. SMT-LIB: ( set-logic <symbol> )
    
    Parameters:
    
    logic - The logic to set.
    
    Throws:
    
    CVC5ApiException - on error
  - isLogicSet
```
public boolean isLogicSet()
```
    Is logic set? Returns whether we called setLogic yet for this solver.
    
    Returns:
    
    whether we called setLogic yet for this solver.
  - getLogic
```
public java.lang.String getLogic()
                          throws CVC5ApiException
```
    Get the logic set the solver.
    
    Returns:
    
    The logic used by the solver.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    Asserts isLogicSet().
  - setOption
```
public void setOption(java.lang.String option,
                      java.lang.String value)
```
    Set option. SMT-LIB: ( set-option <option> )
    
    Parameters:
    
    option - The option name.
    
    value - The option value.
  - declareSygusVar
```
public Term declareSygusVar(java.lang.String symbol,
                            Sort sort)
```
    Append symbol to the current list of universal variables. SyGuS v2: ( declare-var <symbol> <sort> )
    
    Parameters:
    
    sort - The sort of the universal variable.
    
    symbol - The name of the universal variable.
    
    Returns:
    
    The universal variable.
  - mkGrammar
```
public Grammar mkGrammar(Term[] boundVars,
                         Term[] ntSymbols)
```
    Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.
    
    Parameters:
    
    boundVars - The parameters to corresponding synth-fun/synth-inv.
    
    ntSymbols - The pre-declaration of the non-terminal symbols.
    
    Returns:
    
    The grammar.
  - synthFun
```
public Term synthFun(java.lang.String symbol,
                     Term[] boundVars,
                     Sort sort)
```
    Synthesize n-ary function. SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    Returns:
    
    The function.
  - synthFun
```
public Term synthFun(java.lang.String symbol,
                     Term[] boundVars,
                     Sort sort,
                     Grammar grammar)
```
    Synthesize n-ary function following specified syntactic constraints. SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
    
    Parameters:
    
    symbol - The name of the function.
    
    boundVars - The parameters to this function.
    
    sort - The sort of the return value of this function.
    
    grammar - The syntactic constraints.
    
    Returns:
    
    The function.
  - addSygusConstraint
```
public void addSygusConstraint(Term term)
```
    Add a forumla to the set of Sygus constraints. SyGuS v2: ( constraint <term> )
    
    Parameters:
    
    term - The formula to add as a constraint.
  - getSygusConstraints
```
public Term[] getSygusConstraints()
```
    Get the list of sygus constraints.
    
    Returns:
    
    The list of sygus constraints.
  - addSygusAssume
```
public void addSygusAssume(Term term)
```
    Add a forumla to the set of Sygus assumptions. SyGuS v2: ( assume <term> )
    
    Parameters:
    
    term - The formula to add as an assumption.
  - getSygusAssumptions
```
public Term[] getSygusAssumptions()
```
    Get the list of sygus assumptions.
    
    Returns:
    
    The list of sygus assumptions.
  - addSygusInvConstraint
```
public void addSygusInvConstraint(Term inv,
                                  Term pre,
                                  Term trans,
                                  Term post)
```
    Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem. SyGuS v2: ( inv-constraint <inv> <pre> <trans> <post> )
    
    Parameters:
    
    inv - The function-to-synthesize.
    
    pre - The pre-condition.
    
    trans - The transition relation.
    
    post - The post-condition.
  - checkSynth
```
public SynthResult checkSynth()
```
    Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. SyGuS v2: ( check-synth )
    
    Returns:
    
    The result of the check, which is "solution" if the check found a. solution in which case solutions are available via getSynthSolutions, "no solution" if it was determined there is no solution, or "unknown" otherwise.
  - checkSynthNext
```
public SynthResult checkSynthNext()
```
    Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next.
    
    Returns:
    
    The result of the check, which is "solution" if the check found a solution in which case solutions are available via getSynthSolutions, "no solution" if it was determined there is no solution, or "unknown" otherwise.
    
    Note:
    
    Requires incremental mode. SyGuS v2: ( check-synth-next )
  - getSynthSolution
```
public Term getSynthSolution(Term term)
```
    Get the synthesis solution of the given term. This method should be called immediately after the solver answers unsat for sygus input.
    
    Parameters:
    
    term - The term for which the synthesis solution is queried.
    
    Returns:
    
    The synthesis solution of the given term.
  - getSynthSolutions
```
public Term[] getSynthSolutions(Term[] terms)
```
    Get the synthesis solutions of the given terms. This method should be called immediately after the solver answers unsat for sygus input.
    
    Parameters:
    
    terms - The terms for which the synthesis solutions is queried.
    
    Returns:
    
    The synthesis solutions of the given terms.
  - findSynth
```
public Term findSynth(FindSynthTarget fst)
```
    Find a target term of interest using sygus enumeration, with no provided grammar. The solver will infer which grammar to use in this call, which by default will be the grammars specified by the function(s)-to-synthesize in the current context. SyGuS v2: (find-synth :target)
    
    Parameters:
    
    fst - The identifier specifying what kind of term to find
    
    Returns:
    
    The result of the find, which is the null term if this call failed.
    
    Note:
    
    This method is experimental and may change in future versions.
  - findSynth
```
public Term findSynth(FindSynthTarget fst,
                      Grammar grammar)
```
    Find a target term of interest using sygus enumeration with a provided grammar. SyGuS v2: (find-synth :target G)
    
    Parameters:
    
    fst - The identifier specifying what kind of term to find
    
    grammar - The grammar for the term
    
    Returns:
    
    The result of the find, which is the null term if this call failed.
    
    Note:
    
    This method is experimental and may change in future versions.
  - findSynthNext
```
public Term findSynthNext()
```
    Try to find a next target term of interest using sygus enumeration. Must be called immediately after a successful call to find-synth or find-synth-next. SyGuS v2: (find-synth-next)
    
    Returns:
    
    The result of the find, which is the null term if this call failed.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getStatistics
```
public Statistics getStatistics()
```
    Get a snapshot of the current state of the statistic values of this solver. The returned object is completely decoupled from the solver and will not change when the solver is used again.
    
    Returns:
    
    A snapshot of the current state of the statistic values.
  - getVersion
```
public java.lang.String getVersion()
```
    Get a string representation of the version of this solver.
    
    Returns:
    
    The version string.
  - getPointer
```
public long getPointer()
```
  - deletePointer
```
public void deletePointer()
```
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object

Class Solver

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

pointer

Constructor Detail

Solver

Solver

Method Detail

deletePointer

toString

equals

getTermManager

getBooleanSort

getIntegerSort

getRealSort

getRegExpSort

getRoundingModeSort

getStringSort

mkArraySort

mkBitVectorSort

mkFiniteFieldSort

mkFloatingPointSort

mkDatatypeSort

mkDatatypeSorts

mkFunctionSort

mkFunctionSort

mkParamSort

mkParamSort

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

mkRegexpAllchar

mkEmptySet