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.

AbstractPlugin - Class in io.github.cvc5

AbstractPlugin(TermManager) - Constructor for class io.github.cvc5.AbstractPlugin

Create plugin instance.

ACI_NORM - io.github.cvc5.ProofRule

Builtin theory – associative/commutative/idempotency/identity normalization \[ \inferrule{- \mid t = s}{t = s} \] where \(\texttt{expr::isACNorm(t, s)} = \top\).

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.

addPlugin(AbstractPlugin) - Method in class io.github.cvc5.Solver

Add plugin to this solver.

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.

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.

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_ABS_ELIM_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-elim-int

ARITH_ABS_ELIM_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-elim-real

ARITH_ABS_EQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-eq

ARITH_ABS_INT_GT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-int-gt

ARITH_ABS_REAL_GT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-real-gt

ARITH_COSECENT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cosecent-elim

ARITH_COSINE_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cosine-elim

ARITH_COTANGENT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cotangent-elim

ARITH_DIV_ELIM_TO_REAL1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-elim-to-real1

ARITH_DIV_ELIM_TO_REAL2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-elim-to-real2

ARITH_DIV_TOTAL_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-total-int

ARITH_DIV_TOTAL_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-total-real

ARITH_DIV_TOTAL_ZERO_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-total-zero-int

ARITH_DIV_TOTAL_ZERO_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-div-total-zero-real

ARITH_ELIM_GT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-gt

ARITH_ELIM_INT_GT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-int-gt

ARITH_ELIM_INT_LT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-int-lt

ARITH_ELIM_LEQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-leq

ARITH_ELIM_LT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-lt

ARITH_EQ_ELIM_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-eq-elim-int

ARITH_EQ_ELIM_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-eq-elim-real

ARITH_GEQ_NORM1_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-norm1-int

ARITH_GEQ_NORM1_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-norm1-real

ARITH_GEQ_NORM2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-norm2

ARITH_GEQ_TIGHTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-tighten

ARITH_INT_DIV_TOTAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-div-total

ARITH_INT_DIV_TOTAL_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-div-total-one

ARITH_INT_DIV_TOTAL_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-div-total-zero

ARITH_INT_MOD_TOTAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-mod-total

ARITH_INT_MOD_TOTAL_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-mod-total-one

ARITH_INT_MOD_TOTAL_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-int-mod-total-zero

ARITH_LEQ_NORM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-leq-norm

ARITH_MUL_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-mul-one

ARITH_MUL_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-mul-zero

ARITH_MULT_ABS_COMPARISON - io.github.cvc5.ProofRule

Arithmetic – Non-linear multiply absolute value comparison \[ \inferrule{F_1 \dots F_n \mid -}{F} \] where \(F\) is of the form \(\left| t_1 \cdot t_n \right| \diamond \left| s_1 \cdot s_n \right|\).

ARITH_MULT_DIST - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-mult-dist

ARITH_MULT_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-mult-flatten

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 x, y, a, b, \sigma}{(t \leq tplane) = ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = \bot$} \inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) = ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = \top$} \] where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\), \(a,b\) are real constants, \(\sigma \in \{ \top, \bot\}\) and \(tplane := b \cdot x + a \cdot y - a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\).

ARITH_PI_NOT_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-pi-not-int

ARITH_PLUS_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-plus-flatten

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_POLY_NORM_REL - io.github.cvc5.ProofRule

Arithmetic – Polynomial normalization for relations ..

ARITH_POW_ELIM - io.github.cvc5.ProofRewriteRule

Arithmetic – power elimination \[ (x ^ c) = (x \cdot \ldots \cdot x) \] where \(c\) is a non-negative integer.

ARITH_REDUCTION - io.github.cvc5.ProofRule

Arithmetic – Reduction \[ \inferrule{- \mid t}{F} \] where \(t\) is an application of an extended arithmetic operator (e.g.

ARITH_REFL_GEQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-refl-geq

ARITH_REFL_GT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-refl-gt

ARITH_REFL_LEQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-refl-leq

ARITH_REFL_LT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-refl-lt

ARITH_SECENT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-secent-elim

ARITH_SINE_PI2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-sine-pi2

ARITH_SINE_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-sine-zero

ARITH_STRING_PRED_ENTAIL - io.github.cvc5.ProofRewriteRule

Arithmetic – strings predicate entailment \[ (>= n 0) = true \] Where \(n\) can be shown to be greater than or equal to \(0\) by reasoning about string length being positive and basic properties of addition and multiplication.

ARITH_STRING_PRED_SAFE_APPROX - io.github.cvc5.ProofRewriteRule

Arithmetic – strings predicate entailment \[ (>= n 0) = (>= m 0) \] Where \(m\) is a safe under-approximation of \(n\), namely we have that \((>= n m)\) and \((>= m 0)\).

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_TANGENT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-tangent-elim

ARITH_TO_INT_ELIM_TO_REAL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-to-int-elim-to-real

ARITH_TO_REAL_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-to-real-elim

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}{-\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 skolem 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.

ARITH_VTS_DELTA - io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_DELTA_FREE - io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_INFINITY - io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_INFINITY_FREE - io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARRAY_DEQ_DIFF - io.github.cvc5.SkolemId

The array diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (select A k) (select B k)))).

ARRAY_READ_OVER_WRITE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-read-over-write

ARRAY_READ_OVER_WRITE_SPLIT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-read-over-write-split

ARRAY_READ_OVER_WRITE2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-read-over-write2

ARRAY_SORT - io.github.cvc5.SortKind

An array sort, whose argument sorts are the index and element sorts of the array.

ARRAY_STORE_OVERWRITE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-store-overwrite

ARRAY_STORE_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-store-self

ARRAYS_EQ_RANGE_EXPAND - io.github.cvc5.ProofRewriteRule

