Index

A

ABS - Enum constant in enum class io.github.cvc5.Kind

Absolute value.

ABSORB - Enum constant in enum class io.github.cvc5.ProofRule

Builtin theory – absorb \[ \inferrule{- \mid t = z}{t = z} \] where \(t\) contains \(z\) as a subterm, where \(z\) is a zero element.

ABSTRACT_SORT - Enum constant in enum class io.github.cvc5.SortKind

An abstract sort.

AbstractPlugin - Class in io.github.cvc5

A cvc5 plugin abstract class.

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

Create plugin instance.

ACI_NORM - Enum constant in enum class io.github.cvc5.ProofRule

Builtin theory – associative/commutative/idempotency/identity \ normalization \[ \inferrule{- \mid t = s}{t = s} \] where \(t\) and \(s\) are equivalent modulo associativity and identity elements, and (optionally) commutativity and idempotency.

ADD - Enum constant in enum class 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(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 - Enum constant in enum class io.github.cvc5.modes.ProofFormat

Output Alethe proof.

ALETHE_RULE - Enum constant in enum class io.github.cvc5.ProofRule

External – Alethe Place holder for Alethe rules.

ALPHA_EQUIV - Enum constant in enum class 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(F)\) are the free variables of \(F\).

AND - Enum constant in enum class io.github.cvc5.Kind

Logical conjunction.

AND_ELIM - Enum constant in enum class io.github.cvc5.ProofRule

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

AND_INTRO - Enum constant in enum class 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

Applies the oracle to the given array of Term arguments.

APPLY_CONSTRUCTOR - Enum constant in enum class io.github.cvc5.Kind

Datatype constructor application.

APPLY_SELECTOR - Enum constant in enum class io.github.cvc5.Kind

Datatype selector application.

APPLY_TESTER - Enum constant in enum class io.github.cvc5.Kind

Datatype tester application.

APPLY_UF - Enum constant in enum class io.github.cvc5.Kind

Application of an uninterpreted function.

APPLY_UPDATER - Enum constant in enum class io.github.cvc5.Kind

Datatype update application.

ARCCOSECANT - Enum constant in enum class io.github.cvc5.Kind

Arc cosecant function.

ARCCOSINE - Enum constant in enum class io.github.cvc5.Kind

Arc cosine function.

ARCCOTANGENT - Enum constant in enum class io.github.cvc5.Kind

Arc cotangent function.

ARCSECANT - Enum constant in enum class io.github.cvc5.Kind

Arc secant function.

ARCSINE - Enum constant in enum class io.github.cvc5.Kind

Arc sine function.

ARCTANGENT - Enum constant in enum class io.github.cvc5.Kind

Arc tangent function.

ARITH_ABS_EQ - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-abs-eq

ARITH_ABS_INT_GT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_ABS_REAL_GT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_COSECENT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cosecent-elim

ARITH_COSINE_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cosine-elim

ARITH_COTANGENT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-cotangent-elim

ARITH_DIV_ELIM_TO_REAL1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_DIV_ELIM_TO_REAL2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_DIV_TOTAL_ZERO_INT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_DIV_TOTAL_ZERO_REAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_DIVISIBLE_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-divisible-elim

ARITH_ELIM_GT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-gt

ARITH_ELIM_INT_GT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_ELIM_INT_LT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_ELIM_LEQ - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-leq

ARITH_ELIM_LT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-elim-lt

ARITH_EQ_ELIM_INT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_EQ_ELIM_REAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_GEQ_ITE_LIFT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-ite-lift

ARITH_GEQ_NORM1_INT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_GEQ_NORM1_REAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_GEQ_TIGHTEN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-geq-tighten

ARITH_INT_DIV_TOTAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_DIV_TOTAL_NEG - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_DIV_TOTAL_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_DIV_TOTAL_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_EQ_CONFLICT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_GEQ_TIGHTEN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_MOD_TOTAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_MOD_TOTAL_NEG - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_MOD_TOTAL_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_INT_MOD_TOTAL_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_LEQ_ITE_LIFT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-leq-ite-lift

ARITH_LEQ_NORM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-leq-norm

ARITH_MAX_GEQ1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-max-geq1

ARITH_MAX_GEQ2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-max-geq2

ARITH_MIN_LT1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-min-lt1

ARITH_MIN_LT2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-min-lt2

ARITH_MOD_OVER_MOD - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-mod-over-mod

ARITH_MULT_ABS_COMPARISON - Enum constant in enum class 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_NEG - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 greater) that results from the signs of the variables.

ARITH_MULT_TANGENT - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_POLY_NORM - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

Arithmetic – Polynomial normalization for relations ..

ARITH_POW_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_REDUCTION - Enum constant in enum class io.github.cvc5.ProofRule

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

ARITH_SECENT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-secent-elim

ARITH_SINE_PI2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-sine-pi2

ARITH_SINE_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-sine-zero

ARITH_STRING_PRED_ENTAIL - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule arith-tangent-elim

ARITH_TO_INT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_TO_INT_ELIM_TO_REAL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARITH_TRANS_EXP_APPROX_ABOVE_NEG - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 a non-negative number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, n+1, c)\) is the \((n+1)\)'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\) where \(n\) is \(2 \cdot d\).

ARITH_TRANS_EXP_NEG - Enum constant in enum class io.github.cvc5.ProofRule

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

ARITH_TRANS_EXP_POSITIVITY - Enum constant in enum class io.github.cvc5.ProofRule

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

ARITH_TRANS_EXP_SUPER_LIN - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

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

ARITH_TRANS_PI - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..

ARITH_TRANS_SINE_TANGENT_ZERO - Enum constant in enum class io.github.cvc5.ProofRule

Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..

ARITH_TRICHOTOMY - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_DELTA_FREE - Enum constant in enum class io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_INFINITY - Enum constant in enum class io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARITH_VTS_INFINITY_FREE - Enum constant in enum class io.github.cvc5.SkolemId

Used to reason about virtual term substitution.

ARRAY_DEQ_DIFF - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARRAY_READ_OVER_WRITE_SPLIT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARRAY_READ_OVER_WRITE2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ARRAY_SORT - Enum constant in enum class io.github.cvc5.SortKind

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

ARRAY_STORE_OVERWRITE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-store-overwrite

ARRAY_STORE_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-store-self

ARRAY_STORE_SWAP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule array-store-swap

ARRAYS_EQ_RANGE_EXPAND - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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_ALL - Enum constant in enum class io.github.cvc5.Kind

Bag all.

BAG_CARD - Enum constant in enum class io.github.cvc5.Kind

Bag cardinality.

BAG_CHOOSE - Enum constant in enum class io.github.cvc5.Kind

Bag choose.

BAG_COUNT - Enum constant in enum class io.github.cvc5.Kind

Bag element multiplicity.

BAG_DIFFERENCE_REMOVE - Enum constant in enum class io.github.cvc5.Kind

Bag difference remove.

BAG_DIFFERENCE_SUBTRACT - Enum constant in enum class io.github.cvc5.Kind

Bag difference subtract.

BAG_EMPTY - Enum constant in enum class io.github.cvc5.Kind

Empty bag.

BAG_FILTER - Enum constant in enum class io.github.cvc5.Kind

Bag filter.

BAG_FOLD - Enum constant in enum class io.github.cvc5.Kind

Bag fold.

BAG_INTER_MIN - Enum constant in enum class io.github.cvc5.Kind

Bag intersection (min).

BAG_MAKE - Enum constant in enum class io.github.cvc5.Kind

Bag make.

BAG_MAP - Enum constant in enum class io.github.cvc5.Kind

Bag map.

BAG_MEMBER - Enum constant in enum class io.github.cvc5.Kind

Bag membership predicate.

BAG_PARTITION - Enum constant in enum class io.github.cvc5.Kind

Bag partition.

BAG_SETOF - Enum constant in enum class io.github.cvc5.Kind

Bag setof.

BAG_SOME - Enum constant in enum class io.github.cvc5.Kind

Bag some.

BAG_SORT - Enum constant in enum class io.github.cvc5.SortKind

A bag sort, whose argument sort is the element sort of the bag.

