Index

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

A

ABS - io.github.cvc5.Kind: Absolute value.
ADD - io.github.cvc5.Kind: Arithmetic addition.
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.
addRule(Term, Term) - Method in class io.github.cvc5.Grammar: Add rule to the set of rules corresponding to ntSymbol.
addRules(long, long, long[]) - Method in class io.github.cvc5.Grammar
addRules(Term, Term[]) - Method in class io.github.cvc5.Grammar: Add rules to the set of rules corresponding to ntSymbol.
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.
AND - io.github.cvc5.Kind: Logical conjunction.
andTerm(Term) - Method in class io.github.cvc5.Term: Boolean and.
apply(Term[]) - Method in interface io.github.cvc5.IOracle
APPLY_CONSTRUCTOR - io.github.cvc5.Kind: Datatype constructor application.
APPLY_SELECTOR - io.github.cvc5.Kind: Datatype selector application.
APPLY_TESTER - io.github.cvc5.Kind: Datatype tester application.
APPLY_UF - io.github.cvc5.Kind: Application of an uninterpreted function.
APPLY_UPDATER - io.github.cvc5.Kind: Datatype update application.
ARCCOSECANT - io.github.cvc5.Kind: Arc cosecant function.
ARCCOSINE - io.github.cvc5.Kind: Arc cosine function.
ARCCOTANGENT - io.github.cvc5.Kind: Arc cotangent function.
ARCSECANT - io.github.cvc5.Kind: Arc secant function.
ARCSINE - io.github.cvc5.Kind: Arc sine function.
ARCTANGENT - io.github.cvc5.Kind: Arc tangent function.
assertFormula(Term) - Method in class io.github.cvc5.Solver: Assert a formula.

B