Arrays – Expansion of array range equality \[ \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 the \(\texttt{ARRAY_DEQ_DIFF}\) skolem for `(a, 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} \]

ARRAYS_SELECT_CONST - io.github.cvc5.ProofRewriteRule

Arrays – Constant array select \[ (select A x) = c \] where \(A\) is a constant array storing element \(c\).

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.

BAGS_CARD_COMBINE - io.github.cvc5.SkolemId

An uninterpreted function for bag.card operator: To compute (bag.card A), we need a function that counts multiplicities of distinct elements.

BAGS_CHOOSE - io.github.cvc5.SkolemId

An interpreted function uf for bag.choose operator: (bag.choose A) is replaced by (uf A) along with the inference that (>= (bag.count (uf A) A) 1) when A is non-empty.

BAGS_DEQ_DIFF - io.github.cvc5.SkolemId

The bag diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (bag.count k A) (bag.count k B)))).

BAGS_DISTINCT_ELEMENTS - io.github.cvc5.SkolemId

An uninterpreted function for distinct elements of a bag A, which returns the n^th distinct element of the bag.

BAGS_DISTINCT_ELEMENTS_SIZE - io.github.cvc5.SkolemId

A skolem variable for the size of the distinct elements of a bag A.

BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT - io.github.cvc5.SkolemId

An uninterpreted function for the union of distinct elements in a bag (Bag T).

BAGS_FOLD_CARD - io.github.cvc5.SkolemId

An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need to guess the cardinality n of bag A using a skolem function with BAGS_FOLD_CARD id.

BAGS_FOLD_COMBINE - io.github.cvc5.SkolemId

An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function that accumulates intermidiate values.

BAGS_FOLD_ELEMENTS - io.github.cvc5.SkolemId

An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function for elements of A.

BAGS_FOLD_UNION_DISJOINT - io.github.cvc5.SkolemId

An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function for elements of A which is given by elements defined in BAGS_FOLD_ELEMENTS.

BAGS_MAP_INDEX - io.github.cvc5.SkolemId

A skolem variable for the index that is unique per terms (bag.map f A), y, e where: f: (-> E T), A: (Bag E), y: T, e: E Number of skolem indices: 5 1: a map term of the form (bag.map f A).

BAGS_MAP_PREIMAGE_INJECTIVE - io.github.cvc5.SkolemId

A skolem for the preimage of an element y in (bag.map f A) such that (= (f x) y) where f: (-> E T) is an injective function.

BAGS_MAP_SUM - io.github.cvc5.SkolemId

An uninterpreted function for bag.map operator: If bag A is {uf(1), ..., uf(n)} (see BAGS_DISTINCT_ELEMENTS}, then the multiplicity of an element y in a bag (bag.map f A) is sum(n), where sum: (-> Int Int) is a skolem function such that: sum(0) = 0 sum(i) = sum (i-1) + (bag.count (uf i) A) Number of skolem indices: 3 1: the function f of type (-> E T).

BaseInfo() - Constructor for class io.github.cvc5.OptionInfo.BaseInfo

BETA_REDUCE - io.github.cvc5.ProofRewriteRule

Equality – Beta reduction \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1, \ldots, 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_BIT - io.github.cvc5.Kind

Retrieves the bit at the given index from a bit-vector as a Bool term.

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

Converts a list of Bool terms to a bit-vector.

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.

BOOL_AND_CONF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-conf

BOOL_AND_CONF2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-conf2

BOOL_AND_DE_MORGAN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-de-morgan

BOOL_AND_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-false

BOOL_AND_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-flatten

BOOL_DOUBLE_NOT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-double-not-elim

BOOL_EQ_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-false

BOOL_EQ_NREFL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-nrefl

BOOL_EQ_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-true

BOOL_IMPL_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-elim

BOOL_IMPL_FALSE1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-false1

BOOL_IMPL_FALSE2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-false2

BOOL_IMPL_TRUE1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-true1

BOOL_IMPL_TRUE2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-true2

BOOL_IMPLIES_DE_MORGAN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-implies-de-morgan

BOOL_NOT_EQ_ELIM1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-eq-elim1

BOOL_NOT_EQ_ELIM2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-eq-elim2

BOOL_NOT_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-false

BOOL_NOT_ITE_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-ite-elim

BOOL_NOT_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-true

BOOL_NOT_XOR_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-xor-elim

BOOL_OR_AND_DISTRIB - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-and-distrib

BOOL_OR_DE_MORGAN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-de-morgan

BOOL_OR_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-flatten

BOOL_OR_TAUT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-taut

BOOL_OR_TAUT2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-taut2

BOOL_OR_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-true

BOOL_XOR_COMM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-comm

BOOL_XOR_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-elim

BOOL_XOR_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-false

BOOL_XOR_NREFL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-nrefl

BOOL_XOR_REFL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-refl

BOOL_XOR_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-true

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_ADD_COMBINE_LIKE_TERMS - io.github.cvc5.ProofRewriteRule

Bitvectors – Combine like terms during addition by counting terms

BV_ADD_TWO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-add-two

BV_ADD_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-add-zero

BV_AND_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-concat-pullup

BV_AND_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-flatten

BV_AND_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-one

BV_AND_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-simplify-1

BV_AND_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-simplify-2

BV_AND_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-and-zero

BV_ASHR_BY_CONST_0 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ashr-by--0

BV_ASHR_BY_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ashr-by--1

BV_ASHR_BY_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ashr-by--2

BV_ASHR_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ashr-zero

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_BITWISE_IDEMP_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-bitwise-idemp-1

BV_BITWISE_IDEMP_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-bitwise-idemp-2

BV_BITWISE_NOT_AND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-bitwise-not-and

BV_BITWISE_NOT_OR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-bitwise-not-or

BV_BITWISE_SLICING - io.github.cvc5.ProofRewriteRule

Bitvectors – Extract continuous substrings of bitvectors \[ bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ...

BV_COMMUTATIVE_ADD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-add

BV_COMMUTATIVE_AND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-and

BV_COMMUTATIVE_MUL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-mul

BV_COMMUTATIVE_OR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-or

BV_COMMUTATIVE_XOR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-xor

BV_COMP_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-comp-eliminate

BV_CONCAT_EXTRACT_MERGE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-concat-extract-merge

BV_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-concat-flatten

BV_CONCAT_MERGE_CONST - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-concat-merge-

BV_CONCAT_TO_MULT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-concat-to-mult

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.

BV_EMPTY - io.github.cvc5.SkolemId

The empty bitvector.

BV_EQ_EXTRACT_ELIM1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-eq-extract-elim1

BV_EQ_EXTRACT_ELIM2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-eq-extract-elim2

BV_EQ_EXTRACT_ELIM3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-eq-extract-elim3

BV_EXTRACT_BITWISE_AND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-bitwise-and

BV_EXTRACT_BITWISE_OR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-bitwise-or

BV_EXTRACT_BITWISE_XOR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-bitwise-xor

BV_EXTRACT_CONCAT_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-concat-1

BV_EXTRACT_CONCAT_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-concat-2

BV_EXTRACT_CONCAT_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-concat-3

BV_EXTRACT_CONCAT_4 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-concat-4

BV_EXTRACT_EXTRACT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-extract

BV_EXTRACT_MULT_LEADING_BIT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-mult-leading-bit

BV_EXTRACT_NOT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-not

BV_EXTRACT_SIGN_EXTEND_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-sign-extend-1

BV_EXTRACT_SIGN_EXTEND_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-sign-extend-2

BV_EXTRACT_SIGN_EXTEND_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-sign-extend-3

BV_EXTRACT_WHOLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-whole

BV_ITE_CONST_CHILDREN_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite--children-1

BV_ITE_CONST_CHILDREN_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite--children-2

BV_ITE_EQUAL_CHILDREN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-equal-children

BV_ITE_EQUAL_COND_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-equal-cond-1

BV_ITE_EQUAL_COND_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-equal-cond-2

BV_ITE_EQUAL_COND_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-equal-cond-3

BV_ITE_MERGE_ELSE_ELSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-merge-else-else

BV_ITE_MERGE_ELSE_IF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-merge-else-if

BV_ITE_MERGE_THEN_ELSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-merge-then-else

BV_ITE_MERGE_THEN_IF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-merge-then-if

BV_LSHR_BY_CONST_0 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lshr-by--0

BV_LSHR_BY_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lshr-by--1

BV_LSHR_BY_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lshr-by--2

BV_LSHR_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lshr-zero

BV_LT_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lt-self

BV_MERGE_SIGN_EXTEND_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-merge-sign-extend-1

BV_MERGE_SIGN_EXTEND_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-merge-sign-extend-2

BV_MERGE_SIGN_EXTEND_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-merge-sign-extend-3

BV_MUL_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mul-flatten

BV_MUL_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mul-one

BV_MUL_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mul-zero

BV_MULT_DISTRIB_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-distrib-1

BV_MULT_DISTRIB_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-distrib-2

BV_MULT_DISTRIB_CONST_ADD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-distrib--add

BV_MULT_DISTRIB_CONST_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-distrib--neg

BV_MULT_DISTRIB_CONST_SUB - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-distrib--sub

BV_MULT_POW2_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-pow2-1

BV_MULT_POW2_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-pow2-2

BV_MULT_POW2_2B - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-pow2-2b

BV_MULT_SIMPLIFY - io.github.cvc5.ProofRewriteRule

Bitvectors – Extract negations from multiplicands \[ bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c)) \]

BV_MULT_SLT_MULT_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-slt-mult-1

BV_MULT_SLT_MULT_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-mult-slt-mult-2

BV_NAND_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-nand-eliminate

BV_NEG_ADD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-neg-add

BV_NEG_IDEMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-neg-idemp

BV_NEG_MULT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-neg-mult

BV_NEG_SUB - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-neg-sub

BV_NOR_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-nor-eliminate

BV_NOT_IDEMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-idemp

BV_NOT_NEQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-neq

BV_NOT_SLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-sle

BV_NOT_ULE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-ule

BV_NOT_ULT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-ult

BV_NOT_XOR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-xor

BV_OR_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-concat-pullup

BV_OR_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-flatten

BV_OR_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-one

BV_OR_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-simplify-1

BV_OR_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-simplify-2

BV_OR_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-or-zero

BV_REDAND_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-redand-eliminate

BV_REDOR_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-redor-eliminate

BV_REPEAT_ELIM - io.github.cvc5.ProofRewriteRule

Bitvectors – Extract continuous substrings of bitvectors \[ repeat(n,\ t) = concat(t ...

BV_ROTATE_LEFT_ELIMINATE_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-rotate-left-eliminate-1

BV_ROTATE_LEFT_ELIMINATE_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-rotate-left-eliminate-2

BV_ROTATE_RIGHT_ELIMINATE_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-rotate-right-eliminate-1

BV_ROTATE_RIGHT_ELIMINATE_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-rotate-right-eliminate-2

BV_SADDO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-saddo-eliminate

BV_SDIV_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sdiv-eliminate

BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops

BV_SDIVO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sdivo-eliminate

BV_SGE_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sge-eliminate

BV_SGT_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sgt-eliminate

BV_SHL_BY_CONST_0 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-shl-by--0

BV_SHL_BY_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-shl-by--1

BV_SHL_BY_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-shl-by--2

BV_SHL_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-shl-zero

BV_SIGN_EXTEND_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-eliminate

BV_SIGN_EXTEND_ELIMINATE_0 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-eliminate-0

BV_SIGN_EXTEND_EQ_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-eq--1

BV_SIGN_EXTEND_EQ_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-eq--2

BV_SIGN_EXTEND_ULT_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-ult--1

BV_SIGN_EXTEND_ULT_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-ult--2

BV_SIGN_EXTEND_ULT_CONST_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-ult--3

BV_SIGN_EXTEND_ULT_CONST_4 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sign-extend-ult--4

BV_SLE_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sle-eliminate

BV_SLE_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sle-self

BV_SLT_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-slt-eliminate

BV_SLT_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-slt-zero

BV_SMOD_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-smod-eliminate

BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops

BV_SMULO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J.

BV_SREM_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-srem-eliminate

BV_SREM_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops

BV_SSUBO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ssubo-eliminate

BV_SUB_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sub-eliminate

BV_TO_INT_UF - io.github.cvc5.SkolemId

A skolem function introduced by the int-blaster.

BV_TO_NAT_ELIM - io.github.cvc5.ProofRewriteRule

UF – Bitvector to natural elimination \[ \texttt{bv2nat}(t) = t_1 + \ldots + t_n \] where for \(i=1, \ldots, n\), \(t_i\) is \(\texttt{ite}(x[i-1, i-1] = 1, 2^i, 0)\).

BV_UADDO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-uaddo-eliminate

BV_UDIV_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-udiv-one

BV_UDIV_POW2_NOT_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-udiv-pow2-not-one

BV_UDIV_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-udiv-zero

BV_UGE_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-uge-eliminate

BV_UGT_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ugt-eliminate

BV_UGT_UREM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ugt-urem

BV_ULE_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-eliminate

BV_ULE_MAX - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-max

BV_ULE_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-self

BV_ULE_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-zero

BV_ULT_ADD_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-add-one

BV_ULT_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-one

BV_ULT_ONES - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-ones

BV_ULT_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-self

BV_ULT_ZERO_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-zero-1

BV_ULT_ZERO_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-zero-2

BV_UMULO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Bitvectors – Unsigned multiplication overflow detection elimination See M.Gok, M.J.

BV_UREM_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-urem-one

BV_UREM_POW2_NOT_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-urem-pow2-not-one

BV_UREM_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-urem-self

BV_USUBO_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-usubo-eliminate

BV_XNOR_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xnor-eliminate

BV_XOR_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-concat-pullup

BV_XOR_DUPLICATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-duplicate

BV_XOR_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-flatten

BV_XOR_NOT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-not

BV_XOR_ONES - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-ones

BV_XOR_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-simplify-1

BV_XOR_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-simplify-2

BV_XOR_SIMPLIFY_3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-simplify-3

BV_XOR_ZERO - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-zero

BV_ZERO_EXTEND_ELIMINATE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-extend-eliminate

BV_ZERO_EXTEND_ELIMINATE_0 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-extend-eliminate-0

BV_ZERO_EXTEND_EQ_CONST_1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-extend-eq--1

BV_ZERO_EXTEND_EQ_CONST_2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-extend-eq--2

BV_ZERO_ULE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-ule

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,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}, pol_{i-1}} C_i'\) Note the list of polarities and pivots are provided as s-expressions.

check() - Method in class io.github.cvc5.AbstractPlugin

Call to check, return vector of lemmas to add to the SAT solver.

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 \neq 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 = t_3\cdot r)} \] where \(w_1,\,w_2\) are words, \(t_3\) is \(\mathit{pre}(w_2,p)\), \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\), and \(r\) is the purification skolem for \(\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 the purification skolem for \(\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)} \] where \(r\) is the purification Skolem for \(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_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) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\bot$} \] where \(r\) is the purification skolem for \(\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))\) and \(\epsilon\) is the empty string (or sequence).

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 \bot}{t_1 = s_1} \] Alternatively for the reverse: \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) = \mathit{len}(s_2)\mid \top}{t_2 = s_2} \]

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.

CPC - io.github.cvc5.modes.ProofFormat

Output Cooperating Proof Calculus proof based on Eunoia signatures.

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

deletePointer(long) - Method in class io.github.cvc5.TermManager

deletePointers() - Static method in class io.github.cvc5.Context

Delete all cpp pointers for terms, sorts, etc

DISTINCT - io.github.cvc5.Kind

Disequality.

DISTINCT_BINARY_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule distinct-binary-elim

DISTINCT_CARD_CONFLICT - io.github.cvc5.ProofRewriteRule

Builtin – Distinct cardinality conflict \[ \texttt{distinct}(t_1, \ldots, tn) = \bot \] where \(n\) is greater than the cardinality of the type of \(t_1, \ldots, t_n\).

DISTINCT_ELIM - io.github.cvc5.ProofRewriteRule

Builtin – Distinct elimination \[ \texttt{distinct}(t_1, t_2) = \neg (t_1 = t2) \] if \(n = 2\), or \[ \texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i=1}^n \bigwedge_{j=i+1}^n t_i \neq t_j \] if \(n > 2\)

DIV_BY_ZERO - io.github.cvc5.SkolemId

The function for division by zero.

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.

DIVISION_TOTAL - io.github.cvc5.Kind

Real division, division by 0 defined to be 0, 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.

DRAT_REFUTATION - io.github.cvc5.ProofRule

DRAT Refutation \[ \inferrule{F_1 \dots F_n \mid D, P}{\bot} \] where \(F_1 \dots F_n\) correspond to the clauses in the DIMACS file given by filename `D` and `P` is a filename of a file storing a DRAT proof.

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 `id` is a ProofRewriteRule whose definition in the RARE DSL 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_SELECTOR - io.github.cvc5.ProofRewriteRule

Datatypes – collapse selector \[ s_i(c(t_1, \ldots, t_n)) = t_i \] where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

DT_COLLAPSE_TESTER - io.github.cvc5.ProofRewriteRule

Datatypes – collapse tester \[ \mathit{is}_c(c(t_1, \ldots, t_n)) = true \] or alternatively \[ \mathit{is}_c(d(t_1, \ldots, t_n)) = false \] where \(c\) and \(d\) are distinct constructors.

DT_COLLAPSE_TESTER_SINGLETON - io.github.cvc5.ProofRewriteRule

Datatypes – collapse tester \[ \mathit{is}_c(t) = true \] where \(c\) is the only constructor of its associated datatype.

DT_COLLAPSE_UPDATER - io.github.cvc5.ProofRewriteRule

Datatypes – collapse tester \[ u_{c,i}(c(t_1, \ldots, t_i, \ldots, t_n), s) = c(t_1, \ldots, s, \ldots, t_n) \] or alternatively \[ u_{c,i}(d(t_1, \ldots, t_n), s) = d(t_1, \ldots, t_n) \] where \(c\) and \(d\) are distinct constructors.

DT_CONS_EQ - io.github.cvc5.ProofRewriteRule

Datatypes – constructor equality \[ (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(c\) is a constructor.

DT_CONS_EQ_CLASH - io.github.cvc5.ProofRewriteRule

Datatypes – constructor equality clash \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct constructor applications.

DT_CYCLE - io.github.cvc5.ProofRewriteRule

Datatypes – cycle \[ (x = t[x]) = \bot \] where all terms on the path to \(x\) in \(t[x]\) are applications of constructors, and this path is non-empty.

DT_INST - io.github.cvc5.ProofRewriteRule

Datatypes – Instantiation \[ \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_MATCH_ELIM - io.github.cvc5.ProofRewriteRule

Datatypes – match elimination \[ \texttt{match}(t ((p_1 c_1) \ldots (p_n c_n))) = \texttt{ite}(F_1, r_1, \texttt{ite}( \ldots, r_n)) \] where for \(i=1, \ldots, n\), \(F_1\) is a formula that holds iff \(t\) matches \(p_i\) and \(r_i\) is the result of a substitution on \(c_i\) based on this match.

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_UPDATER_ELIM - io.github.cvc5.ProofRewriteRule

Datatypes - updater elimination \[ u_{c,i}(t, s) = ite(\mathit{is}_c(t), c(s_0(t), \ldots, s, \ldots s_n(t)), t) \] where \(s_i\) is the \(i^{th}\) selector for constructor \(c\).

E

ENCODE_EQ_INTRO - io.github.cvc5.ProofRule

Builtin theory – Encode equality introduction \[ \inferrule{- \mid t}{t=t'} \] where \(t\) and \(t'\) 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_COND_DEQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-cond-deq

EQ_ITE_LIFT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-ite-lift

EQ_RANGE - io.github.cvc5.Kind

Equality over arrays \(a\) and \(b\) over a given range \([i,j]\), i.e., \[ \forall k .

EQ_REFL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-refl

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

EQ_SYMM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-symm

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

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.DatatypeConstructor

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.DatatypeConstructorDecl

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.DatatypeDecl

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.DatatypeSelector

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.Grammar

Referential equality operator.

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

Referential equality operator.

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

Operator overloading for equality of two synthesis results.

equals(Object) - Method in class io.github.cvc5.Term

Syntactic equality operator.

equals(Object) - Method in class io.github.cvc5.TermManager

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{evaluate}(t)} \] where \(\texttt{evaluate}\) is implemented by calling the method \(\texttt{Evalutor::evaluate}\) in :cvc5src:`theory/evaluator.h` with an empty substitution.

EXISTS - io.github.cvc5.Kind

Existentially quantified formula.

EXISTS_ELIM - io.github.cvc5.ProofRewriteRule

Quantifiers – Exists elimination \[ \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F \]

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 occurrence of a literal after its first occurrence 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.

FP_MAX_ZERO - io.github.cvc5.SkolemId

A skolem function that is unique per floating-point sort, introduced for the undefined zero case of fp.max.

FP_MIN_ZERO - io.github.cvc5.SkolemId

A skolem function that is unique per floating-point sort, introduced for the undefined zero case of fp.min.

FP_TO_REAL - io.github.cvc5.SkolemId

A skolem function introduced for the undefined of fp.to_real that is unique per floating-point sort.

FP_TO_SBV - io.github.cvc5.SkolemId

A skolem function introduced for the undefined out-ouf-bounds case of fp.to_sbv that is unique per floating-point sort and sort of the arguments to the operator.

FP_TO_UBV - io.github.cvc5.SkolemId

A skolem function introduced for the undefined out-ouf-bounds case of fp.to_ubv that is unique per floating-point sort and sort of the arguments to the operator.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.

getBooleanSort() - Method in class io.github.cvc5.TermManager

Get the Boolean sort.

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

Asserts isBooleanValue().

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

Asserts isCardinalityConstraint().

getChild(int) - Method in class io.github.cvc5.Term

Get the child term at a given index.

getChildren() - Method in class io.github.cvc5.Proof

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

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

Get the name for this command, e.g.

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

Asserts isConstArray().

getConstructor(int) - Method in class io.github.cvc5.Datatype

Get the datatype constructor at a given index.

getConstructor(String) - Method in class io.github.cvc5.Datatype

Get the datatype constructor with the given name.

getCurrentValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo

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

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

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

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

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

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

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

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

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

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

Get the list of sorts that have been declared via `declare-sort` commands.

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

Get the list of terms that have been declared via `declare-fun` and `declare-const`.

getDefaultValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo

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

Get a difficulty estimate for an asserted formula.

getDouble() - Method in class io.github.cvc5.Stat

Return the double value.

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

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

Get the string representation of a finite field value.

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

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

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

Asserts isFloatingPointValue().

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

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

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

getHistogram() - Method in class io.github.cvc5.Stat

Return the histogram value.

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

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

Get info from the solver.

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

Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see Sort.instantiate(Sort[])).

getInstantiatedTerm(Sort) - Method in class io.github.cvc5.DatatypeConstructor

Get the constructor term of this datatype constructor whose return type is retSort.

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

Get a string that contains information about all instantiations made by the quantifiers module.

getInt() - Method in class io.github.cvc5.Stat

Return the integer value.

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

Deprecated.

This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.

getIntegerSort() - Method in class io.github.cvc5.TermManager

Get the integer sort.

getIntegerSort(long) - Method in class io.github.cvc5.TermManager

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

Asserts isIntegerValue().

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

Get an interpolant.

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

Get an interpolant.

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

Get the next interpolant.

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

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

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

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

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

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

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

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

Get the logic set the solver.

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

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

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

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

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

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

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

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

getName() - Method in class io.github.cvc5.AbstractPlugin

Get the name of the plugin (for debugging).

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

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

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

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

getName() - Method in class io.github.cvc5.OptionInfo

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

Get a mapping from terms to names that have been given to them via the :named attribute.

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

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

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

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

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

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

getNumIndicesForSkolemId(SkolemId) - Method in class io.github.cvc5.TermManager

Get the number of indices for a given skolem id.

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

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

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

Get the value of a given option.

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

Get some information about the given option.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.

getRealSort() - Method in class io.github.cvc5.TermManager

Get the real sort.

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

Asserts isRealValue().

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

Deprecated.

This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.

getRegExpSort() - Method in class io.github.cvc5.TermManager

Get the regular expression sort.

getResult() - Method in class io.github.cvc5.Proof

getRewriteRule() - Method in class io.github.cvc5.Proof

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

Deprecated.

This function is deprecated and replaced by TermManager.getRoundingModeSort(). It will be removed in a future release.

getRoundingModeSort() - Method in class io.github.cvc5.TermManager

Get the floating-point rounding mode sort.

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

Asserts isRoundingModeValue().

getRule() - Method in class io.github.cvc5.Proof

getSelector(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().

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

Get skolem identifier of this term.

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

Get the skolem indices of this term.

getSolver() - Method in class io.github.cvc5.InputParser

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

getSorts(long[]) - Static method in class io.github.cvc5.Utils

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

Get a snapshot of the current state of the statistic values of this solver.

getStatistics() - Method in class io.github.cvc5.TermManager

Get a snapshot of the current state of the statistic values of this term manager.

getString() - Method in class io.github.cvc5.Stat

Return the string value.

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

Deprecated.

This function is deprecated and replaced by TermManager.getStringSort(). It will be removed in a future release.

getStringSort() - Method in class io.github.cvc5.TermManager

Get the string sort.

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

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

Get the list of sygus assumptions.

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

Get the list of sygus constraints.

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

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

Asserts hasSymbol().

getSymbolManager() - Method in class io.github.cvc5.InputParser

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

Get the synthesis solution of the given term.

getSynthSolutions(Term[]) - Method in class io.github.cvc5.Solver

Get the synthesis solutions of the given terms.

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

Get the constructor term of this datatype constructor.

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

Get the selector term of this datatype selector.

getTermManager() - Method in class io.github.cvc5.AbstractPlugin

Get the associated term manager instance

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

Get the associated term manager instance

getTerms(long[]) - Static method in class io.github.cvc5.Utils

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

Get the tester term of this datatype constructor.

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

Get a timeout core, which computes a subset of the current assertions that cause a timeout.

getTimeoutCoreAssuming(Term[]) - Method in class io.github.cvc5.Solver

Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions.

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

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

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

Asserts isTupleValue().

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

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

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

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

Asserts isUninterpretedSortValue().

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

Get an explanation for an unknown query result.

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

Get the set of unsat ("failed") assumptions.

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

Get the unsatisfiable core.

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

Get the lemmas used to derive unsatisfiability.

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

Get the updater term of this datatype selector.

getValue() - Method in enum io.github.cvc5.Kind

getValue() - Method in enum io.github.cvc5.modes.BlockModelsMode

getValue() - Method in enum io.github.cvc5.modes.FindSynthTarget

getValue() - Method in enum io.github.cvc5.modes.InputLanguage

getValue() - Method in enum io.github.cvc5.modes.LearnedLitType

getValue() - Method in enum io.github.cvc5.modes.ProofComponent

getValue() - Method in enum io.github.cvc5.modes.ProofFormat

getValue() - Method in enum io.github.cvc5.ProofRewriteRule

getValue() - Method in enum io.github.cvc5.ProofRule

getValue() - Method in enum io.github.cvc5.RoundingMode

getValue() - Method in enum io.github.cvc5.SkolemId

getValue() - 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

GROUND_TERM - io.github.cvc5.SkolemId

An arbitrary ground term of a given sort.

GT - io.github.cvc5.Kind

Greater than, chainable.

H

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

Get the hash value of a datatype.

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

Get the hash value of a datatype constructor.

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

Get the hash value of a datatype constructor declaration.

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

Get the hash value of a datatype declaration.

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

Get the hash value of a datatype selector.

hashCode() - Method in class io.github.cvc5.Grammar

Get the hash value of a grammar.

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

Get the hash value of an operator.

hashCode() - Method in class io.github.cvc5.Proof

Get the hash value of a proof.

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

Get the hash value of a result.

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

Get the hash value of a sort.

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

Get the hash value of a synthesis result.

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

Get the hash value of a term.

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=t'} \] where `t'` is the higher-order application that is equivalent to `t`, as implemented by uf.TheoryUfRewriter.getHoApplyForApplyUf.

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

HO_DEQ_DIFF - io.github.cvc5.SkolemId

The higher-roder diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (A k1 ... kn) (B k1 ... kn)))).

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_DIV_BY_ZERO - io.github.cvc5.SkolemId