BAG_SUBBAG - Enum constant in enum class io.github.cvc5.Kind

Bag inclusion predicate.

BAG_UNION_DISJOINT - Enum constant in enum class io.github.cvc5.Kind

Bag disjoint union (sum).

BAG_UNION_MAX - Enum constant in enum class io.github.cvc5.Kind

Bag max union.

BAGS_CARD_COMBINE - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

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

BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT - Enum constant in enum class io.github.cvc5.SkolemId

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

BAGS_FOLD_CARD - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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

Construct a new BaseInfo.

BETA_REDUCE - Enum constant in enum class 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\} \] or alternatively \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1) = (\lambda x_2 \ldots x_n.\> t)\{x_1 \mapsto t_1\} \] In the former case, the left hand side may either be a term of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.

BITVECTOR_ADD - Enum constant in enum class io.github.cvc5.Kind

Addition of two or more bit-vectors.

BITVECTOR_AND - Enum constant in enum class io.github.cvc5.Kind

Bit-wise and.

BITVECTOR_ASHR - Enum constant in enum class io.github.cvc5.Kind

Bit-vector arithmetic shift right.

BITVECTOR_BIT - Enum constant in enum class io.github.cvc5.Kind

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

BITVECTOR_COMP - Enum constant in enum class io.github.cvc5.Kind

Equality comparison (returns bit-vector of size 1).

BITVECTOR_CONCAT - Enum constant in enum class io.github.cvc5.Kind

Concatenation of two or more bit-vectors.

BITVECTOR_EXTRACT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector extract.

BITVECTOR_FROM_BOOLS - Enum constant in enum class io.github.cvc5.Kind

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

BITVECTOR_ITE - Enum constant in enum class io.github.cvc5.Kind

Bit-vector if-then-else.

BITVECTOR_LSHR - Enum constant in enum class io.github.cvc5.Kind

Bit-vector logical shift right.

BITVECTOR_MULT - Enum constant in enum class io.github.cvc5.Kind

Multiplication of two or more bit-vectors.

BITVECTOR_NAND - Enum constant in enum class io.github.cvc5.Kind

Bit-wise nand.

BITVECTOR_NEG - Enum constant in enum class io.github.cvc5.Kind

Negation of a bit-vector (two's complement).

BITVECTOR_NEGO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector negation overflow detection.

BITVECTOR_NOR - Enum constant in enum class io.github.cvc5.Kind

Bit-wise nor.

BITVECTOR_NOT - Enum constant in enum class io.github.cvc5.Kind

Bit-wise negation.

BITVECTOR_OR - Enum constant in enum class io.github.cvc5.Kind

Bit-wise or.

BITVECTOR_REDAND - Enum constant in enum class io.github.cvc5.Kind

Bit-vector redand.

BITVECTOR_REDOR - Enum constant in enum class io.github.cvc5.Kind

Bit-vector redor.

BITVECTOR_REPEAT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector repeat.

BITVECTOR_ROTATE_LEFT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector rotate left.

BITVECTOR_ROTATE_RIGHT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector rotate right.

BITVECTOR_SADDO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed addition overflow detection.

BITVECTOR_SBV_TO_INT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector conversion, signed bit-vector to integer.

BITVECTOR_SDIV - Enum constant in enum class io.github.cvc5.Kind

Signed bit-vector division.

BITVECTOR_SDIVO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed division overflow detection.

BITVECTOR_SGE - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed greater than or equal.

BITVECTOR_SGT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed greater than.

BITVECTOR_SHL - Enum constant in enum class io.github.cvc5.Kind

Bit-vector shift left.

BITVECTOR_SIGN_EXTEND - Enum constant in enum class io.github.cvc5.Kind

Bit-vector sign extension.

BITVECTOR_SLE - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed less than or equal.

BITVECTOR_SLT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed less than.

BITVECTOR_SLTBV - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed less than returning a bit-vector of size 1.

BITVECTOR_SMOD - Enum constant in enum class io.github.cvc5.Kind

Signed bit-vector remainder (sign follows divisor).

BITVECTOR_SMULO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed multiplication overflow detection.

BITVECTOR_SORT - Enum constant in enum class io.github.cvc5.SortKind

A bit-vector sort, parameterized by an integer denoting its bit-width.

BITVECTOR_SREM - Enum constant in enum class io.github.cvc5.Kind

Signed bit-vector remainder (sign follows dividend).

BITVECTOR_SSUBO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector signed subtraction overflow detection.

BITVECTOR_SUB - Enum constant in enum class io.github.cvc5.Kind

Subtraction of two bit-vectors.

BITVECTOR_TO_NAT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector conversion to (non-negative) integer.

BITVECTOR_UADDO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned addition overflow detection.

BITVECTOR_UBV_TO_INT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector conversion, unsigned bit-vector to integer.

BITVECTOR_UDIV - Enum constant in enum class io.github.cvc5.Kind

Unsigned bit-vector division.

BITVECTOR_UGE - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned greater than or equal.

BITVECTOR_UGT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned greater than.

BITVECTOR_ULE - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned less than or equal.

BITVECTOR_ULT - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned less than.

BITVECTOR_ULTBV - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned less than returning a bit-vector of size 1.

BITVECTOR_UMULO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned multiplication overflow detection.

BITVECTOR_UREM - Enum constant in enum class io.github.cvc5.Kind

Unsigned bit-vector remainder.

BITVECTOR_USUBO - Enum constant in enum class io.github.cvc5.Kind

Bit-vector unsigned subtraction overflow detection.

BITVECTOR_XNOR - Enum constant in enum class io.github.cvc5.Kind

Bit-wise xnor, left associative.

BITVECTOR_XOR - Enum constant in enum class io.github.cvc5.Kind

Bit-wise xor.

BITVECTOR_ZERO_EXTEND - Enum constant in enum class io.github.cvc5.Kind

Bit-vector zero extension.

blockModel(BlockModelsMode) - Method in class io.github.cvc5.Solver

Block the current model.

BlockModelsMode - Enum Class in io.github.cvc5.modes

Enum representing the set of possible values for BlockModelsMode.

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

Block the current model values of (at least) the values in terms.

BOOL_AND_CONF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-conf

BOOL_AND_CONF2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-and-conf2

BOOL_AND_DE_MORGAN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_DOUBLE_NOT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_DUAL_IMPL_EQ - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-dual-impl-eq

BOOL_EQ_FALSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-false

BOOL_EQ_NREFL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-nrefl

BOOL_EQ_TRUE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-eq-true

BOOL_IMPL_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-elim

BOOL_IMPL_FALSE1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-false1

BOOL_IMPL_FALSE2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-false2

BOOL_IMPL_TRUE1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-true1

BOOL_IMPL_TRUE2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-impl-true2

BOOL_IMPLIES_DE_MORGAN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_IMPLIES_OR_DISTRIB - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_NOT_EQ_ELIM1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_NOT_EQ_ELIM2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_NOT_FALSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-false

BOOL_NOT_ITE_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_NOT_TRUE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-not-true

BOOL_NOT_XOR_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_OR_AND_DISTRIB - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_OR_DE_MORGAN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BOOL_OR_TAUT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-taut

BOOL_OR_TAUT2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-or-taut2

BOOL_XOR_COMM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-comm

BOOL_XOR_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-elim

BOOL_XOR_FALSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-false

BOOL_XOR_NREFL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-nrefl

BOOL_XOR_REFL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-refl

BOOL_XOR_TRUE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule boolean-xor-true

BOOLEAN_SORT - Enum constant in enum class io.github.cvc5.SortKind

The Boolean sort.

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

Obtain the current value as a Boolean.

BV_AND_CONCAT_PULLUP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_AND_CONCAT_PULLUP2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_AND_CONCAT_PULLUP3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_AND_SIMPLIFY_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_AND_SIMPLIFY_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ASHR_BY_CONST_0 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ASHR_BY_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ASHR_BY_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ASHR_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ashr-zero

BV_BITBLAST_STEP - Enum constant in enum class 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_SLICING - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-add

BV_COMMUTATIVE_COMP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-comp

BV_COMMUTATIVE_XOR - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-commutative-xor

BV_COMP_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-comp-eliminate

BV_CONCAT_EXTRACT_MERGE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_CONCAT_MERGE_CONST - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EAGER_ATOM - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

The empty bitvector.

BV_EQ_EXTRACT_ELIM1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EQ_EXTRACT_ELIM2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EQ_EXTRACT_ELIM3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EQ_NOT_SOLVE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-eq-not-solve

BV_EQ_XOR_SOLVE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-eq-xor-solve

BV_EXTRACT_CONCAT_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_CONCAT_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_CONCAT_3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_CONCAT_4 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_EXTRACT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-extract

BV_EXTRACT_MULT_LEADING_BIT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_NOT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-not

BV_EXTRACT_SIGN_EXTEND_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_SIGN_EXTEND_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_SIGN_EXTEND_3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_EXTRACT_WHOLE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-extract-whole

BV_ITE_CONST_CHILDREN_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_CONST_CHILDREN_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_EQUAL_CHILDREN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_EQUAL_COND_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_EQUAL_COND_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_EQUAL_COND_3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_MERGE_ELSE_ELSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_MERGE_ELSE_IF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_MERGE_THEN_ELSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_MERGE_THEN_IF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ITE_WIDTH_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-width-one

BV_ITE_WIDTH_ONE_NOT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ite-width-one-not

BV_LSHR_BY_CONST_0 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_LSHR_BY_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_LSHR_BY_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_LSHR_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lshr-zero

BV_LT_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-lt-self

BV_MERGE_SIGN_EXTEND_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MERGE_SIGN_EXTEND_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MULT_POW2_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MULT_POW2_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MULT_POW2_2B - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MULT_SLT_MULT_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_MULT_SLT_MULT_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_NAND_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-nand-eliminate

BV_NEGO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-nego-eliminate

BV_NOR_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-nor-eliminate

BV_NOT_IDEMP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-idemp

BV_NOT_NEQ - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-neq

BV_NOT_ULT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-ult

BV_NOT_XOR - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-not-xor

BV_OR_CONCAT_PULLUP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_OR_CONCAT_PULLUP2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_OR_CONCAT_PULLUP3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_OR_SIMPLIFY_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_OR_SIMPLIFY_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_POLY_NORM - Enum constant in enum class io.github.cvc5.ProofRule

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

BV_POLY_NORM_EQ - Enum constant in enum class io.github.cvc5.ProofRule

Bit-vectors – Polynomial normalization for relations ..

BV_REDAND_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-redand-eliminate

BV_REDOR_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-redor-eliminate

BV_REPEAT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ROTATE_LEFT_ELIMINATE_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ROTATE_LEFT_ELIMINATE_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ROTATE_RIGHT_ELIMINATE_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ROTATE_RIGHT_ELIMINATE_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SADDO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-saddo-eliminate

BV_SDIV_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sdiv-eliminate

BV_SDIVO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sdivo-eliminate

BV_SGE_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sge-eliminate

BV_SGT_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sgt-eliminate

BV_SHL_BY_CONST_0 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SHL_BY_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SHL_BY_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SHL_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-shl-zero

BV_SIGN_EXTEND_ELIMINATE_0 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_EQ_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_EQ_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_ULT_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_ULT_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_ULT_CONST_3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SIGN_EXTEND_ULT_CONST_4 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_SLE_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sle-eliminate

BV_SLE_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sle-self

BV_SMOD_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-smod-eliminate

BV_SMULO_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvsmulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvsmulo}\).

