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

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 corresponding synth-fun or synth-inv with the same sort as ntSymbol.

addConstructor(DatatypeConstructorDecl) - Method in class io.github.cvc5.DatatypeDecl

Add datatype constructor declaration.

addRule(Term, Term) - Method in class io.github.cvc5.Grammar

Add rule to the set of rules corresponding to ntSymbol.

addRules(long, long, long[]) - Method in class io.github.cvc5.Grammar

addRules(Term, Term[]) - Method in class io.github.cvc5.Grammar

Add rules to the set of rules corresponding to ntSymbol.

addSelector(String, Sort) - Method in class io.github.cvc5.DatatypeConstructorDecl

Add datatype selector declaration.

addSelectorSelf(String) - Method in class io.github.cvc5.DatatypeConstructorDecl

Add datatype selector declaration whose codomain type is the datatype itself.

addSelectorUnresolved(String, String) - Method in class io.github.cvc5.DatatypeConstructorDecl

Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.

addSygusAssume(Term) - Method in class io.github.cvc5.Solver

Add a forumla to the set of Sygus assumptions.

addSygusConstraint(Term) - Method in class io.github.cvc5.Solver

Add a forumla to the set of Sygus constraints.

addSygusInvConstraint(Term, Term, Term, Term) - Method in class io.github.cvc5.Solver

Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.

ALETHE - io.github.cvc5.modes.ProofFormat

Output Alethe proof.

ALETHE_RULE - io.github.cvc5.ProofRule

External – Alethe Place holder for Alethe rules.

ALF - io.github.cvc5.modes.ProofFormat

Output AletheLF proof using the cvc5 signatures.

ALPHA_EQUIV - io.github.cvc5.ProofRule

Quantifiers – Alpha equivalence \[ \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} \] Notice that this rule is correct only when \(z_1,\dots,z_n\) are not contained in \(FV(F) \setminus \{ y_1,\dots, y_n \}\), where \(FV(\varphi)\) are the free variables of \(\varphi\).

AND - io.github.cvc5.Kind

Logical conjunction.

AND_ELIM - io.github.cvc5.ProofRule

Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]

AND_INTRO - io.github.cvc5.ProofRule

Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]

andTerm(Term) - Method in class io.github.cvc5.Term

Boolean and.

ANNOTATION - io.github.cvc5.ProofRule

Builtin theory – Annotation \[ \inferrule{F \mid a_1 \dots a_n}{F} \] The terms \(a_1 \dots a_n\) can be anything used to annotate the proof node, one example is where \(a_1\) 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 \[ \inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r} \] where \(\diamond\) is a relation symbol and \(\diamond_{inv}\) the inverted relation symbol.

ARITH_MULT_POS - io.github.cvc5.ProofRule

Arithmetic – Multiplication with positive factor \[ \inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r} \] where \(\diamond\) is a relation symbol.

ARITH_MULT_SIGN - io.github.cvc5.ProofRule

Arithmetic – Sign inference \[ \inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0} \] where \(f_1 \dots f_k\) are variables compared to zero (less, greater or not equal), \(m\) is a monomial from these variables and \(\diamond\) 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 \[ \inferruleSC{- \mid t, x, y, a, b, \sigma}{(t \leq tplane) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = -1$} \inferruleSC{- \mid t, x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$} \] where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\) (possibly under rewriting), \(a,b\) are real constants, \(\sigma \in \{ 1, -1\}\) and \(tplane := b \cdot x + a \cdot y - a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\).

ARITH_NL_COVERING_DIRECT - io.github.cvc5.ProofRule

Arithmetic – Coverings – Direct conflict We use \(\texttt{IRP}_k(poly)\) for an IndexedRootPredicate that is defined as the \(k\)'th root of the polynomial \(poly\).

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 \[ \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}} \]

ARITH_POLY_NORM - io.github.cvc5.ProofRule

Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\).

ARITH_SUM_UB - io.github.cvc5.ProofRule

Arithmetic – Sum upper bounds \[ \inferrule{P_1 \dots P_n \mid -}{L \diamond R} \] where \(P_i\) has the form \(L_i \diamond_i R_i\) and \(\diamond_i \in \{<, \leq, =\}\).

