Index

A B C D E F G H I K L M N O P R S T U V X

A

AbstractPlugin - Class in io.github.cvc5
AbstractPlugin(TermManager) - Constructor for class io.github.cvc5.AbstractPlugin: Create plugin instance.
addAnyConstant(Term) - Method in class io.github.cvc5.Grammar: Allow ntSymbol to be an arbitrary constant.
addAnyVariable(Term) - Method in class io.github.cvc5.Grammar: Allow ntSymbol to be any input variable to corresponding synth-fun or synth-inv with the same sort as ntSymbol.
addConstructor(DatatypeConstructorDecl) - Method in class io.github.cvc5.DatatypeDecl: Add datatype constructor declaration.
addPlugin(AbstractPlugin) - Method in class io.github.cvc5.Solver: Add plugin to this solver.
addRule(Term, Term) - Method in class io.github.cvc5.Grammar: Add rule to the set of rules corresponding to ntSymbol.
addRules(Term, Term[]) - Method in class io.github.cvc5.Grammar: Add rules to the set of rules corresponding to ntSymbol.
addRules(long, long, long[]) - Method in class io.github.cvc5.Grammar
addSelector(String, Sort) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration.
addSelectorSelf(String) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration whose codomain type is the datatype itself.
addSelectorUnresolved(String, String) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.
addSygusAssume(Term) - Method in class io.github.cvc5.Solver: Add a forumla to the set of Sygus assumptions.
addSygusConstraint(Term) - Method in class io.github.cvc5.Solver: Add a forumla to the set of Sygus constraints.
addSygusInvConstraint(Term, Term, Term, Term) - Method in class io.github.cvc5.Solver: Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.
andTerm(Term) - Method in class io.github.cvc5.Term: Boolean and.
appendIncrementalStringInput(String) - Method in class io.github.cvc5.InputParser: Append string to the input being parsed by this parser.
apply(Term[]) - Method in interface io.github.cvc5.IOracle
assertFormula(Term) - Method in class io.github.cvc5.Solver: Assert a formula.

B

BaseInfo() - Constructor for class io.github.cvc5.OptionInfo.BaseInfo
blockModel(BlockModelsMode) - Method in class io.github.cvc5.Solver: Block the current model.
BlockModelsMode - Enum in io.github.cvc5.modes
blockModelValues(Term[]) - Method in class io.github.cvc5.Solver: Block the current model values of (at least) the values in terms.
booleanValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a Boolean.

C

check() - Method in class io.github.cvc5.AbstractPlugin: Call to check, return vector of lemmas to add to the SAT solver.
checkSat() - Method in class io.github.cvc5.Solver: Check satisfiability.
checkSatAssuming(Term) - Method in class io.github.cvc5.Solver: Check satisfiability assuming the given formula.
checkSatAssuming(Term[]) - Method in class io.github.cvc5.Solver: Check satisfiability assuming the given formulas.
checkSynth() - Method in class io.github.cvc5.Solver: Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
checkSynthNext() - Method in class io.github.cvc5.Solver: Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
Command - Class in io.github.cvc5
compareTo(Sort) - Method in class io.github.cvc5.Sort: Comparison for ordering on sorts.
compareTo(Term) - Method in class io.github.cvc5.Term: Comparison for ordering on terms.
ConstIterator() - Constructor for class io.github.cvc5.Datatype.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.DatatypeConstructor.ConstIterator
ConstIterator(boolean, boolean) - Constructor for class io.github.cvc5.Statistics.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Statistics.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Term.ConstIterator
Context - Class in io.github.cvc5
Context() - Constructor for class io.github.cvc5.Context
CURRENT - Static variable in enum io.github.cvc5.Utils.OS
CVC5ApiException - Exception in io.github.cvc5
CVC5ApiException(String) - Constructor for exception io.github.cvc5.CVC5ApiException
CVC5ApiOptionException - Exception in io.github.cvc5
CVC5ApiOptionException(String) - Constructor for exception io.github.cvc5.CVC5ApiOptionException
CVC5ApiRecoverableException - Exception in io.github.cvc5
CVC5ApiRecoverableException(String) - Constructor for exception io.github.cvc5.CVC5ApiRecoverableException
CVC5ParserException - Exception in io.github.cvc5
CVC5ParserException(String) - Constructor for exception io.github.cvc5.CVC5ParserException

D

