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