ARITH_TRANS_EXP_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp is approximated from above for negative values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\).

ARITH_TRANS_EXP_APPROX_ABOVE_POS - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp is approximated from above for positive values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\).

ARITH_TRANS_EXP_APPROX_BELOW - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp is approximated from below \[ \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)} \] where \(d\) is an odd positive number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, d, c)\) is the \(d\)'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\).

ARITH_TRANS_EXP_NEG - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]

ARITH_TRANS_EXP_POSITIVITY - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]

ARITH_TRANS_EXP_SUPER_LIN - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]

ARITH_TRANS_EXP_ZERO - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]

ARITH_TRANS_PI - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Assert bounds on Pi \[ \inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u} \] where \(l,u\) are valid lower and upper bounds on \(\pi\).

ARITH_TRANS_SINE_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is approximated from above for negative values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\).

ARITH_TRANS_SINE_APPROX_ABOVE_POS - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is approximated from above for positive values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)).

ARITH_TRANS_SINE_APPROX_BELOW_NEG - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is approximated from below for negative values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)).

ARITH_TRANS_SINE_APPROX_BELOW_POS - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is approximated from below for positive values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\).

ARITH_TRANS_SINE_BOUNDS - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]

ARITH_TRANS_SINE_SHIFT - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is shifted to -pi...pi \[ \inferrule{- \mid x, y, s}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})} \] where \(x\) is the argument to sine, \(y\) is a new real skolem that is \(x\) shifted into \(-\pi \dots \pi\) and \(s\) is a new integer slolem that is the number of phases \(y\) is shifted.

ARITH_TRANS_SINE_SYMMETRY - io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]

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 \[ \inferrule{A, B \mid -}{C} \] where \(\neg A, \neg B, C\) are \(x < c, x = c, x > c\) 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 \[ \inferrule{-\mid \mathit{eqrange}(a,b,i,j)} {\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)} \]

ARRAYS_EXT - io.github.cvc5.ProofRule

Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where \(k\) is \(\texttt{arrays::SkolemCache::getExtIndexSkolem}(a\neq b)\).

ARRAYS_READ_OVER_WRITE - io.github.cvc5.ProofRule

Arrays – Read over write \[ \inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)} \]

ARRAYS_READ_OVER_WRITE_1 - io.github.cvc5.ProofRule

Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]

ARRAYS_READ_OVER_WRITE_CONTRA - io.github.cvc5.ProofRule

Arrays – Read over write, contrapositive \[ \inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2} \]

assertFormula(Term) - Method in class io.github.cvc5.Solver

Assert a formula.

ASSUME - io.github.cvc5.ProofRule

Assumption (a leaf) \[ \inferrule{- \mid F}{F} \] 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_EMPTY - io.github.cvc5.Kind

Empty bag.

BAG_FILTER - io.github.cvc5.Kind

Bag filter.

BAG_FOLD - io.github.cvc5.Kind

Bag fold.

BAG_INTER_MIN - io.github.cvc5.Kind

Bag intersection (min).

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_SETOF - io.github.cvc5.Kind

Bag setof.

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_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 \[ \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] 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: \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] For terms: \[ \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)} \] where \(t\) is \(k(t_1,\dots,t_n)\).

BV_EAGER_ATOM - io.github.cvc5.ProofRule

Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where \(F\) is of kind BITVECTOR_EAGER_ATOM.

C

CARDINALITY_CONSTRAINT - io.github.cvc5.Kind

Cardinality constraint on uninterpreted sort.

CHAIN_RESOLUTION - io.github.cvc5.ProofRule

Boolean – N-ary Resolution \[ \inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C} \] where let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined above let \(C_1 \diamond_{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined above let \(C_1' = C_1\), for each \(i > 1\), let \(C_i' = C_{i-1} \diamond{L_{i-1}, \mathit{pol}_{i-1}} C_i'\) Note the list of polarities and pivots are provided as s-expressions.

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 \[ \inferrule{- \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n} \]

CNF_AND_POS - io.github.cvc5.ProofRule

Boolean – CNF – And Positive \[ \inferrule{- \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i} \]

CNF_EQUIV_NEG1 - io.github.cvc5.ProofRule

Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]

CNF_EQUIV_NEG2 - io.github.cvc5.ProofRule

Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]

CNF_EQUIV_POS1 - io.github.cvc5.ProofRule

Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]