The function for integer division by zero.

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.

INT_TO_BV_ELIM - io.github.cvc5.ProofRewriteRule

UF – Integer to bitvector elimination \[ \texttt{int2bv}_n(t) = (bvconcat t_1 \ldots t_n) \] where for \(i=1, \ldots, n\), \(t_i\) is \(\texttt{ite}(\texttt{mod}(t,2^n) \geq 2^{n-1}, 1, 0)\).

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

The identifier of the skolem is not exported.

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

Integer division, division by 0 defined to be 0, left associative.

INTS_MODULUS - io.github.cvc5.Kind

Integer modulus, modulus by 0 undefined.

INTS_MODULUS_TOTAL - io.github.cvc5.Kind

Integer modulus, t modulus by 0 defined to be t.

intValue() - Method in class io.github.cvc5.OptionInfo

Obtain the current value as as int.

invoke(Solver, SymbolManager) - Method in class io.github.cvc5.Command

Invoke the command on the solver and symbol manager sm and return any resulting output as a string.

io.github.cvc5 - package io.github.cvc5

io.github.cvc5.modes - package io.github.cvc5.modes

IOracle - Interface in io.github.cvc5

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

Determine if this is the null grammar.

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

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

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

Determine if this is the null sort.

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

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

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

Determine if this a nullable sort.

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

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