BV_SREM_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-srem-eliminate

BV_SSUBO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ssubo-eliminate

BV_SUB_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-sub-eliminate

BV_TO_INT_UF - Enum constant in enum class io.github.cvc5.SkolemId

A skolem function introduced by the int-blaster.

BV_UADDO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-uaddo-eliminate

BV_UDIV_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-udiv-one

BV_UDIV_POW2_NOT_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_UDIV_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-udiv-zero

BV_UGE_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-uge-eliminate

BV_UGT_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ugt-eliminate

BV_UGT_UREM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ugt-urem

BV_ULE_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-eliminate

BV_ULE_MAX - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-max

BV_ULE_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-self

BV_ULE_ZERO - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ule-zero

BV_ULT_ADD_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ULT_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-one

BV_ULT_ONES - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-ones

BV_ULT_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-ult-self

BV_ULT_ZERO_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ULT_ZERO_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_UMULO_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Unsigned multiplication overflow detection elimination \[ \texttt{bvumulo}(x,y) = t \] where \(t\) is the result of eliminating the application of \(\texttt{bvumulo}\).

BV_UREM_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-urem-one

BV_UREM_POW2_NOT_ONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_UREM_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-urem-self

BV_USUBO_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-usubo-eliminate

BV_XNOR_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xnor-eliminate

BV_XOR_CONCAT_PULLUP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_XOR_CONCAT_PULLUP2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_XOR_CONCAT_PULLUP3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_XOR_DUPLICATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-duplicate

BV_XOR_NOT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-not

BV_XOR_ONES - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-xor-ones

BV_XOR_SIMPLIFY_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_XOR_SIMPLIFY_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_XOR_SIMPLIFY_3 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_ELIMINATE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_ELIMINATE_0 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_EQ_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_EQ_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_ULT_CONST_1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_EXTEND_ULT_CONST_2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

BV_ZERO_ULE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule bv-zero-ule

C

CARDINALITY_CONSTRAINT - Enum constant in enum class io.github.cvc5.Kind

Cardinality constraint on uninterpreted sort.

CHAIN_RESOLUTION - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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

Encapsulation of a command.

COMMON - Enum constant in enum class io.github.cvc5.modes.OptionCategory

Common options

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_CPROP - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1 \cdot w_1 \cdot \ldots \cdot t_n) = (w_2 \cdot s_2 \cdot \ldots \cdot s_m),\, \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 - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (c \cdot t_2 \ldots \cdot s_m),\,\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 - Enum constant in enum class 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 \bot}{t = s} \] Alternatively for the reverse: \inferrule{(t \cdot t_1 \cdot \ldots \cdot t_n) = (s \cdot t_1 \cdot \ldots \cdot t_n)\mid \top}{t = s} Notice that \(t\) or \(s\) may be empty, in which case they are implicit in the concatenation above.

CONCAT_LPROP - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \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 - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid \bot}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0} \] 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 - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Core rules – Concatenation unification \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1} \] Alternatively for the reverse: \[ \inferrule{(t_1 \cdot \ldots \cdot t_n) = (s_1 \cdot \ldots \cdot s_m),\, \mathit{len}(t_n) = \mathit{len}(s_m)\mid \top}{t_n = s_m} \]

CONG - Enum constant in enum class io.github.cvc5.ProofRule

Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used when the kind of \(f(t_1,\dots, t_n)\) has a fixed arity.

CONST_ARRAY - Enum constant in enum class io.github.cvc5.Kind

Constant array.

CONST_BITVECTOR - Enum constant in enum class io.github.cvc5.Kind

Fixed-size bit-vector constant.

CONST_BOOLEAN - Enum constant in enum class io.github.cvc5.Kind

Boolean constant.

CONST_FINITE_FIELD - Enum constant in enum class io.github.cvc5.Kind

Finite field constant.

CONST_FLOATINGPOINT - Enum constant in enum class io.github.cvc5.Kind

Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.

CONST_INTEGER - Enum constant in enum class io.github.cvc5.Kind

Arbitrary-precision integer constant.

CONST_RATIONAL - Enum constant in enum class io.github.cvc5.Kind

Arbitrary-precision rational constant.

CONST_ROUNDINGMODE - Enum constant in enum class io.github.cvc5.Kind

RoundingMode constant.

CONST_SEQUENCE - Enum constant in enum class io.github.cvc5.Kind

Constant sequence.

CONST_STRING - Enum constant in enum class io.github.cvc5.Kind

Constant string.

CONSTANT - Enum constant in enum class io.github.cvc5.Kind

Free constant symbol.

CONSTANT_PROP - Enum constant in enum class 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

Constructs a new ConstIterator.

ConstIterator() - Constructor for class io.github.cvc5.DatatypeConstructor.ConstIterator

Constructs a new ConstIterator.

