Deprecated API

Contents

• Methods
• Constructors

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