Determine if this datatype declaration is parametric.

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

Determine if this is a predicate sort.

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

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

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

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

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

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

Determine if this is a record sort.

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

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

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

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

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

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

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

Determine if this is a Sequence sort.

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

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

Determine if this is a Set sort.

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

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

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

Determine if this is the string sort (SMT-LIB: String)..

isString() - Method in class io.github.cvc5.Stat

Is this value a string?

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

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

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

Determine if this a tuple sort.

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

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

Determine if this is an uninterpreted sort.

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

Determine if this is an uninterpreted sort constructor.

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

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

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

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

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

Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.

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} \]

ITE_ELSE_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-false

ITE_ELSE_LOOKAHEAD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-lookahead

ITE_ELSE_LOOKAHEAD_NOT_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-lookahead-not-self

ITE_ELSE_LOOKAHEAD_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-lookahead-self

ITE_ELSE_NEG_LOOKAHEAD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-neg-lookahead

ITE_ELSE_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-true

ITE_EQ - io.github.cvc5.ProofRule

Processing rules – If-then-else equivalence \[ \inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}} \]

ITE_EQ_BRANCH - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-eq-branch

ITE_EXPAND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-expand

ITE_FALSE_COND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-false-cond

ITE_NEG_BRANCH - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-neg-branch

ITE_NOT_COND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-not-cond

ITE_THEN_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-false

ITE_THEN_LOOKAHEAD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-lookahead

ITE_THEN_LOOKAHEAD_NOT_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-lookahead-not-self

ITE_THEN_LOOKAHEAD_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-lookahead-self

ITE_THEN_NEG_LOOKAHEAD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-neg-lookahead

ITE_THEN_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-true

ITE_TRUE_COND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-true-cond

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.

LAMBDA_ELIM - io.github.cvc5.ProofRewriteRule

Equality – Lambda elimination \[ (\lambda x_1 \ldots x_n.\> f(x_1 \ldots x_n)) = f \]

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.

LIBPATH_IN_JAR - Static variable in class io.github.cvc5.Utils

LITERALS - io.github.cvc5.modes.BlockModelsMode

Block models based on the SAT skeleton.

loadLibraries() - Static method in class io.github.cvc5.Utils

