A B C D E F G H I K L M N O P Q R S T U V W X
All Classes All Packages
All Classes All Packages
All Classes All Packages
A
- ABS - io.github.cvc5.Kind
-
Absolute value.
- ABSTRACT_SORT - io.github.cvc5.SortKind
-
An abstract sort.
- 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 correspondingsynth-fun
orsynth-inv
with the same sort asntSymbol
. - 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 tontSymbol
. - 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 tontSymbol
. - 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.
- ALETHE - io.github.cvc5.modes.ProofFormat
-
Output Alethe proof.
- ALETHE_RULE - io.github.cvc5.ProofRule
-
External – Alethe Place holder for Alethe rules.
- ALF_RULE - io.github.cvc5.ProofRule
-
External – AletheLF Place holder for AletheLF rules.
- ALPHA_EQUIV - io.github.cvc5.ProofRule
-
Quantifiers – Alpha equivalence
Notice that this rule is correct only when are not contained in , where are the free variables of . - AND - io.github.cvc5.Kind
-
Logical conjunction.
- AND_ELIM - io.github.cvc5.ProofRule
-
Boolean – And elimination
- AND_INTRO - io.github.cvc5.ProofRule
-
Boolean – And introduction
- andTerm(Term) - Method in class io.github.cvc5.Term
-
Boolean and.
- ANNOTATION - io.github.cvc5.ProofRule
-
Builtin theory – Annotation
The terms can be anything used to annotate the proof node, one example is where is a theory.InferenceId. - appendIncrementalStringInput(String) - Method in class io.github.cvc5.InputParser
-
Append string to the input being parsed by this parser.
- apply(Term[]) - Method in interface io.github.cvc5.IOracle
- 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.
- ARITH_MULT_NEG - io.github.cvc5.ProofRule
-
Arithmetic – Multiplication with negative factor
where is a relation symbol and the inverted relation symbol. - ARITH_MULT_POS - io.github.cvc5.ProofRule
-
Arithmetic – Multiplication with positive factor
where is a relation symbol. - ARITH_MULT_SIGN - io.github.cvc5.ProofRule
-
Arithmetic – Sign inference
where are variables compared to zero (less, greater or not equal), is a monomial from these variables and is the comparison (less or equal) that results from the signs of the variables. - ARITH_MULT_TANGENT - io.github.cvc5.ProofRule
-
Arithmetic – Multiplication tangent plane
where are real terms (variables or extended terms), (possibly under rewriting), are real constants, and is the tangent plane of at . - ARITH_NL_COVERING_DIRECT - io.github.cvc5.ProofRule
-
Arithmetic – Coverings – Direct conflict We use
for an IndexedRootPredicate that is defined as the 'th root of the polynomial . - ARITH_NL_COVERING_RECURSIVE - io.github.cvc5.ProofRule
-
Arithmetic – Coverings – Recursive interval See ARITH_NL_COVERING_DIRECT <cvc5.
ProofRule.ARITH_NL_COVERING_DIRECT
> for the necessary definitions. - ARITH_OP_ELIM_AXIOM - io.github.cvc5.ProofRule
-
Arithmetic – Operator elimination
- ARITH_POLY_NORM - io.github.cvc5.ProofRule
-
Arithmetic – Polynomial normalization
where . - ARITH_SUM_UB - io.github.cvc5.ProofRule
-
Arithmetic – Sum upper bounds
where has the form and . - ARITH_TRANS_EXP_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp is approximated from above for negative values
where is an even positive number, an arithmetic term and are lower and upper bounds on . - ARITH_TRANS_EXP_APPROX_ABOVE_POS - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp is approximated from above for positive values
where is an even positive number, an arithmetic term and are lower and upper bounds on . - ARITH_TRANS_EXP_APPROX_BELOW - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp is approximated from below
where is an odd positive number, an arithmetic term and is the 'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at . - ARITH_TRANS_EXP_NEG - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp at negative values
- ARITH_TRANS_EXP_POSITIVITY - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp is always positive
- ARITH_TRANS_EXP_SUPER_LIN - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp grows super-linearly for positive values
- ARITH_TRANS_EXP_ZERO - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Exp at zero
- ARITH_TRANS_PI - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Assert bounds on Pi
where are valid lower and upper bounds on . - ARITH_TRANS_SINE_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is approximated from above for negative values
where is an even positive number, an arithmetic term, are symbolic lower and upper bounds on (possibly containing ) and the evaluated lower and upper bounds on . - ARITH_TRANS_SINE_APPROX_ABOVE_POS - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is approximated from above for positive values
where is an even positive number, an arithmetic term, an arithmetic constant and are symbolic lower and upper bounds on (possibly containing ). - ARITH_TRANS_SINE_APPROX_BELOW_NEG - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is approximated from below for negative values
where is an even positive number, an arithmetic term, an arithmetic constant and are symbolic lower and upper bounds on (possibly containing ). - ARITH_TRANS_SINE_APPROX_BELOW_POS - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is approximated from below for positive values
where is an even positive number, an arithmetic term, are symbolic lower and upper bounds on (possibly containing ) and the evaluated lower and upper bounds on . - ARITH_TRANS_SINE_BOUNDS - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is always between -1 and 1
- ARITH_TRANS_SINE_SHIFT - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is shifted to -pi...pi
where is the argument to sine, is a new real skolem that is shifted into and is a new integer slolem that is the number of phases is shifted. - ARITH_TRANS_SINE_SYMMETRY - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument
- ARITH_TRANS_SINE_TANGENT_PI - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..
- ARITH_TRANS_SINE_TANGENT_ZERO - io.github.cvc5.ProofRule
-
Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..
- ARITH_TRICHOTOMY - io.github.cvc5.ProofRule
-
Arithmetic – Trichotomy of the reals
where are in some order. - ARRAY_SORT - io.github.cvc5.SortKind
-
An array sort, whose argument sorts are the index and element sorts of the array.
- ARRAYS_EQ_RANGE_EXPAND - io.github.cvc5.ProofRule
-
Arrays – Expansion of array range equality
- ARRAYS_EXT - io.github.cvc5.ProofRule
-
Arrays – Arrays extensionality
where is . - ARRAYS_READ_OVER_WRITE - io.github.cvc5.ProofRule
-
Arrays – Read over write
- ARRAYS_READ_OVER_WRITE_1 - io.github.cvc5.ProofRule
-
Arrays – Read over write 1
- ARRAYS_READ_OVER_WRITE_CONTRA - io.github.cvc5.ProofRule
-
Arrays – Read over write, contrapositive
- assertFormula(Term) - Method in class io.github.cvc5.Solver
-
Assert a formula.
- ASSUME - io.github.cvc5.ProofRule
-
Assumption (a leaf)
This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified.
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_SORT - io.github.cvc5.SortKind
-
A bag sort, whose argument sort is the element sort of the bag.
- 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
- BETA_REDUCE - io.github.cvc5.ProofRule
-
Equality – Beta reduction
The right hand side of the equality in the conclusion is computed using standard substitution via Node.substitute. - 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_NEGO - io.github.cvc5.Kind
-
Bit-vector negation overflow detection.
- 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_SADDO - io.github.cvc5.Kind
-
Bit-vector signed addition overflow detection.
- BITVECTOR_SDIV - io.github.cvc5.Kind
-
Signed bit-vector division.
- BITVECTOR_SDIVO - io.github.cvc5.Kind
-
Bit-vector signed division overflow detection.
- 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_SMULO - io.github.cvc5.Kind
-
Bit-vector signed multiplication overflow detection.
- BITVECTOR_SORT - io.github.cvc5.SortKind
-
A bit-vector sort, parameterized by an integer denoting its bit-width.
- BITVECTOR_SREM - io.github.cvc5.Kind
-
Signed bit-vector remainder (sign follows dividend).
- BITVECTOR_SSUBO - io.github.cvc5.Kind
-
Bit-vector signed subtraction overflow detection.
- 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_UADDO - io.github.cvc5.Kind
-
Bit-vector unsigned addition overflow detection.
- 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_UMULO - io.github.cvc5.Kind
-
Bit-vector unsigned multiplication overflow detection.
- BITVECTOR_UREM - io.github.cvc5.Kind
-
Unsigned bit-vector remainder.
- BITVECTOR_USUBO - io.github.cvc5.Kind
-
Bit-vector unsigned subtraction overflow detection.
- 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.
- BlockModelsMode - Enum in io.github.cvc5.modes
- blockModelValues(Term[]) - Method in class io.github.cvc5.Solver
-
Block the current model values of (at least) the values in terms.
- BOOLEAN_SORT - io.github.cvc5.SortKind
-
The Boolean sort.
- booleanValue() - Method in class io.github.cvc5.OptionInfo
-
Obtain the current value as a Boolean.
- BV_BITBLAST_STEP - io.github.cvc5.ProofRule
-
Bit-vectors – Bitblast bit-vector constant, variable, and terms For constant and variables:
For terms: where is . - BV_EAGER_ATOM - io.github.cvc5.ProofRule
-
Bit-vectors – Bit-vector eager atom
where is of kindBITVECTOR_EAGER_ATOM
.
C
- CARDINALITY_CONSTRAINT - io.github.cvc5.Kind
-
Cardinality constraint on uninterpreted sort.
- CHAIN_RESOLUTION - io.github.cvc5.ProofRule
-
Boolean – N-ary Resolution
where let be nodes viewed as clauses, as defined above let represent the resolution of with with pivot and polarity , as defined above let , for each , let The result of the chain resolution is - 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.
- CNF_AND_NEG - io.github.cvc5.ProofRule
-
Boolean – CNF – And Negative
- CNF_AND_POS - io.github.cvc5.ProofRule
-
Boolean – CNF – And Positive
- CNF_EQUIV_NEG1 - io.github.cvc5.ProofRule
-
Boolean – CNF – Equiv Negative 1
- CNF_EQUIV_NEG2 - io.github.cvc5.ProofRule
-
Boolean – CNF – Equiv Negative 2
- CNF_EQUIV_POS1 - io.github.cvc5.ProofRule
-
Boolean – CNF – Equiv Positive 1
- CNF_EQUIV_POS2 - io.github.cvc5.ProofRule
-
Boolean – CNF – Equiv Positive 2
- CNF_IMPLIES_NEG1 - io.github.cvc5.ProofRule
-
Boolean – CNF – Implies Negative 1
- CNF_IMPLIES_NEG2 - io.github.cvc5.ProofRule
-
Boolean – CNF – Implies Negative 2
- CNF_IMPLIES_POS - io.github.cvc5.ProofRule
-
Boolean – CNF – Implies Positive
- CNF_ITE_NEG1 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Negative 1
- CNF_ITE_NEG2 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Negative 2
- CNF_ITE_NEG3 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Negative 3
- CNF_ITE_POS1 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Positive 1
- CNF_ITE_POS2 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Positive 2
- CNF_ITE_POS3 - io.github.cvc5.ProofRule
-
Boolean – CNF – ITE Positive 3
- CNF_OR_NEG - io.github.cvc5.ProofRule
-
Boolean – CNF – Or Negative
- CNF_OR_POS - io.github.cvc5.ProofRule
-
Boolean – CNF – Or Positive
- CNF_XOR_NEG1 - io.github.cvc5.ProofRule
-
Boolean – CNF – XOR Negative 1
- CNF_XOR_NEG2 - io.github.cvc5.ProofRule
-
Boolean – CNF – XOR Negative 2
- CNF_XOR_POS1 - io.github.cvc5.ProofRule
-
Boolean – CNF – XOR Positive 1
- CNF_XOR_POS2 - io.github.cvc5.ProofRule
-
Boolean – CNF – XOR Positive 2
- Command - Class in io.github.cvc5
- compareTo(Sort) - Method in class io.github.cvc5.Sort
-
Comparison for ordering on sorts.
- compareTo(Term) - Method in class io.github.cvc5.Term
-
Comparison for ordering on terms.
- CONCAT_CONFLICT - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation conflict
where indicates if the direction is reversed, are constants such that is null, in other words, neither is a prefix of the other. - CONCAT_CPROP - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation constant propagation
where are words, is , is , and is . - CONCAT_CSPLIT - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation split for constants
where is . - CONCAT_EQ - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation equality
where stands for string concatenation and indicates if the direction is reversed. - CONCAT_LPROP - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation length propagation
where is . - CONCAT_SPLIT - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation split
where is and is . - CONCAT_UNIFY - io.github.cvc5.ProofRule
-
Strings – Core rules – Concatenation unification
where indicates if the direction is reversed. - CONG - io.github.cvc5.ProofRule
-
Equality – Congruence
where is the application kind. - 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_FINITE_FIELD - io.github.cvc5.Kind
-
Finite field 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.
- CONSTANT_PROP - io.github.cvc5.modes.LearnedLitType
-
An internal literal that can be made into a constant propagation for an input term.
- 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
- Context - Class in io.github.cvc5
- Context() - Constructor for class io.github.cvc5.Context
- CONTRA - io.github.cvc5.ProofRule
-
Boolean – Contradiction
- 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
- CVC5ParserException - Exception in io.github.cvc5
- CVC5ParserException(String) - Constructor for exception io.github.cvc5.CVC5ParserException
D
- Datatype - Class in io.github.cvc5
-
A cvc5 datatype.
- DATATYPE_SORT - io.github.cvc5.SortKind
-
A datatype sort.
- Datatype.ConstIterator - Class in io.github.cvc5
- DatatypeConstructor - Class in io.github.cvc5
-
A cvc5 datatype constructor.
- DatatypeConstructor.ConstIterator - Class in io.github.cvc5
- DatatypeConstructorDecl - Class in io.github.cvc5
-
A cvc5 datatype constructor declaration.
- DatatypeDecl - Class in io.github.cvc5
-
A cvc5 datatype declaration.
- DatatypeDecl() - Constructor for class io.github.cvc5.DatatypeDecl
-
Null datatypeDecl
- DatatypeSelector - Class in io.github.cvc5
-
A cvc5 datatype selector.
- declareDatatype(String, DatatypeConstructorDecl[]) - Method in class io.github.cvc5.Solver
-
Create datatype sort.
- declareFun(String, Sort[], Sort) - Method in class io.github.cvc5.Solver
-
Declare n-ary function symbol.
- declareFun(String, Sort[], Sort, boolean) - Method in class io.github.cvc5.Solver
-
Declare n-ary function symbol.
- declareOracleFun(String, Sort[], Sort, IOracle) - Method in class io.github.cvc5.Solver
-
Declare an oracle function with reference to an implementation.
- declarePool(String, Sort, Term[]) - Method in class io.github.cvc5.Solver
-
Declare a symbolic pool of terms with the given initial value.
- declareSepHeap(Sort, Sort) - Method in class io.github.cvc5.Solver
-
When using separation logic, this sets the location sort and the datatype sort to the given ones.
- declareSort(String, int) - Method in class io.github.cvc5.Solver
-
Declare uninterpreted sort.
- declareSort(String, int, boolean) - Method in class io.github.cvc5.Solver
-
Declare uninterpreted sort.
- declareSygusVar(String, Sort) - Method in class io.github.cvc5.Solver
-
Append
symbol
to the current list of universal variables. - DEFAULT - io.github.cvc5.modes.ProofFormat
-
Use the proof format mode set in the solver options.
- 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.Proof
- deletePointer(long) - Method in class io.github.cvc5.Command
- deletePointer(long) - Method in class io.github.cvc5.Datatype
- deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructor
- deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
- deletePointer(long) - Method in class io.github.cvc5.DatatypeDecl
- deletePointer(long) - Method in class io.github.cvc5.DatatypeSelector
- deletePointer(long) - Method in class io.github.cvc5.Grammar
- deletePointer(long) - Method in class io.github.cvc5.InputParser
- deletePointer(long) - Method in class io.github.cvc5.Op
- deletePointer(long) - Method in class io.github.cvc5.OptionInfo
- deletePointer(long) - Method in class io.github.cvc5.Proof
- deletePointer(long) - Method in class io.github.cvc5.Result
- deletePointer(long) - Method in class io.github.cvc5.Solver
- deletePointer(long) - Method in class io.github.cvc5.Sort
- deletePointer(long) - Method in class io.github.cvc5.Stat
- deletePointer(long) - Method in class io.github.cvc5.Statistics
- deletePointer(long) - Method in class io.github.cvc5.SymbolManager
- deletePointer(long) - Method in class io.github.cvc5.SynthResult
- deletePointer(long) - Method in class io.github.cvc5.Term
- deletePointers() - Static method in class io.github.cvc5.Context
-
Delete all cpp pointers for terms, sorts, etc
- DISTINCT - io.github.cvc5.Kind
-
Disequality.
- DIVISIBLE - io.github.cvc5.Kind
-
Operator for the divisibility-by-
predicate. - DIVISION - io.github.cvc5.Kind
-
Real division, division by 0 undefined, left associative.
- done() - Method in class io.github.cvc5.InputParser
- DOT - io.github.cvc5.modes.ProofFormat
-
Output DOT proof.
- doubleValue() - Method in class io.github.cvc5.OptionInfo
-
Obtain the current value as a double.
- DSL_REWRITE - io.github.cvc5.ProofRule
-
Builtin theory – DSL rewrite
where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n. - DT_CLASH - io.github.cvc5.ProofRule
-
Datatypes – Clash
- DT_COLLAPSE - io.github.cvc5.ProofRule
-
Datatypes – Collapse
where is a constructor, is if is a correctly applied selector, or{@link TypeNode#mkGroundTerm()}
of the proper type otherwise. - DT_INST - io.github.cvc5.ProofRule
-
Datatypes – Instantiation
where is the constructor of the type of t, and is the discriminator (tester) for . - DT_SPLIT - io.github.cvc5.ProofRule
-
Datatypes – Split
where are all the constructors of the type of . - DT_UNIF - io.github.cvc5.ProofRule
-
Datatypes – Unification
where is a constructor.
E
- ENCODE_PRED_TRANSFORM - io.github.cvc5.ProofRule
-
Builtin theory – Encode predicate transformation
where and are equivalent up to their encoding in an external proof format. - ENUM - io.github.cvc5.modes.FindSynthTarget
-
Find the next term in the enumeration of the target grammar.
- EQ_RANGE - io.github.cvc5.Kind
-
Equality over arrays
and over a given range , i.e., \[ \forall k . - EQ_RESOLVE - io.github.cvc5.ProofRule
-
Boolean – Equality resolution
Note this can optionally be seen as a macro for EQUIV_ELIM1 <cvc5.ProofRule.EQUIV_ELIM1
> + RESOLUTION <cvc5.ProofRule.RESOLUTION
>. - 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.Solver
- equals(Object) - Method in class io.github.cvc5.Sort
-
Comparison for structural equality.
- equals(Object) - Method in class io.github.cvc5.SymbolManager
- equals(Object) - Method in class io.github.cvc5.Term
-
Syntactic equality operator.
- equals(Object) - Method in class io.github.cvc5.Triplet
- EQUIV_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – Equivalence elimination version 1
- EQUIV_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – Equivalence elimination version 2
- EVALUATE - io.github.cvc5.ProofRule
-
Builtin theory – Evaluate
Note this is equivalent to:(REWRITE t {@link MethodId#RW_EVALUATE)}
. - EXISTS - io.github.cvc5.Kind
-
Existentially quantified formula.
- EXPONENTIAL - io.github.cvc5.Kind
-
Exponential function.
F
- FACTORING - io.github.cvc5.ProofRule
-
Boolean – Factoring
where is the clause , but every occurence of a literal after its first occurence is omitted. - FALSE_ELIM - io.github.cvc5.ProofRule
-
Equality – False elim
- FALSE_INTRO - io.github.cvc5.ProofRule
-
Equality – False intro
- findSynth(FindSynthTarget) - Method in class io.github.cvc5.Solver
-
Find a target term of interest using sygus enumeration, with no provided grammar.
- findSynth(FindSynthTarget, Grammar) - Method in class io.github.cvc5.Solver
-
Find a target term of interest using sygus enumeration with a provided grammar.
- findSynthNext() - Method in class io.github.cvc5.Solver
-
Try to find a next target term of interest using sygus enumeration.
- FindSynthTarget - Enum in io.github.cvc5.modes
- FINITE_FIELD_ADD - io.github.cvc5.Kind
-
Addition of two or more finite field elements.
- FINITE_FIELD_BITSUM - io.github.cvc5.Kind
-
Bitsum of two or more finite field elements: x + 2y + 4z + ...
- FINITE_FIELD_MULT - io.github.cvc5.Kind
-
Multiplication of two or more finite field elements.
- FINITE_FIELD_NEG - io.github.cvc5.Kind
-
Negation of a finite field element (additive inverse).
- FINITE_FIELD_SORT - io.github.cvc5.SortKind
-
A finite field sort, parameterized by a size.
- 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_SORT - io.github.cvc5.SortKind
-
A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.
- 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.modes.BlockModelsMode
- fromInt(int) - Static method in enum io.github.cvc5.modes.FindSynthTarget
- fromInt(int) - Static method in enum io.github.cvc5.modes.InputLanguage
- fromInt(int) - Static method in enum io.github.cvc5.modes.LearnedLitType
- fromInt(int) - Static method in enum io.github.cvc5.modes.ProofComponent
- fromInt(int) - Static method in enum io.github.cvc5.modes.ProofFormat
- fromInt(int) - Static method in enum io.github.cvc5.ProofRule
- fromInt(int) - Static method in enum io.github.cvc5.RoundingMode
- fromInt(int) - Static method in enum io.github.cvc5.SortKind
- fromInt(int) - Static method in enum io.github.cvc5.UnknownExplanation
- FULL - io.github.cvc5.modes.ProofComponent
-
A proof of false whose free assumptions are a subset of the input formulas F1), ...
- FUNCTION_SORT - io.github.cvc5.SortKind
-
A function sort with given domain sorts and codomain sort.
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.
- getAbstractedKind() - Method in class io.github.cvc5.Sort
- getAliases() - Method in class io.github.cvc5.OptionInfo
- getArguments() - Method in class io.github.cvc5.Proof
- getArrayElementSort() - Method in class io.github.cvc5.Sort
- getArrayIndexSort() - Method in class io.github.cvc5.Sort
- getAssertions() - Method in class io.github.cvc5.Solver
-
Get the list of asserted formulas.
- getBagElementSort() - Method in class io.github.cvc5.Sort
- getBaseInfo() - Method in class io.github.cvc5.OptionInfo
- getBitVectorSize() - Method in class io.github.cvc5.Sort
- getBitVectorValue() - Method in class io.github.cvc5.Term
-
Asserts isBitVectorValue().
- getBitVectorValue(int) - Method in class io.github.cvc5.Term
-
Get the string representation of a bit-vector value.
- getBooleanSort() - Method in class io.github.cvc5.Solver
-
Get the Boolean sort.
- getBooleanValue() - Method in class io.github.cvc5.Term
-
Asserts isBooleanValue().
- getCardinalityConstraint() - Method in class io.github.cvc5.Term
-
Asserts isCardinalityConstraint().
- getChild(int) - Method in class io.github.cvc5.Term
-
Get the child term at a given index.
- getChildren() - Method in class io.github.cvc5.Proof
- getCodomainSort() - Method in class io.github.cvc5.DatatypeSelector
- getCommandName() - Method in class io.github.cvc5.Command
-
Get the name for this command, e.g.
- getConstArrayBase() - Method in class io.github.cvc5.Term
-
Asserts isConstArray().
- getConstructor(int) - Method in class io.github.cvc5.Datatype
-
Get the datatype constructor at a given index.
- getConstructor(String) - Method in class io.github.cvc5.Datatype
-
Get the datatype constructor with the given name.
- getCurrentValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
- getDatatype() - Method in class io.github.cvc5.Sort
- getDatatypeArity() - Method in class io.github.cvc5.Sort
- getDatatypeConstructorArity() - Method in class io.github.cvc5.Sort
- getDatatypeConstructorCodomainSort() - Method in class io.github.cvc5.Sort
- getDatatypeConstructorDomainSorts() - Method in class io.github.cvc5.Sort
- getDatatypeSelectorCodomainSort() - Method in class io.github.cvc5.Sort
- getDatatypeSelectorDomainSort() - Method in class io.github.cvc5.Sort
- getDatatypeTesterCodomainSort() - Method in class io.github.cvc5.Sort
- getDatatypeTesterDomainSort() - Method in class io.github.cvc5.Sort
- getDefaultValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
- getDifficulty() - Method in class io.github.cvc5.Solver
-
Get a difficulty estimate for an asserted formula.
- getDouble() - Method in class io.github.cvc5.Stat
-
Return the double value.
- getFiniteFieldSize() - Method in class io.github.cvc5.Sort
- getFiniteFieldValue() - Method in class io.github.cvc5.Term
-
Get the string representation of a finite field value.
- getFloatingPointExponentSize() - Method in class io.github.cvc5.Sort
- getFloatingPointSignificandSize() - Method in class io.github.cvc5.Sort
- getFloatingPointValue() - Method in class io.github.cvc5.Term
-
Asserts isFloatingPointValue().
- getFunctionArity() - Method in class io.github.cvc5.Sort
- getFunctionCodomainSort() - Method in class io.github.cvc5.Sort
- getFunctionDomainSorts() - Method in class io.github.cvc5.Sort
- getHistogram() - Method in class io.github.cvc5.Stat
-
Return the histogram value.
- getId() - Method in class io.github.cvc5.Term
- getInfo(String) - Method in class io.github.cvc5.Solver
-
Get info from the solver.
- getInstantiatedParameters() - Method in class io.github.cvc5.Sort
-
Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see
Sort.instantiate(Sort[])
). - getInstantiatedTerm(Sort) - Method in class io.github.cvc5.DatatypeConstructor
-
Get the constructor term of this datatype constructor whose return type is
retSort
. - getInstantiations() - Method in class io.github.cvc5.Solver
-
Get a string that contains information about all instantiations made by the quantifiers module.
- getInt() - Method in class io.github.cvc5.Stat
-
Return the integer value.
- getIntegerSort() - Method in class io.github.cvc5.Solver
-
Get the integer sort.
- 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 optionproduce-interpolants
to be set to a mode different fromnone
. - getInterpolant(Term, Grammar) - Method in class io.github.cvc5.Solver
-
Get an interpolant SMT-LIB:
( get-interpolant <conj> <g> )
Requires optionproduce-interpolants
to be set to a mode different fromnone
. - getInterpolantNext() - Method in class io.github.cvc5.Solver
-
Get the next interpolant.
- getKind() - Method in class io.github.cvc5.Op
- getKind() - Method in class io.github.cvc5.Sort
- getKind() - Method in class io.github.cvc5.Term
- getLearnedLiterals() - Method in class io.github.cvc5.Solver
-
Get a list of input literals that are entailed by the current set of assertions.
- getLearnedLiterals(LearnedLitType) - Method in class io.github.cvc5.Solver
-
Get a list of literals that are entailed by the current set of assertions.
- getLogic() - Method in class io.github.cvc5.Solver
-
Get the logic set the solver.
- getLogic() - Method in class io.github.cvc5.SymbolManager
- getMaximum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
- getMinimum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
- getModel(Sort[], Term[]) - Method in class io.github.cvc5.Solver
-
Get the model SMT-LIB:
( get-model )
Requires to enable optionproduce-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
- 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)
andSolver.getOptionInfo(String)
. - getPairs(Pair<K, ? extends AbstractPointer>[]) - Static method in class io.github.cvc5.Utils
- getParameters() - Method in class io.github.cvc5.Datatype
- getPointer() - Method in class io.github.cvc5.Proof
- getPointers(IPointer[]) - Static method in class io.github.cvc5.Utils
- getPointers(IPointer[][]) - Static method in class io.github.cvc5.Utils
- getProof() - Method in class io.github.cvc5.Solver
-
Get refutation proof for the most recent call to checkSat.
- getProof(ProofComponent) - Method in class io.github.cvc5.Solver
-
Get a proof associated with the most recent call to checkSat.
- getProofs(long[]) - Static method in class io.github.cvc5.Utils
-
return proofs array from array of pointers
- 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
- getRealAlgebraicNumberDefiningPolynomial(Term) - Method in class io.github.cvc5.Term
-
Asserts isRealAlgebraicNumber().
- getRealAlgebraicNumberLowerBound() - Method in class io.github.cvc5.Term
-
Asserts isRealAlgebraicNumber().
- getRealAlgebraicNumberUpperBound() - Method in class io.github.cvc5.Term
-
Asserts isRealAlgebraicNumber().
- getRealOrIntegerValueSign() - Method in class io.github.cvc5.Term
-
Get integer or real value sign.
- getRealSort() - Method in class io.github.cvc5.Solver
-
Get the real sort.
- getRealValue() - Method in class io.github.cvc5.Term
-
Asserts isRealValue().
- getRegExpSort() - Method in class io.github.cvc5.Solver
-
Get the regular expression sort.
- getResult() - Method in class io.github.cvc5.Proof
- getRoundingModeSort() - Method in class io.github.cvc5.Solver
-
Get the floating-point rounding mode sort.
- getRoundingModeValue() - Method in class io.github.cvc5.Term
-
Asserts isRoundingModeValue().
- getRule() - Method in class io.github.cvc5.Proof
- getSelector(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().
- getSolver() - Method in class io.github.cvc5.InputParser
- getSort() - Method in class io.github.cvc5.Term
- getSorts(long[]) - Static method in class io.github.cvc5.Utils
- getStatistics() - Method in class io.github.cvc5.Solver
-
Get a snapshot of the current state of the statistic values of this solver.
- getString() - Method in class io.github.cvc5.Stat
-
Return the string value.
- getStringSort() - Method in class io.github.cvc5.Solver
-
Get the string sort.
- getStringValue() - Method in class io.github.cvc5.Term
- getSygusAssumptions() - Method in class io.github.cvc5.Solver
-
Get the list of sygus assumptions.
- getSygusConstraints() - Method in class io.github.cvc5.Solver
-
Get the list of sygus constraints.
- getSymbol() - Method in class io.github.cvc5.Sort
- getSymbol() - Method in class io.github.cvc5.Term
-
Asserts hasSymbol().
- getSymbolManager() - Method in class io.github.cvc5.InputParser
- getSynthSolution(Term) - Method in class io.github.cvc5.Solver
-
Get the synthesis solution of the given term.
- getSynthSolutions(Term[]) - Method in class io.github.cvc5.Solver
-
Get the synthesis solutions of the given terms.
- getTerm() - Method in class io.github.cvc5.DatatypeConstructor
-
Get the constructor term of this datatype constructor.
- getTerm() - Method in class io.github.cvc5.DatatypeSelector
-
Get the selector term of this datatype selector.
- getTerms(long[]) - Static method in class io.github.cvc5.Utils
- getTesterTerm() - Method in class io.github.cvc5.DatatypeConstructor
-
Get the tester term of this datatype constructor.
- getTimeoutCore() - Method in class io.github.cvc5.Solver
-
Get a timeout core, which computes a subset of the current assertions that cause a timeout.
- getTimeoutCoreAssuming(Term[]) - Method in class io.github.cvc5.Solver
-
Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions.
- getTupleLength() - Method in class io.github.cvc5.Sort
- getTupleSorts() - Method in class io.github.cvc5.Sort
- getTupleValue() - Method in class io.github.cvc5.Term
-
Asserts isTupleValue().
- getUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort
-
Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
- getUninterpretedSortConstructorArity() - Method in class io.github.cvc5.Sort
- getUninterpretedSortValue() - Method in class io.github.cvc5.Term
-
Asserts isUninterpretedSortValue().
- getUnknownExplanation() - Method in class io.github.cvc5.Result
- getUnsatAssumptions() - Method in class io.github.cvc5.Solver
-
Get the set of unsat ("failed") assumptions.
- getUnsatCore() - Method in class io.github.cvc5.Solver
-
Get the unsatisfiable core.
- getUnsatCoreLemmas() - Method in class io.github.cvc5.Solver
-
Get the lemmas used to derive unsatisfiability.
- getUpdaterTerm() - Method in class io.github.cvc5.DatatypeSelector
-
Get the updater term of this datatype selector.
- getValue() - Method in enum io.github.cvc5.Kind
- getValue() - Method in enum io.github.cvc5.modes.BlockModelsMode
- getValue() - Method in enum io.github.cvc5.modes.FindSynthTarget
- getValue() - Method in enum io.github.cvc5.modes.InputLanguage
- getValue() - Method in enum io.github.cvc5.modes.LearnedLitType
- getValue() - Method in enum io.github.cvc5.modes.ProofComponent
- getValue() - Method in enum io.github.cvc5.modes.ProofFormat
- getValue() - Method in enum io.github.cvc5.ProofRule
- getValue() - Method in enum io.github.cvc5.RoundingMode
- getValue() - Method in enum io.github.cvc5.SortKind
- 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.
- getVersion() - Method in class io.github.cvc5.Solver
-
Get a string representation of the version of this solver.
- Grammar - Class in io.github.cvc5
-
A Sygus Grammar.
- Grammar(Grammar) - Constructor for class io.github.cvc5.Grammar
- 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_APP_ENCODE - io.github.cvc5.ProofRule
-
Equality – Higher-order application encoding
For example, this rule concludes , where istheHO_APPLY
kind. - HO_APPLY - io.github.cvc5.Kind
-
Higher-order applicative encoding of function application, left associative.
- HO_CONG - io.github.cvc5.ProofRule
-
Equality – Higher-order congruence
Notice that this rule is only used when the application kinds areAPPLY_UF
.
I
- IAND - io.github.cvc5.Kind
-
Integer and.
- IMPLIES - io.github.cvc5.Kind
-
Logical implication.
- IMPLIES_ELIM - io.github.cvc5.ProofRule
-
Boolean – Implication elimination
- impTerm(Term) - Method in class io.github.cvc5.Term
-
Boolean implication.
- INCOMPLETE - io.github.cvc5.UnknownExplanation
-
Incomplete theory solver.
- INPUT - io.github.cvc5.modes.LearnedLitType
-
A literal from the preprocessed set of input formulas that does not occur at top-level after preprocessing.
- InputLanguage - Enum in io.github.cvc5.modes
- InputParser - Class in io.github.cvc5
-
This class is the main interface for retrieving commands and expressions from an input using a parser.
- InputParser(Solver) - Constructor for class io.github.cvc5.InputParser
-
Construct an input parser with an initially empty symbol manager.
- InputParser(Solver, SymbolManager) - Constructor for class io.github.cvc5.InputParser
-
Construct an input parser
- 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.
- INSTANTIATE - io.github.cvc5.ProofRule
-
Quantifiers – Instantiation
The optional argument indicates the inference id that caused the instantiation. - INT_TIGHT_LB - io.github.cvc5.ProofRule
-
Arithmetic – Tighten strict integer lower bounds
where has integer type. - INT_TIGHT_UB - io.github.cvc5.ProofRule
-
Arithmetic – Tighten strict integer upper bounds
where has integer type. - INT_TO_BITVECTOR - io.github.cvc5.Kind
-
Conversion from Int to bit-vector.
- INTEGER_SORT - io.github.cvc5.SortKind
-
The integer sort.
- INTERNAL - io.github.cvc5.modes.LearnedLitType
-
Any internal literal that does not fall into the above categories.
- INTERNAL_KIND - io.github.cvc5.Kind
-
Internal kind.
- INTERNAL_SORT_KIND - io.github.cvc5.SortKind
-
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.
- invoke(Solver, SymbolManager) - Method in class io.github.cvc5.Command
-
Invoke the command on the solver and symbol manager sm, prints the result to output stream out.
- io.github.cvc5 - package io.github.cvc5
- io.github.cvc5.modes - package io.github.cvc5.modes
- IOracle - Interface in io.github.cvc5
- IS_INTEGER - io.github.cvc5.Kind
-
Is-integer predicate.
- isAbstract() - Method in class io.github.cvc5.Sort
-
Determine if this is an abstract sort.
- isArray() - Method in class io.github.cvc5.Sort
-
Determine if this is an array sort.
- isBag() - Method in class io.github.cvc5.Sort
-
Determine if this is a Bag sort.
- isBitVector() - Method in class io.github.cvc5.Sort
-
Determine if this is a bit-vector sort (SMT-LIB:
(_ BitVec i)
). - isBitVectorValue() - Method in class io.github.cvc5.Term
- isBoolean() - Method in class io.github.cvc5.Sort
-
Determine if this is the Boolean sort (SMT-LIB:
Bool
). - isBooleanValue() - Method in class io.github.cvc5.Term
- isCardinalityConstraint() - Method in class io.github.cvc5.Term
- isCodatatype() - Method in class io.github.cvc5.Datatype
- isConstArray() - Method in class io.github.cvc5.Term
- isDatatype() - Method in class io.github.cvc5.Sort
-
Determine if this is a datatype sort.
- isDatatypeConstructor() - Method in class io.github.cvc5.Sort
-
Determine if this is a datatype constructor sort.
- isDatatypeSelector() - Method in class io.github.cvc5.Sort
-
Determine if this is a datatype selector sort.
- isDatatypeTester() - Method in class io.github.cvc5.Sort
-
Determine if this is a datatype tester sort.
- isDatatypeUpdater() - Method in class io.github.cvc5.Sort
-
Determine if this is a datatype updater sort.
- isDefault() - Method in class io.github.cvc5.Stat
-
Does this value hold the default value?
- isDouble() - Method in class io.github.cvc5.Stat
-
Is this value a double?
- isFinite() - Method in class io.github.cvc5.Datatype
- isFiniteField() - Method in class io.github.cvc5.Sort
-
Determine if this is a finite field sort (SMT-LIB:
(_ FiniteField i)
). - isFiniteFieldValue() - Method in class io.github.cvc5.Term
- isFloatingPoint() - Method in class io.github.cvc5.Sort
-
Determine if this is a floatingpoint sort (SMT-LIB:
(_ FloatingPoint eb sb)
). - isFloatingPointNaN() - Method in class io.github.cvc5.Term
- isFloatingPointNegInf() - Method in class io.github.cvc5.Term
- isFloatingPointNegZero() - Method in class io.github.cvc5.Term
- isFloatingPointPosInf() - Method in class io.github.cvc5.Term
- isFloatingPointPosZero() - Method in class io.github.cvc5.Term
- isFloatingPointValue() - Method in class io.github.cvc5.Term
- isFunction() - Method in class io.github.cvc5.Sort
-
Determine if this is a function sort.
- isHistogram() - Method in class io.github.cvc5.Stat
-
Is this value a histogram?
- isIndexed() - Method in class io.github.cvc5.Op
- isInstantiated() - Method in class io.github.cvc5.Sort
-
Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
- isInt() - Method in class io.github.cvc5.Stat
-
Is this value an integer?
- isInteger() - Method in class io.github.cvc5.Sort
-
Determine if this is the integer sort (SMT-LIB:
Int
). - isIntegerValue() - Method in class io.github.cvc5.Term
- isInternal() - Method in class io.github.cvc5.Stat
-
Is this value intended for internal use only?
- isLogicSet() - Method in class io.github.cvc5.Solver
-
Is logic set? Returns whether we called setLogic yet for this solver.
- isLogicSet() - Method in class io.github.cvc5.SymbolManager
- isModelCoreSymbol(Term) - Method in class io.github.cvc5.Solver
-
This returns false if the model value of free constant
v
was not essential for showing the satisfiability of the last call toSolver.checkSat()
using the current model. - isNull() - Method in class io.github.cvc5.Command
- isNull() - Method in class io.github.cvc5.Datatype
- isNull() - Method in class io.github.cvc5.DatatypeConstructor
- isNull() - Method in class io.github.cvc5.DatatypeConstructorDecl
- isNull() - Method in class io.github.cvc5.DatatypeDecl
- isNull() - Method in class io.github.cvc5.DatatypeSelector
- isNull() - Method in class io.github.cvc5.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
-
Determine if this datatype declaration is parametric.
- isPredicate() - Method in class io.github.cvc5.Sort
-
Determine if this is a predicate sort.
- isReal() - Method in class io.github.cvc5.Sort
-
Determine if this is the real sort (SMT-LIB:
Real
). - isRealAlgebraicNumber() - Method in class io.github.cvc5.Term
- isRealValue() - Method in class io.github.cvc5.Term
- isRecord() - Method in class io.github.cvc5.Datatype
- isRecord() - Method in class io.github.cvc5.Sort
-
Determine if this is a record sort.
- isRegExp() - Method in class io.github.cvc5.Sort
-
Determine if this is the regular expression sort (SMT-LIB:
RegLan
). - isRoundingMode() - Method in class io.github.cvc5.Sort
-
Determine if this is the rounding mode sort (SMT-LIB:
RoundingMode
). - isRoundingModeValue() - Method in class io.github.cvc5.Term
- isSat() - Method in class io.github.cvc5.Result
- isSequence() - Method in class io.github.cvc5.Sort
-
Determine if this is a Sequence sort.
- isSequenceValue() - Method in class io.github.cvc5.Term
- isSet() - Method in class io.github.cvc5.Sort
-
Determine if this is a Set sort.
- isSetValue() - Method in class io.github.cvc5.Term
- 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.
- ITE_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – ITE elimination version 1
- ITE_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – ITE elimination version 2
- 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.
- LAST_SORT_KIND - io.github.cvc5.SortKind
-
Marks the upper-bound of this enumeration.
- LearnedLitType - Enum in io.github.cvc5.modes
- LEQ - io.github.cvc5.Kind
-
Less than or equal, chainable.
- LFSC - io.github.cvc5.modes.ProofFormat
-
Output LFSC proof.
- LFSC_RULE - io.github.cvc5.ProofRule
-
External – LFSC Place holder for LFSC rules.
- LITERALS - io.github.cvc5.modes.BlockModelsMode
-
Block models based on the SAT skeleton.
- loadLibraries() - Static method in class io.github.cvc5.Utils
-
Load cvc5 jni library.
- LT - io.github.cvc5.Kind
-
Less than, chainable.
M
- MACRO_ARITH_SCALE_SUM_UB - io.github.cvc5.ProofRule
-
Arithmetic – Adding inequalities An arithmetic literal is a term of the form
where , a polynomial and a rational constant. - MACRO_BV_BITBLAST - io.github.cvc5.ProofRule
-
Bit-vectors – (Macro) Bitblast
wherebitblast()
represents the result of the bit-blasted term as a bit-vector consisting of the output bits of the bit-blasted circuit representation of the term. - MACRO_RESOLUTION - io.github.cvc5.ProofRule
-
Boolean – N-ary Resolution + Factoring + Reordering
where let be nodes viewed as clauses, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION
> let represent the resolution of with with pivot and polarity , as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION
> let be equal, in its set representation, to , for each , let be equal, in its set representation, to The result of the chain resolution is , which is equal, in its set representation, to - MACRO_RESOLUTION_TRUST - io.github.cvc5.ProofRule
-
Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as :cpp:enumerator:`MACRO_RESOLUTION <cvc5.
ProofRule.MACRO_RESOLUTION
>`, but not checked by the internal proof checker. - MACRO_REWRITE - io.github.cvc5.ProofRule
-
Builtin theory – Rewrite
where is a MethodId identifier, which determines the kind of rewriter to apply, e.g. - MACRO_SR_EQ_INTRO - io.github.cvc5.ProofRule
-
Builtin theory – Substitution + Rewriting equality introduction In this rule, we provide a term
and conclude that it is equal to its rewritten form under a (proven) substitution. - MACRO_SR_PRED_ELIM - io.github.cvc5.ProofRule
-
Builtin theory – Substitution + Rewriting predicate elimination
where and are method identifiers. - MACRO_SR_PRED_INTRO - io.github.cvc5.ProofRule
-
Builtin theory – Substitution + Rewriting predicate introduction In this rule, we provide a formula
and conclude it, under the condition that it rewrites to true under a proven substitution. - MACRO_SR_PRED_TRANSFORM - io.github.cvc5.ProofRule
-
Builtin theory – Substitution + Rewriting predicate elimination
where . - MACRO_STRING_INFERENCE - io.github.cvc5.ProofRule
-
Strings – (Macro) String inference
used to bookkeep an inference that has not yet been converted via . - 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.
- mkAbstractSort(SortKind) - Method in class io.github.cvc5.Solver
-
Create an abstract sort.
- 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. - mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.Solver
-
Create a finite field constant in a given field and for a given value.
- mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.Solver
-
Create a finite field sort.
- mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.Solver
-
Create a floating-point value from a bit-vector given in IEEE-754 format.
- mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.Solver
-
Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
- mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.Solver
-
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 enumKind
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(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
- MODUS_PONENS - io.github.cvc5.ProofRule
-
Boolean – Modus Ponens
Note this can optionally be seen as a macro for IMPLIES_ELIM <cvc5.ProofRule.IMPLIES_ELIM
> + RESOLUTION <cvc5.ProofRule.RESOLUTION
>. - 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
- nextCommand() - Method in class io.github.cvc5.InputParser
-
Parse and return the next command.
- nextTerm() - Method in class io.github.cvc5.InputParser
-
Parse and return the next term.
- NONE - io.github.cvc5.modes.ProofFormat
-
Do not translate proof output.
- NOT - io.github.cvc5.Kind
-
Logical negation.
- NOT_AND - io.github.cvc5.ProofRule
-
Boolean – De Morgan – Not And
- NOT_EQUIV_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – Not Equivalence elimination version 1
- NOT_EQUIV_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – Not Equivalence elimination version 2
- NOT_IMPLIES_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – Not Implication elimination version 1
- NOT_IMPLIES_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – Not Implication elimination version 2
- NOT_ITE_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – Not ITE elimination version 1
- NOT_ITE_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – Not ITE elimination version 2
- NOT_NOT_ELIM - io.github.cvc5.ProofRule
-
Boolean – Double negation elimination
- NOT_OR_ELIM - io.github.cvc5.ProofRule
-
Boolean – Not Or elimination
- NOT_XOR_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – Not XOR elimination version 1
- NOT_XOR_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – Not XOR elimination version 2
- notTerm() - Method in class io.github.cvc5.Term
-
Boolean negation.
- NULL_SORT - io.github.cvc5.SortKind
-
Null kind.
- 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.
- Op() - Constructor for class io.github.cvc5.Op
-
Null op
- OptionInfo - Class in io.github.cvc5
-
Holds some description about a particular option, including its name, its aliases, whether the option was explicitly set by the user, and information concerning its value.
- OptionInfo.BaseInfo - Class in io.github.cvc5
-
Abstract class for OptionInfo values
- OptionInfo.ModeInfo - Class in io.github.cvc5
- OptionInfo.NumberInfo<T> - Class in io.github.cvc5
-
Default value, current value, minimum and maximum of a numeric value
- OptionInfo.ValueInfo<T> - Class in io.github.cvc5
-
Has the current and the default value
- OptionInfo.VoidInfo - Class in io.github.cvc5
-
Has no value information
- 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.
- pointer - Variable in class io.github.cvc5.Proof
- pop() - Method in class io.github.cvc5.Solver
-
Pop a level from the assertion stack.
- pop(int) - Method in class io.github.cvc5.Solver
-
Pop (a) level(s) from the assertion stack.
- POW - io.github.cvc5.Kind
-
Arithmetic power.
- POW2 - io.github.cvc5.Kind
-
Power of two.
- PREPROCESS - io.github.cvc5.modes.LearnedLitType
-
A top-level literal (unit clause) from the preprocessed set of input formulas.
- PREPROCESS - io.github.cvc5.modes.ProofComponent
-
Proofs of Gu1 ...
- PREPROCESS_SOLVED - io.github.cvc5.modes.LearnedLitType
-
An equality that was turned into a substitution during preprocessing.
- Proof - Class in io.github.cvc5
-
A cvc5 Proof.
- ProofComponent - Enum in io.github.cvc5.modes
- ProofFormat - Enum in io.github.cvc5.modes
- ProofRule - Enum in io.github.cvc5
- proofToString(Proof) - Method in class io.github.cvc5.Solver
-
Prints a proof into a string with a slected proof format mode.
- proofToString(Proof, ProofFormat) - Method in class io.github.cvc5.Solver
-
Prints a proof into a string with a slected proof format mode.
- 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.
Q
- QUERY - io.github.cvc5.modes.FindSynthTarget
-
Find a query over the given grammar.
R
- RAW_PREPROCESS - io.github.cvc5.modes.ProofComponent
-
Proofs of G1 ...
- RE_ELIM - io.github.cvc5.ProofRule
-
Strings – Regular expressions – Elimination
where is a Boolean indicating whether we are using aggressive eliminations. - RE_INTER - io.github.cvc5.ProofRule
-
Strings – Regular expressions – Intersection
- RE_UNFOLD_NEG - io.github.cvc5.ProofRule
-
Strings – Regular expressions – Negative Unfold
corresponding to the one-step unfolding of the premise. - RE_UNFOLD_NEG_CONCAT_FIXED - io.github.cvc5.ProofRule
-
Strings – Regular expressions – Unfold negative concatenation, fixed
where , corresponding to the one-step unfolding of the premise, optimized for fixed length of component of the regular expression concatenation . - RE_UNFOLD_POS - io.github.cvc5.ProofRule
-
Strings – Regular expressions – Positive Unfold
corresponding to the one-step unfolding of the premise. - REAL_SORT - io.github.cvc5.SortKind
-
The real sort.
- REFL - io.github.cvc5.ProofRule
-
Equality – Reflexivity
- 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.
- REGLAN_SORT - io.github.cvc5.SortKind
-
The regular language sort.
- RELATION_AGGREGATE - io.github.cvc5.Kind
-
Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ...
- RELATION_GROUP - io.github.cvc5.Kind
-
Relation group
partitions tuples of relation such that tuples that have the same projection with indices 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.
- REMOVE_TERM_FORMULA_AXIOM - io.github.cvc5.ProofRule
-
Processing rules – Remove Term Formulas Axiom
- REORDERING - io.github.cvc5.ProofRule
-
Boolean – Reordering
where the set representations of and are the same and the number of literals in is the same of that of . - REQUIRES_CHECK_AGAIN - io.github.cvc5.UnknownExplanation
-
Requires another satisfiability check
- 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.
- RESOLUTION - io.github.cvc5.ProofRule
-
Boolean – Resolution
where and are nodes viewed as clauses, i.e., either anOR
node with each children viewed as a literal or a node viewed as a literal. - RESOURCEOUT - io.github.cvc5.UnknownExplanation
-
Resource limit reached.
- Result - Class in io.github.cvc5
-
Encapsulation of a three-valued solver result, with explanations.
- Result() - Constructor for class io.github.cvc5.Result
-
Null result
- REWRITE - io.github.cvc5.modes.FindSynthTarget
-
Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
- REWRITE_INPUT - io.github.cvc5.modes.FindSynthTarget
-
Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
- REWRITE_UNSOUND - io.github.cvc5.modes.FindSynthTarget
-
Find a term t in the target grammar which rewrites to a term s that is not equivalent to it.
- 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
- ROUNDINGMODE_SORT - io.github.cvc5.SortKind
-
The rounding mode sort.
S
- SAT - io.github.cvc5.modes.ProofComponent
-
A proof of false whose free assumptions are Gu1, ...
- SAT_REFUTATION - io.github.cvc5.ProofRule
-
SAT Refutation for assumption-based unsat cores
where correspond to the unsat core determined by the SAT solver. - SCOPE - io.github.cvc5.ProofRule
-
Scope (a binder for assumptions)
This rule has a dual purpose with :cpp:enumerator:`ASSUME <cvc5.ProofRule.ASSUME
>`. - 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.
- SEQUENCE_SORT - io.github.cvc5.SortKind
-
A sequence sort, whose argument sort is the element sort of the sequence.
- 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 ...
- 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_SORT - io.github.cvc5.SortKind
-
A set sort, whose argument sort is the element sort of the 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.
- setFileInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser
-
Set the input for the given file.
- setIncrementalStringInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser
-
Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
- setInfo(String, String) - Method in class io.github.cvc5.Solver
-
Set info.
- setLogic(String) - Method in class io.github.cvc5.Solver
-
Set logic.
- setOption(String, String) - Method in class io.github.cvc5.Solver
-
Set option.
- setStringInput(InputLanguage, String, String) - Method in class io.github.cvc5.InputParser
-
Set the input to the given concrete input string.
- 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.
- SKOLEM_INTRO - io.github.cvc5.ProofRule
-
Quantifiers – Skolem introduction
where is the unpurified form of skolem . - SKOLEMIZE - io.github.cvc5.ProofRule
-
Quantifiers – Skolemization
or where maps to their representative skolems obtained bySkolemManager.mkSkolemize
, returned in the skolems argument of that method. - SMT_LIB_2_6 - io.github.cvc5.modes.InputLanguage
-
The SMT-LIB version 2.6 language
- SOLVABLE - io.github.cvc5.modes.LearnedLitType
-
An internal literal that is solvable for an input variable.
- 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.
- Sort() - Constructor for class io.github.cvc5.Sort
-
Null sort
- SortKind - Enum in io.github.cvc5
- SPLIT - io.github.cvc5.ProofRule
-
Boolean – Split
- 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_CODE_INJ - io.github.cvc5.ProofRule
-
Strings – Code points
- STRING_CONCAT - io.github.cvc5.Kind
-
String concat.
- STRING_CONTAINS - io.github.cvc5.Kind
-
String contains.
- STRING_DECOMPOSE - io.github.cvc5.ProofRule
-
Strings – Core rules – String decomposition
or alternatively for the reverse: where is and is . - STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule
-
Strings – Extended functions – Eager reduction
where is . - 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_LENGTH_NON_EMPTY - io.github.cvc5.ProofRule
-
Strings – Core rules – Length non-empty
- STRING_LENGTH_POS - io.github.cvc5.ProofRule
-
Strings – Core rules – Length positive
- 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_REDUCTION - io.github.cvc5.ProofRule
-
Strings – Extended functions – Reduction
where is . - 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_SEQ_UNIT_INJ - io.github.cvc5.ProofRule
-
Strings – Sequence unit
Also applies to the case where is a constant sequence of length one. - STRING_SORT - io.github.cvc5.SortKind
-
The string sort.
- 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.
- SUBS - io.github.cvc5.ProofRule
-
Builtin theory – Substitution
where are substitutions, which notice are applied in reverse order. - 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
withreplacements
in this term. - substitute(Term, Term) - Method in class io.github.cvc5.Term
-
Replace
term
withreplacement
in this term. - SYGUS_2_1 - io.github.cvc5.modes.InputLanguage
-
The SyGuS version 2.1 language.
- SymbolManager - Class in io.github.cvc5
- SymbolManager(Solver) - Constructor for class io.github.cvc5.SymbolManager
- SYMM - io.github.cvc5.ProofRule
-
Equality – Symmetry
or - synthFun(String, Term[], Sort) - Method in class io.github.cvc5.Solver
-
Synthesize n-ary function.
- synthFun(String, Term[], Sort, Grammar) - Method in class io.github.cvc5.Solver
-
Synthesize n-ary function following specified syntactic constraints.
- SynthResult - Class in io.github.cvc5
-
Encapsulation of a solver synth result.
- SynthResult() - Constructor for class io.github.cvc5.SynthResult
-
Null synthResult
T
- TABLE_AGGREGATE - io.github.cvc5.Kind
-
Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ...
- TABLE_GROUP - io.github.cvc5.Kind
-
Table group
partitions tuples of table such that tuples that have the same projection with indices are in the same part. - TABLE_JOIN - io.github.cvc5.Kind
-
Table join operator has the form
where are natural numbers, and 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() - Constructor for class io.github.cvc5.Term
-
Null term
- Term.ConstIterator - Class in io.github.cvc5
- THEORY_LEMMAS - io.github.cvc5.modes.ProofComponent
-
Proofs of L1 ...
- 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.Command
- toString(long) - Method in class io.github.cvc5.Datatype
- toString(long) - Method in class io.github.cvc5.DatatypeConstructor
- toString(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
- toString(long) - Method in class io.github.cvc5.DatatypeDecl
- toString(long) - Method in class io.github.cvc5.DatatypeSelector
- toString(long) - Method in class io.github.cvc5.Grammar
- toString(long) - Method in class io.github.cvc5.InputParser
- toString(long) - Method in class io.github.cvc5.Op
- toString(long) - Method in class io.github.cvc5.OptionInfo
- toString(long) - Method in class io.github.cvc5.Result
- toString(long) - Method in class io.github.cvc5.Solver
- toString(long) - Method in class io.github.cvc5.Sort
- toString(long) - Method in class io.github.cvc5.Stat
- toString(long) - Method in class io.github.cvc5.Statistics
- toString(long) - Method in class io.github.cvc5.SymbolManager
- toString(long) - Method in class io.github.cvc5.SynthResult
- toString(long) - Method in class io.github.cvc5.Term
- TRANS - io.github.cvc5.ProofRule
-
Equality – Transitivity
- Triplet<A,B,C> - Class in io.github.cvc5
- Triplet(A, B, C) - Constructor for class io.github.cvc5.Triplet
- TRUE_ELIM - io.github.cvc5.ProofRule
-
Equality – True elim
- TRUE_INTRO - io.github.cvc5.ProofRule
-
Equality – True intro
- TRUST - io.github.cvc5.ProofRule
-
Trusted rule
where is an identifier and is a formula. - TRUST_THEORY_REWRITE - io.github.cvc5.ProofRule
-
Trusted rules – Theory rewrite
where is an equality of the form where is obtained by applying the kind of rewriting given by the method identifier , which is one of:RW_REWRITE_THEORY_PRE
,RW_REWRITE_THEORY_POST
,RW_REWRITE_EQ_EXT
. - TUPLE_PROJECT - io.github.cvc5.Kind
-
Tuple projection.
- TUPLE_SORT - io.github.cvc5.SortKind
-
A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.
U
- UNDEFINED_KIND - io.github.cvc5.Kind
-
Undefined kind.
- UNDEFINED_SORT_KIND - io.github.cvc5.SortKind
-
Undefined kind.
- UNINTERPRETED_SORT - io.github.cvc5.SortKind
-
An uninterpreted sort.
- UNINTERPRETED_SORT_VALUE - io.github.cvc5.Kind
-
The value of an uninterpreted constant.
- UNKNOWN - io.github.cvc5.modes.InputLanguage
-
No language given.
- UNKNOWN - io.github.cvc5.modes.LearnedLitType
-
Special case for when produce-learned-literals is not set.
- UNKNOWN - io.github.cvc5.ProofRule
-
External – AletheLF Place holder for AletheLF rules.
- 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.modes.BlockModelsMode
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.modes.FindSynthTarget
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.modes.InputLanguage
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.modes.LearnedLitType
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.modes.ProofComponent
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.modes.ProofFormat
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.ProofRule
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.RoundingMode
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.SortKind
-
Returns the enum constant of this type with the specified name.
- valueOf(String) - Static method in enum io.github.cvc5.UnknownExplanation
-
Returns the enum constant of this type with the specified name.
- values() - Static method in enum io.github.cvc5.Kind
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.BlockModelsMode
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.FindSynthTarget
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.InputLanguage
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.LearnedLitType
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.ProofComponent
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.modes.ProofFormat
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.ProofRule
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.RoundingMode
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.SortKind
-
Returns an array containing the constants of this enum type, in the order they are declared.
- values() - Static method in enum io.github.cvc5.UnknownExplanation
-
Returns an array containing the constants of this enum type, in the order they are declared.
- VALUES - io.github.cvc5.modes.BlockModelsMode
-
Block models based on the concrete model values for the free variables.
- 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
X
- XOR - io.github.cvc5.Kind
-
Logical exclusive disjunction, left associative.
- XOR_ELIM1 - io.github.cvc5.ProofRule
-
Boolean – XOR elimination version 1
- XOR_ELIM2 - io.github.cvc5.ProofRule
-
Boolean – XOR elimination version 2
- xorTerm(Term) - Method in class io.github.cvc5.Term
-
Boolean exclusive or.
All Classes All Packages