Deprecated API

Contents

• Methods
• Constructors

Methods

Method	Description
io.github.cvc5.Solver.getBooleanSort()	This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.
io.github.cvc5.Solver.getIntegerSort()	This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.
io.github.cvc5.Solver.getRealSort()	This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.
io.github.cvc5.Solver.getRegExpSort()	This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.
io.github.cvc5.Solver.getRoundingModeSort()	This function is deprecated and replaced by TermManager.getRoundingModeSort(). It will be removed in a future release.
io.github.cvc5.Solver.getStringSort()	This function is deprecated and replaced by TermManager.getStringSort(). It will be removed in a future release.
io.github.cvc5.Solver.mkAbstractSort(SortKind)	This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.
io.github.cvc5.Solver.mkArraySort(Sort, Sort)	This function is deprecated and replaced by TermManager.mkArraySort(Sort, Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkBagSort(Sort)	This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkBitVector(int)	This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.
io.github.cvc5.Solver.mkBitVectorSort(int)	This function is deprecated and replaced by TermManager.mkBitVectorSort(int). It will be removed in a future release.
io.github.cvc5.Solver.mkBoolean(boolean)	This function is deprecated and replaced by TermManager.mkBoolean(boolean). It will be removed in a future release.
io.github.cvc5.Solver.mkCardinalityConstraint(Sort, int)	This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.
io.github.cvc5.Solver.mkConst(Sort, String)	This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.
io.github.cvc5.Solver.mkConstArray(Sort, Term)	This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.
io.github.cvc5.Solver.mkDatatypeConstructorDecl(String)	This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.
io.github.cvc5.Solver.mkDatatypeDecl(String)	This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.
io.github.cvc5.Solver.mkDatatypeSort(DatatypeDecl)	This function is deprecated and replaced by TermManager.mkDatatypeSort(DatatypeDecl). It will be removed in a future release.
io.github.cvc5.Solver.mkDatatypeSorts(DatatypeDecl[])	This function is deprecated and replaced by TermManager.mkDatatypeSorts(DatatypeDecl[]). It will be removed in a future release.
io.github.cvc5.Solver.mkEmptyBag(Sort)	This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkEmptySequence(Sort)	This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkEmptySet(Sort)	This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkFalse()	This function is deprecated and replaced by TermManager.mkFalse(). It will be removed in a future release.
io.github.cvc5.Solver.mkFiniteFieldElem(String, Sort, int)	This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFiniteFieldSort(String, int)	This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPoint(int, int, Term)	This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointNaN(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointNegInf(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointNegZero(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointPosInf(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointPosZero(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFloatingPointSort(int, int)	This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.
io.github.cvc5.Solver.mkFunctionSort(Sort, Sort)	This function is deprecated and replaced by TermManager.mkFunctionSort(Sort, Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkInteger(String)	This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableIsNull(Term)	This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableIsSome(Term)	This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableLift(Kind, Term[])	This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableNull(Sort)	This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableSome(Term)	This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableSort(Sort)	This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkNullableVal(Term)	This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.
io.github.cvc5.Solver.mkOp(Kind)	This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.
io.github.cvc5.Solver.mkParamSort(String)	This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.
io.github.cvc5.Solver.mkPi()	This function is deprecated and replaced by TermManager.mkPi(). It will be removed in a future release.
io.github.cvc5.Solver.mkPredicateSort(Sort[])	This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.
io.github.cvc5.Solver.mkReal(String)	This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.
io.github.cvc5.Solver.mkRecordSort(Pair<String, Sort>[])	This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.
io.github.cvc5.Solver.mkRegexpAll()	This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.
io.github.cvc5.Solver.mkRegexpAllchar()	This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.
io.github.cvc5.Solver.mkRegexpNone()	This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.
io.github.cvc5.Solver.mkRoundingMode(RoundingMode)	This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.
io.github.cvc5.Solver.mkSepEmp()	This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.
io.github.cvc5.Solver.mkSepNil(Sort)	This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkSequenceSort(Sort)	This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkSetSort(Sort)	This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkString(String)	This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.
io.github.cvc5.Solver.mkTerm(Kind)	This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.
io.github.cvc5.Solver.mkTrue()	This function is deprecated and replaced by TermManager.mkTrue(). It will be removed in a future release.
io.github.cvc5.Solver.mkTuple(Term[])	This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.
io.github.cvc5.Solver.mkTupleSort(Sort[])	This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.
io.github.cvc5.Solver.mkUninterpretedSort(String)	This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.
io.github.cvc5.Solver.mkUninterpretedSortConstructorSort(int, String)	This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.
io.github.cvc5.Solver.mkUniverseSet(Sort)	This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.
io.github.cvc5.Solver.mkUnresolvedDatatypeSort(String, int)	This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.
io.github.cvc5.Solver.mkVar(Sort)	This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.

Constructors

Constructor	Description
io.github.cvc5.Solver()	This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
io.github.cvc5.SymbolManager(Solver)	This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.