Load cvc5 native libraries.

loadLibraryFromJar(Path, String, String) - Static method in class io.github.cvc5.Utils

Loads a native library from a specified path within a JAR file and loads it into the JVM.

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_ARITH_STRING_PRED_ENTAIL - io.github.cvc5.ProofRewriteRule

Arithmetic – strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where \(c\) is a Boolean constant.

MACRO_ARRAYS_DISTINCT_ARRAYS - io.github.cvc5.ProofRewriteRule

Arrays – Macro distinct arrays \[ (A = B) = \bot \] where \(A\) and \(B\) are distinct array values, that is, the Node.isConst method returns true for both.

MACRO_ARRAYS_NORMALIZE_CONSTANT - io.github.cvc5.ProofRewriteRule

Arrays – Macro normalize constant \[ A = B \] where \(B\) is the result of normalizing the array value \(A\) into a canonical form, using the internal method TheoryArraysRewriter.normalizeConstant.

MACRO_BOOL_NNF_NORM - io.github.cvc5.ProofRewriteRule

Booleans – Negation Normal Form with normalization \[ F = G \] where \(G\) is the result of applying negation normal form to \(F\) with additional normalizations, see TheoryBoolRewriter.computeNnfNorm.

MACRO_BV_BITBLAST - io.github.cvc5.ProofRule

Bit-vectors – (Macro) Bitblast \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] where \(\texttt{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_DT_CONS_EQ - io.github.cvc5.ProofRewriteRule

Datatypes – Macro constructor equality \[ (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] where \(t_1, \ldots, t_n\) and \(s_1, \ldots, s_n\) are subterms of \(t\) and \(s\) that occur at the same position respectively (beneath constructor applications), or alternatively \[ (t = s) = false \] where \(t\) and \(s\) have subterms that occur in the same position (beneath constructor applications) that are distinct.

MACRO_QUANT_MERGE_PRENEX - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro merge prenex \[ \forall X_1.\> \ldots \forall X_n.\> F = \forall X.\> F \] where \(X_1 \ldots X_n\) are lists of variables and \(X\) is the result of removing duplicates from \(X_1 \ldots X_n\).

MACRO_QUANT_MINISCOPE - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro miniscoping \[ \forall X.\> F_1 \wedge \cdots \wedge F_n = G_1 \wedge \cdots \wedge G_n \] where each \(G_i\) is semantically equivalent to \(\forall X.\> F_i\), or alternatively \[ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{G_1}{G_2} \] where \(C\) does not have any free variable in \(X\).

MACRO_QUANT_PARTITION_CONNECTED_FV - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro connected free variable partitioning \[ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_{1,1} \vee \ldots \vee F_{1,k_1}) \vee \ldots \vee (\forall X_m.\> F_{m,1} \vee \ldots \vee F_{m,k_m}) \] where \(X_1, \ldots, X_m\) is a partition of \(X\).

MACRO_QUANT_PRENEX - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro prenex \[ (\forall X.\> F_1 \vee \cdots \vee (\forall Y.\> F_i) \vee \cdots \vee F_n) = (\forall X Z.\> F_1 \vee \cdots \vee F_i\{ Y \mapsto Z \} \vee \cdots \vee F_n) \]

MACRO_QUANT_REWRITE_BODY - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro quantifiers rewrite body \[ \forall X.\> F = \forall X.\> G \] where \(G\) is semantically equivalent to \(F\).

MACRO_QUANT_VAR_ELIM_EQ - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro variable elimination equality \[ \forall x Y.\> F = \forall Y.\> F \{ x \mapsto t \} \] where \(\neg F\) entails \(x = t\).

MACRO_QUANT_VAR_ELIM_INEQ - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro variable elimination inequality \[ \forall x Y.\> F = \forall Y.\> G \] where \(G\) is the result of replacing all literals containing \(x\) with a constant.

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 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{rewrite}_{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{rewrite}_{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{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ\cdots \circ \sigma_{ids, ida}(F_1)) =\\ \texttt{rewrite}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) \] More generally, this rule also holds when: \(\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))\) where \(F'\) and \(G'\) are the result of each side of the equation above.

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}\).

MACRO_SUBSTR_STRIP_SYM_LENGTH - io.github.cvc5.ProofRewriteRule

Strings – strings substring strip symbolic length \[ str.substr(s, n, m) = t \] where \(t\) is obtained by fully or partially stripping components of \(s\) based on \(n\) and \(m\).

MATCH - io.github.cvc5.Kind

Match expression.

MATCH_BIND_CASE - io.github.cvc5.Kind

Match case with binders, for constructors with selectors and variable patterns.

MATCH_CASE - io.github.cvc5.Kind

Match case for nullary constructors.

MEMOUT - io.github.cvc5.UnknownExplanation

Memory limit reached.

mkAbstractSort(SortKind) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.

mkAbstractSort(SortKind) - Method in class io.github.cvc5.TermManager

Create an abstract sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkArraySort(Sort, Sort). It will be removed in a future release.

mkArraySort(Sort, Sort) - Method in class io.github.cvc5.TermManager

Create an array sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.

mkBagSort(Sort) - Method in class io.github.cvc5.TermManager

Create a bag sort.

mkBitVector(int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.

mkBitVector(int) - Method in class io.github.cvc5.TermManager

Create a bit-vector constant of given size and value = 0.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.

mkBitVector(int, long) - Method in class io.github.cvc5.TermManager

Create a bit-vector constant of given size and value.

mkBitVector(int, String, int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkBitVector(int, String, int). It will be removed in a future release.

mkBitVector(int, String, int) - Method in class io.github.cvc5.TermManager

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

mkBitVectorSort(int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkBitVectorSort(int). It will be removed in a future release.

mkBitVectorSort(int) - Method in class io.github.cvc5.TermManager

Create a bit-vector sort.

mkBoolean(boolean) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkBoolean(boolean). It will be removed in a future release.

mkBoolean(boolean) - Method in class io.github.cvc5.TermManager

Create a Boolean constant.

mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.

mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.TermManager

Create a cardinality constraint for an uninterpreted sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkConst(Sort). It will be removed in a future release.

mkConst(Sort) - Method in class io.github.cvc5.TermManager

Create a free constant with a default symbol name.

mkConst(Sort, String) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.

mkConst(Sort, String) - Method in class io.github.cvc5.TermManager

Create a free constant.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.

mkConstArray(Sort, Term) - Method in class io.github.cvc5.TermManager

Create a constant array with the provided constant value stored at every index

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

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.

mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.TermManager

Create a datatype constructor declaration.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.

mkDatatypeDecl(String) - Method in class io.github.cvc5.TermManager

Create a datatype declaration.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.

mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.TermManager

Create a datatype declaration.

mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.

mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.TermManager

Create a datatype declaration.

mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.

mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.TermManager

Create a datatype declaration.

mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeSort(DatatypeDecl). It will be removed in a future release.

mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.TermManager

Create a datatype sort.

mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkDatatypeSorts(DatatypeDecl[]). It will be removed in a future release.

mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.TermManager

Create a vector of datatype sorts.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.

mkEmptyBag(Sort) - Method in class io.github.cvc5.TermManager

Create a constant representing an empty bag of the given sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.

mkEmptySequence(Sort) - Method in class io.github.cvc5.TermManager

Create an empty sequence of the given element sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.

mkEmptySet(Sort) - Method in class io.github.cvc5.TermManager

Create a constant representing an empty set of the given sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFalse(). It will be removed in a future release.

mkFalse() - Method in class io.github.cvc5.TermManager

Create a Boolean false constant.

mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.

mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.TermManager

Create a finite field constant in a given field and for a given value.

mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.

mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.TermManager

Create a finite field sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.

mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.TermManager

Create a floating-point value from a bit-vector given in IEEE-754 format.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, Term). It will be removed in a future release.

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

Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.

mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.TermManager

Create a not-a-number floating-point constant (SMT-LIB: NaN).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.

mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.TermManager

Create a negative infinity floating-point constant (SMT-LIB: -oo).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.

mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.TermManager

Create a negative zero floating-point constant (SMT-LIB: -zero).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.

mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.TermManager

Create a positive infinity floating-point constant (SMT-LIB: +oo).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.

mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.TermManager

Create a positive zero floating-point constant (SMT-LIB: +zero).

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.

mkFloatingPointSort(int, int) - Method in class io.github.cvc5.TermManager

Create a floating-point sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFunctionSort(Sort[], Sort). It will be removed in a future release.

mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.TermManager

Create function sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkFunctionSort(Sort, Sort). It will be removed in a future release.

mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.TermManager

Create function sort.

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

Create a Sygus grammar.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkInteger(long). It will be removed in a future release.

mkInteger(long) - Method in class io.github.cvc5.TermManager

Create an integer constant from a C++ int.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.

mkInteger(String) - Method in class io.github.cvc5.TermManager

Create an integer constant from a string.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.

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

Create a null tester for a nullable term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.

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

Create a some tester for a nullable term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.

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

Create a term that lifts kind to nullable terms.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.

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

Create a constant representing a null value of the given sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.

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

Create a nullable some term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.

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

Create a nullable sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.

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

Create a selector for nullable term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkOp(Kind, int). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkOp(Kind, int[]). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkOp(Kind, int, int). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkParamSort(). It will be removed in a future release.

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

Create a sort parameter.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.

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

Create a sort parameter.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkPi(). It will be removed in a future release.

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

Create a constant representing the number Pi.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.

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

Create a predicate sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkReal(long). It will be removed in a future release.

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

Create a real constant from an integer.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkReal(long, long). It will be removed in a future release.

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

Create a real constant from a rational.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.

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

Create a real constant from a string.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.

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

Create a record sort

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

Deprecated.

This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.

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

Create a rounding mode constant.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.

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

Create a separation logic empty term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.

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

Create a separation logic nil term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.

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

Create a sequence sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.

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

Create a set sort.

mkSkolem(SkolemId, Term[]) - Method in class io.github.cvc5.TermManager

Create a skolem

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

Deprecated.

This function is deprecated and replaced by TermManager.mkString(int[]). It will be removed in a future release.

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

Create a String constant.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.

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

Create a String constant.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkString(String, boolean). It will be removed in a future release.

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

Create a String constant.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.

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

Create 0-ary term of given kind.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.

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

Create a unary term of given kind.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.

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

Create n-ary term of given kind.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.

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

Create binary term of given kind.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.

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

Create ternary term of given kind.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Op). It will be removed in a future release.

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

Create nullary term of given kind from a given operator.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.

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

Create unary term of given kind from a given operator.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.

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

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

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.

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

Create binary term of given kind from a given operator.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). It will be removed in a future release.

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