CNF_EQUIV_POS2 - io.github.cvc5.ProofRule

Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]

CNF_IMPLIES_NEG1 - io.github.cvc5.ProofRule

Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]

CNF_IMPLIES_NEG2 - io.github.cvc5.ProofRule

Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]

CNF_IMPLIES_POS - io.github.cvc5.ProofRule

Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]

CNF_ITE_NEG1 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Negative 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1} \]

CNF_ITE_NEG2 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Negative 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2} \]

CNF_ITE_NEG3 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Negative 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2} \]

CNF_ITE_POS1 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Positive 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1} \]

CNF_ITE_POS2 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Positive 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2} \]

CNF_ITE_POS3 - io.github.cvc5.ProofRule

Boolean – CNF – ITE Positive 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2} \]

CNF_OR_NEG - io.github.cvc5.ProofRule

Boolean – CNF – Or Negative \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i} \]

CNF_OR_POS - io.github.cvc5.ProofRule

Boolean – CNF – Or Positive \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n} \]

CNF_XOR_NEG1 - io.github.cvc5.ProofRule

Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]

CNF_XOR_NEG2 - io.github.cvc5.ProofRule

Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]

CNF_XOR_POS1 - io.github.cvc5.ProofRule

Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]

CNF_XOR_POS2 - io.github.cvc5.ProofRule

Boolean – CNF – XOR Positive 2 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_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 \[ \inferrule{(c_1\cdot t) = (c_2 \cdot s)\mid b}{\bot} \] where \(b\) indicates if the direction is reversed, \(c_1,\,c_2\) are constants such that \(\texttt{Word::splitConstant}(c_1,c_2, \mathit{index},b)\) is null, in other words, neither is a prefix of the other.

CONCAT_CONFLICT_DEQ - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation conflict for disequal characters \[ \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot} \] where $t_1$ and $s_1$ are constants of length one, or otherwise one side of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to that side is the empty sequence.

CONCAT_CPROP - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = w_3\cdot r)} \] where \(w_1,\,w_2,\,w_3\) are words, \(w_3\) is \(\mathit{pre}(w_2,p)\), \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\), and \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(w_3)))\).

CONCAT_CSPLIT - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)} \] where \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,1))\).

CONCAT_EQ - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation equality \[ \inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s} \] where \(\cdot\) stands for string concatenation and \(b\) indicates if the direction is reversed.

CONCAT_LPROP - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r_t)} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\).

CONCAT_SPLIT - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{(t_1 = s_1\cdot r_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\bot$} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{suf}(s_1,\mathit{len}(t_1)))\).

CONCAT_UNIFY - io.github.cvc5.ProofRule

Strings – Core rules – Concatenation unification \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid b}{t_1 = s_1} \] where \(b\) indicates if the direction is reversed.

CONG - io.github.cvc5.ProofRule

Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?)(t_1,\dots, t_n) = k(f?)(s_1,\dots, s_n)} \] where \(k\) 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 \[ \inferrule{F, \neg F \mid -}{\bot} \]

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-\(k\) 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 \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n.

DT_CLASH - io.github.cvc5.ProofRule

Datatypes – Clash \[ \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$} \]

DT_COLLAPSE - io.github.cvc5.ProofRule

Datatypes – Collapse \[ \inferrule{-\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{ \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r} \] where \(C_j\) is a constructor, \(r\) is \(t_i\) if \(\mathit{sel}_i\) is a correctly applied selector, or {@link TypeNode#mkGroundTerm()} of the proper type otherwise.

DT_INST - io.github.cvc5.ProofRule

Datatypes – Instantiation \[ \inferrule{-\mid t,n}{\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))} \] where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of t, and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).

DT_SPLIT - io.github.cvc5.ProofRule

Datatypes – Split \[ \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)} \] where \(C_1,\dots,C_n\) are all the constructors of the type of \(t\).

