Deprecated API

Contents

• Classes
• Methods
• Constructors

• Deprecated Classes

  Class

  Description

  io.github.cvc5.Context

  Native memory is managed automatically. This class will be removed in a future release.

• Deprecated Methods

  Method

  Description

  io.github.cvc5.Context.deletePointers()

  Native memory is released automatically once the corresponding Java objects are no longer reachable. Use deletePointer() or close() to release individual objects deterministically.

  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.mkBitVector(int, long)

  This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.

  io.github.cvc5.Solver.mkBitVector(int, String, int)

  This function is deprecated and replaced by TermManager.mkBitVector(int, String, 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)

  This function is deprecated and replaced by TermManager.mkConst(Sort). 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.mkDatatypeDecl(String, boolean)

  This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.

  io.github.cvc5.Solver.mkDatatypeDecl(String, Sort[])

  This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.

  io.github.cvc5.Solver.mkDatatypeDecl(String, Sort[], boolean)

  This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). 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.mkFloatingPoint(Term, Term, Term)

  This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, 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.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.mkGrammar(Term[], Term[])

  This function is deprecated and replaced by TermManager.mkGrammar(Term[], Term[]). It will be removed in a future release.

  io.github.cvc5.Solver.mkInteger(long)

  This function is deprecated and replaced by TermManager.mkInteger(long). 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.mkOp(Kind, int)

  This function is deprecated and replaced by TermManager.mkOp(Kind, int). It will be removed in a future release.

  io.github.cvc5.Solver.mkOp(Kind, int[])

  This function is deprecated and replaced by TermManager.mkOp(Kind, int[]). It will be removed in a future release.

  io.github.cvc5.Solver.mkOp(Kind, int, int)

  This function is deprecated and replaced by TermManager.mkOp(Kind, int, int). It will be removed in a future release.

  io.github.cvc5.Solver.mkOp(Kind, String)

  This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.

  io.github.cvc5.Solver.mkParamSort()

  This function is deprecated and replaced by TermManager.mkParamSort(). 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(long)

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

  io.github.cvc5.Solver.mkReal(long, long)

  This function is deprecated and replaced by TermManager.mkReal(long, long). 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(int[])

  This function is deprecated and replaced by TermManager.mkString(int[]). 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.mkString(String, boolean)

  This function is deprecated and replaced by TermManager.mkString(String, boolean). 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.mkTerm(Kind, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Kind, Term[])

  This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Kind, Term, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Kind, Term, Term, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Op)

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

  io.github.cvc5.Solver.mkTerm(Op, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Op, Term[])

  This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Op, Term, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.

  io.github.cvc5.Solver.mkTerm(Op, Term, Term, Term)

  This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). 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()

  This function is deprecated and replaced by TermManager.mkUninterpretedSort(). 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)

  This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). 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)

  This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). 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.

  io.github.cvc5.Solver.mkVar(Sort, String)

  This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.

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