Create ternary term of given kind from a given operator.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTrue(). It will be removed in a future release.

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

Create a Boolean true constant.

mkTuple(Term[]) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.

mkTuple(Term[]) - Method in class io.github.cvc5.TermManager

Create a tuple term.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.

mkTupleSort(Sort[]) - Method in class io.github.cvc5.TermManager

Create a tuple sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkUninterpretedSort(). It will be removed in a future release.

mkUninterpretedSort() - Method in class io.github.cvc5.TermManager

Create an uninterpreted sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.

mkUninterpretedSort(String) - Method in class io.github.cvc5.TermManager

Create an uninterpreted sort.

mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). It will be removed in a future release.

mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.TermManager

Create a sort constructor sort.

mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.

mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.TermManager

Create a sort constructor sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.

mkUniverseSet(Sort) - Method in class io.github.cvc5.TermManager

Create a universe set of the given sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). It will be removed in a future release.

mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.TermManager

Create an unresolved datatype sort.

mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.

mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.TermManager

Create an unresolved datatype sort.

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

Deprecated.

This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.

mkVar(Sort) - Method in class io.github.cvc5.TermManager

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).

mkVar(Sort, String) - Method in class io.github.cvc5.Solver

Deprecated.

This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.

mkVar(Sort, String) - Method in class io.github.cvc5.TermManager

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).

MOD_BY_ZERO - io.github.cvc5.SkolemId

The function for integer modulus by zero.

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.

NONE - io.github.cvc5.ProofRewriteRule

This enumeration represents the rewrite rules used in a rewrite proof.

NONE - io.github.cvc5.SkolemId

Indicates this is not a skolem.

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} \]

notifySatClause(Term) - Method in class io.github.cvc5.AbstractPlugin

Notify SAT clause, called when cl is a clause learned by the SAT solver.

notifyTheoryLemma(Term) - Method in class io.github.cvc5.AbstractPlugin

Notify theory lemma, called when lem is a theory lemma sent by a theory solver.

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.

Proof() - Constructor for class io.github.cvc5.Proof

Null proof

ProofComponent - Enum in io.github.cvc5.modes

ProofFormat - Enum in io.github.cvc5.modes

ProofRewriteRule - Enum in io.github.cvc5

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.

proofToString(Proof, ProofFormat, Map) - Method in class io.github.cvc5.Solver

Prints a proof into a string with a slected proof format mode.

PURIFY - io.github.cvc5.SkolemId

The purification skolem for a term.

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

QUANT_DT_SPLIT - io.github.cvc5.ProofRewriteRule

Quantifiers – Datatypes Split \[ (\forall x Y.\> F) = (\forall X_1 Y.

QUANT_MERGE_PRENEX - io.github.cvc5.ProofRewriteRule

Quantifiers – Merge prenex \[ \forall X_1.\> \ldots \forall X_n.\> F = \forall X_1 \ldots X_n.\> F \] where \(X_1 \ldots X_n\) are lists of variables.

QUANT_MINISCOPE_AND - io.github.cvc5.ProofRewriteRule

Quantifiers – Miniscoping and \[ \forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n) \]

QUANT_MINISCOPE_ITE - io.github.cvc5.ProofRewriteRule

Quantifiers – Miniscoping ite \[ \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{\forall X.\> F_1}{\forall X.\> F_2} \] where \(C\) does not have any free variable in \(X\).

QUANT_MINISCOPE_OR - io.github.cvc5.ProofRewriteRule

Quantifiers – Miniscoping or \[ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_1) \vee \ldots \vee (\forall X_n.\> F_n) \] where \(X = X_1 \ldots X_n\), and the right hand side does not have any free variable in \(X\).

QUANT_UNUSED_VARS - io.github.cvc5.ProofRewriteRule

Quantifiers – Unused variables \[ \forall X.\> F = \forall X_1.\> F \] where \(X_1\) is the subset of \(X\) that appear free in \(F\) and \(X_1\) does not contain duplicate variables.

QUANT_VAR_ELIM_EQ - io.github.cvc5.ProofRewriteRule

Quantifiers – Macro variable elimination equality ..

QUANT_VAR_REORDERING - io.github.cvc5.ProofRule

Quantifiers – Variable reordering \[ \inferrule{-\mid (\forall X.\> F) = (\forall Y.\> F)} {(\forall X.\> F) = (\forall Y.\> F)} \] where \(Y\) is a reordering of \(X\).

QUANTIFIERS_SKOLEMIZE - io.github.cvc5.SkolemId

The n^th skolem for the negation of universally quantified formula 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_ALL_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-all-elim

RE_CONCAT_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-emp

RE_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-flatten

RE_CONCAT_MERGE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-merge

RE_CONCAT_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-none

RE_CONCAT_STAR_REPEAT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-star-repeat

RE_CONCAT_STAR_SWAP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-star-swap

RE_DIFF_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-diff-elim

RE_FIRST_MATCH - io.github.cvc5.SkolemId

For string a and regular expression R, this skolem is the string that the first, shortest match of R was matched to in a.

RE_FIRST_MATCH_POST - io.github.cvc5.SkolemId

For string a and regular expression R, this skolem is the remainder of a after the first, shortest match of R in a.

RE_FIRST_MATCH_PRE - io.github.cvc5.SkolemId

The next three skolems are used to decompose the match of a regular expression in string.

RE_IN_COMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-comp

RE_IN_CSTRING - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-cstring

RE_IN_EMPTY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-empty

RE_IN_SIGMA - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-sigma

RE_IN_SIGMA_STAR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-sigma-star

RE_INTER - io.github.cvc5.ProofRule

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

RE_INTER_ALL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-all

RE_INTER_CSTRING - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-cstring

RE_INTER_CSTRING_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-cstring-neg

RE_INTER_DUP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-dup

RE_INTER_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-flatten

RE_INTER_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-none

RE_INTER_UNION_INCLUSION - io.github.cvc5.ProofRewriteRule

Strings – regular expression intersection/union inclusion \[ (re.inter\ R) = \mathit{re.inter}(\mathit{re.none}, R_0) \] where \(R\) is a list of regular expressions containing `r_1`, `re.comp(r_2)` and the list \(R_0\) where `r_2` is a superset of `r_1`.

RE_LOOP_ELIM - io.github.cvc5.ProofRewriteRule

Strings – regular expression loop elimination \[ re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u) \] where \(u \geq l\).

RE_LOOP_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-loop-neg

RE_OPT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-opt-elim

RE_STAR_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-star-none

RE_UNFOLD_NEG - io.github.cvc5.ProofRule

