- 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.
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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.
- mkAbstractSort(SortKind) - Method in class io.github.cvc5.Solver
-
- mkAbstractSort(SortKind) - Method in class io.github.cvc5.TermManager
-
Create an abstract sort.
- mkArraySort(Sort, Sort) - Method in class io.github.cvc5.Solver
-
- mkArraySort(Sort, Sort) - Method in class io.github.cvc5.TermManager
-
Create an array sort.
- mkBagSort(Sort) - Method in class io.github.cvc5.Solver
-
- mkBagSort(Sort) - Method in class io.github.cvc5.TermManager
-
Create a bag sort.
- mkBitVector(int) - Method in class io.github.cvc5.Solver
-
- mkBitVector(int, long) - Method in class io.github.cvc5.Solver
-
- mkBitVector(int, String, int) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkBitVectorSort(int) - Method in class io.github.cvc5.TermManager
-
Create a bit-vector sort.
- mkBoolean(boolean) - Method in class io.github.cvc5.Solver
-
- mkBoolean(boolean) - Method in class io.github.cvc5.TermManager
-
Create a Boolean constant.
- mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkConst(Sort) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.TermManager
-
Create a datatype constructor declaration.
- mkDatatypeDecl(String) - Method in class io.github.cvc5.Solver
-
- mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.Solver
-
- mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.Solver
-
- mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.TermManager
-
Create a datatype sort.
- mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.Solver
-
- mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.TermManager
-
Create a vector of datatype sorts.
- mkEmptyBag(Sort) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- 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
-
- mkFalse() - Method in class io.github.cvc5.TermManager
-
Create a Boolean false
constant.
- mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkInteger(long) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- 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
-
- 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
-
- 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
-
- mkNullableSome(Term) - Method in class io.github.cvc5.TermManager
-
Create a nullable some term.
- mkNullableSort(Sort) - Method in class io.github.cvc5.Solver
-
- mkNullableSort(Sort) - Method in class io.github.cvc5.TermManager
-
Create a nullable sort.
- mkNullableVal(Term) - Method in class io.github.cvc5.Solver
-
- mkNullableVal(Term) - Method in class io.github.cvc5.TermManager
-
Create a selector for nullable term.
- mkOp(Kind) - Method in class io.github.cvc5.Solver
-
- mkOp(Kind, String) - Method in class io.github.cvc5.Solver
-
- mkOp(Kind, int) - Method in class io.github.cvc5.Solver
-
- mkOp(Kind, int, int) - Method in class io.github.cvc5.Solver
-
- mkOp(Kind, int[]) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkParamSort() - Method in class io.github.cvc5.Solver
-
- 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
-
- mkPi() - Method in class io.github.cvc5.TermManager
-
Create a constant representing the number Pi.
- mkPredicateSort(Sort[]) - Method in class io.github.cvc5.Solver
-
- mkPredicateSort(Sort[]) - Method in class io.github.cvc5.TermManager
-
Create a predicate sort.
- mkReal(String) - Method in class io.github.cvc5.Solver
-
- mkReal(long) - Method in class io.github.cvc5.Solver
-
- mkReal(long, long) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.TermManager
-
Create a record sort
- mkRegexpAll() - Method in class io.github.cvc5.Solver
-
- mkRegexpAll() - Method in class io.github.cvc5.TermManager
-
Create a regular expression all (re.all
) term.
- mkRegexpAllchar() - Method in class io.github.cvc5.Solver
-
- mkRegexpAllchar() - Method in class io.github.cvc5.TermManager
-
Create a regular expression allchar (re.allchar
) term.
- mkRegexpNone() - Method in class io.github.cvc5.Solver
-
- 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
-
- mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.TermManager
-
Create a rounding mode constant.
- mkSepEmp() - Method in class io.github.cvc5.Solver
-
- mkSepEmp() - Method in class io.github.cvc5.TermManager
-
Create a separation logic empty term.
- mkSepNil(Sort) - Method in class io.github.cvc5.Solver
-
- mkSepNil(Sort) - Method in class io.github.cvc5.TermManager
-
Create a separation logic nil term.
- mkSequenceSort(Sort) - Method in class io.github.cvc5.Solver
-
- mkSequenceSort(Sort) - Method in class io.github.cvc5.TermManager
-
Create a sequence sort.
- mkSetSort(Sort) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkString(String, boolean) - Method in class io.github.cvc5.Solver
-
- mkString(int[]) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkTerm(Kind, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Kind, Term[]) - Method in class io.github.cvc5.Solver
-
- mkTerm(Op) - Method in class io.github.cvc5.Solver
-
- mkTerm(Op, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Op, Term, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.Solver
-
- mkTerm(Op, Term[]) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkTrue() - Method in class io.github.cvc5.TermManager
-
Create a Boolean true
constant.
- mkTuple(Term[]) - Method in class io.github.cvc5.Solver
-
- mkTuple(Term[]) - Method in class io.github.cvc5.TermManager
-
Create a tuple term.
- mkTupleSort(Sort[]) - Method in class io.github.cvc5.Solver
-
- mkTupleSort(Sort[]) - Method in class io.github.cvc5.TermManager
-
Create a tuple sort.
- mkUninterpretedSort(String) - Method in class io.github.cvc5.Solver
-
- mkUninterpretedSort() - Method in class io.github.cvc5.Solver
-
- 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
-
- mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-
- mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.Solver
-
- 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
-
- mkVar(Sort, String) - Method in class io.github.cvc5.Solver
-
- 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
-
- 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
-