BAG_CARD - io.github.cvc5.Kind: Bag cardinality.
BAG_CHOOSE - io.github.cvc5.Kind: Bag choose.
BAG_COUNT - io.github.cvc5.Kind: Bag element multiplicity.
BAG_DIFFERENCE_REMOVE - io.github.cvc5.Kind: Bag difference remove.
BAG_DIFFERENCE_SUBTRACT - io.github.cvc5.Kind: Bag difference subtract.
BAG_DUPLICATE_REMOVAL - io.github.cvc5.Kind: Bag duplicate removal.
BAG_EMPTY - io.github.cvc5.Kind: Empty bag.
BAG_FILTER - io.github.cvc5.Kind: Bag filter.
BAG_FOLD - io.github.cvc5.Kind: Bag fold.
BAG_FROM_SET - io.github.cvc5.Kind: Conversion from set to bag.
BAG_INTER_MIN - io.github.cvc5.Kind: Bag intersection (min).
BAG_IS_SINGLETON - io.github.cvc5.Kind: Bag is singleton tester.
BAG_MAKE - io.github.cvc5.Kind: Bag make.
BAG_MAP - io.github.cvc5.Kind: Bag map.
BAG_MEMBER - io.github.cvc5.Kind: Bag membership predicate.
BAG_PARTITION - io.github.cvc5.Kind: Bag partition.
BAG_SUBBAG - io.github.cvc5.Kind: Bag inclusion predicate.
BAG_TO_SET - io.github.cvc5.Kind: Conversion from bag to set.
BAG_UNION_DISJOINT - io.github.cvc5.Kind: Bag disjoint union (sum).
BAG_UNION_MAX - io.github.cvc5.Kind: Bag max union.
BaseInfo() - Constructor for class io.github.cvc5.OptionInfo.BaseInfo
BITVECTOR_ADD - io.github.cvc5.Kind: Addition of two or more bit-vectors.
BITVECTOR_AND - io.github.cvc5.Kind: Bit-wise and.
BITVECTOR_ASHR - io.github.cvc5.Kind: Bit-vector arithmetic shift right.
BITVECTOR_COMP - io.github.cvc5.Kind: Equality comparison (returns bit-vector of size 1).
BITVECTOR_CONCAT - io.github.cvc5.Kind: Concatenation of two or more bit-vectors.
BITVECTOR_EXTRACT - io.github.cvc5.Kind: Bit-vector extract.
BITVECTOR_ITE - io.github.cvc5.Kind: Bit-vector if-then-else.
BITVECTOR_LSHR - io.github.cvc5.Kind: Bit-vector logical shift right.
BITVECTOR_MULT - io.github.cvc5.Kind: Multiplication of two or more bit-vectors.
BITVECTOR_NAND - io.github.cvc5.Kind: Bit-wise nand.
BITVECTOR_NEG - io.github.cvc5.Kind: Negation of a bit-vector (two's complement).
BITVECTOR_NOR - io.github.cvc5.Kind: Bit-wise nor.
BITVECTOR_NOT - io.github.cvc5.Kind: Bit-wise negation.
BITVECTOR_OR - io.github.cvc5.Kind: Bit-wise or.
BITVECTOR_REDAND - io.github.cvc5.Kind: Bit-vector redand.
BITVECTOR_REDOR - io.github.cvc5.Kind: Bit-vector redor.
BITVECTOR_REPEAT - io.github.cvc5.Kind: Bit-vector repeat.
BITVECTOR_ROTATE_LEFT - io.github.cvc5.Kind: Bit-vector rotate left.
BITVECTOR_ROTATE_RIGHT - io.github.cvc5.Kind: Bit-vector rotate right.
BITVECTOR_SDIV - io.github.cvc5.Kind: Signed bit-vector division.
BITVECTOR_SGE - io.github.cvc5.Kind: Bit-vector signed greater than or equal.
BITVECTOR_SGT - io.github.cvc5.Kind: Bit-vector signed greater than.
BITVECTOR_SHL - io.github.cvc5.Kind: Bit-vector shift left.
BITVECTOR_SIGN_EXTEND - io.github.cvc5.Kind: Bit-vector sign extension.
BITVECTOR_SLE - io.github.cvc5.Kind: Bit-vector signed less than or equal.
BITVECTOR_SLT - io.github.cvc5.Kind: Bit-vector signed less than.
BITVECTOR_SLTBV - io.github.cvc5.Kind: Bit-vector signed less than returning a bit-vector of size 1.
BITVECTOR_SMOD - io.github.cvc5.Kind: Signed bit-vector remainder (sign follows divisor).
BITVECTOR_SREM - io.github.cvc5.Kind: Signed bit-vector remainder (sign follows dividend).
BITVECTOR_SUB - io.github.cvc5.Kind: Subtraction of two bit-vectors.
BITVECTOR_TO_NAT - io.github.cvc5.Kind: Bit-vector conversion to (non-negative) integer.
BITVECTOR_UDIV - io.github.cvc5.Kind: Unsigned bit-vector division.
BITVECTOR_UGE - io.github.cvc5.Kind: Bit-vector unsigned greater than or equal.
BITVECTOR_UGT - io.github.cvc5.Kind: Bit-vector unsigned greater than.
BITVECTOR_ULE - io.github.cvc5.Kind: Bit-vector unsigned less than or equal.
BITVECTOR_ULT - io.github.cvc5.Kind: Bit-vector unsigned less than.
BITVECTOR_ULTBV - io.github.cvc5.Kind: Bit-vector unsigned less than returning a bit-vector of size 1.
BITVECTOR_UREM - io.github.cvc5.Kind: Unsigned bit-vector remainder.
BITVECTOR_XNOR - io.github.cvc5.Kind: Bit-wise xnor, left associative.
BITVECTOR_XOR - io.github.cvc5.Kind: Bit-wise xor.
BITVECTOR_ZERO_EXTEND - io.github.cvc5.Kind: Bit-vector zero extension.
blockModel(BlockModelsMode) - Method in class io.github.cvc5.Solver: Block the current model.
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

CARDINALITY_CONSTRAINT - io.github.cvc5.Kind: Cardinality constraint on uninterpreted sort.
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.
close() - Method in class io.github.cvc5.Solver
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.
CONST_ARRAY - io.github.cvc5.Kind: Constant array.
CONST_BITVECTOR - io.github.cvc5.Kind: Fixed-size bit-vector constant.
CONST_BOOLEAN - io.github.cvc5.Kind: Boolean constant.
CONST_FLOATINGPOINT - io.github.cvc5.Kind: Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.
CONST_INTEGER - io.github.cvc5.Kind: Arbitrary-precision integer constant.
CONST_RATIONAL - io.github.cvc5.Kind: Arbitrary-precision rational constant.
CONST_ROUNDINGMODE - io.github.cvc5.Kind: RoundingMode constant.
CONST_SEQUENCE - io.github.cvc5.Kind: Constant sequence.
CONST_STRING - io.github.cvc5.Kind: Constant string.
CONSTANT - io.github.cvc5.Kind: Free constant symbol.
ConstIterator() - Constructor for class io.github.cvc5.Datatype.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.DatatypeConstructor.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Statistics.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Term.ConstIterator
ConstIterator(boolean, boolean) - Constructor for class io.github.cvc5.Statistics.ConstIterator
COSECANT - io.github.cvc5.Kind: Cosecant function.
COSINE - io.github.cvc5.Kind: Cosine function.
COTANGENT - io.github.cvc5.Kind: Cotangent function.
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

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.
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.
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.
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(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.
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.
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() - Method in class io.github.cvc5.Solver
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.Op
deletePointer(long) - Method in class io.github.cvc5.OptionInfo
deletePointer(long) - Method in class io.github.cvc5.Result
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.SynthResult
deletePointer(long) - Method in class io.github.cvc5.Term
DISTINCT - io.github.cvc5.Kind: Disequality.
DIVISIBLE - io.github.cvc5.Kind: Operator for the divisibility-by-k predicate.
DIVISION - io.github.cvc5.Kind: Real division, division by 0 undefined, left associative.
doubleValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a double.

E

EQ_RANGE - io.github.cvc5.Kind: Equality over arrays a and b over a given range [i,j], i.e., ..
eqTerm(Term) - Method in class io.github.cvc5.Term: Equality.
EQUAL - io.github.cvc5.Kind: Equality, chainable.
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.Result: Operator overloading for equality of two results.
equals(Object) - Method in class io.github.cvc5.Sort: Comparison for structural equality.
equals(Object) - Method in class io.github.cvc5.Term: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Triplet
EXISTS - io.github.cvc5.Kind: Existentially quantified formula.
EXPONENTIAL - io.github.cvc5.Kind: Exponential function.

F

first - Variable in class io.github.cvc5.Pair
first - Variable in class io.github.cvc5.Triplet
FLOATINGPOINT_ABS - io.github.cvc5.Kind: Floating-point absolute value.
FLOATINGPOINT_ADD - io.github.cvc5.Kind: Floating-point addition.
FLOATINGPOINT_DIV - io.github.cvc5.Kind: Floating-point division.
FLOATINGPOINT_EQ - io.github.cvc5.Kind: Floating-point equality.
FLOATINGPOINT_FMA - io.github.cvc5.Kind: Floating-point fused multiply and add.
FLOATINGPOINT_FP - io.github.cvc5.Kind: Create floating-point literal from bit-vector triple.
FLOATINGPOINT_GEQ - io.github.cvc5.Kind: Floating-point greater than or equal.
FLOATINGPOINT_GT - io.github.cvc5.Kind: Floating-point greater than.
FLOATINGPOINT_IS_INF - io.github.cvc5.Kind: Floating-point is infinite tester.
FLOATINGPOINT_IS_NAN - io.github.cvc5.Kind: Floating-point is NaN tester.
FLOATINGPOINT_IS_NEG - io.github.cvc5.Kind: Floating-point is negative tester.
FLOATINGPOINT_IS_NORMAL - io.github.cvc5.Kind: Floating-point is normal tester.
FLOATINGPOINT_IS_POS - io.github.cvc5.Kind: Floating-point is positive tester.
FLOATINGPOINT_IS_SUBNORMAL - io.github.cvc5.Kind: Floating-point is sub-normal tester.
FLOATINGPOINT_IS_ZERO - io.github.cvc5.Kind: Floating-point is zero tester.
FLOATINGPOINT_LEQ - io.github.cvc5.Kind: Floating-point less than or equal.
FLOATINGPOINT_LT - io.github.cvc5.Kind: Floating-point less than.
FLOATINGPOINT_MAX - io.github.cvc5.Kind: Floating-point maximum.
FLOATINGPOINT_MIN - io.github.cvc5.Kind: Floating-point minimum.
FLOATINGPOINT_MULT - io.github.cvc5.Kind: Floating-point multiply.
FLOATINGPOINT_NEG - io.github.cvc5.Kind: Floating-point negation.
FLOATINGPOINT_REM - io.github.cvc5.Kind: Floating-point remainder.
FLOATINGPOINT_RTI - io.github.cvc5.Kind: Floating-point round to integral.
FLOATINGPOINT_SQRT - io.github.cvc5.Kind: Floating-point square root.
FLOATINGPOINT_SUB - io.github.cvc5.Kind: Floating-point sutraction.
FLOATINGPOINT_TO_FP_FROM_FP - io.github.cvc5.Kind: Conversion to floating-point from floating-point.
FLOATINGPOINT_TO_FP_FROM_IEEE_BV - io.github.cvc5.Kind: Conversion to floating-point from IEEE-754 bit-vector.
FLOATINGPOINT_TO_FP_FROM_REAL - io.github.cvc5.Kind: Conversion to floating-point from Real.
FLOATINGPOINT_TO_FP_FROM_SBV - io.github.cvc5.Kind: Conversion to floating-point from signed bit-vector.
FLOATINGPOINT_TO_FP_FROM_UBV - io.github.cvc5.Kind: Conversion to floating-point from unsigned bit-vector.
FLOATINGPOINT_TO_REAL - io.github.cvc5.Kind: Conversion to Real from floating-point.
FLOATINGPOINT_TO_SBV - io.github.cvc5.Kind: Conversion to signed bit-vector from floating-point.
FLOATINGPOINT_TO_UBV - io.github.cvc5.Kind: Conversion to unsigned bit-vector from floating-point.
FORALL - io.github.cvc5.Kind: Universally quantified formula.
fromInt(int) - Static method in enum io.github.cvc5.Kind
fromInt(int) - Static method in enum io.github.cvc5.RoundingMode
fromInt(int) - Static method in enum io.github.cvc5.UnknownExplanation

G

GEQ - io.github.cvc5.Kind: Greater than or equal, chainable.
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.
getAliases() - Method in class io.github.cvc5.OptionInfo
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
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.
getCodomainSort() - Method in class io.github.cvc5.DatatypeSelector
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
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.
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: Return 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(long) - Method in class io.github.cvc5.Solver
getIntegerValue() - Method in class io.github.cvc5.Term: Asserts isIntegerValue().
getInterpolant(Term) - Method in class io.github.cvc5.Solver: Get an interpolant SMT-LIB: ( get-interpolant <conj> ) Requires option produce-interpolants to be set to a mode different from none.
getInterpolant(Term, Grammar) - Method in class io.github.cvc5.Solver: Get an interpolant SMT-LIB: ( get-interpolant <conj> <g> ) Requires option produce-interpolants to be set to a mode different from none.
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.Term
getLearnedLiterals() - Method in class io.github.cvc5.Solver: Get a list of literals that are entailed by the current set of assertions.
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.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
getNullDatatypeDecl() - Method in class io.github.cvc5.Solver
getNullOp() - Method in class io.github.cvc5.Solver
getNullResult() - Method in class io.github.cvc5.Solver
getNullSort() - Method in class io.github.cvc5.Solver
getNullSynthResult() - Method in class io.github.cvc5.Solver
getNullTerm() - Method in class io.github.cvc5.Solver
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
getNumSelectors() - Method in class io.github.cvc5.DatatypeConstructor
getOp() - Method in class io.github.cvc5.Term
getOption(String) - Method in class io.github.cvc5.Solver: Get the value of a given option.
getOptionInfo(String) - Method in class io.github.cvc5.Solver: Get some information about the given option.
getOptionNames() - Method in class io.github.cvc5.Solver: Get all option names that can be used with Solver.setOption(String, String), Solver.getOption(String) and Solver.getOptionInfo(String).
getPairs(Pair<K, ? extends AbstractPointer>[]) - Static method in class io.github.cvc5.Utils
getParameters() - Method in class io.github.cvc5.Datatype
getPointer() - Method in class io.github.cvc5.Datatype
getPointer() - Method in class io.github.cvc5.DatatypeConstructor
getPointer() - Method in class io.github.cvc5.DatatypeConstructorDecl
getPointer() - Method in class io.github.cvc5.DatatypeDecl
getPointer() - Method in class io.github.cvc5.DatatypeSelector
getPointer() - Method in class io.github.cvc5.Grammar
getPointer() - Method in class io.github.cvc5.Op
getPointer() - Method in class io.github.cvc5.OptionInfo
getPointer() - Method in class io.github.cvc5.Result
getPointer() - Method in class io.github.cvc5.Solver
getPointer() - Method in class io.github.cvc5.Sort
getPointer() - Method in class io.github.cvc5.Stat
getPointer() - Method in class io.github.cvc5.Statistics
getPointer() - Method in class io.github.cvc5.SynthResult
getPointer() - Method in class io.github.cvc5.Term
getPointers(IPointer[]) - Static method in class io.github.cvc5.Utils: get pointers from one dimensional array
getPointers(IPointer[][]) - Static method in class io.github.cvc5.Utils: get pointers from two dimensional matrix
getProof() - Method in class io.github.cvc5.Solver: Get the refutation proof SMT-LIB: ( get-proof ) Requires to enable option produce-proofs.
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(Pair<BigInteger, BigInteger>) - Static method in class io.github.cvc5.Utils: Convert a pair of BigIntegers to a rational string a/b
getRational(String) - Static method in class io.github.cvc5.Utils: Convert a rational string a/b to a pair of BigIntegers
getRealOrIntegerValueSign() - Method in class io.github.cvc5.Term: Get integer or real value sign.
getRealSort() - Method in class io.github.cvc5.Solver
getRealValue() - Method in class io.github.cvc5.Term: Asserts isRealValue().
getRegExpSort() - Method in class io.github.cvc5.Solver
getRoundingModeSort() - Method in class io.github.cvc5.Solver
getRoundingModeValue() - Method in class io.github.cvc5.Term: Asserts isRoundingModeValue().
getSelector(int) - Method in class io.github.cvc5.DatatypeConstructor: Get the DatatypeSelector at the given index
getSelector(String) - Method in class io.github.cvc5.Datatype: Get the datatype constructor with the given name.
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().
getSort() - Method in class io.github.cvc5.Term
getSorts(Solver, long[]) - Static method in class io.github.cvc5.Utils: return sorts array from array of pointers
getStatistics() - Method in class io.github.cvc5.Solver: Returns a snapshot of the current state of the statistic values of this solver.
getString() - Method in class io.github.cvc5.Stat: Return the string value.
getStringSort() - Method in class io.github.cvc5.Solver
getStringValue() - Method in class io.github.cvc5.Term
getSymbol() - Method in class io.github.cvc5.Sort
getSymbol() - Method in class io.github.cvc5.Term: Asserts hasSymbol().
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.
getTerms(Solver, long[]) - Static method in class io.github.cvc5.Utils: return terms array from array of pointers
getTesterTerm() - Method in class io.github.cvc5.DatatypeConstructor: Get the tester term of this datatype constructor.
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
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.
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.RoundingMode
getValue() - Method in enum io.github.cvc5.UnknownExplanation
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.
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.
Grammar - Class in io.github.cvc5: A Sygus Grammar.
Grammar(Grammar) - Constructor for class io.github.cvc5.Grammar
GT - io.github.cvc5.Kind: Greater than, chainable.

H

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
HO_APPLY - io.github.cvc5.Kind: Higher-order applicative encoding of function application, left associative.

I

IAND - io.github.cvc5.Kind: Integer and.
IMPLIES - io.github.cvc5.Kind: Logical implication.
impTerm(Term) - Method in class io.github.cvc5.Term: Boolean implication.
INCOMPLETE - io.github.cvc5.UnknownExplanation: Incomplete theory solver.
INST_ADD_TO_POOL - io.github.cvc5.Kind: A instantantiation-add-to-pool annotation.
INST_ATTRIBUTE - io.github.cvc5.Kind: Instantiation attribute.
INST_NO_PATTERN - io.github.cvc5.Kind: Instantiation no-pattern.
INST_PATTERN - io.github.cvc5.Kind: Instantiation pattern.
INST_PATTERN_LIST - io.github.cvc5.Kind: A list of instantiation patterns, attributes or annotations.
INST_POOL - io.github.cvc5.Kind: Instantiation pool annotation.
instantiate(Sort[]) - Method in class io.github.cvc5.Sort: Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
INT_TO_BITVECTOR - io.github.cvc5.Kind: Conversion from Int to bit-vector.
INTERNAL_KIND - io.github.cvc5.Kind: Internal kind.
INTERRUPTED - io.github.cvc5.UnknownExplanation: Solver was interrupted.
INTS_DIVISION - io.github.cvc5.Kind: Integer division, division by 0 undefined, left associative.
INTS_MODULUS - io.github.cvc5.Kind: Integer modulus, modulus by 0 undefined.
intValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as as int.
io.github.cvc5 - package io.github.cvc5
IOracle - Interface in io.github.cvc5
IS_INTEGER - io.github.cvc5.Kind: Is-integer predicate.
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
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?
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.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.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
isParametric() - Method in class io.github.cvc5.Datatype
isParametric() - Method in class io.github.cvc5.DatatypeDecl
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).
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
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.
ITE - io.github.cvc5.Kind: If-then-else.
iterator() - Method in class io.github.cvc5.Datatype
iterator() - Method in class io.github.cvc5.DatatypeConstructor
iterator() - Method in class io.github.cvc5.Statistics
iterator() - Method in class io.github.cvc5.Term
iterator(boolean, boolean) - Method in class io.github.cvc5.Statistics
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

LAMBDA - io.github.cvc5.Kind: Lambda expression.
LAST_KIND - io.github.cvc5.Kind: Marks the upper-bound of this enumeration.
LEQ - io.github.cvc5.Kind: Less than or equal, chainable.
loadLibraries() - Static method in class io.github.cvc5.Utils: load cvc5 jni library
LT - io.github.cvc5.Kind: Less than, chainable.

M

MATCH - io.github.cvc5.Kind: Match expression.
MATCH_BIND_CASE - io.github.cvc5.Kind: Match case with binders, for constructors with selectors and variable patterns.
MATCH_CASE - io.github.cvc5.Kind: Match case for nullary constructors.
MEMOUT - io.github.cvc5.UnknownExplanation: Memory limit reached.
mkArraySort(Sort, Sort) - Method in class io.github.cvc5.Solver: Create an array sort.
mkBagSort(Sort) - Method in class io.github.cvc5.Solver: Create a bag sort.
mkBitVector(int) - Method in class io.github.cvc5.Solver: Create a bit-vector constant of given size and value = 0.
mkBitVector(int, long) - Method in class io.github.cvc5.Solver: Create a bit-vector constant of given size and value.
mkBitVector(int, String, int) - Method in class io.github.cvc5.Solver: 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: Create a bit-vector sort.
mkBoolean(boolean) - Method in class io.github.cvc5.Solver: Create a Boolean constant.
mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.Solver: Create a cardinality constraint for an uninterpreted sort.
mkConst(Sort) - Method in class io.github.cvc5.Solver: Create a free constant with a default symbol name.
mkConst(Sort, String) - Method in class io.github.cvc5.Solver: Create a free constant.
mkConstArray(Sort, Term) - Method in class io.github.cvc5.Solver: Create a constant array with the provided constant value stored at every index
mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.Solver: Create a datatype constructor declaration.
mkDatatypeDecl(String) - Method in class io.github.cvc5.Solver: Create a datatype declaration.
mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.Solver: Create a datatype declaration.
mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.Solver: Create a datatype declaration.
mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.Solver: Create a datatype declaration.
mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.Solver: Create a datatype sort.
mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.Solver: Create a vector of datatype sorts.
mkEmptyBag(Sort) - Method in class io.github.cvc5.Solver: Create a constant representing an empty bag of the given sort.
mkEmptySequence(Sort) - Method in class io.github.cvc5.Solver: Create an empty sequence of the given element sort.
mkEmptySet(Sort) - Method in class io.github.cvc5.Solver: Create a constant representing an empty set of the given sort.
mkFalse() - Method in class io.github.cvc5.Solver: Create a Boolean false constant.
mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.Solver: Create a floating-point constant.
mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.Solver: Create a not-a-number floating-point constant (SMT-LIB: NaN).
mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.Solver: Create a negative infinity floating-point constant (SMT-LIB: -oo).
mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.Solver: Create a negative zero floating-point constant (SMT-LIB: -zero).
mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.Solver: Create a positive infinity floating-point constant (SMT-LIB: +oo).
mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.Solver: Create a positive zero floating-point constant (SMT-LIB: +zero).
mkFloatingPointSort(int, int) - Method in class io.github.cvc5.Solver: Create a floating-point sort.
mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.Solver: Create function sort.
mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.Solver: Create function sort.
mkGrammar(Term[], Term[]) - Method in class io.github.cvc5.Solver: Create a Sygus grammar.
mkInteger(long) - Method in class io.github.cvc5.Solver: Create an integer constant from a C++ int.
mkInteger(String) - Method in class io.github.cvc5.Solver: Create an integer constant from a string.
mkOp(Kind) - Method in class io.github.cvc5.Solver: 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, int) - Method in class io.github.cvc5.Solver: 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[]) - Method in class io.github.cvc5.Solver: Create operator of Kind: TUPLE_PROJECT See enum Kind for a description of the parameters.
mkOp(Kind, int, int) - Method in class io.github.cvc5.Solver: 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, String) - Method in class io.github.cvc5.Solver: Create operator of kind: Kind.DIVISIBLE (to support arbitrary precision integers) See enum Kind for a description of the parameters.
mkParamSort() - Method in class io.github.cvc5.Solver: Create a sort parameter.
mkParamSort(String) - Method in class io.github.cvc5.Solver: Create a sort parameter.
mkPi() - Method in class io.github.cvc5.Solver: Create a constant representing the number Pi.
mkPredicateSort(Sort[]) - Method in class io.github.cvc5.Solver: Create a predicate sort.
mkReal(long) - Method in class io.github.cvc5.Solver: Create a real constant from an integer.
mkReal(long, long) - Method in class io.github.cvc5.Solver: Create a real constant from a rational.
mkReal(String) - Method in class io.github.cvc5.Solver: Create a real constant from a string.
mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.Solver: Create a record sort
mkRegexpAll() - Method in class io.github.cvc5.Solver: Create a regular expression all (re.all) term.
mkRegexpAllchar() - Method in class io.github.cvc5.Solver: Create a regular expression allchar (re.allchar) term.
mkRegexpNone() - Method in class io.github.cvc5.Solver: Create a regular expression none (re.none) term.
mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.Solver: Create a rounding mode constant.
mkSepEmp() - Method in class io.github.cvc5.Solver: Create a separation logic empty term.
mkSepNil(Sort) - Method in class io.github.cvc5.Solver: Create a separation logic nil term.
mkSequenceSort(Sort) - Method in class io.github.cvc5.Solver: Create a sequence sort.
mkSetSort(Sort) - Method in class io.github.cvc5.Solver: Create a set sort.
mkString(int[]) - Method in class io.github.cvc5.Solver: Create a String constant.
mkString(String) - Method in class io.github.cvc5.Solver: Create a String constant.
mkString(String, boolean) - Method in class io.github.cvc5.Solver: Create a String constant.
mkTerm(Kind) - Method in class io.github.cvc5.Solver: Create 0-ary term of given kind.
mkTerm(Kind, Term) - Method in class io.github.cvc5.Solver: Create a unary term of given kind.
mkTerm(Kind, Term[]) - Method in class io.github.cvc5.Solver: Create n-ary term of given kind.
mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.Solver: Create binary term of given kind.
mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.Solver: Create ternary term of given kind.
mkTerm(Op) - Method in class io.github.cvc5.Solver: Create nullary term of given kind from a given operator.
mkTerm(Op, Term) - Method in class io.github.cvc5.Solver: Create unary term of given kind from a given operator.
mkTerm(Op, Term[]) - Method in class io.github.cvc5.Solver: Create n-ary term of given kind from a given operator.
mkTerm(Op, Term, Term) - Method in class io.github.cvc5.Solver: Create binary term of given kind from a given operator.
mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.Solver: Create ternary term of given kind from a given operator.
mkTrue() - Method in class io.github.cvc5.Solver: Create a Boolean true constant.
mkTuple(Sort[], Term[]) - Method in class io.github.cvc5.Solver: Create a tuple term.
mkTupleSort(Sort[]) - Method in class io.github.cvc5.Solver: Create a tuple sort.
mkUninterpretedSort() - Method in class io.github.cvc5.Solver: Create an uninterpreted sort.
mkUninterpretedSort(String) - Method in class io.github.cvc5.Solver: Create an uninterpreted sort.
mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.Solver: Create a sort constructor sort.
mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.Solver: Create a sort constructor sort.
mkUniverseSet(Sort) - Method in class io.github.cvc5.Solver: Create a universe set of the given sort.
mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.Solver: Create an unresolved datatype sort.
mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.Solver: Create an unresolved datatype sort.
mkVar(Sort) - Method in class io.github.cvc5.Solver: 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.Solver: 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
MULT - io.github.cvc5.Kind: Arithmetic multiplication.