Datatype - Class in io.github.cvc5: A cvc5 datatype.
Datatype.ConstIterator - Class in io.github.cvc5
DatatypeConstructor - Class in io.github.cvc5: A cvc5 datatype constructor.
DatatypeConstructor.ConstIterator - Class in io.github.cvc5
DatatypeConstructorDecl - Class in io.github.cvc5: A cvc5 datatype constructor declaration.
DatatypeDecl - Class in io.github.cvc5: A cvc5 datatype declaration.
DatatypeDecl() - Constructor for class io.github.cvc5.DatatypeDecl: Null datatypeDecl
DatatypeSelector - Class in io.github.cvc5: A cvc5 datatype selector.
declareDatatype(String, DatatypeConstructorDecl[]) - Method in class io.github.cvc5.Solver: Create datatype sort.
declareFun(String, Sort[], Sort) - Method in class io.github.cvc5.Solver: Declare n-ary function symbol.
declareFun(String, Sort[], Sort, boolean) - Method in class io.github.cvc5.Solver: Declare n-ary function symbol.
declareOracleFun(String, Sort[], Sort, IOracle) - Method in class io.github.cvc5.Solver: Declare an oracle function with reference to an implementation.
declarePool(String, Sort, Term[]) - Method in class io.github.cvc5.Solver: Declare a symbolic pool of terms with the given initial value.
declareSepHeap(Sort, Sort) - Method in class io.github.cvc5.Solver: When using separation logic, this sets the location sort and the datatype sort to the given ones.
declareSort(String, int) - Method in class io.github.cvc5.Solver: Declare uninterpreted sort.
declareSort(String, int, boolean) - Method in class io.github.cvc5.Solver: Declare uninterpreted sort.
declareSygusVar(String, Sort) - Method in class io.github.cvc5.Solver: Append symbol to the current list of universal variables.
defineFun(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver: Define n-ary function in the current context.
defineFun(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver: Define n-ary function.
defineFunRec(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver: Define recursive function in the current context.
defineFunRec(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver: Define recursive function.
defineFunRec(Term, Term[], Term) - Method in class io.github.cvc5.Solver: Define recursive function in the current context.
defineFunRec(Term, Term[], Term, boolean) - Method in class io.github.cvc5.Solver: Define recursive function.
defineFunsRec(Term[], Term[][], Term[]) - Method in class io.github.cvc5.Solver: Define recursive functions in the current context.
defineFunsRec(Term[], Term[][], Term[], boolean) - Method in class io.github.cvc5.Solver: Define recursive functions.
deletePointer(long) - Method in class io.github.cvc5.Command
deletePointer(long) - Method in class io.github.cvc5.Datatype
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructor
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
deletePointer(long) - Method in class io.github.cvc5.DatatypeDecl
deletePointer(long) - Method in class io.github.cvc5.DatatypeSelector
deletePointer(long) - Method in class io.github.cvc5.Grammar
deletePointer(long) - Method in class io.github.cvc5.InputParser
deletePointer(long) - Method in class io.github.cvc5.Op
deletePointer(long) - Method in class io.github.cvc5.OptionInfo
deletePointer() - Method in class io.github.cvc5.Proof
deletePointer(long) - Method in class io.github.cvc5.Proof
deletePointer(long) - Method in class io.github.cvc5.Result
deletePointer(long) - Method in class io.github.cvc5.Solver
deletePointer(long) - Method in class io.github.cvc5.Sort
deletePointer(long) - Method in class io.github.cvc5.Stat
deletePointer(long) - Method in class io.github.cvc5.Statistics
deletePointer(long) - Method in class io.github.cvc5.SymbolManager
deletePointer(long) - Method in class io.github.cvc5.SynthResult
deletePointer(long) - Method in class io.github.cvc5.Term
deletePointer(long) - Method in class io.github.cvc5.TermManager
deletePointers() - Static method in class io.github.cvc5.Context: Delete all cpp pointers for terms, sorts, etc
done() - Method in class io.github.cvc5.InputParser
doubleValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a double.

E

eqTerm(Term) - Method in class io.github.cvc5.Term: Equality.
equals(Object) - Method in class io.github.cvc5.Datatype: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeConstructor: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeConstructorDecl: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeDecl: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeSelector: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Grammar: Referential equality operator.
equals(Object) - Method in class io.github.cvc5.Op: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Pair
equals(Object) - Method in class io.github.cvc5.Proof: Referential equality operator.
equals(Object) - Method in class io.github.cvc5.Result: Operator overloading for equality of two results.
equals(Object) - Method in class io.github.cvc5.Solver
equals(Object) - Method in class io.github.cvc5.Sort: Comparison for structural equality.
equals(Object) - Method in class io.github.cvc5.SymbolManager
equals(Object) - Method in class io.github.cvc5.SynthResult: Operator overloading for equality of two synthesis results.
equals(Object) - Method in class io.github.cvc5.Term: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.TermManager
equals(Object) - Method in class io.github.cvc5.Triplet

F

findSynth(FindSynthTarget) - Method in class io.github.cvc5.Solver: Find a target term of interest using sygus enumeration, with no provided grammar.
findSynth(FindSynthTarget, Grammar) - Method in class io.github.cvc5.Solver: Find a target term of interest using sygus enumeration with a provided grammar.
findSynthNext() - Method in class io.github.cvc5.Solver: Try to find a next target term of interest using sygus enumeration.
FindSynthTarget - Enum in io.github.cvc5.modes
first - Variable in class io.github.cvc5.Pair
first - Variable in class io.github.cvc5.Triplet
fromInt(int) - Static method in enum io.github.cvc5.Kind
fromInt(int) - Static method in enum io.github.cvc5.modes.BlockModelsMode
fromInt(int) - Static method in enum io.github.cvc5.modes.FindSynthTarget
fromInt(int) - Static method in enum io.github.cvc5.modes.InputLanguage
fromInt(int) - Static method in enum io.github.cvc5.modes.LearnedLitType
fromInt(int) - Static method in enum io.github.cvc5.modes.OptionCategory
fromInt(int) - Static method in enum io.github.cvc5.modes.ProofComponent
fromInt(int) - Static method in enum io.github.cvc5.modes.ProofFormat
fromInt(int) - Static method in enum io.github.cvc5.ProofRewriteRule
fromInt(int) - Static method in enum io.github.cvc5.ProofRule
fromInt(int) - Static method in enum io.github.cvc5.RoundingMode
fromInt(int) - Static method in enum io.github.cvc5.SkolemId
fromInt(int) - Static method in enum io.github.cvc5.SortKind
fromInt(int) - Static method in enum io.github.cvc5.UnknownExplanation

G

get(int) - Method in class io.github.cvc5.Op: Get the index at position i.
get(String) - Method in class io.github.cvc5.Statistics: Retrieve the statistic with the given name.
getAbduct(Term) - Method in class io.github.cvc5.Solver: Get an abduct.
getAbduct(Term, Grammar) - Method in class io.github.cvc5.Solver: Get an abduct.
getAbductNext() - Method in class io.github.cvc5.Solver: Get the next abduct.
getAbstractedKind() - Method in class io.github.cvc5.Sort
getAliases() - Method in class io.github.cvc5.OptionInfo
getArguments() - Method in class io.github.cvc5.Proof
getArrayElementSort() - Method in class io.github.cvc5.Sort
getArrayIndexSort() - Method in class io.github.cvc5.Sort
getAssertions() - Method in class io.github.cvc5.Solver: Get the list of asserted formulas.
getBagElementSort() - Method in class io.github.cvc5.Sort
getBaseInfo() - Method in class io.github.cvc5.OptionInfo
getBitVectorSize() - Method in class io.github.cvc5.Sort
getBitVectorValue() - Method in class io.github.cvc5.Term: Asserts isBitVectorValue().
getBitVectorValue(int) - Method in class io.github.cvc5.Term: Get the string representation of a bit-vector value.
getBooleanSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.
getBooleanSort() - Method in class io.github.cvc5.TermManager: Get the Boolean sort.
getBooleanValue() - Method in class io.github.cvc5.Term: Asserts isBooleanValue().
getCardinalityConstraint() - Method in class io.github.cvc5.Term: Asserts isCardinalityConstraint().
getChild(int) - Method in class io.github.cvc5.Term: Get the child term at a given index.
getChildren() - Method in class io.github.cvc5.Proof
getCodomainSort() - Method in class io.github.cvc5.DatatypeSelector
getCommandName() - Method in class io.github.cvc5.Command: Get the name for this command, e.g.
getConstArrayBase() - Method in class io.github.cvc5.Term: Asserts isConstArray().
getConstructor(int) - Method in class io.github.cvc5.Datatype: Get the datatype constructor at a given index.
getConstructor(String) - Method in class io.github.cvc5.Datatype: Get the datatype constructor with the given name.
getCurrentValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
getDatatype() - Method in class io.github.cvc5.Sort
getDatatypeArity() - Method in class io.github.cvc5.Sort
getDatatypeConstructorArity() - Method in class io.github.cvc5.Sort
getDatatypeConstructorCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeConstructorDomainSorts() - Method in class io.github.cvc5.Sort
getDatatypeSelectorCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeSelectorDomainSort() - Method in class io.github.cvc5.Sort
getDatatypeTesterCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeTesterDomainSort() - Method in class io.github.cvc5.Sort
getDeclaredSorts() - Method in class io.github.cvc5.SymbolManager: Get the list of sorts that have been declared via `declare-sort` commands.
getDeclaredTerms() - Method in class io.github.cvc5.SymbolManager: Get the list of terms that have been declared via `declare-fun` and `declare-const`.
getDefaultValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
getDifficulty() - Method in class io.github.cvc5.Solver: Get a difficulty estimate for an asserted formula.
getDouble() - Method in class io.github.cvc5.Stat: Return the double value.
getFiniteFieldSize() - Method in class io.github.cvc5.Sort
getFiniteFieldValue() - Method in class io.github.cvc5.Term: Get the string representation of a finite field value.
getFloatingPointExponentSize() - Method in class io.github.cvc5.Sort
getFloatingPointSignificandSize() - Method in class io.github.cvc5.Sort
getFloatingPointValue() - Method in class io.github.cvc5.Term: Asserts isFloatingPointValue().
getFunctionArity() - Method in class io.github.cvc5.Sort
getFunctionCodomainSort() - Method in class io.github.cvc5.Sort
getFunctionDomainSorts() - Method in class io.github.cvc5.Sort
getHistogram() - Method in class io.github.cvc5.Stat: Return the histogram value.
getId() - Method in class io.github.cvc5.Term
getInfo(String) - Method in class io.github.cvc5.Solver: Get info from the solver.
getInstantiatedParameters() - Method in class io.github.cvc5.Sort: Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see Sort.instantiate(Sort[])).
getInstantiatedTerm(Sort) - Method in class io.github.cvc5.DatatypeConstructor: Get the constructor term of this datatype constructor whose return type is retSort.
getInstantiations() - Method in class io.github.cvc5.Solver: Get a string that contains information about all instantiations made by the quantifiers module.
getInt() - Method in class io.github.cvc5.Stat: Return the integer value.
getIntegerSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.
getIntegerSort() - Method in class io.github.cvc5.TermManager: Get the integer sort.
getIntegerSort(long) - Method in class io.github.cvc5.TermManager
getIntegerValue() - Method in class io.github.cvc5.Term: Asserts isIntegerValue().
getInterpolant(Term) - Method in class io.github.cvc5.Solver: Get an interpolant.
getInterpolant(Term, Grammar) - Method in class io.github.cvc5.Solver: Get an interpolant.
getInterpolantNext() - Method in class io.github.cvc5.Solver: Get the next interpolant.
getKind() - Method in class io.github.cvc5.Op
getKind() - Method in class io.github.cvc5.Sort
getKind() - Method in class io.github.cvc5.Term
getLearnedLiterals() - Method in class io.github.cvc5.Solver: Get a list of input literals that are entailed by the current set of assertions.
getLearnedLiterals(LearnedLitType) - Method in class io.github.cvc5.Solver: Get a list of literals that are entailed by the current set of assertions.
getLogic() - Method in class io.github.cvc5.Solver: Get the logic set the solver.
getLogic() - Method in class io.github.cvc5.SymbolManager
getMaximum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
getMinimum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
getModel(Sort[], Term[]) - Method in class io.github.cvc5.Solver: Get the model SMT-LIB: ( get-model ) Requires to enable option produce-models.
getModelDomainElements(Sort) - Method in class io.github.cvc5.Solver: Get the domain elements of uninterpreted sort s in the current model.
getModes() - Method in class io.github.cvc5.OptionInfo.ModeInfo
getName() - Method in class io.github.cvc5.AbstractPlugin: Get the name of the plugin (for debugging).
getName() - Method in class io.github.cvc5.Datatype
getName() - Method in class io.github.cvc5.DatatypeConstructor
getName() - Method in class io.github.cvc5.DatatypeDecl
getName() - Method in class io.github.cvc5.DatatypeSelector
getName() - Method in class io.github.cvc5.OptionInfo
getNamedTerms() - Method in class io.github.cvc5.SymbolManager: Get a mapping from terms to names that have been given to them via the :named attribute.
getNullableElementSort() - Method in class io.github.cvc5.Sort
getNumChildren() - Method in class io.github.cvc5.Term
getNumConstructors() - Method in class io.github.cvc5.Datatype
getNumConstructors() - Method in class io.github.cvc5.DatatypeDecl: Get the number of constructors (so far) for this Datatype declaration.
getNumIndices() - Method in class io.github.cvc5.Op
getNumIndicesForSkolemId(SkolemId) - Method in class io.github.cvc5.TermManager: Get the number of indices for a given skolem id.
getNumSelectors() - Method in class io.github.cvc5.DatatypeConstructor
getOp() - Method in class io.github.cvc5.Term
getOption(String) - Method in class io.github.cvc5.Solver: Get the value of a given option.
getOptionInfo(String) - Method in class io.github.cvc5.Solver: Get some information about the given option.
getOptionNames() - Method in class io.github.cvc5.Solver: Get all option names that can be used with Solver.setOption(String, String), Solver.getOption(String) and Solver.getOptionInfo(String).
getPairs(Pair<K, ? extends AbstractPointer>[]) - Static method in class io.github.cvc5.Utils
getParameters() - Method in class io.github.cvc5.Datatype
getPointer() - Method in class io.github.cvc5.Proof
getPointers(IPointer[]) - Static method in class io.github.cvc5.Utils
getPointers(IPointer[][]) - Static method in class io.github.cvc5.Utils
getProof() - Method in class io.github.cvc5.Solver: Get refutation proof for the most recent call to checkSat.
getProof(ProofComponent) - Method in class io.github.cvc5.Solver: Get a proof associated with the most recent call to checkSat.
getProofs(long[]) - Static method in class io.github.cvc5.Utils
getQuantifierElimination(Term) - Method in class io.github.cvc5.Solver: Do quantifier elimination.
getQuantifierEliminationDisjunct(Term) - Method in class io.github.cvc5.Solver: Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.
getRational(String) - Static method in class io.github.cvc5.Utils: Convert a rational string a/b to a pair of BigIntegers
getRational(Pair<BigInteger, BigInteger>) - Static method in class io.github.cvc5.Utils: Convert a pair of BigIntegers to a rational string a/b
getRealAlgebraicNumberDefiningPolynomial(Term) - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealAlgebraicNumberLowerBound() - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealAlgebraicNumberUpperBound() - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealOrIntegerValueSign() - Method in class io.github.cvc5.Term: Get integer or real value sign.
getRealSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.
getRealSort() - Method in class io.github.cvc5.TermManager: Get the real sort.
getRealValue() - Method in class io.github.cvc5.Term: Asserts isRealValue().
getRegExpSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.
getRegExpSort() - Method in class io.github.cvc5.TermManager: Get the regular expression sort.
getResult() - Method in class io.github.cvc5.Proof
getRewriteRule() - Method in class io.github.cvc5.Proof
getRoundingModeSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRoundingModeSort(). It will be removed in a future release.
getRoundingModeSort() - Method in class io.github.cvc5.TermManager: Get the floating-point rounding mode sort.
getRoundingModeValue() - Method in class io.github.cvc5.Term: Asserts isRoundingModeValue().
getRule() - Method in class io.github.cvc5.Proof
getSelector(String) - Method in class io.github.cvc5.Datatype: Get the datatype constructor with the given name.
getSelector(int) - Method in class io.github.cvc5.DatatypeConstructor: Get the DatatypeSelector at the given index
getSelector(String) - Method in class io.github.cvc5.DatatypeConstructor: Get the datatype selector with the given name.
getSequenceElementSort() - Method in class io.github.cvc5.Sort
getSequenceValue() - Method in class io.github.cvc5.Term: Asserts isSequenceValue().
getSetByUser() - Method in class io.github.cvc5.OptionInfo
getSetElementSort() - Method in class io.github.cvc5.Sort
getSetValue() - Method in class io.github.cvc5.Term: Asserts isSetValue().
getSkolemId() - Method in class io.github.cvc5.Term: Get skolem identifier of this term.
getSkolemIndices() - Method in class io.github.cvc5.Term: Get the skolem indices of this term.
getSolver() - Method in class io.github.cvc5.InputParser
getSort() - Method in class io.github.cvc5.Term
getSorts(long[]) - Static method in class io.github.cvc5.Utils
getStatistics() - Method in class io.github.cvc5.Solver: Get a snapshot of the current state of the statistic values of this solver.
getStatistics() - Method in class io.github.cvc5.TermManager: Get a snapshot of the current state of the statistic values of this term manager.
getString() - Method in class io.github.cvc5.Stat: Return the string value.
getStringSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getStringSort(). It will be removed in a future release.
getStringSort() - Method in class io.github.cvc5.TermManager: Get the string sort.
getStringValue() - Method in class io.github.cvc5.Term
getSygusAssumptions() - Method in class io.github.cvc5.Solver: Get the list of sygus assumptions.
getSygusConstraints() - Method in class io.github.cvc5.Solver: Get the list of sygus constraints.
getSymbol() - Method in class io.github.cvc5.Sort
getSymbol() - Method in class io.github.cvc5.Term: Asserts hasSymbol().
getSymbolManager() - Method in class io.github.cvc5.InputParser
getSynthSolution(Term) - Method in class io.github.cvc5.Solver: Get the synthesis solution of the given term.
getSynthSolutions(Term[]) - Method in class io.github.cvc5.Solver: Get the synthesis solutions of the given terms.
getTerm() - Method in class io.github.cvc5.DatatypeConstructor: Get the constructor term of this datatype constructor.
getTerm() - Method in class io.github.cvc5.DatatypeSelector: Get the selector term of this datatype selector.
getTermManager() - Method in class io.github.cvc5.AbstractPlugin: Get the associated term manager instance
getTermManager() - Method in class io.github.cvc5.Solver: Get the associated term manager instance
getTerms(long[]) - Static method in class io.github.cvc5.Utils
getTesterTerm() - Method in class io.github.cvc5.DatatypeConstructor: Get the tester term of this datatype constructor.
getTimeoutCore() - Method in class io.github.cvc5.Solver: Get a timeout core, which computes a subset of the current assertions that cause a timeout.
getTimeoutCoreAssuming(Term[]) - Method in class io.github.cvc5.Solver: Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions.
getTupleLength() - Method in class io.github.cvc5.Sort
getTupleSorts() - Method in class io.github.cvc5.Sort
getTupleValue() - Method in class io.github.cvc5.Term: Asserts isTupleValue().
getUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort: Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
getUninterpretedSortConstructorArity() - Method in class io.github.cvc5.Sort
getUninterpretedSortValue() - Method in class io.github.cvc5.Term: Asserts isUninterpretedSortValue().
getUnknownExplanation() - Method in class io.github.cvc5.Result: Get an explanation for an unknown query result.
getUnsatAssumptions() - Method in class io.github.cvc5.Solver: Get the set of unsat ("failed") assumptions.
getUnsatCore() - Method in class io.github.cvc5.Solver: Get the unsatisfiable core.
getUnsatCoreLemmas() - Method in class io.github.cvc5.Solver: Get the lemmas used to derive unsatisfiability.
getUpdaterTerm() - Method in class io.github.cvc5.DatatypeSelector: Get the updater term of this datatype selector.
getValue() - Method in enum io.github.cvc5.Kind
getValue() - Method in enum io.github.cvc5.modes.BlockModelsMode
getValue() - Method in enum io.github.cvc5.modes.FindSynthTarget
getValue() - Method in enum io.github.cvc5.modes.InputLanguage
getValue() - Method in enum io.github.cvc5.modes.LearnedLitType
getValue() - Method in enum io.github.cvc5.modes.OptionCategory
getValue() - Method in enum io.github.cvc5.modes.ProofComponent
getValue() - Method in enum io.github.cvc5.modes.ProofFormat
getValue() - Method in enum io.github.cvc5.ProofRewriteRule
getValue() - Method in enum io.github.cvc5.ProofRule
getValue() - Method in enum io.github.cvc5.RoundingMode
getValue() - Method in enum io.github.cvc5.SkolemId
getValue(Term) - Method in class io.github.cvc5.Solver: Get the value of the given term in the current model.
getValue(Term[]) - Method in class io.github.cvc5.Solver: Get the values of the given terms in the current model.
getValue() - Method in enum io.github.cvc5.SortKind
getValue() - Method in enum io.github.cvc5.UnknownExplanation
getValueSepHeap() - Method in class io.github.cvc5.Solver: When using separation logic, obtain the term for the heap.
getValueSepNil() - Method in class io.github.cvc5.Solver: When using separation logic, obtain the term for nil.
getVersion() - Method in class io.github.cvc5.Solver: Get a string representation of the version of this solver.
Grammar - Class in io.github.cvc5: A Sygus Grammar.
Grammar(Grammar) - Constructor for class io.github.cvc5.Grammar

H

hashCode() - Method in class io.github.cvc5.Datatype: Get the hash value of a datatype.
hashCode() - Method in class io.github.cvc5.DatatypeConstructor: Get the hash value of a datatype constructor.
hashCode() - Method in class io.github.cvc5.DatatypeConstructorDecl: Get the hash value of a datatype constructor declaration.
hashCode() - Method in class io.github.cvc5.DatatypeDecl: Get the hash value of a datatype declaration.
hashCode() - Method in class io.github.cvc5.DatatypeSelector: Get the hash value of a datatype selector.
hashCode() - Method in class io.github.cvc5.Grammar: Get the hash value of a grammar.
hashCode() - Method in class io.github.cvc5.Op: Get the hash value of an operator.
hashCode() - Method in class io.github.cvc5.Proof: Get the hash value of a proof.
hashCode() - Method in class io.github.cvc5.Result: Get the hash value of a result.
hashCode() - Method in class io.github.cvc5.Sort: Get the hash value of a sort.
hashCode() - Method in class io.github.cvc5.SynthResult: Get the hash value of a synthesis result.
hashCode() - Method in class io.github.cvc5.Term: Get the hash value of a term.
hasNext() - Method in class io.github.cvc5.Datatype.ConstIterator
hasNext() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
hasNext() - Method in class io.github.cvc5.Statistics.ConstIterator
hasNext() - Method in class io.github.cvc5.Term.ConstIterator
hasNoSolution() - Method in class io.github.cvc5.SynthResult
hasOp() - Method in class io.github.cvc5.Term
hasSolution() - Method in class io.github.cvc5.SynthResult
hasSymbol() - Method in class io.github.cvc5.Sort
hasSymbol() - Method in class io.github.cvc5.Term

I

impTerm(Term) - Method in class io.github.cvc5.Term: Boolean implication.
InputLanguage - Enum in io.github.cvc5.modes
InputParser - Class in io.github.cvc5: This class is the main interface for retrieving commands and expressions from an input using a parser.
InputParser(Solver, SymbolManager) - Constructor for class io.github.cvc5.InputParser: Construct an input parser
InputParser(Solver) - Constructor for class io.github.cvc5.InputParser: Construct an input parser with an initially empty symbol manager.
instantiate(Sort[]) - Method in class io.github.cvc5.Sort: Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
intValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as as int.
invoke(Solver, SymbolManager) - Method in class io.github.cvc5.Command: Invoke the command on the solver and symbol manager sm and return any resulting output as a string.
io.github.cvc5 - package io.github.cvc5
io.github.cvc5.modes - package io.github.cvc5.modes
IOracle - Interface in io.github.cvc5
isAbstract() - Method in class io.github.cvc5.Sort: Determine if this is an abstract sort.
isArray() - Method in class io.github.cvc5.Sort: Determine if this is an array sort.
isBag() - Method in class io.github.cvc5.Sort: Determine if this is a Bag sort.
isBitVector() - Method in class io.github.cvc5.Sort: Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).
isBitVectorValue() - Method in class io.github.cvc5.Term
isBoolean() - Method in class io.github.cvc5.Sort: Determine if this is the Boolean sort (SMT-LIB: Bool).
isBooleanValue() - Method in class io.github.cvc5.Term
isCardinalityConstraint() - Method in class io.github.cvc5.Term
isCodatatype() - Method in class io.github.cvc5.Datatype
isConstArray() - Method in class io.github.cvc5.Term
isDatatype() - Method in class io.github.cvc5.Sort: Determine if this is a datatype sort.
isDatatypeConstructor() - Method in class io.github.cvc5.Sort: Determine if this is a datatype constructor sort.
isDatatypeSelector() - Method in class io.github.cvc5.Sort: Determine if this is a datatype selector sort.
isDatatypeTester() - Method in class io.github.cvc5.Sort: Determine if this is a datatype tester sort.
isDatatypeUpdater() - Method in class io.github.cvc5.Sort: Determine if this is a datatype updater sort.
isDefault() - Method in class io.github.cvc5.Stat: Does this value hold the default value?
isDouble() - Method in class io.github.cvc5.Stat: Is this value a double?
isFinite() - Method in class io.github.cvc5.Datatype
isFiniteField() - Method in class io.github.cvc5.Sort: Determine if this is a finite field sort (SMT-LIB: (_ FiniteField i)).
isFiniteFieldValue() - Method in class io.github.cvc5.Term
isFloatingPoint() - Method in class io.github.cvc5.Sort: Determine if this is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)).
isFloatingPointNaN() - Method in class io.github.cvc5.Term
isFloatingPointNegInf() - Method in class io.github.cvc5.Term
isFloatingPointNegZero() - Method in class io.github.cvc5.Term
isFloatingPointPosInf() - Method in class io.github.cvc5.Term
isFloatingPointPosZero() - Method in class io.github.cvc5.Term
isFloatingPointValue() - Method in class io.github.cvc5.Term
isFunction() - Method in class io.github.cvc5.Sort: Determine if this is a function sort.
isHistogram() - Method in class io.github.cvc5.Stat: Is this value a histogram?
isIndexed() - Method in class io.github.cvc5.Op
isInstantiated() - Method in class io.github.cvc5.Sort: Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
isInt() - Method in class io.github.cvc5.Stat: Is this value an integer?
isInteger() - Method in class io.github.cvc5.Sort: Determine if this is the integer sort (SMT-LIB: Int).
isIntegerValue() - Method in class io.github.cvc5.Term
isInternal() - Method in class io.github.cvc5.Stat: Is this value intended for internal use only?
isLogicSet() - Method in class io.github.cvc5.Solver: Is logic set? Returns whether we called setLogic yet for this solver.
isLogicSet() - Method in class io.github.cvc5.SymbolManager
isModelCoreSymbol(Term) - Method in class io.github.cvc5.Solver: This returns false if the model value of free constant v was not essential for showing the satisfiability of the last call to Solver.checkSat() using the current model.
isNull() - Method in class io.github.cvc5.Command
isNull() - Method in class io.github.cvc5.Datatype
isNull() - Method in class io.github.cvc5.DatatypeConstructor
isNull() - Method in class io.github.cvc5.DatatypeConstructorDecl
isNull() - Method in class io.github.cvc5.DatatypeDecl
isNull() - Method in class io.github.cvc5.DatatypeSelector
isNull() - Method in class io.github.cvc5.Grammar: Determine if this is the null grammar.
isNull() - Method in class io.github.cvc5.Op
isNull() - Method in class io.github.cvc5.Result
isNull() - Method in class io.github.cvc5.Sort: Determine if this is the null sort.
isNull() - Method in class io.github.cvc5.SynthResult
isNull() - Method in class io.github.cvc5.Term
isNullable() - Method in class io.github.cvc5.Sort: Determine if this a nullable sort.
isParametric() - Method in class io.github.cvc5.Datatype
isParametric() - Method in class io.github.cvc5.DatatypeDecl: Determine if this datatype declaration is parametric.
isPredicate() - Method in class io.github.cvc5.Sort: Determine if this is a predicate sort.
isReal() - Method in class io.github.cvc5.Sort: Determine if this is the real sort (SMT-LIB: Real).
isRealAlgebraicNumber() - Method in class io.github.cvc5.Term
isRealValue() - Method in class io.github.cvc5.Term
isRecord() - Method in class io.github.cvc5.Datatype
isRecord() - Method in class io.github.cvc5.Sort: Determine if this is a record sort.
isRegExp() - Method in class io.github.cvc5.Sort: Determine if this is the regular expression sort (SMT-LIB: RegLan).
isRoundingMode() - Method in class io.github.cvc5.Sort: Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).
isRoundingModeValue() - Method in class io.github.cvc5.Term
isSat() - Method in class io.github.cvc5.Result
isSequence() - Method in class io.github.cvc5.Sort: Determine if this is a Sequence sort.
isSequenceValue() - Method in class io.github.cvc5.Term
isSet() - Method in class io.github.cvc5.Sort: Determine if this is a Set sort.
isSetValue() - Method in class io.github.cvc5.Term
isSkolem() - Method in class io.github.cvc5.Term
isString() - Method in class io.github.cvc5.Sort: Determine if this is the string sort (SMT-LIB: String)..
isString() - Method in class io.github.cvc5.Stat: Is this value a string?
isStringValue() - Method in class io.github.cvc5.Term
isTuple() - Method in class io.github.cvc5.Datatype
isTuple() - Method in class io.github.cvc5.Sort: Determine if this a tuple sort.
isTupleValue() - Method in class io.github.cvc5.Term
isUninterpretedSort() - Method in class io.github.cvc5.Sort: Determine if this is an uninterpreted sort.
isUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort: Determine if this is an uninterpreted sort constructor.
isUninterpretedSortValue() - Method in class io.github.cvc5.Term
isUnknown() - Method in class io.github.cvc5.Result
isUnknown() - Method in class io.github.cvc5.SynthResult
isUnsat() - Method in class io.github.cvc5.Result
isWellFounded() - Method in class io.github.cvc5.Datatype: Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
iterator() - Method in class io.github.cvc5.Datatype
iterator() - Method in class io.github.cvc5.DatatypeConstructor
iterator(boolean, boolean) - Method in class io.github.cvc5.Statistics
iterator() - Method in class io.github.cvc5.Statistics
iterator() - Method in class io.github.cvc5.Term
iteTerm(Term, Term) - Method in class io.github.cvc5.Term: If-then-else with this term as the Boolean condition.

