Skip navigation links
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.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
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.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
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.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.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 
Skip navigation links