ConstIterator() - Constructor for class io.github.cvc5.Statistics.ConstIterator

Constructs a new iterator over the statistics using default visibility options.

ConstIterator() - Constructor for class io.github.cvc5.Term.ConstIterator

Constructs a new ConstIterator.

ConstIterator(boolean, boolean) - Constructor for class io.github.cvc5.Statistics.ConstIterator

Constructs a new iterator over the statistics with specific filtering options.

Context - Class in io.github.cvc5

The Context class is responsible for tracking and deleting pointers to native C++ cvc5 objects associated with their corresponding Java counterparts.

CONTRA - Enum constant in enum class io.github.cvc5.ProofRule

Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]

COSECANT - Enum constant in enum class io.github.cvc5.Kind

Cosecant function.

COSINE - Enum constant in enum class io.github.cvc5.Kind

Cosine function.

COTANGENT - Enum constant in enum class io.github.cvc5.Kind

Cotangent function.

CPC - Enum constant in enum class io.github.cvc5.modes.ProofFormat

Output Cooperating Proof Calculus proof based on Eunoia signatures.

CURRENT - Static variable in enum class io.github.cvc5.Utils.OS

The detected operating system on which the application is currently running.

CVC5ApiException - Exception Class in io.github.cvc5

Base class for all API exceptions.

CVC5ApiException(String) - Constructor for exception class io.github.cvc5.CVC5ApiException

Construct with message from a string.

CVC5ApiOptionException - Exception Class in io.github.cvc5

An option-related API exception.

CVC5ApiOptionException(String) - Constructor for exception class io.github.cvc5.CVC5ApiOptionException

Construct with message from a string.

CVC5ApiRecoverableException - Exception Class in io.github.cvc5

A recoverable API exception.

CVC5ApiRecoverableException(String) - Constructor for exception class io.github.cvc5.CVC5ApiRecoverableException

Construct with message from a string.

CVC5ParserException - Exception Class in io.github.cvc5

A parser-related API exception.

CVC5ParserException(String) - Constructor for exception class io.github.cvc5.CVC5ParserException

Construct with message from a string.

D

Datatype - Class in io.github.cvc5

A cvc5 datatype.

DATATYPE_SORT - Enum constant in enum class io.github.cvc5.SortKind

A datatype sort.

Datatype.ConstIterator - Class in io.github.cvc5

ConstIterator is an implementation of the Iterator interface for iterating over a collection of DatatypeConstructor objects.

DatatypeConstructor - Class in io.github.cvc5

A cvc5 datatype constructor.

DatatypeConstructor.ConstIterator - Class in io.github.cvc5

ConstIterator is an implementation of the Iterator interface for iterating over a collection of DatatypeSelector objects.

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 - Enum constant in enum class 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.Command

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

deletePointer() - Method in class io.github.cvc5.Statistics

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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

Free the native resource associated with this pointer.

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 registered native pointers in reverse order of their registration.

DISTINCT - Enum constant in enum class io.github.cvc5.Kind

Disequality.

DISTINCT_BINARY_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule distinct-binary-elim

DISTINCT_CARD_CONFLICT - Enum constant in enum class 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 - Enum constant in enum class 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\)

DISTINCT_VALUES - Enum constant in enum class io.github.cvc5.ProofRule

Builtin theory – Distinct values \[ \inferrule{- \mid t, s}{\neg t = s} \] where \(t\) and \(s\) are distinct values.

DIV_BY_ZERO - Enum constant in enum class io.github.cvc5.SkolemId

The function for division by zero.

DIVISIBLE - Enum constant in enum class io.github.cvc5.Kind

Operator for the divisibility-by-\(k\) predicate.

DIVISION - Enum constant in enum class io.github.cvc5.Kind

Real division, division by 0 undefined, left associative.

DIVISION_TOTAL - Enum constant in enum class io.github.cvc5.Kind

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

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

Determine if this parser done reading input.

DOT - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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_COLLAPSE_SELECTOR - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.modes.FindSynthTarget

Find the next term in the enumeration of the target grammar.

EQ_COND_DEQ - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-cond-deq

EQ_ITE_LIFT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-ite-lift

EQ_RANGE - Enum constant in enum class io.github.cvc5.Kind

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

EQ_REFL - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-refl

EQ_RESOLVE - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule eq-symm

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

Equality.

EQUAL - Enum constant in enum class 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

Compare this Pair to the specified object for equality.

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

Indicate whether some other object is "equal to" this one.

EQUIV_ELIM1 - Enum constant in enum class io.github.cvc5.ProofRule

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

EQUIV_ELIM2 - Enum constant in enum class io.github.cvc5.ProofRule

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

EVALUATE - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Existentially quantified formula.

EXISTS_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

EXISTS_STRING_LENGTH - Enum constant in enum class io.github.cvc5.ProofRule

Quantifiers – Exists string length \[ \inferrule{-\mid T n i} {\mathit{len}(k) = n} \] where \(k\) is a skolem of string or sequence type \(T\) and \(n\) is a non-negative integer.

EXPERT - Enum constant in enum class io.github.cvc5.modes.OptionCategory

Option available to expert users

EXPONENTIAL - Enum constant in enum class io.github.cvc5.Kind

Exponential function.

F

FACTORING - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

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

FALSE_INTRO - Enum constant in enum class 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 Class in io.github.cvc5.modes

Enum representing the set of possible values for FindSynthTarget.

FINITE_FIELD_ADD - Enum constant in enum class io.github.cvc5.Kind

Addition of two or more finite field elements.

FINITE_FIELD_BITSUM - Enum constant in enum class io.github.cvc5.Kind

Bitsum of two or more finite field elements: x + 2y + 4z + ...

FINITE_FIELD_MULT - Enum constant in enum class io.github.cvc5.Kind

Multiplication of two or more finite field elements.

FINITE_FIELD_NEG - Enum constant in enum class io.github.cvc5.Kind

Negation of a finite field element (additive inverse).

FINITE_FIELD_SORT - Enum constant in enum class io.github.cvc5.SortKind

A finite field sort, parameterized by a size.

first - Variable in class io.github.cvc5.Pair

The first element of the pair.

first - Variable in class io.github.cvc5.Triplet

The first element of the triplet.

FLOATINGPOINT_ABS - Enum constant in enum class io.github.cvc5.Kind

Floating-point absolute value.

FLOATINGPOINT_ADD - Enum constant in enum class io.github.cvc5.Kind

Floating-point addition.

FLOATINGPOINT_DIV - Enum constant in enum class io.github.cvc5.Kind

Floating-point division.

FLOATINGPOINT_EQ - Enum constant in enum class io.github.cvc5.Kind

Floating-point equality.

FLOATINGPOINT_FMA - Enum constant in enum class io.github.cvc5.Kind

Floating-point fused multiply and add.

FLOATINGPOINT_FP - Enum constant in enum class io.github.cvc5.Kind

Create floating-point literal from bit-vector triple.

FLOATINGPOINT_GEQ - Enum constant in enum class io.github.cvc5.Kind

Floating-point greater than or equal.

FLOATINGPOINT_GT - Enum constant in enum class io.github.cvc5.Kind

Floating-point greater than.

FLOATINGPOINT_IS_INF - Enum constant in enum class io.github.cvc5.Kind

Floating-point is infinite tester.

FLOATINGPOINT_IS_NAN - Enum constant in enum class io.github.cvc5.Kind

Floating-point is NaN tester.

FLOATINGPOINT_IS_NEG - Enum constant in enum class io.github.cvc5.Kind

Floating-point is negative tester.

FLOATINGPOINT_IS_NORMAL - Enum constant in enum class io.github.cvc5.Kind

Floating-point is normal tester.

FLOATINGPOINT_IS_POS - Enum constant in enum class io.github.cvc5.Kind

Floating-point is positive tester.

FLOATINGPOINT_IS_SUBNORMAL - Enum constant in enum class io.github.cvc5.Kind

Floating-point is sub-normal tester.

FLOATINGPOINT_IS_ZERO - Enum constant in enum class io.github.cvc5.Kind

Floating-point is zero tester.

FLOATINGPOINT_LEQ - Enum constant in enum class io.github.cvc5.Kind