DT_UNIF - io.github.cvc5.ProofRule

Datatypes – Unification \[ \inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i} \] where \(C\) is a constructor.

E

ENCODE_PRED_TRANSFORM - io.github.cvc5.ProofRule

Builtin theory – Encode predicate transformation \[ \inferrule{F \mid G}{G} \] where \(F\) and \(G\) 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 \(a\) and \(b\) over a given range \([i,j]\), i.e., \[ \forall k .

EQ_RESOLVE - io.github.cvc5.ProofRule

Boolean – Equality resolution \[ \inferrule{F_1, (F_1 = F_2) \mid -}{F_2} \] 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 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]

EQUIV_ELIM2 - io.github.cvc5.ProofRule

Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]

EVALUATE - io.github.cvc5.ProofRule

Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{Evaluator::evaluate}(t)} \] 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 \[ \inferrule{C_1 \mid -}{C_2} \] where \(C_2\) is the clause \(C_1\), but every occurence of a literal after its first occurence is omitted.

FALSE_ELIM - io.github.cvc5.ProofRule

Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]

FALSE_INTRO - io.github.cvc5.ProofRule

Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]

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 option produce-interpolants to be set to a mode different from none.

getInterpolant(Term, Grammar) - Method in class io.github.cvc5.Solver

Get an interpolant SMT-LIB: ( get-interpolant <conj> <g> ) Requires option produce-interpolants to be set to a mode different from none.

getInterpolantNext() - Method in class io.github.cvc5.Solver

Get the next interpolant.

getKind() - Method in class io.github.cvc5.Op

getKind() - Method in class io.github.cvc5.Sort

getKind() - Method in class io.github.cvc5.Term

getLearnedLiterals() - Method in class io.github.cvc5.Solver

Get a list of input literals that are entailed by the current set of assertions.

getLearnedLiterals(LearnedLitType) - Method in class io.github.cvc5.Solver

Get a list of literals that are entailed by the current set of assertions.

getLogic() - Method in class io.github.cvc5.Solver

Get the logic set the solver.

getLogic() - Method in class io.github.cvc5.SymbolManager

getMaximum() - Method in class io.github.cvc5.OptionInfo.NumberInfo

getMinimum() - Method in class io.github.cvc5.OptionInfo.NumberInfo

getModel(Sort[], Term[]) - Method in class io.github.cvc5.Solver

Get the model SMT-LIB: ( get-model ) Requires to enable option produce-models.

getModelDomainElements(Sort) - Method in class io.github.cvc5.Solver

Get the domain elements of uninterpreted sort s in the current model.

getModes() - Method in class io.github.cvc5.OptionInfo.ModeInfo

getName() - Method in class io.github.cvc5.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

getNullableElementSort() - Method in class io.github.cvc5.Sort

getNumChildren() - Method in class io.github.cvc5.Term

getNumConstructors() - Method in class io.github.cvc5.Datatype

getNumConstructors() - Method in class io.github.cvc5.DatatypeDecl

Get the number of constructors (so far) for this Datatype declaration.

getNumIndices() - Method in class io.github.cvc5.Op

getNumSelectors() - Method in class io.github.cvc5.DatatypeConstructor

getOp() - Method in class io.github.cvc5.Term

getOption(String) - Method in class io.github.cvc5.Solver

Get the value of a given option.

getOptionInfo(String) - Method in class io.github.cvc5.Solver

Get some information about the given option.

getOptionNames() - Method in class io.github.cvc5.Solver

Get all option names that can be used with Solver.setOption(String, String), Solver.getOption(String) and Solver.getOptionInfo(String).

getPairs(Pair<K, ? extends AbstractPointer>[]) - Static method in class io.github.cvc5.Utils

getParameters() - Method in class io.github.cvc5.Datatype