K

Kind - Enum in io.github.cvc5

L

LearnedLitType - Enum in io.github.cvc5.modes
LIBPATH_IN_JAR - Static variable in class io.github.cvc5.Utils
loadLibraries() - Static method in class io.github.cvc5.Utils: Load cvc5 native libraries.
loadLibraryFromJar(Path, String, String) - Static method in class io.github.cvc5.Utils: Loads a native library from a specified path within a JAR file and loads it into the JVM.

M

mkAbstractSort(SortKind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.
mkAbstractSort(SortKind) - Method in class io.github.cvc5.TermManager: Create an abstract sort.
mkArraySort(Sort, Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkArraySort(Sort, Sort). It will be removed in a future release.
mkArraySort(Sort, Sort) - Method in class io.github.cvc5.TermManager: Create an array sort.
mkBagSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.
mkBagSort(Sort) - Method in class io.github.cvc5.TermManager: Create a bag sort.
mkBitVector(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.
mkBitVector(int, long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.
mkBitVector(int, String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int, String, int). It will be removed in a future release.
mkBitVector(int) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of given size and value = 0.
mkBitVector(int, long) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of given size and value.
mkBitVector(int, String, int) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
mkBitVectorSort(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVectorSort(int). It will be removed in a future release.
mkBitVectorSort(int) - Method in class io.github.cvc5.TermManager: Create a bit-vector sort.
mkBoolean(boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBoolean(boolean). It will be removed in a future release.
mkBoolean(boolean) - Method in class io.github.cvc5.TermManager: Create a Boolean constant.
mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.
mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.TermManager: Create a cardinality constraint for an uninterpreted sort.
mkConst(Sort, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.
mkConst(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConst(Sort). It will be removed in a future release.
mkConst(Sort, String) - Method in class io.github.cvc5.TermManager: Create a free constant.
mkConst(Sort) - Method in class io.github.cvc5.TermManager: Create a free constant with a default symbol name.
mkConstArray(Sort, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.
mkConstArray(Sort, Term) - Method in class io.github.cvc5.TermManager: Create a constant array with the provided constant value stored at every index
mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.
mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.TermManager: Create a datatype constructor declaration.
mkDatatypeDecl(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.
mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.
mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
mkDatatypeDecl(String) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeSort(DatatypeDecl). It will be removed in a future release.
mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.TermManager: Create a datatype sort.
mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeSorts(DatatypeDecl[]). It will be removed in a future release.
mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.TermManager: Create a vector of datatype sorts.
mkEmptyBag(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.
mkEmptyBag(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing an empty bag of the given sort.
mkEmptySequence(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.
mkEmptySequence(Sort) - Method in class io.github.cvc5.TermManager: Create an empty sequence of the given element sort.
mkEmptySet(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.
mkEmptySet(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing an empty set of the given sort.
mkFalse() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFalse(). It will be removed in a future release.
mkFalse() - Method in class io.github.cvc5.TermManager: Create a Boolean false constant.
mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.
mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.TermManager: Create a finite field constant in a given field and for a given value.
mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.
mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.TermManager: Create a finite field sort.
mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.
mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, Term). It will be removed in a future release.
mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.TermManager: Create a floating-point value from a bit-vector given in IEEE-754 format.
mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.
mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.TermManager: Create a not-a-number floating-point constant (SMT-LIB: NaN).
mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.
mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.TermManager: Create a negative infinity floating-point constant (SMT-LIB: -oo).
mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.
mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.TermManager: Create a negative zero floating-point constant (SMT-LIB: -zero).
mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.
mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.TermManager: Create a positive infinity floating-point constant (SMT-LIB: +oo).
mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.
mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.TermManager: Create a positive zero floating-point constant (SMT-LIB: +zero).
mkFloatingPointSort(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.
mkFloatingPointSort(int, int) - Method in class io.github.cvc5.TermManager: Create a floating-point sort.
mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFunctionSort(Sort, Sort). It will be removed in a future release.
mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFunctionSort(Sort[], Sort). It will be removed in a future release.
mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.TermManager: Create function sort.
mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.TermManager: Create function sort.
mkGrammar(Term[], Term[]) - Method in class io.github.cvc5.Solver: Create a Sygus grammar.
mkInteger(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.
mkInteger(long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkInteger(long). It will be removed in a future release.
mkInteger(String) - Method in class io.github.cvc5.TermManager: Create an integer constant from a string.
mkInteger(long) - Method in class io.github.cvc5.TermManager: Create an integer constant from a C++ int.
mkNullableIsNull(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.
mkNullableIsNull(Term) - Method in class io.github.cvc5.TermManager: Create a null tester for a nullable term.
mkNullableIsSome(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.
mkNullableIsSome(Term) - Method in class io.github.cvc5.TermManager: Create a some tester for a nullable term.
mkNullableLift(Kind, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.
mkNullableLift(Kind, Term[]) - Method in class io.github.cvc5.TermManager: Create a term that lifts kind to nullable terms.
mkNullableNull(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.
mkNullableNull(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing a null value of the given sort.
mkNullableSome(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.
mkNullableSome(Term) - Method in class io.github.cvc5.TermManager: Create a nullable some term.
mkNullableSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.
mkNullableSort(Sort) - Method in class io.github.cvc5.TermManager: Create a nullable sort.
mkNullableVal(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.
mkNullableVal(Term) - Method in class io.github.cvc5.TermManager: Create a selector for nullable term.
mkOp(Kind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.
mkOp(Kind, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.
mkOp(Kind, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int). It will be removed in a future release.
mkOp(Kind, int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int, int). It will be removed in a future release.
mkOp(Kind, int[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int[]). It will be removed in a future release.
mkOp(Kind) - Method in class io.github.cvc5.TermManager: Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).
mkOp(Kind, String) - Method in class io.github.cvc5.TermManager: Create operator of kind: Kind.DIVISIBLE (to support arbitrary precision integers) See enum Kind for a description of the parameters.
mkOp(Kind, int) - Method in class io.github.cvc5.TermManager: 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.
mkOp(Kind, int, int) - Method in class io.github.cvc5.TermManager: 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.
mkOp(Kind, int[]) - Method in class io.github.cvc5.TermManager: Create operator of Kind: TUPLE_PROJECT See enum Kind for a description of the parameters.
mkParamSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.
mkParamSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkParamSort(). It will be removed in a future release.
mkParamSort(String) - Method in class io.github.cvc5.TermManager: Create a sort parameter.
mkParamSort() - Method in class io.github.cvc5.TermManager: Create a sort parameter.
mkPi() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkPi(). It will be removed in a future release.
mkPi() - Method in class io.github.cvc5.TermManager: Create a constant representing the number Pi.
mkPredicateSort(Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.
mkPredicateSort(Sort[]) - Method in class io.github.cvc5.TermManager: Create a predicate sort.
mkReal(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.
mkReal(long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(long). It will be removed in a future release.
mkReal(long, long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(long, long). It will be removed in a future release.
mkReal(String) - Method in class io.github.cvc5.TermManager: Create a real constant from a string.
mkReal(long) - Method in class io.github.cvc5.TermManager: Create a real constant from an integer.
mkReal(long, long) - Method in class io.github.cvc5.TermManager: Create a real constant from a rational.
mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.
mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.TermManager: Create a record sort
mkRegexpAll() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.
mkRegexpAll() - Method in class io.github.cvc5.TermManager: Create a regular expression all (re.all) term.
mkRegexpAllchar() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.
mkRegexpAllchar() - Method in class io.github.cvc5.TermManager: Create a regular expression allchar (re.allchar) term.
mkRegexpNone() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.
mkRegexpNone() - Method in class io.github.cvc5.TermManager: Create a regular expression none (re.none) term.
mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.
mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.TermManager: Create a rounding mode constant.
mkSepEmp() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.
mkSepEmp() - Method in class io.github.cvc5.TermManager: Create a separation logic empty term.
mkSepNil(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.
mkSepNil(Sort) - Method in class io.github.cvc5.TermManager: Create a separation logic nil term.
mkSequenceSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.
mkSequenceSort(Sort) - Method in class io.github.cvc5.TermManager: Create a sequence sort.
mkSetSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.
mkSetSort(Sort) - Method in class io.github.cvc5.TermManager: Create a set sort.
mkSkolem(SkolemId, Term[]) - Method in class io.github.cvc5.TermManager: Create a skolem
mkString(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.
mkString(String, boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(String, boolean). It will be removed in a future release.
mkString(int[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(int[]). It will be removed in a future release.
mkString(String) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkString(String, boolean) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkString(int[]) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkTerm(Kind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.
mkTerm(Kind, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.
mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.
mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.
mkTerm(Kind, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.
mkTerm(Op) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op). It will be removed in a future release.
mkTerm(Op, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.
mkTerm(Op, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.
mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). It will be removed in a future release.
mkTerm(Op, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.
mkTerm(Kind) - Method in class io.github.cvc5.TermManager: Create 0-ary term of given kind.
mkTerm(Kind, Term) - Method in class io.github.cvc5.TermManager: Create a unary term of given kind.
mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.TermManager: Create binary term of given kind.
mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create ternary term of given kind.
mkTerm(Kind, Term[]) - Method in class io.github.cvc5.TermManager: Create n-ary term of given kind.
mkTerm(Op) - Method in class io.github.cvc5.TermManager: Create nullary term of given kind from a given operator.
mkTerm(Op, Term) - Method in class io.github.cvc5.TermManager: Create unary term of given kind from a given operator.
mkTerm(Op, Term, Term) - Method in class io.github.cvc5.TermManager: Create binary term of given kind from a given operator.
mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create ternary term of given kind from a given operator.
mkTerm(Op, Term[]) - Method in class io.github.cvc5.TermManager: Create n-ary term of given kind from a given operator.
mkTrue() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTrue(). It will be removed in a future release.
mkTrue() - Method in class io.github.cvc5.TermManager: Create a Boolean true constant.
mkTuple(Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.
mkTuple(Term[]) - Method in class io.github.cvc5.TermManager: Create a tuple term.
mkTupleSort(Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.
mkTupleSort(Sort[]) - Method in class io.github.cvc5.TermManager: Create a tuple sort.
mkUninterpretedSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.
mkUninterpretedSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSort(). It will be removed in a future release.
mkUninterpretedSort(String) - Method in class io.github.cvc5.TermManager: Create an uninterpreted sort.
mkUninterpretedSort() - Method in class io.github.cvc5.TermManager: Create an uninterpreted sort.
mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.
mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). It will be removed in a future release.
mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.TermManager: Create a sort constructor sort.
mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.TermManager: Create a sort constructor sort.
mkUniverseSet(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.
mkUniverseSet(Sort) - Method in class io.github.cvc5.TermManager: Create a universe set of the given sort.
mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.
mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). It will be removed in a future release.
mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.TermManager: Create an unresolved datatype sort.
mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.TermManager: Create an unresolved datatype sort.
mkVar(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.
mkVar(Sort, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.
mkVar(Sort) - Method in class io.github.cvc5.TermManager: Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
mkVar(Sort, String) - Method in class io.github.cvc5.TermManager: Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
ModeInfo(String, String, String[]) - Constructor for class io.github.cvc5.OptionInfo.ModeInfo

N

next() - Method in class io.github.cvc5.Datatype.ConstIterator
next() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
next() - Method in class io.github.cvc5.Statistics.ConstIterator
next() - Method in class io.github.cvc5.Term.ConstIterator
nextCommand() - Method in class io.github.cvc5.InputParser: Parse and return the next command.
nextTerm() - Method in class io.github.cvc5.InputParser: Parse and return the next term.
notifySatClause(Term) - Method in class io.github.cvc5.AbstractPlugin: Notify SAT clause, called when cl is a clause learned by the SAT solver.
notifyTheoryLemma(Term) - Method in class io.github.cvc5.AbstractPlugin: Notify theory lemma, called when lem is a theory lemma sent by a theory solver.
notTerm() - Method in class io.github.cvc5.Term: Boolean negation.
NumberInfo(T, T, T, T) - Constructor for class io.github.cvc5.OptionInfo.NumberInfo

O

Op - Class in io.github.cvc5: A cvc5 operator.
Op() - Constructor for class io.github.cvc5.Op: Null op
OptionCategory - Enum in io.github.cvc5.modes
OptionInfo - Class in io.github.cvc5: Holds some description about a particular option, including its name, its aliases, whether the option was explicitly set by the user, and information concerning its value.
OptionInfo.BaseInfo - Class in io.github.cvc5: Abstract class for OptionInfo values
OptionInfo.ModeInfo - Class in io.github.cvc5
OptionInfo.NumberInfo<T> - Class in io.github.cvc5: Default value, current value, minimum and maximum of a numeric value
OptionInfo.ValueInfo<T> - Class in io.github.cvc5: Has the current and the default value
OptionInfo.VoidInfo - Class in io.github.cvc5: Has no value information
orTerm(Term) - Method in class io.github.cvc5.Term: Boolean or.

P

Pair<K,V> - Class in io.github.cvc5
Pair(K, V) - Constructor for class io.github.cvc5.Pair
pointer - Variable in class io.github.cvc5.Proof
pop() - Method in class io.github.cvc5.Solver: Pop a level from the assertion stack.
pop(int) - Method in class io.github.cvc5.Solver: Pop (a) level(s) from the assertion stack.
Proof - Class in io.github.cvc5: A cvc5 Proof.
Proof() - Constructor for class io.github.cvc5.Proof: Null proof
ProofComponent - Enum in io.github.cvc5.modes
ProofFormat - Enum in io.github.cvc5.modes
ProofRewriteRule - Enum in io.github.cvc5
ProofRule - Enum in io.github.cvc5
proofToString(Proof) - Method in class io.github.cvc5.Solver: Prints a proof into a string with a slected proof format mode.
proofToString(Proof, ProofFormat) - Method in class io.github.cvc5.Solver: Prints a proof into a string with a slected proof format mode.
proofToString(Proof, ProofFormat, Map) - Method in class io.github.cvc5.Solver: Prints a proof into a string with a slected proof format mode.
push() - Method in class io.github.cvc5.Solver: Push a level to the assertion stack.
push(int) - Method in class io.github.cvc5.Solver: Push (a) level(s) to the assertion stack.

R

resetAssertions() - Method in class io.github.cvc5.Solver: Remove all assertions.
Result - Class in io.github.cvc5: Encapsulation of a three-valued solver result, with explanations.
Result() - Constructor for class io.github.cvc5.Result: Null result
RoundingMode - Enum in io.github.cvc5

S

second - Variable in class io.github.cvc5.Pair
second - Variable in class io.github.cvc5.Triplet
setFileInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser: Set the input for the given file.
setIncrementalStringInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser: Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
setInfo(String, String) - Method in class io.github.cvc5.Solver: Set info.
setLogic(String) - Method in class io.github.cvc5.Solver: Set logic.
setOption(String, String) - Method in class io.github.cvc5.Solver: Set option.
setStringInput(InputLanguage, String, String) - Method in class io.github.cvc5.InputParser: Set the input to the given concrete input string.
simplify(Term) - Method in class io.github.cvc5.Solver: Simplify a term or formula based on rewriting.
simplify(Term, boolean) - Method in class io.github.cvc5.Solver: Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.
SkolemId - Enum in io.github.cvc5
Solver - Class in io.github.cvc5: A cvc5 solver.
Solver() - Constructor for class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
Solver(TermManager) - Constructor for class io.github.cvc5.Solver: Create solver instance.
Sort - Class in io.github.cvc5: The sort of a cvc5 term.
Sort() - Constructor for class io.github.cvc5.Sort: Null sort
SortKind - Enum in io.github.cvc5
Stat - Class in io.github.cvc5: Represents a snapshot of a single statistic value.
Statistics - Class in io.github.cvc5
Statistics.ConstIterator - Class in io.github.cvc5
stringValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a string.
substitute(Sort, Sort) - Method in class io.github.cvc5.Sort: Substitution of Sorts.
substitute(Sort[], Sort[]) - Method in class io.github.cvc5.Sort: Simultaneous substitution of Sorts.
substitute(Term, Term) - Method in class io.github.cvc5.Term: Replace term with replacement in this term.
substitute(Term[], Term[]) - Method in class io.github.cvc5.Term: Simultaneously replace terms with replacements in this term.
SymbolManager - Class in io.github.cvc5
SymbolManager(TermManager) - Constructor for class io.github.cvc5.SymbolManager: Create symbol manager instance.
SymbolManager(Solver) - Constructor for class io.github.cvc5.SymbolManager: Deprecated.
This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
synthFun(String, Term[], Sort) - Method in class io.github.cvc5.Solver: Synthesize n-ary function.
synthFun(String, Term[], Sort, Grammar) - Method in class io.github.cvc5.Solver: Synthesize n-ary function following specified syntactic constraints.
SynthResult - Class in io.github.cvc5: Encapsulation of a solver synth result.
SynthResult() - Constructor for class io.github.cvc5.SynthResult: Null synthResult

T

Term - Class in io.github.cvc5: A cvc5 Term.
Term() - Constructor for class io.github.cvc5.Term: Null term
Term.ConstIterator - Class in io.github.cvc5
termManager - Variable in class io.github.cvc5.AbstractPlugin
TermManager - Class in io.github.cvc5: A cvc5 term manager.
TermManager() - Constructor for class io.github.cvc5.TermManager: Create a term manager instance.
third - Variable in class io.github.cvc5.Triplet
toString(long) - Method in class io.github.cvc5.Command
toString(long) - Method in class io.github.cvc5.Datatype
toString(long) - Method in class io.github.cvc5.DatatypeConstructor
toString(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
toString(long) - Method in class io.github.cvc5.DatatypeDecl
toString(long) - Method in class io.github.cvc5.DatatypeSelector
toString(long) - Method in class io.github.cvc5.Grammar
toString(long) - Method in class io.github.cvc5.InputParser
toString(long) - Method in class io.github.cvc5.Op
toString() - Method in class io.github.cvc5.OptionInfo
toString(long) - Method in class io.github.cvc5.OptionInfo
toString(long) - Method in class io.github.cvc5.Result
toString(long) - Method in class io.github.cvc5.Solver
toString(long) - Method in class io.github.cvc5.Sort
toString(long) - Method in class io.github.cvc5.Stat
toString(long) - Method in class io.github.cvc5.Statistics
toString(long) - Method in class io.github.cvc5.SymbolManager
toString(long) - Method in class io.github.cvc5.SynthResult
toString(long) - Method in class io.github.cvc5.Term
toString(long) - Method in class io.github.cvc5.TermManager
transferTo(InputStream, FileOutputStream) - Static method in class io.github.cvc5.Utils: Transfers all bytes from the provided InputStream to the specified FileOutputStream.
Triplet<A,B,C> - Class in io.github.cvc5
Triplet(A, B, C) - Constructor for class io.github.cvc5.Triplet

U

UnknownExplanation - Enum in io.github.cvc5
Utils - Class in io.github.cvc5
Utils() - Constructor for class io.github.cvc5.Utils
Utils.OS - Enum in io.github.cvc5

V

validateUnsigned(int, String) - Static method in class io.github.cvc5.Utils
validateUnsigned(long, String) - Static method in class io.github.cvc5.Utils
validateUnsigned(int[], String) - Static method in class io.github.cvc5.Utils
validateUnsigned(long[], String) - Static method in class io.github.cvc5.Utils
ValueInfo(T, T) - Constructor for class io.github.cvc5.OptionInfo.ValueInfo
valueOf(String) - Static method in enum io.github.cvc5.Kind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.BlockModelsMode: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.FindSynthTarget: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.InputLanguage: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.LearnedLitType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.OptionCategory: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.ProofComponent: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.ProofFormat: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.ProofRewriteRule: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.ProofRule: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.RoundingMode: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.SkolemId: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.SortKind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.UnknownExplanation: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.Utils.OS: Returns the enum constant of this type with the specified name.
values() - Static method in enum io.github.cvc5.Kind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.BlockModelsMode: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.FindSynthTarget: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.InputLanguage: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.LearnedLitType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.OptionCategory: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.ProofComponent: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.ProofFormat: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.ProofRewriteRule: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.ProofRule: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.RoundingMode: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.SkolemId: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.SortKind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.UnknownExplanation: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.Utils.OS: Returns an array containing the constants of this enum type, in the order they are declared.
VoidInfo() - Constructor for class io.github.cvc5.OptionInfo.VoidInfo

X

xorTerm(Term) - Method in class io.github.cvc5.Term: Boolean exclusive or.

A B C D E F G H I K L M N O P R S T U V X