Strings – Regular expressions – Negative Unfold \[ \inferrule{t \not \in \mathit{re}.\text{*}(R) \mid -}{t \neq \ \epsilon \ \wedge \forall L.

RE_UNFOLD_NEG_CONCAT_FIXED - io.github.cvc5.ProofRule

Strings – Regular expressions – Unfold negative concatenation, fixed ..

RE_UNFOLD_POS - io.github.cvc5.ProofRule

Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{F} \] where \(F\) corresponds to the one-step unfolding of the premise.

RE_UNFOLD_POS_COMPONENT - io.github.cvc5.SkolemId

Regular expression unfold component: if (str.in_re a R), where R is (re.++ R0 ... Rn), then the RE_UNFOLD_POS_COMPONENT for indices (a,R,i) is a string ki such that (= a (str.++ k0 ... kn)) and (str.in_re k0 R0) for i = 0, ..., n.

RE_UNION_ALL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union-all

RE_UNION_DUP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union-dup

RE_UNION_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union-flatten

RE_UNION_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union-none

readLibraryFilenames(String) - Static method in class io.github.cvc5.Utils

Reads a text file from the specified path within the JAR file and returns a list of library filenames.

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

Table join operator for relations has the form \(((\_ \; rel.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 relations.

RELATION_TCLOSURE - io.github.cvc5.Kind

Relation transitive closure.

RELATION_TRANSPOSE - io.github.cvc5.Kind

Relation transpose.

RELATIONS_GROUP_PART - io.github.cvc5.SkolemId

Given a group term ((_ rel.group n1 ... nk) A) of type (Set (Relation T)) this skolem maps elements of A to their parts in the resulting partition.

RELATIONS_GROUP_PART_ELEMENT - io.github.cvc5.SkolemId

Given a group term ((_ rel.group n1 ...

REORDERING - io.github.cvc5.ProofRule

Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the multiset representations of \(C_1\) and \(C_2\) are the same.

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_EXTERNAL_PROVE - io.github.cvc5.ProofRule

SAT external prove Refutation \[ \inferrule{F_1 \dots F_n \mid D}{\bot} \] where \(F_1 \dots F_n\) correspond to the input clauses in the DIMACS file `D`.

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 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_LEN_EMPTY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-len-empty

SEQ_LEN_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-len-rev

SEQ_LEN_UNIT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-len-unit

SEQ_LENGTH - io.github.cvc5.Kind

Sequence length.

SEQ_NTH - io.github.cvc5.Kind

Sequence nth.

SEQ_NTH_UNIT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-nth-unit

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_REV_CONCAT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-rev-concat

SEQ_REV_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-rev-rev

SEQ_REV_UNIT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule seq-rev-unit

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

Set all.

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

Set is empty tester.

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

Set some.

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.

SETS_CARD_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-card-emp

SETS_CARD_MINUS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-card-minus

SETS_CARD_SINGLETON - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-card-singleton

SETS_CARD_UNION - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-card-union

SETS_CHOOSE - io.github.cvc5.SkolemId

An interpreted function for set.choose operator, where (set.choose A) is expanded to (uf A) along with the inference (set.member (uf A) A)) when A is non-empty, where uf: (-> (Set E) E) is this skolem function, and E is the type of elements of A.

SETS_CHOOSE_SINGLETON - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-choose-singleton

SETS_DEQ_DIFF - io.github.cvc5.SkolemId

The set diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (set.member k A) (set.member k B)))).

SETS_EQ_SINGLETON_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-eq-singleton-emp

SETS_EXT - io.github.cvc5.ProofRule

Sets – Sets extensionality \[ \inferrule{a \neq b\mid -} {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)} \] where \(k\) is the \(\texttt{SETS_DEQ_DIFF}\) skolem for `(a, b)`.

SETS_FILTER_DOWN - io.github.cvc5.ProofRule

Sets – Sets filter down \[ \inferrule{\mathit{set.member}(x,\mathit{set.filter}(P, a))\mid -} {\mathit{set.member}(x,a) \wedge P(x)} \]

SETS_FILTER_UP - io.github.cvc5.ProofRule

Sets – Sets filter up \[ \inferrule{\mathit{set.member}(x,a)\mid P} {\mathit{set.member}(x, \mathit{set.filter}(P, a)) = P(x)} \]

SETS_FOLD_CARD - io.github.cvc5.SkolemId

An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need to guess the cardinality n of set A using a skolem function with SETS_FOLD_CARD id.

SETS_FOLD_COMBINE - io.github.cvc5.SkolemId

An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function that accumulates intermidiate values.

SETS_FOLD_ELEMENTS - io.github.cvc5.SkolemId

An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function for elements of A.

SETS_FOLD_UNION - io.github.cvc5.SkolemId

An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function for elements of A which is given by elements defined in SETS_FOLD_ELEMENTS.

SETS_INSERT_ELIM - io.github.cvc5.ProofRewriteRule

Sets – sets insert elimination \[ \mathit{sets.insert}(t_1, \ldots, t_n, S) = \texttt{set.union}(\texttt{sets.singleton}(t_1), \ldots, \texttt{sets.singleton}(t_n), S) \]

SETS_INTER_COMM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-inter-comm

SETS_INTER_EMP1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-inter-emp1

SETS_INTER_EMP2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-inter-emp2

SETS_INTER_MEMBER - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-inter-member

SETS_IS_EMPTY_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-is-empty-elim

SETS_IS_EMPTY_EVAL - io.github.cvc5.ProofRewriteRule

Sets – empty tester evaluation \[ \mathit{sets.is\_empty}(\epsilon) = \top \] where \(\epsilon\) is the empty set, or alternatively: \[ \mathit{sets.is\_empty}(c) = \bot \] where \(c\) is a constant set that is not the empty set.

SETS_MAP_DOWN_ELEMENT - io.github.cvc5.SkolemId

A skolem variable that is unique per terms (set.map f A), y which is an element in (set.map f A).

SETS_MEMBER_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-member-emp

SETS_MEMBER_SINGLETON - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-member-singleton

SETS_MINUS_EMP1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-minus-emp1

SETS_MINUS_EMP2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-minus-emp2

SETS_MINUS_MEMBER - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-minus-member

SETS_MINUS_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-minus-self

SETS_SINGLETON_INJ - io.github.cvc5.ProofRule

Sets – Singleton injectivity \[ \inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid -}{t=s} \]

SETS_SUBSET_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-subset-elim

SETS_UNION_COMM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-union-comm

SETS_UNION_EMP1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-union-emp1

SETS_UNION_EMP2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-union-emp2

SETS_UNION_MEMBER - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule sets-union-member

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.

SHARED_SELECTOR - io.github.cvc5.SkolemId

A shared datatype selector, see Reynolds et.

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

Simplify a term or formula based on rewriting.

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

Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.

SINE - io.github.cvc5.Kind

Sine function.

SKOLEM - io.github.cvc5.Kind

A Skolem.

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

SkolemId - Enum in io.github.cvc5

SKOLEMIZE - io.github.cvc5.ProofRule

Quantifiers – Skolemization \[ \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, which are skolems \(k_1,\dots,k_n\).

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

Deprecated.

This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.

Solver(TermManager) - Constructor for class io.github.cvc5.Solver

Create solver instance.

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.

STR_AT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-at-elim

STR_CONCAT_CLASH - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash

STR_CONCAT_CLASH_CHAR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash-char

STR_CONCAT_CLASH_CHAR_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash-char-rev

STR_CONCAT_CLASH_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash-rev

STR_CONCAT_CLASH2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash2

STR_CONCAT_CLASH2_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-clash2-rev

STR_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-flatten

STR_CONCAT_FLATTEN_EQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-flatten-eq

STR_CONCAT_FLATTEN_EQ_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-flatten-eq-rev

STR_CONCAT_UNIFY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-unify

STR_CONCAT_UNIFY_BASE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-unify-base

STR_CONCAT_UNIFY_BASE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-unify-base-rev

STR_CONCAT_UNIFY_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-concat-unify-rev

STR_CONTAINS_CONCAT_FIND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-concat-find

STR_CONTAINS_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-emp

STR_CONTAINS_IS_EMP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-is-emp

STR_CONTAINS_LEQ_LEN_EQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-leq-len-eq

STR_CONTAINS_LT_LEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-lt-len

STR_CONTAINS_REFL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-refl

STR_CONTAINS_SPLIT_CHAR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-contains-split-char

STR_EQ_CTN_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-eq-ctn-false

STR_EQ_CTN_FULL_FALSE1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-eq-ctn-full-false1

STR_EQ_CTN_FULL_FALSE2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-eq-ctn-full-false2

STR_IN_RE_CONCAT_STAR_CHAR - io.github.cvc5.ProofRewriteRule

Strings – string in regular expression concatenation star character \[ \mathit{str.in\_re}(\mathit{str}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R)) \] where all strings in \(R\) have length one.

STR_IN_RE_CONSUME - io.github.cvc5.ProofRewriteRule

Strings – regular expression membership consume \[ \mathit{str.in_re}(s, R) = b \] where \(b\) is either \(false\) or the result of stripping entailed prefixes and suffixes off of \(s\) and \(R\).

STR_IN_RE_CONTAINS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-contains

STR_IN_RE_EVAL - io.github.cvc5.ProofRewriteRule

Strings – regular expression membership evaluation \[ \mathit{str.in\_re}(s, R) = c \] where \(s\) is a constant string, \(R\) is a constant regular expression and \(c\) is true or false.

STR_IN_RE_INTER_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-inter-elim

STR_IN_RE_RANGE_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-range-elim

STR_IN_RE_REQ_UNFOLD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-req-unfold

STR_IN_RE_REQ_UNFOLD_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-req-unfold-rev

STR_IN_RE_SIGMA - io.github.cvc5.ProofRewriteRule

Strings – string in regular expression sigma \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n) \] or alternatively: \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}, \mathit{re}.\text{*}(\mathit{re.allchar}))) = (\mathit{str.len}(s) \ge n) \]

STR_IN_RE_SIGMA_STAR - io.github.cvc5.ProofRewriteRule

Strings – string in regular expression sigma star \[ \mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0) \] where \(n\) is the number of \(\mathit{re.allchar}\) arguments to \(\mathit{re}.\text{++}\).

STR_IN_RE_SKIP_UNFOLD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-skip-unfold

STR_IN_RE_SKIP_UNFOLD_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-skip-unfold-rev

STR_IN_RE_STRIP_CHAR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-char

STR_IN_RE_STRIP_CHAR_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-char-rev

STR_IN_RE_STRIP_CHAR_S_SINGLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-char-s-single

STR_IN_RE_STRIP_CHAR_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-char-s-single-rev

STR_IN_RE_STRIP_PREFIX - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix

STR_IN_RE_STRIP_PREFIX_BASE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base

STR_IN_RE_STRIP_PREFIX_BASE_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-neg

STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-neg-rev

STR_IN_RE_STRIP_PREFIX_BASE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-rev

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-rev

STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-rev

STR_IN_RE_STRIP_PREFIX_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-neg

STR_IN_RE_STRIP_PREFIX_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev

STR_IN_RE_STRIP_PREFIX_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-rev

STR_IN_RE_STRIP_PREFIX_S_SINGLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-s-single

STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg

STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-rev

STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-s-single-rev

STR_IN_RE_STRIP_PREFIX_SR_SINGLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-rev

STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-rev

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-rev

STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev

STR_IN_RE_TEST_UNFOLD - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-test-unfold

STR_IN_RE_TEST_UNFOLD_REV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-test-unfold-rev

STR_IN_RE_UNION_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-in-re-union-elim

STR_INDEXOF_CONTAINS_PRE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-indexof-contains-pre

STR_INDEXOF_NO_CONTAINS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-indexof-no-contains

STR_INDEXOF_RE_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-indexof-re-none

STR_INDEXOF_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-indexof-self

STR_LEN_CONCAT_REC - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-concat-rec

STR_LEN_REPLACE_INV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-replace-inv

STR_LEN_SUBSTR_IN_RANGE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-substr-in-range

STR_LEN_SUBSTR_UB1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-substr-ub1

STR_LEN_SUBSTR_UB2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-substr-ub2

STR_LEN_UPDATE_INV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-len-update-inv

STR_LEQ_CONCAT_FALSE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-leq-concat-false

STR_LEQ_CONCAT_TRUE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-leq-concat-true

STR_LEQ_EMPTY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-leq-empty

STR_LEQ_EMPTY_EQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-leq-empty-eq

STR_LT_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-lt-elim

STR_PREFIXOF_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-prefixof-elim

STR_PREFIXOF_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-prefixof-one

STR_REPLACE_ALL_NO_CONTAINS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-all-no-contains

STR_REPLACE_CONTAINS_PRE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-contains-pre

STR_REPLACE_EMPTY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-empty

STR_REPLACE_NO_CONTAINS - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-no-contains

STR_REPLACE_PREFIX - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-prefix

STR_REPLACE_RE_ALL_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-re-all-none

STR_REPLACE_RE_NONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-re-none

STR_REPLACE_SELF - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-replace-self

STR_SUBSTR_COMBINE1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-combine1

STR_SUBSTR_COMBINE2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-combine2

STR_SUBSTR_COMBINE3 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-combine3

STR_SUBSTR_COMBINE4 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-combine4

STR_SUBSTR_CONCAT1 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-concat1

STR_SUBSTR_CONCAT2 - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-concat2

STR_SUBSTR_EMPTY_RANGE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-empty-range

STR_SUBSTR_EMPTY_START - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-empty-start

STR_SUBSTR_EMPTY_START_NEG - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-empty-start-neg

STR_SUBSTR_EMPTY_STR - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-empty-str

STR_SUBSTR_EQ_EMPTY - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-eq-empty

STR_SUBSTR_FULL - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-full

STR_SUBSTR_FULL_EQ - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-full-eq

STR_SUBSTR_LEN_INCLUDE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-len-include

STR_SUBSTR_LEN_INCLUDE_PRE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-len-include-pre

STR_SUBSTR_LEN_SKIP - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-substr-len-skip

STR_SUFFIXOF_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-suffixof-elim

STR_SUFFIXOF_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-suffixof-one

STR_TO_INT_CONCAT_NEG_ONE - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-int-concat-neg-one

STR_TO_LOWER_CONCAT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-lower-concat

STR_TO_LOWER_FROM_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-lower-from-int

STR_TO_LOWER_LEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-lower-len

STR_TO_LOWER_UPPER - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-lower-upper

STR_TO_UPPER_CONCAT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-upper-concat

STR_TO_UPPER_FROM_INT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-upper-from-int

STR_TO_UPPER_LEN - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-upper-len

STR_TO_UPPER_LOWER - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule str-to-upper-lower

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 = 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} \] where \(w_1\) is the purification skolem for \(\mathit{pre}(t,n)\) and \(w_2\) is the purification skolem for \(\mathit{suf}(t,n)\).

STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule

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

STRING_EXT - io.github.cvc5.ProofRule

Strings – Extensionality \[ \inferrule{s \neq t\mid -} {\mathit{seq.len}(s) \neq \mathit{seq.len}(t) \vee (\mathit{seq.nth}(s,k)\neq\mathit{set.nth}(t,k) \wedge 0 \leq k \wedge k < \mathit{seq.len}(s))} \] where \(s,t\) are terms of sequence type, \(k\) is the \(\texttt{STRINGS_DEQ_DIFF}\) skolem for \(s,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 \epsilon\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= \epsilon)\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{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.

STRINGS_DEQ_DIFF - io.github.cvc5.SkolemId

Difference index for string disequalities, such that k is the witness for the inference (=> (not (= a b)) (not (= (substr a k 1) (substr b k 1)))) where note that `k` may be out of bounds for at most of a,b.

STRINGS_ITOS_RESULT - io.github.cvc5.SkolemId

A function used to define intermediate results of str.from_int applications.

STRINGS_NUM_OCCUR - io.github.cvc5.SkolemId

An integer corresponding to the number of times a string occurs in another string.

STRINGS_NUM_OCCUR_RE - io.github.cvc5.SkolemId

Analogous to STRINGS_NUM_OCCUR, but for regular expressions.

STRINGS_OCCUR_INDEX - io.github.cvc5.SkolemId

A function k such that for x = 0...n, (k x) is the end index of the x^th occurrence of a string b in string a, where n is the number of occurrences of b in a, and (= (k 0) 0).

STRINGS_OCCUR_INDEX_RE - io.github.cvc5.SkolemId

Analogous to STRINGS_OCCUR_INDEX, but for regular expressions.

STRINGS_OCCUR_LEN_RE - io.github.cvc5.SkolemId

A function k where for x = 0...n, (k x) is the length of the x^th occurrence of R in a (excluding matches of empty strings) where R is a regular expression, n is the number of occurrences of R in a, and (= (k 0) 0).

STRINGS_REPLACE_ALL_RESULT - io.github.cvc5.SkolemId

A function used to define intermediate results of str.replace_all and str.replace_re_all applications.

STRINGS_STOI_NON_DIGIT - io.github.cvc5.SkolemId

A position containing a non-digit in a string, used when (str.to_int a) is equal to -1.

STRINGS_STOI_RESULT - io.github.cvc5.SkolemId

A function used to define intermediate results of str.from_int applications.

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

Deprecated.

This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.

SymbolManager(TermManager) - Constructor for class io.github.cvc5.SymbolManager

Create symbol manager instance.

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.

TABLES_GROUP_PART - io.github.cvc5.SkolemId

Given a group term ((_ table.group n1 ... nk) A) of type (Bag (Table T)), this skolem maps elements of A to their parts in the resulting partition.

TABLES_GROUP_PART_ELEMENT - io.github.cvc5.SkolemId

Given a group term ((_ table.group n1 ... nk) A) of type (Bag (Table T)) and a part B of type (Table T), this function returns a skolem element that is a member of B if B is not empty.

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

termManager - Variable in class io.github.cvc5.AbstractPlugin

TermManager - Class in io.github.cvc5

A cvc5 term manager.

TermManager() - Constructor for class io.github.cvc5.TermManager

Create a term manager instance.

THEORY_LEMMAS - io.github.cvc5.modes.ProofComponent

Proofs of L1 ...

THEORY_REWRITE - io.github.cvc5.ProofRule

Other theory rewrite rules \[ \inferrule{- \mid id, t = t'}{t = t'} \] where `id` is the ProofRewriteRule of the theory rewrite rule which transforms \(t\) to \(t'\).

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

toString(long) - Method in class io.github.cvc5.TermManager

TRANS - io.github.cvc5.ProofRule

Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]

TRANSCENDENTAL_PURIFY - io.github.cvc5.SkolemId

A function introduced to eliminate extended trancendental functions.

TRANSCENDENTAL_PURIFY_ARG - io.github.cvc5.SkolemId

Argument used to purify trancendental function app (f x).

TRANSCENDENTAL_SINE_PHASE_SHIFT - io.github.cvc5.SkolemId

Argument used to reason about the phase shift of arguments to sine.

transferTo(InputStream, FileOutputStream) - Static method in class io.github.cvc5.Utils

Transfers all bytes from the provided InputStream to the specified FileOutputStream.

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

UF_BV2NAT_GEQ_ELIM - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-bv2nat-geq-elim

UF_BV2NAT_INT2BV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-bv2nat-int2bv

UF_BV2NAT_INT2BV_EXTEND - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-bv2nat-int2bv-extend

UF_BV2NAT_INT2BV_EXTRACT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-bv2nat-int2bv-extract

UF_INT2BV_BV2NAT - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-int2bv-bv2nat

UF_INT2BV_BVULE_EQUIV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-int2bv-bvule-equiv

UF_INT2BV_BVULT_EQUIV - io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule uf-int2bv-bvult-equiv

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

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum io.github.cvc5.ProofRule

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum io.github.cvc5.RoundingMode

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum io.github.cvc5.SkolemId

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum io.github.cvc5.SortKind

Returns the enum constant of this type with the specified name.

valueOf(String) - Static method in enum io.github.cvc5.UnknownExplanation

Returns the enum constant of this type with the specified name.

values() - Static method in enum io.github.cvc5.Kind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.BlockModelsMode

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.FindSynthTarget

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.InputLanguage

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.LearnedLitType

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.ProofComponent

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.modes.ProofFormat

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.ProofRewriteRule

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.ProofRule

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.RoundingMode

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.SkolemId

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.SortKind

Returns an array containing the constants of this enum type, in the order they are declared.

values() - Static method in enum io.github.cvc5.UnknownExplanation

Returns an array containing the constants of this enum type, in the order they are declared.

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