Floating-point less than or equal.

FLOATINGPOINT_LT - Enum constant in enum class io.github.cvc5.Kind

Floating-point less than.

FLOATINGPOINT_MAX - Enum constant in enum class io.github.cvc5.Kind

Floating-point maximum.

FLOATINGPOINT_MIN - Enum constant in enum class io.github.cvc5.Kind

Floating-point minimum.

FLOATINGPOINT_MULT - Enum constant in enum class io.github.cvc5.Kind

Floating-point multiply.

FLOATINGPOINT_NEG - Enum constant in enum class io.github.cvc5.Kind

Floating-point negation.

FLOATINGPOINT_REM - Enum constant in enum class io.github.cvc5.Kind

Floating-point remainder.

FLOATINGPOINT_RTI - Enum constant in enum class io.github.cvc5.Kind

Floating-point round to integral.

FLOATINGPOINT_SORT - Enum constant in enum class io.github.cvc5.SortKind

A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.

FLOATINGPOINT_SQRT - Enum constant in enum class io.github.cvc5.Kind

Floating-point square root.

FLOATINGPOINT_SUB - Enum constant in enum class io.github.cvc5.Kind

Floating-point sutraction.

FLOATINGPOINT_TO_FP_FROM_FP - Enum constant in enum class io.github.cvc5.Kind

Conversion to floating-point from floating-point.

FLOATINGPOINT_TO_FP_FROM_IEEE_BV - Enum constant in enum class io.github.cvc5.Kind

Conversion to floating-point from IEEE-754 bit-vector.

FLOATINGPOINT_TO_FP_FROM_REAL - Enum constant in enum class io.github.cvc5.Kind

Conversion to floating-point from Real.

FLOATINGPOINT_TO_FP_FROM_SBV - Enum constant in enum class io.github.cvc5.Kind

Conversion to floating-point from signed bit-vector.

FLOATINGPOINT_TO_FP_FROM_UBV - Enum constant in enum class io.github.cvc5.Kind

Conversion to floating-point from unsigned bit-vector.

FLOATINGPOINT_TO_REAL - Enum constant in enum class io.github.cvc5.Kind

Conversion to Real from floating-point.

FLOATINGPOINT_TO_SBV - Enum constant in enum class io.github.cvc5.Kind

Conversion to signed bit-vector from floating-point.

FLOATINGPOINT_TO_UBV - Enum constant in enum class io.github.cvc5.Kind

Conversion to unsigned bit-vector from floating-point.

FORALL - Enum constant in enum class io.github.cvc5.Kind

Universally quantified formula.

FP_MAX_ZERO - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 class io.github.cvc5.Kind

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.BlockModelsMode

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.FindSynthTarget

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.InputLanguage

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.LearnedLitType

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.OptionCategory

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.ProofComponent

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.modes.ProofFormat

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.ProofRewriteRule

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.ProofRule

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.RoundingMode

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.SkolemId

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.SortKind

Converts an integer value to the corresponding enum constant.

fromInt(int) - Static method in enum class io.github.cvc5.UnknownExplanation

Converts an integer value to the corresponding enum constant.

FULL - Enum constant in enum class io.github.cvc5.modes.ProofComponent

A proof of false whose free assumptions are a subset of the input formulas F1), ...

FUNCTION_SORT - Enum constant in enum class io.github.cvc5.SortKind

A function sort with given domain sorts and codomain sort.

G

GEQ - Enum constant in enum class 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

Get the sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

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

Get the option name aliases.

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

Get the arguments of the root step of the proof as a vector of terms.

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

Get the array element sort of an array element sort.

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

Get the array index sort of an array sort.

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

Get the list of asserted formulas.

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

Get the element sort of a bag sort.

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

Get base info.

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

Get the bit-width of the bit-vector 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

Get the premises of the root step of the proof.

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

Get the Codomain sort of this selector.

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

Get the current value.

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

Get the underlying datatype of a datatype sort.

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

Get the arity of a datatype sort.

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

Get the arity of a datatype constructor sort.

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

Get the codomain sort of a datatype constructor sort.

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

Get the domain sorts of a datatype constructor sort.

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

Get the codomain sort of a datatype selector sort.

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

Get the domain sort of a datatype selector sort.

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

Get the codomain sort of a datatype tester sort, which is the Boolean sort.

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

Get the domain sort of a datatype tester 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

Get the default value.

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

Get the bit-width of the bit-vector 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

Get the bit-width of the exponent of the floating-point sort.

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

Get the width of the significand of the floating-point sort.

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

Asserts isFloatingPointValue().

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

Get the arity of a function sort.

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

Get the codomain sort of a function sort.

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

Get the domain sorts of a function sort.

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

Return the histogram value.

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

Get the id of this 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.

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

Get the kind of this operator.

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

Get the kind of this sort.

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

Get the kind of this 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

Get the logic used by this symbol manager.

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

Get the maximum value.

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

Get the minimum value.

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

Get the list of valid mode values.

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

Get the name of the plugin (for debugging).

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

Get the name of this Datatype.

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

Get the name of this Datatype constructor.

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

Get the name of this datatype declaration.

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

Get the Name of this Datatype selector.

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

Get the name of the option.

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

Get the element sort of a nullable sort.

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

Get the number of children of this term.

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

Get the number of constructors for this 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

Get the number of indices of this 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

Get the number of selectors (so far) of this Datatype constructor.

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

Get the Op used to create this 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

Convert an array of Pair objects, where the second element extends AbstractPointer, into an array of Pair objects with the second element as a Long representing the native pointer.

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

Get the parameters of this datatype.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

getPointer() - Method in class io.github.cvc5.Statistics

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

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

Return the raw native pointer.

getPointers(IPointer[]) - Static method in class io.github.cvc5.Utils

Extract native pointer values from a one-dimensional array of IPointer objects.

getPointers(IPointer[][]) - Static method in class io.github.cvc5.Utils

Extract native pointer values from a two-dimensional matrix of IPointer objects.

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

Construct an array of Proof objects from an array of native pointers.

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

Do quantifier elimination.

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

Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.

getRational(Pair<BigInteger, BigInteger>) - Static method in class io.github.cvc5.Utils

Convert a pair of BigIntegers to a rational string a/b

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

Convert a rational string a/b to a pair of BigIntegers

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

Asserts isRealAlgebraicNumber().

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

Asserts isRealAlgebraicNumber().

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

Asserts isRealAlgebraicNumber().

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

Get integer or real value sign.

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

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

Get the conclusion of the root step of the proof.

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

Get the proof rewrite rule used by the root step of the 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

Get the proof rule used by the root step of the 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

Get the element sort of a sequence sort.

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

Asserts isSequenceValue().

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

Determine if the option was set by the user.

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

Get the element sort of a set 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

Get the underlying solver of this input parser.

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

Get the sort of this term.

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

Construct an array of Sort objects from an array of native pointers.

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

Get the stored string constant.

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

Get the raw symbol of the symbol.

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

Asserts hasSymbol().

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

Get the underlying symbol manager of this input parser.

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

Construct an array of Term objects from an array of native pointers.

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

Get the length of a tuple sort.

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

Get the element sorts of a tuple 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

Get the arity of an uninterpreted sort constructor 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 class io.github.cvc5.Kind

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

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

Get the integer value associated with this enum constant.

getValue() - Method in enum class io.github.cvc5.SortKind

Get the integer value associated with this enum constant.

getValue() - Method in enum class io.github.cvc5.UnknownExplanation

Get the integer value associated with this enum constant.

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

Constructs a new Grammar instance by creating a deep copy of the specified Grammar.

GROUND_TERM - Enum constant in enum class io.github.cvc5.SkolemId

An arbitrary ground term of a given sort.

GT - Enum constant in enum class 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

Determine if the synthesis query has no solution.

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

Determine if this term has an operator.

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

Determine if the synthesis query has a solution.

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

Determine if the sort has a symbol.

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

Determine if the term has a symbol.

HO_APP_ENCODE - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Higher-order applicative encoding of function application, left associative.

HO_CONG - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Integer and.

IMPLIES - Enum constant in enum class io.github.cvc5.Kind

Logical implication.