getPointer() - Method in class io.github.cvc5.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 \[ \inferrule{-\mid t}{t= \texttt{TheoryUfRewriter::getHoApplyForApplyUf}(t)} \] For example, this rule concludes \(f(x,y) = @(@(f,x),y)\), where \(@\) isthe HO_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 \[ \inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)} \] Notice that this rule is only used when the application kind \(k\) is either `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.

I

IAND - io.github.cvc5.Kind

Integer and.

IMPLIES - io.github.cvc5.Kind

Logical implication.

IMPLIES_ELIM - io.github.cvc5.ProofRule

Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]

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 \[ \inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The list of terms to instantiate \((t_1 \dots t_n)\) is provided as an s-expression as the first argument.

INT_TIGHT_LB - io.github.cvc5.ProofRule

Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where \(i\) has integer type.

INT_TIGHT_UB - io.github.cvc5.ProofRule

Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where \(i\) 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 to Solver.checkSat() using the current model.

isNull() - Method in class io.github.cvc5.Command

isNull() - Method in class io.github.cvc5.Datatype

isNull() - Method in class io.github.cvc5.DatatypeConstructor

isNull() - Method in class io.github.cvc5.DatatypeConstructorDecl

isNull() - Method in class io.github.cvc5.DatatypeDecl

isNull() - Method in class io.github.cvc5.DatatypeSelector

isNull() - Method in class io.github.cvc5.Op

isNull() - Method in class io.github.cvc5.Result

isNull() - Method in class io.github.cvc5.Sort

Determine if this is the null sort.

isNull() - Method in class io.github.cvc5.SynthResult

isNull() - Method in class io.github.cvc5.Term

isNullable() - Method in class io.github.cvc5.Sort

Determine if this a nullable sort.

isParametric() - Method in class io.github.cvc5.Datatype

isParametric() - Method in class io.github.cvc5.DatatypeDecl

Determine if this datatype declaration is parametric.

isPredicate() - Method in class io.github.cvc5.Sort

Determine if this is a predicate sort.

isReal() - Method in class io.github.cvc5.Sort

Determine if this is the real sort (SMT-LIB: Real).

isRealAlgebraicNumber() - Method in class io.github.cvc5.Term

isRealValue() - Method in class io.github.cvc5.Term

isRecord() - Method in class io.github.cvc5.Datatype

isRecord() - Method in class io.github.cvc5.Sort

Determine if this is a record sort.

isRegExp() - Method in class io.github.cvc5.Sort

Determine if this is the regular expression sort (SMT-LIB: RegLan).

isRoundingMode() - Method in class io.github.cvc5.Sort

Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).

isRoundingModeValue() - Method in class io.github.cvc5.Term

isSat() - Method in class io.github.cvc5.Result

isSequence() - Method in class io.github.cvc5.Sort

Determine if this is a Sequence sort.

isSequenceValue() - Method in class io.github.cvc5.Term

isSet() - Method in class io.github.cvc5.Sort

Determine if this is a Set sort.

isSetValue() - Method in class io.github.cvc5.Term

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 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]

ITE_ELIM2 - io.github.cvc5.ProofRule

Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_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 \(p \diamond c\) where \(\diamond \in \{ <, \leq, =, \geq, > \}\), \(p\) a polynomial and \(c\) a rational constant.

MACRO_BV_BITBLAST - io.github.cvc5.ProofRule

Bit-vectors – (Macro) Bitblast \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] where bitblast() 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 \[ \inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C} \] where let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let \(C_1 \diamond{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let \(C_1'\) be equal, in its set representation, to \(C_1\), for each \(i > 1\), let \(C_i'\) be equal, in its set representation, to \(C_{i-1} \diamond{L_{i-1},\mathit{pol}_{i-1}} C_i'\) The result of the chain resolution is \(C\), which is equal, in its set representation, to \(C_n'\)

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 \[ \inferrule{- \mid t, idr}{t = \texttt{Rewriter}_{idr}(t)} \] where \(idr\) 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 \(t\) 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 \[ \inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))} \] where \(ids\) and \(idr\) are method identifiers.

MACRO_SR_PRED_INTRO - io.github.cvc5.ProofRule

Builtin theory – Substitution + Rewriting predicate introduction In this rule, we provide a formula \(F\) 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 \[ \inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G} \] where \(\texttt{Rewriter}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) = \texttt{Rewriter}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))\).

MACRO_STRING_INFERENCE - io.github.cvc5.ProofRule

Strings – (Macro) String inference \[ \inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F} \] used to bookkeep an inference that has not yet been converted via \(\texttt{strings::InferProofCons::convert}\).

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.

mkNullableIsNull(Term) - Method in class io.github.cvc5.Solver

Create a null tester for a nullable term.

mkNullableIsSome(Term) - Method in class io.github.cvc5.Solver

Create a some tester for a nullable term.

mkNullableLift(Kind, Term[]) - Method in class io.github.cvc5.Solver

Create a term that lifts kind to nullable terms.

mkNullableNull(Sort) - Method in class io.github.cvc5.Solver

Create a constant representing an null of the given sort.

mkNullableSome(Term) - Method in class io.github.cvc5.Solver

Create a nullable some term.

mkNullableSort(Sort) - Method in class io.github.cvc5.Solver

Create a nullable sort.

mkNullableVal(Term) - Method in class io.github.cvc5.Solver

Create a selector for nullable term.

mkOp(Kind) - Method in class io.github.cvc5.Solver

Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).

mkOp(Kind, int) - Method in class io.github.cvc5.Solver

Create operator of kind: DIVISIBLE BITVECTOR_REPEAT BITVECTOR_ZERO_EXTEND BITVECTOR_SIGN_EXTEND BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_RIGHT INT_TO_BITVECTOR FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_TOTAL FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_TOTAL TUPLE_UPDATE See enum Kind for a description of the parameters.

mkOp(Kind, int[]) - Method in class io.github.cvc5.Solver

Create operator of Kind: TUPLE_PROJECT See enum Kind for a description of the parameters.

mkOp(Kind, int, int) - Method in class io.github.cvc5.Solver

Create operator of Kind: BITVECTOR_EXTRACT FLOATINGPOINT_TO_FP_FROM_IEEE_BV FLOATINGPOINT_TO_FP_FROM_FP FLOATINGPOINT_TO_FP_FROM_REAL FLOATINGPOINT_TO_FP_FROM_SBV FLOATINGPOINT_TO_FP_FROM_UBV See enum Kind for a description of the parameters.

mkOp(Kind, String) - Method in class io.github.cvc5.Solver

Create operator of kind: Kind.DIVISIBLE (to support arbitrary precision integers) See enum Kind for a description of the parameters.

mkParamSort() - Method in class io.github.cvc5.Solver

Create a sort parameter.

mkParamSort(String) - Method in class io.github.cvc5.Solver

Create a sort parameter.

mkPi() - Method in class io.github.cvc5.Solver

Create a constant representing the number Pi.

mkPredicateSort(Sort[]) - Method in class io.github.cvc5.Solver

Create a predicate sort.

mkReal(long) - Method in class io.github.cvc5.Solver

Create a real constant from an integer.

mkReal(long, long) - Method in class io.github.cvc5.Solver

Create a real constant from a rational.

mkReal(String) - Method in class io.github.cvc5.Solver

Create a real constant from a string.

mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.Solver

Create a record sort

mkRegexpAll() - Method in class io.github.cvc5.Solver

Create a regular expression all (re.all) term.

mkRegexpAllchar() - Method in class io.github.cvc5.Solver

Create a regular expression allchar (re.allchar) term.

mkRegexpNone() - Method in class io.github.cvc5.Solver

Create a regular expression none (re.none) term.

mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.Solver

Create a rounding mode constant.

mkSepEmp() - Method in class io.github.cvc5.Solver

Create a separation logic empty term.

mkSepNil(Sort) - Method in class io.github.cvc5.Solver

Create a separation logic nil term.

mkSequenceSort(Sort) - Method in class io.github.cvc5.Solver

Create a sequence sort.

mkSetSort(Sort) - Method in class io.github.cvc5.Solver

Create a set sort.

mkString(int[]) - Method in class io.github.cvc5.Solver

Create a String constant.

mkString(String) - Method in class io.github.cvc5.Solver

Create a String constant.

mkString(String, boolean) - Method in class io.github.cvc5.Solver

Create a String constant.

mkTerm(Kind) - Method in class io.github.cvc5.Solver

Create 0-ary term of given kind.

mkTerm(Kind, Term) - Method in class io.github.cvc5.Solver

Create a unary term of given kind.

mkTerm(Kind, Term[]) - Method in class io.github.cvc5.Solver

Create n-ary term of given kind.

mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.Solver

Create binary term of given kind.

mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.Solver

Create ternary term of given kind.

mkTerm(Op) - Method in class io.github.cvc5.Solver

Create nullary term of given kind from a given operator.

mkTerm(Op, Term) - Method in class io.github.cvc5.Solver

Create unary term of given kind from a given operator.

mkTerm(Op, Term[]) - Method in class io.github.cvc5.Solver

Create n-ary term of given kind from a given operator.

mkTerm(Op, Term, Term) - Method in class io.github.cvc5.Solver

Create binary term of given kind from a given operator.

mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.Solver

Create ternary term of given kind from a given operator.

mkTrue() - Method in class io.github.cvc5.Solver

Create a Boolean true constant.

mkTuple(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 \[ \inferrule{F_1, (F_1 \rightarrow F_2) \mid -}{F_2} \] 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

NARY_CONG - io.github.cvc5.ProofRule

Equality – N-ary Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid k}{k(t_1,\dots, t_n) = k(s_1,\dots, s_n)} \] where \(k\) is the application kind.

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 \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]

NOT_EQUIV_ELIM1 - io.github.cvc5.ProofRule

Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]

NOT_EQUIV_ELIM2 - io.github.cvc5.ProofRule

Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]

NOT_IMPLIES_ELIM1 - io.github.cvc5.ProofRule

Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]

NOT_IMPLIES_ELIM2 - io.github.cvc5.ProofRule

Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]

NOT_ITE_ELIM1 - io.github.cvc5.ProofRule

Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]

NOT_ITE_ELIM2 - io.github.cvc5.ProofRule

Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]

NOT_NOT_ELIM - io.github.cvc5.ProofRule

Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]

NOT_OR_ELIM - io.github.cvc5.ProofRule

Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]

NOT_XOR_ELIM1 - io.github.cvc5.ProofRule

Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]

NOT_XOR_ELIM2 - io.github.cvc5.ProofRule

Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_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.

NULLABLE_LIFT - io.github.cvc5.Kind

Lifting operator for nullable terms.

NULLABLE_SORT - io.github.cvc5.SortKind

A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.

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 \[ \inferrule{-\mid F,b}{F = \texttt{strings::RegExpElimination::eliminate}(F, b)} \] where \(b\) is a Boolean indicating whether we are using aggressive eliminations.

RE_INTER - io.github.cvc5.ProofRule

Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{inter}(R_1,R_2)} \]

RE_UNFOLD_NEG - io.github.cvc5.ProofRule

Strings – Regular expressions – Negative Unfold \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNeg}(t\not\in R)} \] 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 \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNegConcatFixed}(t\not\in R,L,i)} \] where \(\texttt{RegExpOpr::getRegExpConcatFixed}(t\not\in R, i) = L\), corresponding to the one-step unfolding of the premise, optimized for fixed length of component \(i\) of the regular expression concatenation \(R\).

RE_UNFOLD_POS - io.github.cvc5.ProofRule

Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{\texttt{RegExpOpr::reduceRegExpPos}(t\in R)} \] 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 \[ \inferrule{-\mid t}{t = t} \]

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 \(((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of relation \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part.

RELATION_IDEN - io.github.cvc5.Kind

Relation identity.

RELATION_JOIN - io.github.cvc5.Kind

Relation join.

RELATION_JOIN_IMAGE - io.github.cvc5.Kind

Relation join image.

RELATION_PRODUCT - io.github.cvc5.Kind

Relation cartesian product.

RELATION_PROJECT - io.github.cvc5.Kind

Relation projection operator extends tuple projection operator to sets.

RELATION_TCLOSURE - io.github.cvc5.Kind

Relation transitive closure.

RELATION_TRANSPOSE - io.github.cvc5.Kind

Relation transpose.

REMOVE_TERM_FORMULA_AXIOM - io.github.cvc5.ProofRule

Processing rules – Remove Term Formulas Axiom \[ \inferrule{- \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)} \]

REORDERING - io.github.cvc5.ProofRule

Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the set representations of \(C_1\) and \(C_2\) are the same and the number of literals in \(C_2\) is the same of that of \(C_1\).

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 \[ \inferrule{C_1, C_2 \mid pol, L}{C} \] where \(C_1\) and \(C_2\) are nodes viewed as clauses, i.e., either an OR 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 \[ \inferrule{F_1 \dots F_n \mid -}{\bot} \] where \(F_1 \dots F_n\) correspond to the unsat core determined by the SAT solver.

SCOPE - io.github.cvc5.ProofRule

Scope (a binder for assumptions) \[ \inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$} \] 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 \[ \inferrule{-\mid k}{k = t} \] where \(t\) is the unpurified form of skolem \(k\).

SKOLEMIZE - io.github.cvc5.ProofRule

Quantifiers – Skolemization \[ \inferrule{\exists x_1\dots x_n.\> F\mid -}{F\sigma} \] or \[ \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} \] where \(\sigma\) maps \(x_1,\dots,x_n\) to their representative skolems obtained by SkolemManager.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 \[ \inferrule{- \mid F}{F \lor \neg F} \]

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 \[ \inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t\neq s} \]

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 \[ \inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n} \] or alternatively for the reverse: \[ \inferrule{\mathit{len}(t) \geq n\mid \top}{t = w_1\cdot w_2 \wedge \mathit{len}(w_2) = n} \] where \(w_1\) is \(\mathit{skolem}(\mathit{pre}(t,n)\) and \(w_2\) is \(\mathit{skolem}(\mathit{suf}(t,n)\).

STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule

Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).

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 \[ \inferrule{t\neq ''\mid -}{\mathit{len}(t) \neq 0} \]

STRING_LENGTH_POS - io.github.cvc5.ProofRule

Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0} \]

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 \[ \inferrule{-\mid t}{R\wedge t = w} \] where \(w\) is \(\texttt{strings::StringsPreprocess::reduce}(t, R, \dots)\).

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 \[ \inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y} \] Also applies to the case where \(\mathit{unit}(y)\) 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 \[ \inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)} \] where \(\sigma_{ids}(F_i)\) 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 with replacements in this term.

substitute(Term, Term) - Method in class io.github.cvc5.Term

Replace term with replacement 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 \[ \inferrule{t_1 = t_2\mid -}{t_2 = t_1} \] or \[ \inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1} \]

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 \(((\_ \; table.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of table \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part.

TABLE_JOIN - io.github.cvc5.Kind

Table join operator has the form \(((\_ \; table.join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)\) where \(m_1 \; n_1 \; \dots \; m_k \; n_k\) are natural numbers, and \(A, B\) are tables.

TABLE_PRODUCT - io.github.cvc5.Kind

Table cross product.

TABLE_PROJECT - io.github.cvc5.Kind

Table projection operator extends tuple projection operator to tables.

TANGENT - io.github.cvc5.Kind

Tangent function.

Term - Class in io.github.cvc5

A cvc5 Term.

Term() - 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 \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]

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 \[ \inferrule{F=\top\mid -}{F} \]

TRUE_INTRO - io.github.cvc5.ProofRule

Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]

TRUST - io.github.cvc5.ProofRule

Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where \(tid\) is an identifier and \(F\) is a formula.

TRUST_THEORY_REWRITE - io.github.cvc5.ProofRule

Trusted rules – Theory rewrite \[ \inferrule{- \mid F, tid, rid}{F} \] where \(F\) is an equality of the form \(t = t'\) where \(t'\) is obtained by applying the kind of rewriting given by the method identifier \(rid\), 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 – Alethe Place holder for Alethe 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

WITNESS - io.github.cvc5.Kind

Witness.

X

XOR - io.github.cvc5.Kind

Logical exclusive disjunction, left associative.

XOR_ELIM1 - io.github.cvc5.ProofRule

Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]

XOR_ELIM2 - io.github.cvc5.ProofRule

Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]

xorTerm(Term) - Method in class io.github.cvc5.Term

Boolean exclusive or.

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