N

NEG - io.github.cvc5.Kind: Arithmetic negation.
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
NOT - io.github.cvc5.Kind: Logical negation.
notTerm() - Method in class io.github.cvc5.Term: Boolean negation.
NULL_TERM - io.github.cvc5.Kind: Null kind.
NumberInfo(T, T, T, T) - Constructor for class io.github.cvc5.OptionInfo.NumberInfo

O

Op - Class in io.github.cvc5: A cvc5 operator.
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
OR - io.github.cvc5.Kind: Logical disjunction.
orTerm(Term) - Method in class io.github.cvc5.Term: Boolean or.
OTHER - io.github.cvc5.UnknownExplanation: Other reason.

P

Pair<K,V> - Class in io.github.cvc5
Pair(K, V) - Constructor for class io.github.cvc5.Pair
PI - io.github.cvc5.Kind: Pi constant.
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.
POW - io.github.cvc5.Kind: Arithmetic power.
POW2 - io.github.cvc5.Kind: Power of two.
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

REGEXP_ALL - io.github.cvc5.Kind: Regular expression all.
REGEXP_ALLCHAR - io.github.cvc5.Kind: Regular expression all characters.
REGEXP_COMPLEMENT - io.github.cvc5.Kind: Regular expression complement.
REGEXP_CONCAT - io.github.cvc5.Kind: Regular expression concatenation.
REGEXP_DIFF - io.github.cvc5.Kind: Regular expression difference.
REGEXP_INTER - io.github.cvc5.Kind: Regular expression intersection.
REGEXP_LOOP - io.github.cvc5.Kind: Regular expression loop.
REGEXP_NONE - io.github.cvc5.Kind: Regular expression none.
REGEXP_OPT - io.github.cvc5.Kind: Regular expression ?.
REGEXP_PLUS - io.github.cvc5.Kind: Regular expression +.
REGEXP_RANGE - io.github.cvc5.Kind: Regular expression range.
REGEXP_REPEAT - io.github.cvc5.Kind: Operator for regular expression repeat.
REGEXP_STAR - io.github.cvc5.Kind: Regular expression \*.
REGEXP_UNION - io.github.cvc5.Kind: Regular expression union.
RELATION_AGGREGATE - io.github.cvc5.Kind: Relation aggregate operator has the form ((\_ \; rel.aggr \; n_1 ... n_k) \; f \; i \; A) where n_1, ..., n_k are natural numbers, f is a function of type (\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T), i has the type T, and A has type (Relation \; T_1 \; ... \; T_j).
RELATION_GROUP - io.github.cvc5.Kind: Relation group ((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A) partitions tuples of relation A such that tuples that have the same projection with indices n_1 \; \dots \; n_k are in the same part.
RELATION_IDEN - io.github.cvc5.Kind: Relation identity.
RELATION_JOIN - io.github.cvc5.Kind: Relation join.
RELATION_JOIN_IMAGE - io.github.cvc5.Kind: Relation join image.
RELATION_PRODUCT - io.github.cvc5.Kind: Relation cartesian product.
RELATION_PROJECT - io.github.cvc5.Kind: Relation projection operator extends tuple projection operator to sets.
RELATION_TCLOSURE - io.github.cvc5.Kind: Relation transitive closure.
RELATION_TRANSPOSE - io.github.cvc5.Kind: Relation transpose.
REQUIRES_FULL_CHECK - io.github.cvc5.UnknownExplanation: Full satisfiability check required (e.g., if only preprocessing was performed).
resetAssertions() - Method in class io.github.cvc5.Solver: Remove all assertions.
RESOURCEOUT - io.github.cvc5.UnknownExplanation: Resource limit reached.
Result - Class in io.github.cvc5: Encapsulation of a three-valued solver result, with explanations.
ROUND_NEAREST_TIES_TO_AWAY - io.github.cvc5.RoundingMode: Round to the nearest number away from zero.
ROUND_NEAREST_TIES_TO_EVEN - io.github.cvc5.RoundingMode: Round to the nearest even number.
ROUND_TOWARD_NEGATIVE - io.github.cvc5.RoundingMode: Round towards negative infinity (-oo).
ROUND_TOWARD_POSITIVE - io.github.cvc5.RoundingMode: Round towards positive infinity (SMT-LIB: +oo).
ROUND_TOWARD_ZERO - io.github.cvc5.RoundingMode: Round towards zero.
RoundingMode - Enum in io.github.cvc5

S

SECANT - io.github.cvc5.Kind: Secant function.
second - Variable in class io.github.cvc5.Pair
second - Variable in class io.github.cvc5.Triplet
SELECT - io.github.cvc5.Kind: Array select.
SEP_EMP - io.github.cvc5.Kind: Separation logic empty heap.
SEP_NIL - io.github.cvc5.Kind: Separation logic nil.
SEP_PTO - io.github.cvc5.Kind: Separation logic points-to relation.
SEP_STAR - io.github.cvc5.Kind: Separation logic star.
SEP_WAND - io.github.cvc5.Kind: Separation logic magic wand.
SEQ_AT - io.github.cvc5.Kind: Sequence element at.
SEQ_CONCAT - io.github.cvc5.Kind: Sequence concat.
SEQ_CONTAINS - io.github.cvc5.Kind: Sequence contains.
SEQ_EXTRACT - io.github.cvc5.Kind: Sequence extract.
SEQ_INDEXOF - io.github.cvc5.Kind: Sequence index-of.
SEQ_LENGTH - io.github.cvc5.Kind: Sequence length.
SEQ_NTH - io.github.cvc5.Kind: Sequence nth.
SEQ_PREFIX - io.github.cvc5.Kind: Sequence prefix-of.
SEQ_REPLACE - io.github.cvc5.Kind: Sequence replace.
SEQ_REPLACE_ALL - io.github.cvc5.Kind: Sequence replace all.
SEQ_REV - io.github.cvc5.Kind: Sequence reverse.
SEQ_SUFFIX - io.github.cvc5.Kind: Sequence suffix-of.
SEQ_UNIT - io.github.cvc5.Kind: Sequence unit.
SEQ_UPDATE - io.github.cvc5.Kind: Sequence update.
SET_CARD - io.github.cvc5.Kind: Set cardinality.
SET_CHOOSE - io.github.cvc5.Kind: Set choose.
SET_COMPLEMENT - io.github.cvc5.Kind: Set complement with respect to finite universe.
SET_COMPREHENSION - io.github.cvc5.Kind: Set comprehension A set comprehension is specified by a variable list x_1 ... x_n, a predicate P[x_1...x_n], and a term t[x_1...x_n].
SET_EMPTY - io.github.cvc5.Kind: Empty set.
SET_FILTER - io.github.cvc5.Kind: Set filter.
SET_FOLD - io.github.cvc5.Kind: Set fold.
SET_INSERT - io.github.cvc5.Kind: The set obtained by inserting elements; Arity: n > 0 1..n-1: Terms of any Sort (must match the element sort of the given set Term) n: Term of set Sort Create Term of this Kind with: Solver.mkTerm(Kind, Term[]) Solver.mkTerm(Op, Term[]) Create Op of this kind with: Solver.mkOp(Kind, int[])
SET_INTER - io.github.cvc5.Kind: Set intersection.
SET_IS_SINGLETON - io.github.cvc5.Kind: Set is singleton tester.
SET_MAP - io.github.cvc5.Kind: Set map.
SET_MEMBER - io.github.cvc5.Kind: Set membership predicate.
SET_MINUS - io.github.cvc5.Kind: Set subtraction.
SET_SINGLETON - io.github.cvc5.Kind: Singleton set.
SET_SUBSET - io.github.cvc5.Kind: Subset predicate.
SET_UNION - io.github.cvc5.Kind: Set union.
SET_UNIVERSE - io.github.cvc5.Kind: Finite universe set.
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.
SEXPR - io.github.cvc5.Kind: Symbolic expression.
simplify(Term) - Method in class io.github.cvc5.Solver: Simplify a formula without doing "much" work.
SINE - io.github.cvc5.Kind: Sine function.
SKOLEM_ADD_TO_POOL - io.github.cvc5.Kind: A skolemization-add-to-pool annotation.
Solver - Class in io.github.cvc5: A cvc5 solver.
Solver() - Constructor for class io.github.cvc5.Solver
Sort - Class in io.github.cvc5: The sort of a cvc5 term.
SQRT - io.github.cvc5.Kind: Square root.
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
STORE - io.github.cvc5.Kind: Array store.
STRING_CHARAT - io.github.cvc5.Kind: String character at.
STRING_CONCAT - io.github.cvc5.Kind: String concat.
STRING_CONTAINS - io.github.cvc5.Kind: String contains.
STRING_FROM_CODE - io.github.cvc5.Kind: String from code.
STRING_FROM_INT - io.github.cvc5.Kind: Conversion from Int to String.
STRING_IN_REGEXP - io.github.cvc5.Kind: String membership.
STRING_INDEXOF - io.github.cvc5.Kind: String index-of.
STRING_INDEXOF_RE - io.github.cvc5.Kind: String index-of regular expression match.
STRING_IS_DIGIT - io.github.cvc5.Kind: String is-digit.
STRING_LENGTH - io.github.cvc5.Kind: String length.
STRING_LEQ - io.github.cvc5.Kind: String less than or equal.
STRING_LT - io.github.cvc5.Kind: String less than.
STRING_PREFIX - io.github.cvc5.Kind: String prefix-of.
STRING_REPLACE - io.github.cvc5.Kind: String replace.
STRING_REPLACE_ALL - io.github.cvc5.Kind: String replace all.
STRING_REPLACE_RE - io.github.cvc5.Kind: String replace regular expression match.
STRING_REPLACE_RE_ALL - io.github.cvc5.Kind: String replace all regular expression matches.
STRING_REV - io.github.cvc5.Kind: String reverse.
STRING_SUBSTR - io.github.cvc5.Kind: String substring.
STRING_SUFFIX - io.github.cvc5.Kind: String suffix-of.
STRING_TO_CODE - io.github.cvc5.Kind: String to code.
STRING_TO_INT - io.github.cvc5.Kind: String to integer (total function).
STRING_TO_LOWER - io.github.cvc5.Kind: String to lower case.
STRING_TO_REGEXP - io.github.cvc5.Kind: Conversion from string to regexp.
STRING_TO_UPPER - io.github.cvc5.Kind: String to upper case.
STRING_UPDATE - io.github.cvc5.Kind: String update.
stringValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a string.
SUB - io.github.cvc5.Kind: Arithmetic subtraction, left associative.
substitute(Sort[], Sort[]) - Method in class io.github.cvc5.Sort: Simultaneous substitution of Sorts.
substitute(Sort, Sort) - Method in class io.github.cvc5.Sort: Substitution of Sorts.
substitute(Term[], Term[]) - Method in class io.github.cvc5.Term: Simultaneously replace terms with replacements in this term.
substitute(Term, Term) - Method in class io.github.cvc5.Term: Replace term with replacement in this term.
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.
synthInv(String, Term[]) - Method in class io.github.cvc5.Solver: Synthesize invariant.
synthInv(String, Term[], Grammar) - Method in class io.github.cvc5.Solver: Synthesize invariant following specified syntactic constraints.
SynthResult - Class in io.github.cvc5: Encapsulation of a solver synth result.

T

TABLE_AGGREGATE - io.github.cvc5.Kind: Table aggregate operator has the form ((\_ \; table.aggr \; n_1 ... n_k) \; f \; i \; A) where n_1, ..., n_k are natural numbers, f is a function of type (\rightarrow (Tuple \; T_1 \; ... \; T_j)\; T \; T), i has the type T, and A has type (Table \; T_1 \; ... \; T_j).
TABLE_GROUP - io.github.cvc5.Kind: Table group ((\_ \; table.group \; n_1 \; \dots \; n_k) \; A) partitions tuples of table A such that tuples that have the same projection with indices n_1 \; \dots \; n_k are in the same part.
TABLE_JOIN - io.github.cvc5.Kind: Table join operator has the form ((\_ \; table.join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B) where m_1 \; n_1 \; \dots \; m_k \; n_k are natural numbers, and A, B are tables.
TABLE_PRODUCT - io.github.cvc5.Kind: Table cross product.
TABLE_PROJECT - io.github.cvc5.Kind: Table projection operator extends tuple projection operator to tables.
TANGENT - io.github.cvc5.Kind: Tangent function.
Term - Class in io.github.cvc5: A cvc5 Term.
Term.ConstIterator - Class in io.github.cvc5
third - Variable in class io.github.cvc5.Triplet
TIMEOUT - io.github.cvc5.UnknownExplanation: Time limit reached.
TO_INTEGER - io.github.cvc5.Kind: Convert Term of sort Int or Real to Int via the floor function.
TO_REAL - io.github.cvc5.Kind: Convert Term of Sort Int or Real to Real.
toString() - Method in class io.github.cvc5.OptionInfo
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.Op
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.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.SynthResult
toString(long) - Method in class io.github.cvc5.Term
Triplet<A,B,C> - Class in io.github.cvc5
Triplet(A, B, C) - Constructor for class io.github.cvc5.Triplet
TUPLE_PROJECT - io.github.cvc5.Kind: Tuple projection.

U

UNDEFINED_KIND - io.github.cvc5.Kind: Undefined kind.
UNINTERPRETED_SORT_VALUE - io.github.cvc5.Kind: The value of an uninterpreted constant.
UNKNOWN_REASON - io.github.cvc5.UnknownExplanation: No specific reason given.
UnknownExplanation - Enum in io.github.cvc5
UNSUPPORTED - io.github.cvc5.UnknownExplanation: Unsupported feature encountered.
Utils - Class in io.github.cvc5
Utils() - Constructor for class io.github.cvc5.Utils

V

validateUnsigned(int[], 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
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.RoundingMode: 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.
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.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.UnknownExplanation: Returns an array containing the constants of this enum type, in the order they are declared.
VARIABLE - io.github.cvc5.Kind: (Bound) variable.
VARIABLE_LIST - io.github.cvc5.Kind: Variable list.
VoidInfo() - Constructor for class io.github.cvc5.OptionInfo.VoidInfo

W

WITNESS - io.github.cvc5.Kind: Witness.

X

XOR - io.github.cvc5.Kind: Logical exclusive disjunction, left associative.
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 W X
All Classes All Packages