IMPLIES_ELIM - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.UnknownExplanation

Incomplete theory solver.

INPUT - Enum constant in enum class 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 Class in io.github.cvc5.modes

Enum representing the set of possible values for InputLanguage.

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 - Enum constant in enum class io.github.cvc5.Kind

A instantantiation-add-to-pool annotation.

INST_ATTRIBUTE - Enum constant in enum class io.github.cvc5.Kind

Instantiation attribute.

INST_NO_PATTERN - Enum constant in enum class io.github.cvc5.Kind

Instantiation no-pattern.

INST_PATTERN - Enum constant in enum class io.github.cvc5.Kind

Instantiation pattern.

INST_PATTERN_LIST - Enum constant in enum class io.github.cvc5.Kind

A list of instantiation patterns, attributes or annotations.

INST_POOL - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

The function for integer division by zero.

INT_TIGHT_LB - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Conversion from Int to bit-vector.

INT_TO_BV_ELIM - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SortKind

The integer sort.

INTERNAL - Enum constant in enum class io.github.cvc5.modes.LearnedLitType

Any internal literal that does not fall into the above categories.

INTERNAL - Enum constant in enum class io.github.cvc5.SkolemId

The identifier of the skolem is not exported.

INTERNAL_KIND - Enum constant in enum class io.github.cvc5.Kind

Internal kind.

INTERNAL_SORT_KIND - Enum constant in enum class io.github.cvc5.SortKind

Internal kind.

INTERRUPTED - Enum constant in enum class io.github.cvc5.UnknownExplanation

Solver was interrupted.

INTS_DIVISION - Enum constant in enum class io.github.cvc5.Kind

Integer division, division by 0 undefined, left associative.

INTS_DIVISION_TOTAL - Enum constant in enum class io.github.cvc5.Kind

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

INTS_MODULUS - Enum constant in enum class io.github.cvc5.Kind

Integer modulus, modulus by 0 undefined.

INTS_MODULUS_TOTAL - Enum constant in enum class 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

Functional interface representing an oracle function that operates on an array of Term objects and produces a single Term as output.

IS_INTEGER - Enum constant in enum class 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

Determine if the term is a bit-vector value.

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

Determine if the term is a Boolean value.

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

Determine if the term is a cardinality constraint.

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

Determine if this datatype corresponds to a co-datatype.

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

Determine if the term is a constant array.

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

Determine if this datatype is finite.

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

Determine if the term is a finite field value.

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

Determine if the term is the floating-point value for not a number.

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

Determine if the term is the floating-point value for negative.

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

Determine if the term is the floating-point value for negative zero.

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

Determine if the term is the floating-point value for positive.

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

Determine if the term is the floating-point value for positive zero.

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

Determine if the term is a floating-point value.

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

Determine if this operator is indexed.

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

Determine if the term is an integer value.

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

Determine if the logic of this symbol manager has been set.

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

Determine if this command is null.

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

Determine if this Datatype is a null object.

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

Determine if this DatatypeConstructor is a null object.

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

Determine if this DatatypeConstructorDecl is a null declaration.

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

Determine if this DatatypeDecl is a null object.

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

Determine if this DatatypeSelector is a null object.

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

Determine if this is the null grammar.

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

Determine if this operator is a null term.

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

Determine if Result is empty, i.e., a nullary Result, and not an actual result returned from a checkSat() (and friends) query.

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

Determine if this is the null sort.

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

Determine if SynthResult is empty, i.e., a nullary SynthResult, and not an actual result returned from a synthesis query.

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

Determine if this term is a null term.

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

Determine if this a nullable sort.

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

Determine if this datatype is parametric.

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

Determine if the term is a real algebraic number.

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

Determine if the term is a rational value.

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

Determine if this datatype corresponds to a record.

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

Determine if the term is a floating-point rounding mode value.

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

Determine if query was a satisfiable checkSat() or checkSatAssuming() query.

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

Determine if this is a Sequence sort.

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

Determine if the term is a sequence value.

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

Determine if this is a Set sort.

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

Determine if the term is a set value.

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

Determine if this term is a skolem function.

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

Determine if the term is a string constant.

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

Determine if this datatype corresponds to a tuple.

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

Determine if this a tuple sort.

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

Determine if the term is a tuple value.

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

Determine if the term is an uninterpreted sort value.

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

Determine if query was a checkSat() or checkSatAssuming() query and cvc5 was not able to determine (un)satisfiability.

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

Determine if the result of the synthesis query could not be determined.

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

Determine if if query was an unsatisfiable checkSat() or checkSatAssuming() query.

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 - Enum constant in enum class io.github.cvc5.Kind

If-then-else.

ITE_ELIM1 - Enum constant in enum class io.github.cvc5.ProofRule

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

ITE_ELIM2 - Enum constant in enum class io.github.cvc5.ProofRule

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

ITE_ELSE_FALSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-false

ITE_ELSE_LOOKAHEAD - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-lookahead

ITE_ELSE_LOOKAHEAD_NOT_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_ELSE_LOOKAHEAD_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_ELSE_NEG_LOOKAHEAD - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_ELSE_TRUE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-else-true

ITE_EQ - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-eq-branch

ITE_EXPAND - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-expand

ITE_FALSE_COND - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-false-cond

ITE_NEG_BRANCH - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-neg-branch

ITE_NOT_COND - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-not-cond

ITE_THEN_FALSE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-false

ITE_THEN_LOOKAHEAD - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-lookahead

ITE_THEN_LOOKAHEAD_NOT_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_THEN_LOOKAHEAD_SELF - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_THEN_NEG_LOOKAHEAD - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

ITE_THEN_TRUE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule ite-then-true

ITE_TRUE_COND - Enum constant in enum class 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

Begin iteration over the statistics values.

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

If-then-else with this term as the Boolean condition.

K

Kind - Enum Class in io.github.cvc5

Enum representing the set of possible values for Kind.

L

LAMBDA - Enum constant in enum class io.github.cvc5.Kind

Lambda expression.

LAMBDA_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

LAST_KIND - Enum constant in enum class io.github.cvc5.Kind

Marks the upper-bound of this enumeration.

LAST_SORT_KIND - Enum constant in enum class io.github.cvc5.SortKind

Marks the upper-bound of this enumeration.

LearnedLitType - Enum Class in io.github.cvc5.modes

Enum representing the set of possible values for LearnedLitType.

LEQ - Enum constant in enum class io.github.cvc5.Kind

Less than or equal, chainable.

LFSC - Enum constant in enum class io.github.cvc5.modes.ProofFormat

Output LFSC proof.

LFSC_RULE - Enum constant in enum class io.github.cvc5.ProofRule

External – LFSC Place holder for LFSC rules.

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

The base path inside the JAR where native libraries are stored.

LINUX - Enum constant in enum class io.github.cvc5.Utils.OS

Linux-based operating system.

LITERALS - Enum constant in enum class 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

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

LT - Enum constant in enum class io.github.cvc5.Kind

Less than, chainable.

M

MAC - Enum constant in enum class io.github.cvc5.Utils.OS

Apple macOS operating system.

MACRO_ARITH_INT_EQ_CONFLICT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Arithmetic – Integer equality conflict \[ (t=s) = \bot \] where \(t=s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to \((r = c)\) where \(r\) is an integral term and \(c\) is a non-integral constant.

MACRO_ARITH_INT_GEQ_TIGHTEN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Arithmetic – Integer inequality tightening \[ (t \geq s) = ( r \geq \lceil c \rceil) \] or \[ (t \geq s) = \neg( r \geq \lceil c \rceil) \] where \(t \geq s\) is equivalent (via ARITH_POLY_NORM <cvc5.ProofRule.ARITH_POLY_NORM>) to the right hand side where \(r\) is an integral term and \(c\) is a non-integral constant.

MACRO_ARITH_SCALE_SUM_UB - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

MACRO_ARRAYS_NORMALIZE_CONSTANT - Enum constant in enum class 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_ARRAYS_NORMALIZE_OP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Arrays – Macro normalize operation \[ A = B \] where \(B\) is the result of normalizing the array operation \(A\) into a canonical form, based on commutativity of disjoint indices.

MACRO_BOOL_BV_INVERT_SOLVE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Booleans – Bitvector invert solve \[ ((t_1 = t_2) = (x = r)) = \top \] where \(x\) occurs on an invertible path in \(t_1 = t_2\) and has solved form \(r\).

MACRO_BOOL_NNF_NORM - Enum constant in enum class 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_AND_OR_XOR_CONCAT_PULLUP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro and/or/xor concat pullup \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndOrXorConcatPullup.

MACRO_BV_AND_SIMPLIFY - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro and simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule AndSimplify.

MACRO_BV_BITBLAST - Enum constant in enum class 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_BV_CONCAT_CONSTANT_MERGE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro concat constant merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatConstantMerge.

MACRO_BV_CONCAT_EXTRACT_MERGE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro concat extract merge \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ConcatExtractMerge.

MACRO_BV_EQ_SOLVE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro equality solve \[ (a = b) = \bot \] where \(bvsub(a,b)\) normalizes to a non-zero constant, or alternatively \[ (a = b) = \top \] where \(bvsub(a,b)\) normalizes to zero.

MACRO_BV_EXTRACT_CONCAT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro extract and concat \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule ExtractConcat.

MACRO_BV_MULT_SLT_MULT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro multiply signed less than multiply \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule MultSltMult.

MACRO_BV_OR_SIMPLIFY - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro or simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule OrSimplify.

MACRO_BV_XOR_SIMPLIFY - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Bitvectors – Macro xor simplify \[ a = b \] where \(a\) is rewritten to \(b\) by the internal rewrite rule XorSimplify.

MACRO_DT_CONS_EQ - Enum constant in enum class 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_LAMBDA_CAPTURE_AVOID - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Equality – Macro lambda application capture avoid \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = ((\lambda y_1 \ldots y_n.\> t') \ t_1 \ldots t_n) \] The terms may either be of kind `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.

MACRO_QUANT_DT_VAR_EXPAND - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Quantifiers – Macro datatype variable expand \[ (\forall Y x Z.\> F) = (\forall Y X_1 Z.

MACRO_QUANT_MERGE_PRENEX - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

MACRO_RE_INTER_UNION_CONST_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro regular expression intersection/union constant elimination One of the following forms: \[ \mathit{re.union}(R) = \mathit{re.union}(R') \] where \(R\) is a list of regular expressions containing \(R_i\) and \(\mathit{str.to_re(c)}\) where \(c\) is a string in \(R_i\) and \(R'\) is the result of removing \(\mathit{str.to_re(c)}\) from \(R\).

MACRO_RE_INTER_UNION_INCLUSION - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – regular expression intersection/union inclusion \[ \mathit{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`.

MACRO_RESOLUTION - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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., Rewriter.rewrite.

MACRO_SR_EQ_INTRO - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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_STR_COMPONENT_CTN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro string component contains \[ \mathit{str.contains}(t, s) = \top \] where a substring of \(t\) can be inferred to be a superstring of \(s\) based on iterating on components of string concatenation terms as well as prefix and suffix reasoning.

MACRO_STR_CONST_NCTN_CONCAT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro string constant no contains concatenation \[ \mathit{str.contains}(c, \mathit{str.++}(t_1, \ldots, t_n)) = \bot \] where \(c\) is not contained in \(R_t\), where the regular expression \(R_t\) overapproximates the possible values of \(\mathit{str.++}(t_1, \ldots, t_n)\).

MACRO_STR_EQ_LEN_UNIFY - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – String equality length unify \[ (\mathit{str}.\text{++}(s_1, \ldots, s_n) = \mathit{str}.\text{++}(t_1, \ldots, t_m)) = (r_1 = u_1 \wedge \ldots r_k = u_k) \] where for each \(i = 1, \ldots, k\), we can show the length of \(r_i\) and \(u_i\) are equal, \(s_1, \ldots, s_n\) is \(r_1, \ldots, r_k\), and \(t_1, \ldots, t_m\) is \(u_1, \ldots, u_k\).

MACRO_STR_EQ_LEN_UNIFY_PREFIX - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – String equality length unify prefix \[ (s = \mathit{str}.\text{++}(t_1, \ldots, t_n)) = (s = \mathit{str}.\text{++}(t_1, \ldots t_i)) \wedge t_{i+1} = \epsilon \wedge \ldots \wedge t_n = \epsilon \] where we can show \(s\) has a length that is at least the length of \(\text{++}(t_1, \ldots t_i)\).

MACRO_STR_IN_RE_INCLUSION - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro string in regular expression inclusion \[ \mathit{str.in_re}(s, R) = \top \] where \(R\) includes the regular expression \(R_s\) which overapproximates the possible values of string \(s\).

MACRO_STR_SPLIT_CTN - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro string split contains \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_1, s) \vee \mathit{str.contains}(t_2, s) \] where \(t_1\) and \(t_2\) are substrings of \(t\).

MACRO_STR_STRIP_ENDPOINTS - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – Macro string strip endpoints One of the following forms: \[ \mathit{str.contains}(t, s) = \mathit{str.contains}(t_2, s) \] \[ \mathit{str.indexof}(t, s, n) = \mathit{str.indexof}(t_2, s, n) \] \[ \mathit{str.replace}(t, s, r) = \mathit{str.++}(t_1, \mathit{str.replace}(t_2, s, r) t_3) \] where in each case we reason about removing portions of \(t\) that are irrelevant to the evaluation of the term.

MACRO_STRING_INFERENCE - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Match expression.

MATCH_BIND_CASE - Enum constant in enum class io.github.cvc5.Kind

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

MATCH_CASE - Enum constant in enum class io.github.cvc5.Kind

Match case for nullary constructors.

MEMOUT - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

The function for integer modulus by zero.

ModeInfo(String, String, String[]) - Constructor for class io.github.cvc5.OptionInfo.ModeInfo

Constructs a ModeInfo instance with the specified default value, current value, and available mode options.

MODUS_PONENS - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Arithmetic multiplication.

N

NARY_CONG - Enum constant in enum class io.github.cvc5.ProofRule

Equality – N-ary Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid f(t_1,\dots, t_n)}{f(t_1,\dots, t_n) = f(s_1,\dots, s_n)} \] This rule is used for terms \(f(t_1,\dots, t_n)\) whose kinds \(k\) have variadic arity, such as cvc5.Kind.AND, cvc5.Kind.PLUS and so on.

NEG - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.modes.ProofFormat

Do not translate proof output.

NONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

NONE - Enum constant in enum class io.github.cvc5.SkolemId

Indicates this is not a skolem.

NOT - Enum constant in enum class io.github.cvc5.Kind

Logical negation.

NOT_AND - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

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

NOT_IMPLIES_ELIM2 - Enum constant in enum class io.github.cvc5.ProofRule

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

NOT_ITE_ELIM1 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

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

NOT_OR_ELIM - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SortKind

Null kind.

NULL_TERM - Enum constant in enum class io.github.cvc5.Kind

Null kind.

NULLABLE_LIFT - Enum constant in enum class io.github.cvc5.Kind

Lifting operator for nullable terms.

NULLABLE_SORT - Enum constant in enum class 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

Construct a NumberInfo instance with specified default value, current value, minimum, and maximum.

O

Op - Class in io.github.cvc5

A cvc5 operator.

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

Null op

OptionCategory - Enum Class in io.github.cvc5.modes

Enum representing the set of possible values for OptionCategory.

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

Information for mode option values.

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 - Enum constant in enum class io.github.cvc5.Kind

Logical disjunction.

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

Boolean or.

OTHER - Enum constant in enum class io.github.cvc5.UnknownExplanation

Other reason.

P

Pair<K,V> - Class in io.github.cvc5

A simple generic container class to hold a pair of objects.

Pair(K, V) - Constructor for class io.github.cvc5.Pair

Construct a new Pair with the given values.

PI - Enum constant in enum class io.github.cvc5.Kind

Pi constant.

pointer - Variable in class io.github.cvc5.Command

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Datatype

The raw native pointer value.

pointer - Variable in class io.github.cvc5.DatatypeConstructor

The raw native pointer value.

pointer - Variable in class io.github.cvc5.DatatypeConstructorDecl

The raw native pointer value.

pointer - Variable in class io.github.cvc5.DatatypeDecl

The raw native pointer value.

pointer - Variable in class io.github.cvc5.DatatypeSelector

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Grammar

The raw native pointer value.

pointer - Variable in class io.github.cvc5.InputParser

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Op

The raw native pointer value.

pointer - Variable in class io.github.cvc5.OptionInfo

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Proof

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Result

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Solver

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Sort

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Stat

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Statistics

The raw native pointer value.

pointer - Variable in class io.github.cvc5.SymbolManager

The raw native pointer value.

pointer - Variable in class io.github.cvc5.SynthResult

The raw native pointer value.

pointer - Variable in class io.github.cvc5.Term

The raw native pointer value.

pointer - Variable in class io.github.cvc5.TermManager

The raw native pointer value.

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 - Enum constant in enum class io.github.cvc5.Kind

Arithmetic power.

POW2 - Enum constant in enum class io.github.cvc5.Kind

Power of two.

PREPROCESS - Enum constant in enum class io.github.cvc5.modes.LearnedLitType

A top-level literal (unit clause) from the preprocessed set of input formulas.

PREPROCESS - Enum constant in enum class io.github.cvc5.modes.ProofComponent

Proofs of Gu1 ...

PREPROCESS_SOLVED - Enum constant in enum class 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 Class in io.github.cvc5.modes

Enum representing the set of possible values for ProofComponent.

ProofFormat - Enum Class in io.github.cvc5.modes

Enum representing the set of possible values for ProofFormat.

ProofRewriteRule - Enum Class in io.github.cvc5

Enum representing the set of possible values for ProofRewriteRule.

ProofRule - Enum Class in io.github.cvc5

Enum representing the set of possible values for ProofRule.

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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

QUANT_MERGE_PRENEX - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Quantifiers – Macro variable elimination equality ..

QUANT_VAR_REORDERING - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

The n^th skolem for the negation of universally quantified formula Q.

QUERY - Enum constant in enum class io.github.cvc5.modes.FindSynthTarget

Find a query over the given grammar.

R

RAW_PREPROCESS - Enum constant in enum class io.github.cvc5.modes.ProofComponent

Proofs of G1 ...

RE_ALL_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-all-elim

RE_CONCAT - Enum constant in enum class io.github.cvc5.ProofRule

Strings – Regular expressions – Concatenation \[ \inferrule{t_1\in R_1,\,\ldots,\,t_n\in R_n\mid -}{\text{str.++}(t_1, \ldots, t_n)\in \text{re.++}(R_1, \ldots, R_n)} \]

RE_CONCAT_MERGE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-concat-merge

RE_CONCAT_STAR_REPEAT - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_CONCAT_STAR_SUBSUME1 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_CONCAT_STAR_SUBSUME2 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_CONCAT_STAR_SWAP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_DIFF_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-diff-elim

RE_FIRST_MATCH - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

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

RE_IN_COMP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-comp

RE_IN_CSTRING - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-cstring

RE_IN_EMPTY - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-empty

RE_IN_SIGMA - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-in-sigma

RE_IN_SIGMA_STAR - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_INTER - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-all

RE_INTER_CSTRING - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-inter-cstring

RE_INTER_CSTRING_NEG - Enum constant in enum class io.github.cvc5.ProofRewriteRule

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

RE_INTER_INCLUSION - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – regular expression intersection inclusion \[ \mathit{re.inter}(r_1, re.comp(r_2)) = \mathit{re.none} \] where \(r_2\) is a superset of \(r_1\).

RE_LOOP_ELIM - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-loop-neg

RE_OPT_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-opt-elim

RE_PLUS_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-plus-elim

RE_STAR_EMP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-star-emp

RE_STAR_NONE - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-star-none

RE_STAR_STAR - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-star-star

RE_STAR_UNION_DROP_EMP - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-star-union-drop-emp

RE_UNFOLD_NEG - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRule

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

RE_UNFOLD_POS - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union-all

RE_UNION_CONST_ELIM - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Auto-generated from RARE rule re-union--elim

RE_UNION_INCLUSION - Enum constant in enum class io.github.cvc5.ProofRewriteRule

Strings – regular expression union inclusion \[ \mathit{re.union}(r_1, re.comp(r_2)) = \mathit{re}.\text{*}(\mathit{re.allchar}) \] where \(r_1\) is a superset of \(r_2\).

REAL_SORT - Enum constant in enum class io.github.cvc5.SortKind

The real sort.

REFL - Enum constant in enum class io.github.cvc5.ProofRule

Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]

REGEXP_ALL - Enum constant in enum class io.github.cvc5.Kind

Regular expression all.

REGEXP_ALLCHAR - Enum constant in enum class io.github.cvc5.Kind

Regular expression all characters.

REGEXP_COMPLEMENT - Enum constant in enum class io.github.cvc5.Kind

Regular expression complement.

REGEXP_CONCAT - Enum constant in enum class io.github.cvc5.Kind

Regular expression concatenation.

REGEXP_DIFF - Enum constant in enum class io.github.cvc5.Kind

Regular expression difference.

REGEXP_INTER - Enum constant in enum class io.github.cvc5.Kind

Regular expression intersection.

REGEXP_LOOP - Enum constant in enum class io.github.cvc5.Kind

Regular expression loop.

REGEXP_NONE - Enum constant in enum class io.github.cvc5.Kind

Regular expression none.

REGEXP_OPT - Enum constant in enum class io.github.cvc5.Kind

Regular expression ?.

REGEXP_PLUS - Enum constant in enum class io.github.cvc5.Kind

Regular expression +.

REGEXP_RANGE - Enum constant in enum class io.github.cvc5.Kind

Regular expression range.

REGEXP_REPEAT - Enum constant in enum class io.github.cvc5.Kind

Operator for regular expression repeat.

REGEXP_STAR - Enum constant in enum class io.github.cvc5.Kind

Regular expression \*.

REGEXP_UNION - Enum constant in enum class io.github.cvc5.Kind

Regular expression union.

REGLAN_SORT - Enum constant in enum class io.github.cvc5.SortKind

The regular language sort.

REGULAR - Enum constant in enum class io.github.cvc5.modes.OptionCategory

Option available to regular users

RELATION_AGGREGATE - Enum constant in enum class io.github.cvc5.Kind

Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ...

RELATION_GROUP - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Relation identity.

RELATION_JOIN - Enum constant in enum class io.github.cvc5.Kind

Relation join.

RELATION_JOIN_IMAGE - Enum constant in enum class io.github.cvc5.Kind

Relation join image.

RELATION_PRODUCT - Enum constant in enum class io.github.cvc5.Kind

Relation cartesian product.

RELATION_PROJECT - Enum constant in enum class io.github.cvc5.Kind

Relation projection operator extends tuple projection operator to sets.

RELATION_TABLE_JOIN - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.Kind

Relation transitive closure.

RELATION_TRANSPOSE - Enum constant in enum class io.github.cvc5.Kind

Relation transpose.

RELATIONS_GROUP_PART - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.SkolemId

Given a group term ((_ rel.group n1 ...

REORDERING - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.UnknownExplanation

Requires another satisfiability check

REQUIRES_FULL_CHECK - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class 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 - Enum constant in enum class io.github.cvc5.RoundingMode

Round to the nearest number away from zero.

ROUND_NEAREST_TIES_TO_EVEN - Enum constant in enum class io.github.cvc5.RoundingMode

Round to the nearest even number.

ROUND_TOWARD_NEGATIVE - Enum constant in enum class io.github.cvc5.RoundingMode

Round towards negative infinity (-oo).

ROUND_TOWARD_POSITIVE - Enum constant in enum class io.github.cvc5.RoundingMode

Round towards positive infinity (SMT-LIB: +oo).

ROUND_TOWARD_ZERO - Enum constant in enum class io.github.cvc5.RoundingMode

Round towards zero.

RoundingMode - Enum Class in io.github.cvc5

Enum representing the set of possible values for RoundingMode.

ROUNDINGMODE_SORT - Enum constant in enum class io.github.cvc5.SortKind

The rounding mode sort.