Index

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

A

ABS - io.github.cvc5.Kind: Absolute value.
ABSTRACT_SORT - io.github.cvc5.SortKind: An abstract sort.
AbstractPlugin - Class in io.github.cvc5
AbstractPlugin(TermManager) - Constructor for class io.github.cvc5.AbstractPlugin: Create plugin instance.
ACI_NORM - io.github.cvc5.ProofRule: Builtin theory – associative/commutative/idempotency/identity normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{expr::isACNorm(t, s)} = \top$.
ADD - io.github.cvc5.Kind: Arithmetic addition.
addAnyConstant(Term) - Method in class io.github.cvc5.Grammar: Allow ntSymbol to be an arbitrary constant.
addAnyVariable(Term) - Method in class io.github.cvc5.Grammar: Allow ntSymbol to be any input variable to corresponding synth-fun or synth-inv with the same sort as ntSymbol.
addConstructor(DatatypeConstructorDecl) - Method in class io.github.cvc5.DatatypeDecl: Add datatype constructor declaration.
addPlugin(AbstractPlugin) - Method in class io.github.cvc5.Solver: Add plugin to this solver.
addRule(Term, Term) - Method in class io.github.cvc5.Grammar: Add rule to the set of rules corresponding to ntSymbol.
addRules(long, long, long[]) - Method in class io.github.cvc5.Grammar
addRules(Term, Term[]) - Method in class io.github.cvc5.Grammar: Add rules to the set of rules corresponding to ntSymbol.
addSelector(String, Sort) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration.
addSelectorSelf(String) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration whose codomain type is the datatype itself.
addSelectorUnresolved(String, String) - Method in class io.github.cvc5.DatatypeConstructorDecl: Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.
addSygusAssume(Term) - Method in class io.github.cvc5.Solver: Add a forumla to the set of Sygus assumptions.
addSygusConstraint(Term) - Method in class io.github.cvc5.Solver: Add a forumla to the set of Sygus constraints.
addSygusInvConstraint(Term, Term, Term, Term) - Method in class io.github.cvc5.Solver: Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.
ALETHE - io.github.cvc5.modes.ProofFormat: Output Alethe proof.
ALETHE_RULE - io.github.cvc5.ProofRule: External – Alethe Place holder for Alethe rules.
ALPHA_EQUIV - io.github.cvc5.ProofRule: Quantifiers – Alpha equivalence \[ \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} \] Notice that this rule is correct only when $z_1,\dots,z_n$ are not contained in $FV(F) \setminus \{ y_1,\dots, y_n \}$, where $FV(\varphi)$ are the free variables of $\varphi$.
AND - io.github.cvc5.Kind: Logical conjunction.
AND_ELIM - io.github.cvc5.ProofRule: Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
AND_INTRO - io.github.cvc5.ProofRule: Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
andTerm(Term) - Method in class io.github.cvc5.Term: Boolean and.
ANNOTATION - io.github.cvc5.ProofRule: Builtin theory – Annotation \[ \inferrule{F \mid a_1 \dots a_n}{F} \] The terms $a_1 \dots a_n$ can be anything used to annotate the proof node, one example is where $a_1$ is a theory.InferenceId.
appendIncrementalStringInput(String) - Method in class io.github.cvc5.InputParser: Append string to the input being parsed by this parser.
apply(Term[]) - Method in interface io.github.cvc5.IOracle
APPLY_CONSTRUCTOR - io.github.cvc5.Kind: Datatype constructor application.
APPLY_SELECTOR - io.github.cvc5.Kind: Datatype selector application.
APPLY_TESTER - io.github.cvc5.Kind: Datatype tester application.
APPLY_UF - io.github.cvc5.Kind: Application of an uninterpreted function.
APPLY_UPDATER - io.github.cvc5.Kind: Datatype update application.
ARCCOSECANT - io.github.cvc5.Kind: Arc cosecant function.
ARCCOSINE - io.github.cvc5.Kind: Arc cosine function.
ARCCOTANGENT - io.github.cvc5.Kind: Arc cotangent function.
ARCSECANT - io.github.cvc5.Kind: Arc secant function.
ARCSINE - io.github.cvc5.Kind: Arc sine function.
ARCTANGENT - io.github.cvc5.Kind: Arc tangent function.
ARITH_ABS_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-abs-elim
ARITH_DIV_BY_CONST_ELIM - io.github.cvc5.ProofRewriteRule: Arith – Division by constant elimination \[ t / c = t * 1/c \] where $c$ is a constant.
ARITH_DIV_ELIM_TO_REAL1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-div-elim-to-real1
ARITH_DIV_ELIM_TO_REAL2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-div-elim-to-real2
ARITH_DIV_TOTAL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-div-total
ARITH_ELIM_GT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-gt
ARITH_ELIM_INT_GT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-int-gt
ARITH_ELIM_INT_LT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-int-lt
ARITH_ELIM_LEQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-leq
ARITH_ELIM_LT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-lt
ARITH_ELIM_MINUS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-minus
ARITH_ELIM_UMINUS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-elim-uminus
ARITH_GEQ_NORM1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-geq-norm1
ARITH_GEQ_NORM2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-geq-norm2
ARITH_GEQ_TIGHTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-geq-tighten
ARITH_INT_DIV_TOTAL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-div-total
ARITH_INT_DIV_TOTAL_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-div-total-one
ARITH_INT_DIV_TOTAL_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-div-total-zero
ARITH_INT_EQ_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-eq-elim
ARITH_INT_MOD_TOTAL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-mod-total
ARITH_INT_MOD_TOTAL_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-mod-total-one
ARITH_INT_MOD_TOTAL_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-int-mod-total-zero
ARITH_LEQ_NORM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-leq-norm
ARITH_MUL_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-mul-one
ARITH_MUL_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-mul-zero
ARITH_MULT_DIST - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-mult-dist
ARITH_MULT_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-mult-flatten
ARITH_MULT_NEG - io.github.cvc5.ProofRule: Arithmetic – Multiplication with negative factor \[ \inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r} \] where $\diamond$ is a relation symbol and $\diamond_{inv}$ the inverted relation symbol.
ARITH_MULT_POS - io.github.cvc5.ProofRule: Arithmetic – Multiplication with positive factor \[ \inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r} \] where $\diamond$ is a relation symbol.
ARITH_MULT_SIGN - io.github.cvc5.ProofRule: Arithmetic – Sign inference \[ \inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0} \] where $f_1 \dots f_k$ are variables compared to zero (less, greater or not equal), $m$ is a monomial from these variables and $\diamond$ is the comparison (less or equal) that results from the signs of the variables.
ARITH_MULT_TANGENT - io.github.cvc5.ProofRule: Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid x, y, a, b, \sigma}{(t \leq tplane) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = -1$} \inferruleSC{- \mid x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$} \] where $x,y$ are real terms (variables or extended terms), $t = x \cdot y$, $a,b$ are real constants, $\sigma \in \{ 1, -1\}$ and $tplane := b \cdot x + a \cdot y - a \cdot b$ is the tangent plane of $x \cdot y$ at $(a,b)$.
ARITH_NEG_NEG_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-neg-neg-one
ARITH_OP_ELIM_AXIOM - io.github.cvc5.ProofRule: Arithmetic – Operator elimination \[ \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}} \]
ARITH_PLUS_CANCEL1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-plus-cancel1
ARITH_PLUS_CANCEL2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-plus-cancel2
ARITH_PLUS_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-plus-flatten
ARITH_PLUS_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-plus-zero
ARITH_POLY_NORM - io.github.cvc5.ProofRule: Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where $\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top$.
ARITH_POLY_NORM_REL - io.github.cvc5.ProofRule: Arithmetic – Polynomial normalization for relations ..
ARITH_REAL_EQ_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-real-eq-elim
ARITH_REFL_GEQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-refl-geq
ARITH_REFL_GT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-refl-gt
ARITH_REFL_LEQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-refl-leq
ARITH_REFL_LT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-refl-lt
ARITH_STRING_PRED_ENTAIL - io.github.cvc5.ProofRewriteRule: Arithmetic - strings predicate entailment \[ (>= n 0) = true \] Where $n$ can be shown to be greater than or equal to $0$ by reasoning about string length being positive and basic properties of addition and multiplication.
ARITH_STRING_PRED_SAFE_APPROX - io.github.cvc5.ProofRewriteRule: Arithmetic - strings predicate entailment \[ (>= n 0) = (>= m 0) \] Where $m$ is a safe under-approximation of $n$, namely we have that $(>= n m)$ and $(>= m 0)$.
ARITH_SUM_UB - io.github.cvc5.ProofRule: Arithmetic – Sum upper bounds \[ \inferrule{P_1 \dots P_n \mid -}{L \diamond R} \] where $P_i$ has the form $L_i \diamond_i R_i$ and $\diamond_i \in \{<, \leq, =\}$.
ARITH_TO_INT_ELIM_TO_REAL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-to-int-elim-to-real
ARITH_TO_REAL_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule arith-to-real-elim
ARITH_TRANS_EXP_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp is approximated from above for negative values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$.
ARITH_TRANS_EXP_APPROX_ABOVE_POS - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp is approximated from above for positive values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term and $l,u$ are lower and upper bounds on $t$.
ARITH_TRANS_EXP_APPROX_BELOW - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp is approximated from below \[ \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)} \] where $d$ is an odd positive number, $t$ an arithmetic term and $\texttt{maclaurin}(\exp, d, c)$ is the $d$'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at $c$.
ARITH_TRANS_EXP_NEG - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
ARITH_TRANS_EXP_POSITIVITY - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
ARITH_TRANS_EXP_SUPER_LIN - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
ARITH_TRANS_EXP_ZERO - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
ARITH_TRANS_PI - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Assert bounds on Pi \[ \inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u} \] where $l,u$ are valid lower and upper bounds on $\pi$.
ARITH_TRANS_SINE_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is approximated from above for negative values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$.
ARITH_TRANS_SINE_APPROX_ABOVE_POS - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is approximated from above for positive values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$).
ARITH_TRANS_SINE_APPROX_BELOW_NEG - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is approximated from below for negative values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)} \] where $d$ is an even positive number, $t$ an arithmetic term, $c$ an arithmetic constant and $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$).
ARITH_TRANS_SINE_APPROX_BELOW_POS - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is approximated from below for positive values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)} \] where $d$ is an even positive number, $t$ an arithmetic term, $lb,ub$ are symbolic lower and upper bounds on $t$ (possibly containing $\pi$) and $l,u$ the evaluated lower and upper bounds on $t$.
ARITH_TRANS_SINE_BOUNDS - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
ARITH_TRANS_SINE_SHIFT - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is shifted to -pi...pi \[ \inferrule{- \mid x}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})} \] where $x$ is the argument to sine, $y$ is a new real skolem that is $x$ shifted into $-\pi \dots \pi$ and $s$ is a new integer skolem that is the number of phases $y$ is shifted.
ARITH_TRANS_SINE_SYMMETRY - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
ARITH_TRANS_SINE_TANGENT_PI - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..
ARITH_TRANS_SINE_TANGENT_ZERO - io.github.cvc5.ProofRule: Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..
ARITH_TRICHOTOMY - io.github.cvc5.ProofRule: Arithmetic – Trichotomy of the reals \[ \inferrule{A, B \mid -}{C} \] where $\neg A, \neg B, C$ are $x < c, x = c, x > c$ in some order.
ARRAY_DEQ_DIFF - io.github.cvc5.SkolemId: The array diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (select A k) (select B k)))).
ARRAY_READ_OVER_WRITE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule array-read-over-write
ARRAY_READ_OVER_WRITE2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule array-read-over-write2
ARRAY_SORT - io.github.cvc5.SortKind: An array sort, whose argument sorts are the index and element sorts of the array.
ARRAY_STORE_OVERWRITE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule array-store-overwrite
ARRAY_STORE_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule array-store-self
ARRAYS_EQ_RANGE_EXPAND - io.github.cvc5.ProofRewriteRule: Arrays – Expansion of array range equality \[ \mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x) \]
ARRAYS_EXT - io.github.cvc5.ProofRule: Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where $k$ is the $\texttt{ARRAY_DEQ_DIFF}$ skolem for `(a, b)`.
ARRAYS_READ_OVER_WRITE - io.github.cvc5.ProofRule: Arrays – Read over write \[ \inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)} \]
ARRAYS_READ_OVER_WRITE_1 - io.github.cvc5.ProofRule: Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
ARRAYS_READ_OVER_WRITE_CONTRA - io.github.cvc5.ProofRule: Arrays – Read over write, contrapositive \[ \inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2} \]
assertFormula(Term) - Method in class io.github.cvc5.Solver: Assert a formula.
ASSUME - io.github.cvc5.ProofRule: Assumption (a leaf) \[ \inferrule{- \mid F}{F} \] This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified.

B

BAG_CARD - io.github.cvc5.Kind: Bag cardinality.
BAG_CHOOSE - io.github.cvc5.Kind: Bag choose.
BAG_COUNT - io.github.cvc5.Kind: Bag element multiplicity.
BAG_DIFFERENCE_REMOVE - io.github.cvc5.Kind: Bag difference remove.
BAG_DIFFERENCE_SUBTRACT - io.github.cvc5.Kind: Bag difference subtract.
BAG_EMPTY - io.github.cvc5.Kind: Empty bag.
BAG_FILTER - io.github.cvc5.Kind: Bag filter.
BAG_FOLD - io.github.cvc5.Kind: Bag fold.
BAG_INTER_MIN - io.github.cvc5.Kind: Bag intersection (min).
BAG_MAKE - io.github.cvc5.Kind: Bag make.
BAG_MAP - io.github.cvc5.Kind: Bag map.
BAG_MEMBER - io.github.cvc5.Kind: Bag membership predicate.
BAG_PARTITION - io.github.cvc5.Kind: Bag partition.
BAG_SETOF - io.github.cvc5.Kind: Bag setof.
BAG_SORT - io.github.cvc5.SortKind: A bag sort, whose argument sort is the element sort of the bag.
BAG_SUBBAG - io.github.cvc5.Kind: Bag inclusion predicate.
BAG_UNION_DISJOINT - io.github.cvc5.Kind: Bag disjoint union (sum).
BAG_UNION_MAX - io.github.cvc5.Kind: Bag max union.
BAGS_CARD_COMBINE - io.github.cvc5.SkolemId: An uninterpreted function for bag.card operator: To compute (bag.card A), we need a function that counts multiplicities of distinct elements.
BAGS_CHOOSE - io.github.cvc5.SkolemId: An interpreted function uf for bag.choose operator: (bag.choose A) is replaced by (uf A) along with the inference that (>= (bag.count (uf A) A) 1) when A is non-empty.
BAGS_DEQ_DIFF - io.github.cvc5.SkolemId: The bag diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (bag.count k A) (bag.count k B)))).
BAGS_DISTINCT_ELEMENTS - io.github.cvc5.SkolemId: An uninterpreted function for distinct elements of a bag A, which returns the n^th distinct element of the bag.
BAGS_DISTINCT_ELEMENTS_SIZE - io.github.cvc5.SkolemId: A skolem variable for the size of the distinct elements of a bag A.
BAGS_DISTINCT_ELEMENTS_UNION_DISJOINT - io.github.cvc5.SkolemId: An uninterpreted function for the union of distinct elements in a bag (Bag T).
BAGS_FOLD_CARD - io.github.cvc5.SkolemId: An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need to guess the cardinality n of bag A using a skolem function with BAGS_FOLD_CARD id.
BAGS_FOLD_COMBINE - io.github.cvc5.SkolemId: An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function that accumulates intermidiate values.
BAGS_FOLD_ELEMENTS - io.github.cvc5.SkolemId: An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function for elements of A.
BAGS_FOLD_UNION_DISJOINT - io.github.cvc5.SkolemId: An uninterpreted function for bag.fold operator: To compute (bag.fold f t A), we need a function for elements of A which is given by elements defined in BAGS_FOLD_ELEMENTS.
BAGS_MAP_INDEX - io.github.cvc5.SkolemId: A skolem variable for the index that is unique per terms (bag.map f A), y, e where: f: (-> E T), A: (Bag E), y: T, e: E Number of skolem indices: 5 1: a map term of the form (bag.map f A).
BAGS_MAP_PREIMAGE_INJECTIVE - io.github.cvc5.SkolemId: A skolem for the preimage of an element y in (bag.map f A) such that (= (f x) y) where f: (-> E T) is an injective function.
BAGS_MAP_SUM - io.github.cvc5.SkolemId: An uninterpreted function for bag.map operator: If bag A is {uf(1), ..., uf(n)} (see BAGS_DISTINCT_ELEMENTS}, then the multiplicity of an element y in a bag (bag.map f A) is sum(n), where sum: (-> Int Int) is a skolem function such that: sum(0) = 0 sum(i) = sum (i-1) + (bag.count (uf i) A) Number of skolem indices: 3 1: the function f of type (-> E T).
BaseInfo() - Constructor for class io.github.cvc5.OptionInfo.BaseInfo
BETA_REDUCE - io.github.cvc5.ProofRewriteRule: Equality – Beta reduction \[ ((\lambda x_1 \ldots x_n.\> t) \ t_1 \ldots t_n) = t\{x_1 \mapsto t_1, \ldots, x_n \mapsto t_n\} \] The right hand side of the equality in the conclusion is computed using standard substitution via Node.substitute.
BITVECTOR_ADD - io.github.cvc5.Kind: Addition of two or more bit-vectors.
BITVECTOR_AND - io.github.cvc5.Kind: Bit-wise and.
BITVECTOR_ASHR - io.github.cvc5.Kind: Bit-vector arithmetic shift right.
BITVECTOR_BIT - io.github.cvc5.Kind: Retrieves the bit at the given index from a bit-vector as a Bool term.
BITVECTOR_COMP - io.github.cvc5.Kind: Equality comparison (returns bit-vector of size 1).
BITVECTOR_CONCAT - io.github.cvc5.Kind: Concatenation of two or more bit-vectors.
BITVECTOR_EXTRACT - io.github.cvc5.Kind: Bit-vector extract.
BITVECTOR_FROM_BOOLS - io.github.cvc5.Kind: Converts a list of Bool terms to a bit-vector.
BITVECTOR_ITE - io.github.cvc5.Kind: Bit-vector if-then-else.
BITVECTOR_LSHR - io.github.cvc5.Kind: Bit-vector logical shift right.
BITVECTOR_MULT - io.github.cvc5.Kind: Multiplication of two or more bit-vectors.
BITVECTOR_NAND - io.github.cvc5.Kind: Bit-wise nand.
BITVECTOR_NEG - io.github.cvc5.Kind: Negation of a bit-vector (two's complement).
BITVECTOR_NEGO - io.github.cvc5.Kind: Bit-vector negation overflow detection.
BITVECTOR_NOR - io.github.cvc5.Kind: Bit-wise nor.
BITVECTOR_NOT - io.github.cvc5.Kind: Bit-wise negation.
BITVECTOR_OR - io.github.cvc5.Kind: Bit-wise or.
BITVECTOR_REDAND - io.github.cvc5.Kind: Bit-vector redand.
BITVECTOR_REDOR - io.github.cvc5.Kind: Bit-vector redor.
BITVECTOR_REPEAT - io.github.cvc5.Kind: Bit-vector repeat.
BITVECTOR_ROTATE_LEFT - io.github.cvc5.Kind: Bit-vector rotate left.
BITVECTOR_ROTATE_RIGHT - io.github.cvc5.Kind: Bit-vector rotate right.
BITVECTOR_SADDO - io.github.cvc5.Kind: Bit-vector signed addition overflow detection.
BITVECTOR_SDIV - io.github.cvc5.Kind: Signed bit-vector division.
BITVECTOR_SDIVO - io.github.cvc5.Kind: Bit-vector signed division overflow detection.
BITVECTOR_SGE - io.github.cvc5.Kind: Bit-vector signed greater than or equal.
BITVECTOR_SGT - io.github.cvc5.Kind: Bit-vector signed greater than.
BITVECTOR_SHL - io.github.cvc5.Kind: Bit-vector shift left.
BITVECTOR_SIGN_EXTEND - io.github.cvc5.Kind: Bit-vector sign extension.
BITVECTOR_SLE - io.github.cvc5.Kind: Bit-vector signed less than or equal.
BITVECTOR_SLT - io.github.cvc5.Kind: Bit-vector signed less than.
BITVECTOR_SLTBV - io.github.cvc5.Kind: Bit-vector signed less than returning a bit-vector of size 1.
BITVECTOR_SMOD - io.github.cvc5.Kind: Signed bit-vector remainder (sign follows divisor).
BITVECTOR_SMULO - io.github.cvc5.Kind: Bit-vector signed multiplication overflow detection.
BITVECTOR_SORT - io.github.cvc5.SortKind: A bit-vector sort, parameterized by an integer denoting its bit-width.
BITVECTOR_SREM - io.github.cvc5.Kind: Signed bit-vector remainder (sign follows dividend).
BITVECTOR_SSUBO - io.github.cvc5.Kind: Bit-vector signed subtraction overflow detection.
BITVECTOR_SUB - io.github.cvc5.Kind: Subtraction of two bit-vectors.
BITVECTOR_TO_NAT - io.github.cvc5.Kind: Bit-vector conversion to (non-negative) integer.
BITVECTOR_UADDO - io.github.cvc5.Kind: Bit-vector unsigned addition overflow detection.
BITVECTOR_UDIV - io.github.cvc5.Kind: Unsigned bit-vector division.
BITVECTOR_UGE - io.github.cvc5.Kind: Bit-vector unsigned greater than or equal.
BITVECTOR_UGT - io.github.cvc5.Kind: Bit-vector unsigned greater than.
BITVECTOR_ULE - io.github.cvc5.Kind: Bit-vector unsigned less than or equal.
BITVECTOR_ULT - io.github.cvc5.Kind: Bit-vector unsigned less than.
BITVECTOR_ULTBV - io.github.cvc5.Kind: Bit-vector unsigned less than returning a bit-vector of size 1.
BITVECTOR_UMULO - io.github.cvc5.Kind: Bit-vector unsigned multiplication overflow detection.
BITVECTOR_UREM - io.github.cvc5.Kind: Unsigned bit-vector remainder.
BITVECTOR_USUBO - io.github.cvc5.Kind: Bit-vector unsigned subtraction overflow detection.
BITVECTOR_XNOR - io.github.cvc5.Kind: Bit-wise xnor, left associative.
BITVECTOR_XOR - io.github.cvc5.Kind: Bit-wise xor.
BITVECTOR_ZERO_EXTEND - io.github.cvc5.Kind: Bit-vector zero extension.
blockModel(BlockModelsMode) - Method in class io.github.cvc5.Solver: Block the current model.
BlockModelsMode - Enum in io.github.cvc5.modes
blockModelValues(Term[]) - Method in class io.github.cvc5.Solver: Block the current model values of (at least) the values in terms.
BOOL_AND_CONF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-conf
BOOL_AND_DE_MORGAN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-de-morgan
BOOL_AND_DUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-dup
BOOL_AND_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-false
BOOL_AND_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-flatten
BOOL_AND_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-and-true
BOOL_DOUBLE_NOT_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-double-not-elim
BOOL_EQ_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-eq-false
BOOL_EQ_NREFL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-eq-nrefl
BOOL_EQ_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-eq-true
BOOL_IMPL_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-impl-elim
BOOL_IMPL_FALSE1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-impl-false1
BOOL_IMPL_FALSE2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-impl-false2
BOOL_IMPL_TRUE1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-impl-true1
BOOL_IMPL_TRUE2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-impl-true2
BOOL_IMPLIES_DE_MORGAN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-implies-de-morgan
BOOL_NOT_EQ_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-not-eq-elim
BOOL_NOT_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-not-false
BOOL_NOT_ITE_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-not-ite-elim
BOOL_NOT_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-not-true
BOOL_NOT_XOR_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-not-xor-elim
BOOL_OR_DE_MORGAN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-de-morgan
BOOL_OR_DUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-dup
BOOL_OR_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-false
BOOL_OR_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-flatten
BOOL_OR_TAUT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-taut
BOOL_OR_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-or-true
BOOL_XOR_COMM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-comm
BOOL_XOR_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-elim
BOOL_XOR_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-false
BOOL_XOR_NREFL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-nrefl
BOOL_XOR_REFL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-refl
BOOL_XOR_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule boolean-xor-true
BOOLEAN_SORT - io.github.cvc5.SortKind: The Boolean sort.
booleanValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a Boolean.
BV_ADD_COMBINE_LIKE_TERMS - io.github.cvc5.ProofRewriteRule: Bitvectors - Combine like terms during addition by counting terms
BV_ADD_TWO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-add-two
BV_ADD_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-add-zero
BV_AND_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-concat-pullup
BV_AND_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-flatten
BV_AND_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-one
BV_AND_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-simplify-1
BV_AND_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-simplify-2
BV_AND_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-and-zero
BV_ASHR_BY_CONST_0 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ashr-by--0
BV_ASHR_BY_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ashr-by--1
BV_ASHR_BY_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ashr-by--2
BV_ASHR_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ashr-zero
BV_BITBLAST_STEP - io.github.cvc5.ProofRule: Bit-vectors – Bitblast bit-vector constant, variable, and terms For constant and variables: \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] For terms: \[ \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)} \] where $t$ is $k(t_1,\dots,t_n)$.
BV_BITWISE_IDEMP_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-bitwise-idemp-1
BV_BITWISE_IDEMP_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-bitwise-idemp-2
BV_BITWISE_NOT_AND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-bitwise-not-and
BV_BITWISE_NOT_OR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-bitwise-not-or
BV_BITWISE_SLICING - io.github.cvc5.ProofRewriteRule: Bitvectors - Extract continuous substrings of bitvectors \[ bvand(a,\ c) = concat(bvand(a[i_0:j_0],\ c_0) ...
BV_COMMUTATIVE_ADD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-commutative-add
BV_COMMUTATIVE_AND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-commutative-and
BV_COMMUTATIVE_MUL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-commutative-mul
BV_COMMUTATIVE_OR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-commutative-or
BV_COMMUTATIVE_XOR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-commutative-xor
BV_COMP_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-comp-eliminate
BV_CONCAT_EXTRACT_MERGE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-concat-extract-merge
BV_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-concat-flatten
BV_CONCAT_MERGE_CONST - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-concat-merge-
BV_CONCAT_TO_MULT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-concat-to-mult
BV_EAGER_ATOM - io.github.cvc5.ProofRule: Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where $F$ is of kind BITVECTOR_EAGER_ATOM.
BV_EMPTY - io.github.cvc5.SkolemId: The empty bitvector.
BV_EXTRACT_BITWISE_AND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-bitwise-and
BV_EXTRACT_BITWISE_OR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-bitwise-or
BV_EXTRACT_BITWISE_XOR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-bitwise-xor
BV_EXTRACT_CONCAT_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-concat-1
BV_EXTRACT_CONCAT_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-concat-2
BV_EXTRACT_CONCAT_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-concat-3
BV_EXTRACT_CONCAT_4 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-concat-4
BV_EXTRACT_EXTRACT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-extract
BV_EXTRACT_MULT_LEADING_BIT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-mult-leading-bit
BV_EXTRACT_NOT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-not
BV_EXTRACT_SIGN_EXTEND_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-sign-extend-1
BV_EXTRACT_SIGN_EXTEND_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-sign-extend-2
BV_EXTRACT_SIGN_EXTEND_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-sign-extend-3
BV_EXTRACT_WHOLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-extract-whole
BV_ITE_CONST_CHILDREN_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite--children-1
BV_ITE_CONST_CHILDREN_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite--children-2
BV_ITE_EQUAL_CHILDREN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-equal-children
BV_ITE_EQUAL_COND_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-equal-cond-1
BV_ITE_EQUAL_COND_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-equal-cond-2
BV_ITE_EQUAL_COND_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-equal-cond-3
BV_ITE_MERGE_ELSE_ELSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-merge-else-else
BV_ITE_MERGE_ELSE_IF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-merge-else-if
BV_ITE_MERGE_THEN_ELSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-merge-then-else
BV_ITE_MERGE_THEN_IF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ite-merge-then-if
BV_LSHR_BY_CONST_0 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-lshr-by--0
BV_LSHR_BY_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-lshr-by--1
BV_LSHR_BY_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-lshr-by--2
BV_LSHR_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-lshr-zero
BV_LT_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-lt-self
BV_MERGE_SIGN_EXTEND_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-merge-sign-extend-1
BV_MERGE_SIGN_EXTEND_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-merge-sign-extend-2
BV_MERGE_SIGN_EXTEND_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-merge-sign-extend-3
BV_MUL_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mul-flatten
BV_MUL_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mul-one
BV_MUL_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mul-zero
BV_MULT_DISTRIB_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-distrib-1
BV_MULT_DISTRIB_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-distrib-2
BV_MULT_DISTRIB_CONST_ADD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-distrib--add
BV_MULT_DISTRIB_CONST_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-distrib--neg
BV_MULT_DISTRIB_CONST_SUB - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-distrib--sub
BV_MULT_POW2_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-pow2-1
BV_MULT_POW2_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-pow2-2
BV_MULT_POW2_2B - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-pow2-2b
BV_MULT_SIMPLIFY - io.github.cvc5.ProofRewriteRule: Bitvectors - Extract negations from multiplicands \[ bvmul(bvneg(a),\ b,\ c) = bvneg(bvmul(a,\ b,\ c)) \]
BV_MULT_SLT_MULT_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-slt-mult-1
BV_MULT_SLT_MULT_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-mult-slt-mult-2
BV_NAND_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-nand-eliminate
BV_NEG_ADD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-neg-add
BV_NEG_IDEMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-neg-idemp
BV_NEG_MULT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-neg-mult
BV_NEG_SUB - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-neg-sub
BV_NOR_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-nor-eliminate
BV_NOT_IDEMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-idemp
BV_NOT_NEQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-neq
BV_NOT_SLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-sle
BV_NOT_ULE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-ule
BV_NOT_ULT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-ult
BV_NOT_XOR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-not-xor
BV_OR_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-concat-pullup
BV_OR_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-flatten
BV_OR_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-one
BV_OR_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-simplify-1
BV_OR_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-simplify-2
BV_OR_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-or-zero
BV_REDAND_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-redand-eliminate
BV_REDOR_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-redor-eliminate
BV_REPEAT_ELIMINATE_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-repeat-eliminate-1
BV_REPEAT_ELIMINATE_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-repeat-eliminate-2
BV_ROTATE_LEFT_ELIMINATE_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-rotate-left-eliminate-1
BV_ROTATE_LEFT_ELIMINATE_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-rotate-left-eliminate-2
BV_ROTATE_RIGHT_ELIMINATE_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-rotate-right-eliminate-1
BV_ROTATE_RIGHT_ELIMINATE_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-rotate-right-eliminate-2
BV_SADDO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-saddo-eliminate
BV_SDIV_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sdiv-eliminate
BV_SDIV_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sdiv-eliminate-fewer-bitwise-ops
BV_SDIVO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sdivo-eliminate
BV_SGE_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sge-eliminate
BV_SGT_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sgt-eliminate
BV_SHL_BY_CONST_0 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-shl-by--0
BV_SHL_BY_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-shl-by--1
BV_SHL_BY_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-shl-by--2
BV_SHL_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-shl-zero
BV_SIGN_EXTEND_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-eliminate
BV_SIGN_EXTEND_ELIMINATE_0 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-eliminate-0
BV_SIGN_EXTEND_EQ_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-eq--1
BV_SIGN_EXTEND_EQ_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-eq--2
BV_SIGN_EXTEND_ULT_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-ult--1
BV_SIGN_EXTEND_ULT_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-ult--2
BV_SIGN_EXTEND_ULT_CONST_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-ult--3
BV_SIGN_EXTEND_ULT_CONST_4 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sign-extend-ult--4
BV_SLE_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sle-eliminate
BV_SLE_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sle-self
BV_SLT_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-slt-eliminate
BV_SLT_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-slt-zero
BV_SMOD_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-smod-eliminate
BV_SMOD_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-smod-eliminate-fewer-bitwise-ops
BV_SMULO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Bitvectors - Unsigned multiplication overflow detection elimination See M.Gok, M.J.
BV_SREM_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-srem-eliminate
BV_SREM_ELIMINATE_FEWER_BITWISE_OPS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-srem-eliminate-fewer-bitwise-ops
BV_SSUBO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ssubo-eliminate
BV_SUB_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-sub-eliminate
BV_UADDO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-uaddo-eliminate
BV_UDIV_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-udiv-one
BV_UDIV_POW2_NOT_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-udiv-pow2-not-one
BV_UDIV_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-udiv-zero
BV_UGE_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-uge-eliminate
BV_UGT_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ugt-eliminate
BV_UGT_UREM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ugt-urem
BV_ULE_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ule-eliminate
BV_ULE_MAX - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ule-max
BV_ULE_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ule-self
BV_ULE_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ule-zero
BV_ULT_ADD_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-add-one
BV_ULT_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-one
BV_ULT_ONES - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-ones
BV_ULT_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-self
BV_ULT_ZERO_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-zero-1
BV_ULT_ZERO_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-ult-zero-2
BV_UMULO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Bitvectors - Unsigned multiplication overflow detection elimination See M.Gok, M.J.
BV_UREM_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-urem-one
BV_UREM_POW2_NOT_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-urem-pow2-not-one
BV_UREM_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-urem-self
BV_USUBO_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-usubo-eliminate
BV_XNOR_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xnor-eliminate
BV_XOR_CONCAT_PULLUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-concat-pullup
BV_XOR_DUPLICATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-duplicate
BV_XOR_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-flatten
BV_XOR_NOT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-not
BV_XOR_ONES - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-ones
BV_XOR_SIMPLIFY_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-simplify-1
BV_XOR_SIMPLIFY_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-simplify-2
BV_XOR_SIMPLIFY_3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-simplify-3
BV_XOR_ZERO - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-xor-zero
BV_ZERO_EXTEND_ELIMINATE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-eliminate
BV_ZERO_EXTEND_ELIMINATE_0 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-eliminate-0
BV_ZERO_EXTEND_EQ_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-eq--1
BV_ZERO_EXTEND_EQ_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-eq--2
BV_ZERO_EXTEND_ULT_CONST_1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-ult--1
BV_ZERO_EXTEND_ULT_CONST_2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-extend-ult--2
BV_ZERO_ULE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule bv-zero-ule

C

CARDINALITY_CONSTRAINT - io.github.cvc5.Kind: Cardinality constraint on uninterpreted sort.
CHAIN_RESOLUTION - io.github.cvc5.ProofRule: Boolean – N-ary Resolution \[ \inferrule{C_1 \dots C_n \mid (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C} \] where let $C_1 \dots C_n$ be nodes viewed as clauses, as defined above let $C_1 \diamond_{L,pol} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined above let $C_1' = C_1$, for each $i > 1$, let $C_i' = C_{i-1} \diamond_{L_{i-1}, pol_{i-1}} C_i'$ Note the list of polarities and pivots are provided as s-expressions.
check() - Method in class io.github.cvc5.AbstractPlugin: Call to check, return vector of lemmas to add to the SAT solver.
checkSat() - Method in class io.github.cvc5.Solver: Check satisfiability.
checkSatAssuming(Term) - Method in class io.github.cvc5.Solver: Check satisfiability assuming the given formula.
checkSatAssuming(Term[]) - Method in class io.github.cvc5.Solver: Check satisfiability assuming the given formulas.
checkSynth() - Method in class io.github.cvc5.Solver: Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
checkSynthNext() - Method in class io.github.cvc5.Solver: Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
CNF_AND_NEG - io.github.cvc5.ProofRule: Boolean – CNF – And Negative \[ \inferrule{- \mid (F_1 \land \dots \land F_n)}{(F_1 \land \dots \land F_n) \lor \neg F_1 \lor \dots \lor \neg F_n} \]
CNF_AND_POS - io.github.cvc5.ProofRule: Boolean – CNF – And Positive \[ \inferrule{- \mid (F_1 \land \dots \land F_n), i}{\neg (F_1 \land \dots \land F_n) \lor F_i} \]
CNF_EQUIV_NEG1 - io.github.cvc5.ProofRule: Boolean – CNF – Equiv Negative 1 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor F_1 \lor F_2} \]
CNF_EQUIV_NEG2 - io.github.cvc5.ProofRule: Boolean – CNF – Equiv Negative 2 \[ \inferrule{- \mid F_1 = F_2}{(F_1 = F_2) \lor \neg F_1 \lor \neg F_2} \]
CNF_EQUIV_POS1 - io.github.cvc5.ProofRule: Boolean – CNF – Equiv Positive 1 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor \neg F_1 \lor F_2} \]
CNF_EQUIV_POS2 - io.github.cvc5.ProofRule: Boolean – CNF – Equiv Positive 2 \[ \inferrule{- \mid F_1 = F_2}{F_1 \neq F_2 \lor F_1 \lor \neg F_2} \]
CNF_IMPLIES_NEG1 - io.github.cvc5.ProofRule: Boolean – CNF – Implies Negative 1 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor F_1} \]
CNF_IMPLIES_NEG2 - io.github.cvc5.ProofRule: Boolean – CNF – Implies Negative 2 \[ \inferrule{- \mid F_1 \rightarrow F_2}{(F_1 \rightarrow F_2) \lor \neg F_2} \]
CNF_IMPLIES_POS - io.github.cvc5.ProofRule: Boolean – CNF – Implies Positive \[ \inferrule{- \mid F_1 \rightarrow F_2}{\neg(F_1 \rightarrow F_2) \lor \neg F_1 \lor F_2} \]
CNF_ITE_NEG1 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Negative 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C \lor \neg F_1} \]
CNF_ITE_NEG2 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Negative 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor C \lor \neg F_2} \]
CNF_ITE_NEG3 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Negative 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg F_1 \lor \neg F_2} \]
CNF_ITE_POS1 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Positive 1 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor \neg C \lor F_1} \]
CNF_ITE_POS2 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Positive 2 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor C \lor F_2} \]
CNF_ITE_POS3 - io.github.cvc5.ProofRule: Boolean – CNF – ITE Positive 3 \[ \inferrule{- \mid (\ite{C}{F_1}{F_2})}{\neg(\ite{C}{F_1}{F_2}) \lor F_1 \lor F_2} \]
CNF_OR_NEG - io.github.cvc5.ProofRule: Boolean – CNF – Or Negative \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n), i}{(F_1 \lor \dots \lor F_n) \lor \neg F_i} \]
CNF_OR_POS - io.github.cvc5.ProofRule: Boolean – CNF – Or Positive \[ \inferrule{- \mid (F_1 \lor \dots \lor F_n)}{\neg(F_1 \lor \dots \lor F_n) \lor F_1 \lor \dots \lor F_n} \]
CNF_XOR_NEG1 - io.github.cvc5.ProofRule: Boolean – CNF – XOR Negative 1 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor \neg F_1 \lor F_2} \]
CNF_XOR_NEG2 - io.github.cvc5.ProofRule: Boolean – CNF – XOR Negative 2 \[ \inferrule{- \mid F_1 \xor F_2}{(F_1 \xor F_2) \lor F_1 \lor \neg F_2} \]
CNF_XOR_POS1 - io.github.cvc5.ProofRule: Boolean – CNF – XOR Positive 1 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor F_1 \lor F_2} \]
CNF_XOR_POS2 - io.github.cvc5.ProofRule: Boolean – CNF – XOR Positive 2 \[ \inferrule{- \mid F_1 \xor F_2}{\neg(F_1 \xor F_2) \lor \neg F_1 \lor \neg F_2} \]
Command - Class in io.github.cvc5
compareTo(Sort) - Method in class io.github.cvc5.Sort: Comparison for ordering on sorts.
compareTo(Term) - Method in class io.github.cvc5.Term: Comparison for ordering on terms.
CONCAT_CONFLICT - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation conflict \[ \inferrule{(c_1\cdot t) = (c_2 \cdot s)\mid b}{\bot} \] where $b$ indicates if the direction is reversed, $c_1,\,c_2$ are constants such that $\texttt{Word::splitConstant}(c_1,c_2, \mathit{index},b)$ is null, in other words, neither is a prefix of the other.
CONCAT_CONFLICT_DEQ - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation conflict for disequal characters \[ \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \neq s_1 \mid b}{\bot} \] where $t_1$ and $s_1$ are constants of length one, or otherwise one side of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to that side is the empty sequence.
CONCAT_CPROP - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = t_3\cdot r)} \] where $w_1,\,w_2$ are words, $t_3$ is $\mathit{pre}(w_2,p)$, $p$ is $\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)$, and $r$ is the purification skolem for $\mathit{suf}(t_1,\mathit{len}(w_3))$.
CONCAT_CSPLIT - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)} \] where $r$ is the purification skolem for $\mathit{suf}(t_1,1)$.
CONCAT_EQ - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation equality \[ \inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s} \] where $\cdot$ stands for string concatenation and $b$ indicates if the direction is reversed.
CONCAT_LPROP - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r)} \] where $r$ is the purification Skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$.
CONCAT_SPLIT - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{((t_1 = s_1\cdot r) \vee (s_1 = t_1\cdot r)) \wedge r \neq \epsilon \wedge \mathit{len}(r)>0}{if $b=\bot$} \] where $r$ is the purification skolem for $\mathit{ite}( \mathit{len}(t_1) >= \mathit{len}(s_1), \mathit{suf}(t_1,\mathit{len}(s_1)), \mathit{suf}(s_1,\mathit{len}(t_1)))$ and $\epsilon$ is the empty string (or sequence).
CONCAT_UNIFY - io.github.cvc5.ProofRule: Strings – Core rules – Concatenation unification \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid \bot}{t_1 = s_1} \] Alternatively for the reverse: \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_2) = \mathit{len}(s_2)\mid \top}{t_2 = s_2} \]
CONG - io.github.cvc5.ProofRule: Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?, t_1,\dots, t_n) = k(f?, s_1,\dots, s_n)} \] where $k$ is the application kind.
CONST_ARRAY - io.github.cvc5.Kind: Constant array.
CONST_BITVECTOR - io.github.cvc5.Kind: Fixed-size bit-vector constant.
CONST_BOOLEAN - io.github.cvc5.Kind: Boolean constant.
CONST_FINITE_FIELD - io.github.cvc5.Kind: Finite field constant.
CONST_FLOATINGPOINT - io.github.cvc5.Kind: Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.
CONST_INTEGER - io.github.cvc5.Kind: Arbitrary-precision integer constant.
CONST_RATIONAL - io.github.cvc5.Kind: Arbitrary-precision rational constant.
CONST_ROUNDINGMODE - io.github.cvc5.Kind: RoundingMode constant.
CONST_SEQUENCE - io.github.cvc5.Kind: Constant sequence.
CONST_STRING - io.github.cvc5.Kind: Constant string.
CONSTANT - io.github.cvc5.Kind: Free constant symbol.
CONSTANT_PROP - io.github.cvc5.modes.LearnedLitType: An internal literal that can be made into a constant propagation for an input term.
ConstIterator() - Constructor for class io.github.cvc5.Datatype.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.DatatypeConstructor.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Statistics.ConstIterator
ConstIterator() - Constructor for class io.github.cvc5.Term.ConstIterator
ConstIterator(boolean, boolean) - Constructor for class io.github.cvc5.Statistics.ConstIterator
Context - Class in io.github.cvc5
Context() - Constructor for class io.github.cvc5.Context
CONTRA - io.github.cvc5.ProofRule: Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
COSECANT - io.github.cvc5.Kind: Cosecant function.
COSINE - io.github.cvc5.Kind: Cosine function.
COTANGENT - io.github.cvc5.Kind: Cotangent function.
CPC - io.github.cvc5.modes.ProofFormat: Output Cooperating Proof Calculus proof based on Eunoia signatures.
CVC5ApiException - Exception in io.github.cvc5
CVC5ApiException(String) - Constructor for exception io.github.cvc5.CVC5ApiException
CVC5ApiOptionException - Exception in io.github.cvc5
CVC5ApiOptionException(String) - Constructor for exception io.github.cvc5.CVC5ApiOptionException
CVC5ApiRecoverableException - Exception in io.github.cvc5
CVC5ApiRecoverableException(String) - Constructor for exception io.github.cvc5.CVC5ApiRecoverableException
CVC5ParserException - Exception in io.github.cvc5
CVC5ParserException(String) - Constructor for exception io.github.cvc5.CVC5ParserException

D

Datatype - Class in io.github.cvc5: A cvc5 datatype.
DATATYPE_SORT - io.github.cvc5.SortKind: A datatype sort.
Datatype.ConstIterator - Class in io.github.cvc5
DatatypeConstructor - Class in io.github.cvc5: A cvc5 datatype constructor.
DatatypeConstructor.ConstIterator - Class in io.github.cvc5
DatatypeConstructorDecl - Class in io.github.cvc5: A cvc5 datatype constructor declaration.
DatatypeDecl - Class in io.github.cvc5: A cvc5 datatype declaration.
DatatypeDecl() - Constructor for class io.github.cvc5.DatatypeDecl: Null datatypeDecl
DatatypeSelector - Class in io.github.cvc5: A cvc5 datatype selector.
declareDatatype(String, DatatypeConstructorDecl[]) - Method in class io.github.cvc5.Solver: Create datatype sort.
declareFun(String, Sort[], Sort) - Method in class io.github.cvc5.Solver: Declare n-ary function symbol.
declareFun(String, Sort[], Sort, boolean) - Method in class io.github.cvc5.Solver: Declare n-ary function symbol.
declareOracleFun(String, Sort[], Sort, IOracle) - Method in class io.github.cvc5.Solver: Declare an oracle function with reference to an implementation.
declarePool(String, Sort, Term[]) - Method in class io.github.cvc5.Solver: Declare a symbolic pool of terms with the given initial value.
declareSepHeap(Sort, Sort) - Method in class io.github.cvc5.Solver: When using separation logic, this sets the location sort and the datatype sort to the given ones.
declareSort(String, int) - Method in class io.github.cvc5.Solver: Declare uninterpreted sort.
declareSort(String, int, boolean) - Method in class io.github.cvc5.Solver: Declare uninterpreted sort.
declareSygusVar(String, Sort) - Method in class io.github.cvc5.Solver: Append symbol to the current list of universal variables.
DEFAULT - io.github.cvc5.modes.ProofFormat: Use the proof format mode set in the solver options.
defineFun(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver: Define n-ary function in the current context.
defineFun(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver: Define n-ary function.
defineFunRec(Term, Term[], Term) - Method in class io.github.cvc5.Solver: Define recursive function in the current context.
defineFunRec(Term, Term[], Term, boolean) - Method in class io.github.cvc5.Solver: Define recursive function.
defineFunRec(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver: Define recursive function in the current context.
defineFunRec(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver: Define recursive function.
defineFunsRec(Term[], Term[][], Term[]) - Method in class io.github.cvc5.Solver: Define recursive functions in the current context.
defineFunsRec(Term[], Term[][], Term[], boolean) - Method in class io.github.cvc5.Solver: Define recursive functions.
deletePointer() - Method in class io.github.cvc5.Proof
deletePointer(long) - Method in class io.github.cvc5.Command
deletePointer(long) - Method in class io.github.cvc5.Datatype
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructor
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
deletePointer(long) - Method in class io.github.cvc5.DatatypeDecl
deletePointer(long) - Method in class io.github.cvc5.DatatypeSelector
deletePointer(long) - Method in class io.github.cvc5.Grammar
deletePointer(long) - Method in class io.github.cvc5.InputParser
deletePointer(long) - Method in class io.github.cvc5.Op
deletePointer(long) - Method in class io.github.cvc5.OptionInfo
deletePointer(long) - Method in class io.github.cvc5.Proof
deletePointer(long) - Method in class io.github.cvc5.Result
deletePointer(long) - Method in class io.github.cvc5.Solver
deletePointer(long) - Method in class io.github.cvc5.Sort
deletePointer(long) - Method in class io.github.cvc5.Stat
deletePointer(long) - Method in class io.github.cvc5.Statistics
deletePointer(long) - Method in class io.github.cvc5.SymbolManager
deletePointer(long) - Method in class io.github.cvc5.SynthResult
deletePointer(long) - Method in class io.github.cvc5.Term
deletePointer(long) - Method in class io.github.cvc5.TermManager
deletePointers() - Static method in class io.github.cvc5.Context: Delete all cpp pointers for terms, sorts, etc
DISTINCT - io.github.cvc5.Kind: Disequality.
DISTINCT_BINARY_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule distinct-binary-elim
DISTINCT_ELIM - io.github.cvc5.ProofRewriteRule: Builtin – Distinct elimination \[ \texttt{distinct}(t_1, \ldots, tn) = \bigwedge_{i \neq j} t_i \neq t_j \]
DIV_BY_ZERO - io.github.cvc5.SkolemId: The function for division by zero.
DIVISIBLE - io.github.cvc5.Kind: Operator for the divisibility-by-$k$ predicate.
DIVISION - io.github.cvc5.Kind: Real division, division by 0 undefined, left associative.
DIVISION_TOTAL - io.github.cvc5.Kind: Real division, division by 0 defined to be 0, left associative.
done() - Method in class io.github.cvc5.InputParser
DOT - io.github.cvc5.modes.ProofFormat: Output DOT proof.
doubleValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a double.
DRAT_REFUTATION - io.github.cvc5.ProofRule: DRAT Refutation \[ \inferrule{F_1 \dots F_n \mid D, P}{\bot} \] where $F_1 \dots F_n$ correspond to the clauses in the DIMACS file given by filename `D` and `P` is a filename of a file storing a DRAT proof.
DSL_REWRITE - io.github.cvc5.ProofRule: Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where `id` is a ProofRewriteRule whose definition in the RARE DSL is \(\forall x_1 \dots x_n.
DT_CLASH - io.github.cvc5.ProofRule: Datatypes – Clash \[ \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$} \]
DT_COLLAPSE_SELECTOR - io.github.cvc5.ProofRewriteRule: Datatypes - collapse selector \[ s_i(c(t_1, \ldots, t_n)) = t_i \] where $s_i$ is the $i^{th}$ selector for constructor $c$.
DT_COLLAPSE_TESTER - io.github.cvc5.ProofRewriteRule: Datatypes - collapse tester \[ \mathit{is}_c(c(t_1, \ldots, t_n)) = true \] or alternatively \[ \mathit{is}_c(d(t_1, \ldots, t_n)) = false \] where $c$ and $d$ are distinct constructors.
DT_COLLAPSE_TESTER_SINGLETON - io.github.cvc5.ProofRewriteRule: Datatypes - collapse tester \[ \mathit{is}_c(t) = true \] where $c$ is the only constructor of its associated datatype.
DT_CONS_EQ - io.github.cvc5.ProofRewriteRule: Datatypes - constructor equality \[ (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) \] or alternatively \[ (c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false \] where $c$ and $d$ are distinct constructors.
DT_INST - io.github.cvc5.ProofRewriteRule: Datatypes – Instantiation \[ \mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t))) \] where $C$ is the $n^{\mathit{th}}$ constructor of the type of $t$, and $\mathit{is}_C$ is the discriminator (tester) for $C$.
DT_SPLIT - io.github.cvc5.ProofRule: Datatypes – Split \[ \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)} \] where $C_1,\dots,C_n$ are all the constructors of the type of $t$.
DT_UNIF - io.github.cvc5.ProofRule: Datatypes – Unification \[ \inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i} \] where $C$ is a constructor.

E

ENCODE_EQ_INTRO - io.github.cvc5.ProofRule: Builtin theory – Encode equality introduction \[ \inferrule{- \mid t}{t=t'} \] where $t$ and $t'$ are equivalent up to their encoding in an external proof format.
ENUM - io.github.cvc5.modes.FindSynthTarget: Find the next term in the enumeration of the target grammar.
EQ_RANGE - io.github.cvc5.Kind: Equality over arrays $a$ and $b$ over a given range $[i,j]$, i.e., \[ \forall k .
EQ_REFL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule eq-refl
EQ_RESOLVE - io.github.cvc5.ProofRule: Boolean – Equality resolution \[ \inferrule{F_1, (F_1 = F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for EQUIV_ELIM1 <cvc5.ProofRule.EQUIV_ELIM1> + RESOLUTION <cvc5.ProofRule.RESOLUTION>.
EQ_SYMM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule eq-symm
eqTerm(Term) - Method in class io.github.cvc5.Term: Equality.
EQUAL - io.github.cvc5.Kind: Equality, chainable.
equals(Object) - Method in class io.github.cvc5.Datatype: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeConstructor: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeConstructorDecl: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeDecl: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.DatatypeSelector: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Grammar: Referential equality operator.
equals(Object) - Method in class io.github.cvc5.Op: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Pair
equals(Object) - Method in class io.github.cvc5.Proof: Referential equality operator.
equals(Object) - Method in class io.github.cvc5.Result: Operator overloading for equality of two results.
equals(Object) - Method in class io.github.cvc5.Solver
equals(Object) - Method in class io.github.cvc5.Sort: Comparison for structural equality.
equals(Object) - Method in class io.github.cvc5.SymbolManager
equals(Object) - Method in class io.github.cvc5.SynthResult: Operator overloading for equality of two synthesis results.
equals(Object) - Method in class io.github.cvc5.Term: Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.TermManager
equals(Object) - Method in class io.github.cvc5.Triplet
EQUIV_ELIM1 - io.github.cvc5.ProofRule: Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
EQUIV_ELIM2 - io.github.cvc5.ProofRule: Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
EVALUATE - io.github.cvc5.ProofRule: Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{evaluate}(t)} \] where $\texttt{evaluate}$ is implemented by calling the method $\texttt{Evalutor::evaluate}$ in :cvc5src:`theory/evaluator.h` with an empty substitution.
EXISTS - io.github.cvc5.Kind: Existentially quantified formula.
EXISTS_ELIM - io.github.cvc5.ProofRewriteRule: Quantifiers – Exists elimination \[ \exists x_1\dots x_n.\> F = \neg \forall x_1\dots x_n.\> \neg F \]
EXPONENTIAL - io.github.cvc5.Kind: Exponential function.

F

FACTORING - io.github.cvc5.ProofRule: Boolean – Factoring \[ \inferrule{C_1 \mid -}{C_2} \] where $C_2$ is the clause $C_1$, but every occurrence of a literal after its first occurrence is omitted.
FALSE_ELIM - io.github.cvc5.ProofRule: Equality – False elim \[ \inferrule{F=\bot\mid -}{\neg F} \]
FALSE_INTRO - io.github.cvc5.ProofRule: Equality – False intro \[ \inferrule{\neg F\mid -}{F = \bot} \]
findSynth(FindSynthTarget) - Method in class io.github.cvc5.Solver: Find a target term of interest using sygus enumeration, with no provided grammar.
findSynth(FindSynthTarget, Grammar) - Method in class io.github.cvc5.Solver: Find a target term of interest using sygus enumeration with a provided grammar.
findSynthNext() - Method in class io.github.cvc5.Solver: Try to find a next target term of interest using sygus enumeration.
FindSynthTarget - Enum in io.github.cvc5.modes
FINITE_FIELD_ADD - io.github.cvc5.Kind: Addition of two or more finite field elements.
FINITE_FIELD_BITSUM - io.github.cvc5.Kind: Bitsum of two or more finite field elements: x + 2y + 4z + ...
FINITE_FIELD_MULT - io.github.cvc5.Kind: Multiplication of two or more finite field elements.
FINITE_FIELD_NEG - io.github.cvc5.Kind: Negation of a finite field element (additive inverse).
FINITE_FIELD_SORT - io.github.cvc5.SortKind: A finite field sort, parameterized by a size.
first - Variable in class io.github.cvc5.Pair
first - Variable in class io.github.cvc5.Triplet
FLOATINGPOINT_ABS - io.github.cvc5.Kind: Floating-point absolute value.
FLOATINGPOINT_ADD - io.github.cvc5.Kind: Floating-point addition.
FLOATINGPOINT_DIV - io.github.cvc5.Kind: Floating-point division.
FLOATINGPOINT_EQ - io.github.cvc5.Kind: Floating-point equality.
FLOATINGPOINT_FMA - io.github.cvc5.Kind: Floating-point fused multiply and add.
FLOATINGPOINT_FP - io.github.cvc5.Kind: Create floating-point literal from bit-vector triple.
FLOATINGPOINT_GEQ - io.github.cvc5.Kind: Floating-point greater than or equal.
FLOATINGPOINT_GT - io.github.cvc5.Kind: Floating-point greater than.
FLOATINGPOINT_IS_INF - io.github.cvc5.Kind: Floating-point is infinite tester.
FLOATINGPOINT_IS_NAN - io.github.cvc5.Kind: Floating-point is NaN tester.
FLOATINGPOINT_IS_NEG - io.github.cvc5.Kind: Floating-point is negative tester.
FLOATINGPOINT_IS_NORMAL - io.github.cvc5.Kind: Floating-point is normal tester.
FLOATINGPOINT_IS_POS - io.github.cvc5.Kind: Floating-point is positive tester.
FLOATINGPOINT_IS_SUBNORMAL - io.github.cvc5.Kind: Floating-point is sub-normal tester.
FLOATINGPOINT_IS_ZERO - io.github.cvc5.Kind: Floating-point is zero tester.
FLOATINGPOINT_LEQ - io.github.cvc5.Kind: Floating-point less than or equal.
FLOATINGPOINT_LT - io.github.cvc5.Kind: Floating-point less than.
FLOATINGPOINT_MAX - io.github.cvc5.Kind: Floating-point maximum.
FLOATINGPOINT_MIN - io.github.cvc5.Kind: Floating-point minimum.
FLOATINGPOINT_MULT - io.github.cvc5.Kind: Floating-point multiply.
FLOATINGPOINT_NEG - io.github.cvc5.Kind: Floating-point negation.
FLOATINGPOINT_REM - io.github.cvc5.Kind: Floating-point remainder.
FLOATINGPOINT_RTI - io.github.cvc5.Kind: Floating-point round to integral.
FLOATINGPOINT_SORT - io.github.cvc5.SortKind: A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.
FLOATINGPOINT_SQRT - io.github.cvc5.Kind: Floating-point square root.
FLOATINGPOINT_SUB - io.github.cvc5.Kind: Floating-point sutraction.
FLOATINGPOINT_TO_FP_FROM_FP - io.github.cvc5.Kind: Conversion to floating-point from floating-point.
FLOATINGPOINT_TO_FP_FROM_IEEE_BV - io.github.cvc5.Kind: Conversion to floating-point from IEEE-754 bit-vector.
FLOATINGPOINT_TO_FP_FROM_REAL - io.github.cvc5.Kind: Conversion to floating-point from Real.
FLOATINGPOINT_TO_FP_FROM_SBV - io.github.cvc5.Kind: Conversion to floating-point from signed bit-vector.
FLOATINGPOINT_TO_FP_FROM_UBV - io.github.cvc5.Kind: Conversion to floating-point from unsigned bit-vector.
FLOATINGPOINT_TO_REAL - io.github.cvc5.Kind: Conversion to Real from floating-point.
FLOATINGPOINT_TO_SBV - io.github.cvc5.Kind: Conversion to signed bit-vector from floating-point.
FLOATINGPOINT_TO_UBV - io.github.cvc5.Kind: Conversion to unsigned bit-vector from floating-point.
FORALL - io.github.cvc5.Kind: Universally quantified formula.
FP_MAX_ZERO - io.github.cvc5.SkolemId: A skolem function that is unique per floating-point sort, introduced for the undefined zero case of fp.max.
FP_MIN_ZERO - io.github.cvc5.SkolemId: A skolem function that is unique per floating-point sort, introduced for the undefined zero case of fp.min.
FP_TO_REAL - io.github.cvc5.SkolemId: A skolem function introduced for the undefined of fp.to_real that is unique per floating-point sort.
FP_TO_SBV - io.github.cvc5.SkolemId: A skolem function introduced for the undefined out-ouf-bounds case of fp.to_sbv that is unique per floating-point sort and sort of the arguments to the operator.
FP_TO_UBV - io.github.cvc5.SkolemId: A skolem function introduced for the undefined out-ouf-bounds case of fp.to_ubv that is unique per floating-point sort and sort of the arguments to the operator.
fromInt(int) - Static method in enum io.github.cvc5.Kind
fromInt(int) - Static method in enum io.github.cvc5.modes.BlockModelsMode
fromInt(int) - Static method in enum io.github.cvc5.modes.FindSynthTarget
fromInt(int) - Static method in enum io.github.cvc5.modes.InputLanguage
fromInt(int) - Static method in enum io.github.cvc5.modes.LearnedLitType
fromInt(int) - Static method in enum io.github.cvc5.modes.ProofComponent
fromInt(int) - Static method in enum io.github.cvc5.modes.ProofFormat
fromInt(int) - Static method in enum io.github.cvc5.ProofRewriteRule
fromInt(int) - Static method in enum io.github.cvc5.ProofRule
fromInt(int) - Static method in enum io.github.cvc5.RoundingMode
fromInt(int) - Static method in enum io.github.cvc5.SkolemId
fromInt(int) - Static method in enum io.github.cvc5.SortKind
fromInt(int) - Static method in enum io.github.cvc5.UnknownExplanation
FULL - io.github.cvc5.modes.ProofComponent: A proof of false whose free assumptions are a subset of the input formulas F1), ...
FUNCTION_SORT - io.github.cvc5.SortKind: A function sort with given domain sorts and codomain sort.

G

GEQ - io.github.cvc5.Kind: Greater than or equal, chainable.
get(int) - Method in class io.github.cvc5.Op: Get the index at position i.
get(String) - Method in class io.github.cvc5.Statistics: Retrieve the statistic with the given name.
getAbduct(Term) - Method in class io.github.cvc5.Solver: Get an abduct.
getAbduct(Term, Grammar) - Method in class io.github.cvc5.Solver: Get an abduct.
getAbductNext() - Method in class io.github.cvc5.Solver: Get the next abduct.
getAbstractedKind() - Method in class io.github.cvc5.Sort
getAliases() - Method in class io.github.cvc5.OptionInfo
getArguments() - Method in class io.github.cvc5.Proof
getArrayElementSort() - Method in class io.github.cvc5.Sort
getArrayIndexSort() - Method in class io.github.cvc5.Sort
getAssertions() - Method in class io.github.cvc5.Solver: Get the list of asserted formulas.
getBagElementSort() - Method in class io.github.cvc5.Sort
getBaseInfo() - Method in class io.github.cvc5.OptionInfo
getBitVectorSize() - Method in class io.github.cvc5.Sort
getBitVectorValue() - Method in class io.github.cvc5.Term: Asserts isBitVectorValue().
getBitVectorValue(int) - Method in class io.github.cvc5.Term: Get the string representation of a bit-vector value.
getBooleanSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getBooleanSort(). It will be removed in a future release.
getBooleanSort() - Method in class io.github.cvc5.TermManager: Get the Boolean sort.
getBooleanValue() - Method in class io.github.cvc5.Term: Asserts isBooleanValue().
getCardinalityConstraint() - Method in class io.github.cvc5.Term: Asserts isCardinalityConstraint().
getChild(int) - Method in class io.github.cvc5.Term: Get the child term at a given index.
getChildren() - Method in class io.github.cvc5.Proof
getCodomainSort() - Method in class io.github.cvc5.DatatypeSelector
getCommandName() - Method in class io.github.cvc5.Command: Get the name for this command, e.g.
getConstArrayBase() - Method in class io.github.cvc5.Term: Asserts isConstArray().
getConstructor(int) - Method in class io.github.cvc5.Datatype: Get the datatype constructor at a given index.
getConstructor(String) - Method in class io.github.cvc5.Datatype: Get the datatype constructor with the given name.
getCurrentValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
getDatatype() - Method in class io.github.cvc5.Sort
getDatatypeArity() - Method in class io.github.cvc5.Sort
getDatatypeConstructorArity() - Method in class io.github.cvc5.Sort
getDatatypeConstructorCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeConstructorDomainSorts() - Method in class io.github.cvc5.Sort
getDatatypeSelectorCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeSelectorDomainSort() - Method in class io.github.cvc5.Sort
getDatatypeTesterCodomainSort() - Method in class io.github.cvc5.Sort
getDatatypeTesterDomainSort() - Method in class io.github.cvc5.Sort
getDeclaredSorts() - Method in class io.github.cvc5.SymbolManager: Get the list of sorts that have been declared via `declare-sort` commands.
getDeclaredTerms() - Method in class io.github.cvc5.SymbolManager: Get the list of terms that have been declared via `declare-fun` and `declare-const`.
getDefaultValue() - Method in class io.github.cvc5.OptionInfo.ValueInfo
getDifficulty() - Method in class io.github.cvc5.Solver: Get a difficulty estimate for an asserted formula.
getDouble() - Method in class io.github.cvc5.Stat: Return the double value.
getFiniteFieldSize() - Method in class io.github.cvc5.Sort
getFiniteFieldValue() - Method in class io.github.cvc5.Term: Get the string representation of a finite field value.
getFloatingPointExponentSize() - Method in class io.github.cvc5.Sort
getFloatingPointSignificandSize() - Method in class io.github.cvc5.Sort
getFloatingPointValue() - Method in class io.github.cvc5.Term: Asserts isFloatingPointValue().
getFunctionArity() - Method in class io.github.cvc5.Sort
getFunctionCodomainSort() - Method in class io.github.cvc5.Sort
getFunctionDomainSorts() - Method in class io.github.cvc5.Sort
getHistogram() - Method in class io.github.cvc5.Stat: Return the histogram value.
getId() - Method in class io.github.cvc5.Term
getInfo(String) - Method in class io.github.cvc5.Solver: Get info from the solver.
getInstantiatedParameters() - Method in class io.github.cvc5.Sort: Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see Sort.instantiate(Sort[])).
getInstantiatedTerm(Sort) - Method in class io.github.cvc5.DatatypeConstructor: Get the constructor term of this datatype constructor whose return type is retSort.
getInstantiations() - Method in class io.github.cvc5.Solver: Get a string that contains information about all instantiations made by the quantifiers module.
getInt() - Method in class io.github.cvc5.Stat: Return the integer value.
getIntegerSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getIntegerSort(). It will be removed in a future release.
getIntegerSort() - Method in class io.github.cvc5.TermManager: Get the integer sort.
getIntegerSort(long) - Method in class io.github.cvc5.TermManager
getIntegerValue() - Method in class io.github.cvc5.Term: Asserts isIntegerValue().
getInterpolant(Term) - Method in class io.github.cvc5.Solver: Get an interpolant SMT-LIB: ( get-interpolant <conj> ) Requires option produce-interpolants to be set to a mode different from none.
getInterpolant(Term, Grammar) - Method in class io.github.cvc5.Solver: Get an interpolant SMT-LIB: ( get-interpolant <conj> <g> ) Requires option produce-interpolants to be set to a mode different from none.
getInterpolantNext() - Method in class io.github.cvc5.Solver: Get the next interpolant.
getKind() - Method in class io.github.cvc5.Op
getKind() - Method in class io.github.cvc5.Sort
getKind() - Method in class io.github.cvc5.Term
getLearnedLiterals() - Method in class io.github.cvc5.Solver: Get a list of input literals that are entailed by the current set of assertions.
getLearnedLiterals(LearnedLitType) - Method in class io.github.cvc5.Solver: Get a list of literals that are entailed by the current set of assertions.
getLogic() - Method in class io.github.cvc5.Solver: Get the logic set the solver.
getLogic() - Method in class io.github.cvc5.SymbolManager
getMaximum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
getMinimum() - Method in class io.github.cvc5.OptionInfo.NumberInfo
getModel(Sort[], Term[]) - Method in class io.github.cvc5.Solver: Get the model SMT-LIB: ( get-model ) Requires to enable option produce-models.
getModelDomainElements(Sort) - Method in class io.github.cvc5.Solver: Get the domain elements of uninterpreted sort s in the current model.
getModes() - Method in class io.github.cvc5.OptionInfo.ModeInfo
getName() - Method in class io.github.cvc5.AbstractPlugin: Get the name of the plugin (for debugging).
getName() - Method in class io.github.cvc5.Datatype
getName() - Method in class io.github.cvc5.DatatypeConstructor
getName() - Method in class io.github.cvc5.DatatypeDecl
getName() - Method in class io.github.cvc5.DatatypeSelector
getName() - Method in class io.github.cvc5.OptionInfo
getNullableElementSort() - Method in class io.github.cvc5.Sort
getNumChildren() - Method in class io.github.cvc5.Term
getNumConstructors() - Method in class io.github.cvc5.Datatype
getNumConstructors() - Method in class io.github.cvc5.DatatypeDecl: Get the number of constructors (so far) for this Datatype declaration.
getNumIndices() - Method in class io.github.cvc5.Op
getNumIndicesForSkolemId(SkolemId) - Method in class io.github.cvc5.TermManager: Get the number of indices for a given skolem id.
getNumSelectors() - Method in class io.github.cvc5.DatatypeConstructor
getOp() - Method in class io.github.cvc5.Term
getOption(String) - Method in class io.github.cvc5.Solver: Get the value of a given option.
getOptionInfo(String) - Method in class io.github.cvc5.Solver: Get some information about the given option.
getOptionNames() - Method in class io.github.cvc5.Solver: Get all option names that can be used with Solver.setOption(String, String), Solver.getOption(String) and Solver.getOptionInfo(String).
getPairs(Pair<K, ? extends AbstractPointer>[]) - Static method in class io.github.cvc5.Utils
getParameters() - Method in class io.github.cvc5.Datatype
getPointer() - Method in class io.github.cvc5.Proof
getPointers(IPointer[]) - Static method in class io.github.cvc5.Utils
getPointers(IPointer[][]) - Static method in class io.github.cvc5.Utils
getProof() - Method in class io.github.cvc5.Solver: Get refutation proof for the most recent call to checkSat.
getProof(ProofComponent) - Method in class io.github.cvc5.Solver: Get a proof associated with the most recent call to checkSat.
getProofs(long[]) - Static method in class io.github.cvc5.Utils
getQuantifierElimination(Term) - Method in class io.github.cvc5.Solver: Do quantifier elimination.
getQuantifierEliminationDisjunct(Term) - Method in class io.github.cvc5.Solver: Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.
getRational(Pair<BigInteger, BigInteger>) - Static method in class io.github.cvc5.Utils: Convert a pair of BigIntegers to a rational string a/b
getRational(String) - Static method in class io.github.cvc5.Utils: Convert a rational string a/b to a pair of BigIntegers
getRealAlgebraicNumberDefiningPolynomial(Term) - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealAlgebraicNumberLowerBound() - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealAlgebraicNumberUpperBound() - Method in class io.github.cvc5.Term: Asserts isRealAlgebraicNumber().
getRealOrIntegerValueSign() - Method in class io.github.cvc5.Term: Get integer or real value sign.
getRealSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRealSort(). It will be removed in a future release.
getRealSort() - Method in class io.github.cvc5.TermManager: Get the real sort.
getRealValue() - Method in class io.github.cvc5.Term: Asserts isRealValue().
getRegExpSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRegExpSort(). It will be removed in a future release.
getRegExpSort() - Method in class io.github.cvc5.TermManager: Get the regular expression sort.
getResult() - Method in class io.github.cvc5.Proof
getRewriteRule() - Method in class io.github.cvc5.Proof
getRoundingModeSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getRoundingModeSort(). It will be removed in a future release.
getRoundingModeSort() - Method in class io.github.cvc5.TermManager: Get the floating-point rounding mode sort.
getRoundingModeValue() - Method in class io.github.cvc5.Term: Asserts isRoundingModeValue().
getRule() - Method in class io.github.cvc5.Proof
getSelector(int) - Method in class io.github.cvc5.DatatypeConstructor: Get the DatatypeSelector at the given index
getSelector(String) - Method in class io.github.cvc5.Datatype: Get the datatype constructor with the given name.
getSelector(String) - Method in class io.github.cvc5.DatatypeConstructor: Get the datatype selector with the given name.
getSequenceElementSort() - Method in class io.github.cvc5.Sort
getSequenceValue() - Method in class io.github.cvc5.Term: Asserts isSequenceValue().
getSetByUser() - Method in class io.github.cvc5.OptionInfo
getSetElementSort() - Method in class io.github.cvc5.Sort
getSetValue() - Method in class io.github.cvc5.Term: Asserts isSetValue().
getSkolemId() - Method in class io.github.cvc5.Term: Get skolem identifier of this term.
getSkolemIndices() - Method in class io.github.cvc5.Term: Get the skolem indices of this term.
getSolver() - Method in class io.github.cvc5.InputParser
getSort() - Method in class io.github.cvc5.Term
getSorts(long[]) - Static method in class io.github.cvc5.Utils
getStatistics() - Method in class io.github.cvc5.Solver: Get a snapshot of the current state of the statistic values of this solver.
getStatistics() - Method in class io.github.cvc5.TermManager: Get a snapshot of the current state of the statistic values of this term manager.
getString() - Method in class io.github.cvc5.Stat: Return the string value.
getStringSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.getStringSort(). It will be removed in a future release.
getStringSort() - Method in class io.github.cvc5.TermManager: Get the string sort.
getStringValue() - Method in class io.github.cvc5.Term
getSygusAssumptions() - Method in class io.github.cvc5.Solver: Get the list of sygus assumptions.
getSygusConstraints() - Method in class io.github.cvc5.Solver: Get the list of sygus constraints.
getSymbol() - Method in class io.github.cvc5.Sort
getSymbol() - Method in class io.github.cvc5.Term: Asserts hasSymbol().
getSymbolManager() - Method in class io.github.cvc5.InputParser
getSynthSolution(Term) - Method in class io.github.cvc5.Solver: Get the synthesis solution of the given term.
getSynthSolutions(Term[]) - Method in class io.github.cvc5.Solver: Get the synthesis solutions of the given terms.
getTerm() - Method in class io.github.cvc5.DatatypeConstructor: Get the constructor term of this datatype constructor.
getTerm() - Method in class io.github.cvc5.DatatypeSelector: Get the selector term of this datatype selector.
getTermManager() - Method in class io.github.cvc5.AbstractPlugin: Get the associated term manager instance
getTermManager() - Method in class io.github.cvc5.Solver: Get the associated term manager instance
getTerms(long[]) - Static method in class io.github.cvc5.Utils
getTesterTerm() - Method in class io.github.cvc5.DatatypeConstructor: Get the tester term of this datatype constructor.
getTimeoutCore() - Method in class io.github.cvc5.Solver: Get a timeout core, which computes a subset of the current assertions that cause a timeout.
getTimeoutCoreAssuming(Term[]) - Method in class io.github.cvc5.Solver: Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions.
getTupleLength() - Method in class io.github.cvc5.Sort
getTupleSorts() - Method in class io.github.cvc5.Sort
getTupleValue() - Method in class io.github.cvc5.Term: Asserts isTupleValue().
getUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort: Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
getUninterpretedSortConstructorArity() - Method in class io.github.cvc5.Sort
getUninterpretedSortValue() - Method in class io.github.cvc5.Term: Asserts isUninterpretedSortValue().
getUnknownExplanation() - Method in class io.github.cvc5.Result: Get an explanation for an unknown query result.
getUnsatAssumptions() - Method in class io.github.cvc5.Solver: Get the set of unsat ("failed") assumptions.
getUnsatCore() - Method in class io.github.cvc5.Solver: Get the unsatisfiable core.
getUnsatCoreLemmas() - Method in class io.github.cvc5.Solver: Get the lemmas used to derive unsatisfiability.
getUpdaterTerm() - Method in class io.github.cvc5.DatatypeSelector: Get the updater term of this datatype selector.
getValue() - Method in enum io.github.cvc5.Kind
getValue() - Method in enum io.github.cvc5.modes.BlockModelsMode
getValue() - Method in enum io.github.cvc5.modes.FindSynthTarget
getValue() - Method in enum io.github.cvc5.modes.InputLanguage
getValue() - Method in enum io.github.cvc5.modes.LearnedLitType
getValue() - Method in enum io.github.cvc5.modes.ProofComponent
getValue() - Method in enum io.github.cvc5.modes.ProofFormat
getValue() - Method in enum io.github.cvc5.ProofRewriteRule
getValue() - Method in enum io.github.cvc5.ProofRule
getValue() - Method in enum io.github.cvc5.RoundingMode
getValue() - Method in enum io.github.cvc5.SkolemId
getValue() - Method in enum io.github.cvc5.SortKind
getValue() - Method in enum io.github.cvc5.UnknownExplanation
getValue(Term) - Method in class io.github.cvc5.Solver: Get the value of the given term in the current model.
getValue(Term[]) - Method in class io.github.cvc5.Solver: Get the values of the given terms in the current model.
getValueSepHeap() - Method in class io.github.cvc5.Solver: When using separation logic, obtain the term for the heap.
getValueSepNil() - Method in class io.github.cvc5.Solver: When using separation logic, obtain the term for nil.
getVersion() - Method in class io.github.cvc5.Solver: Get a string representation of the version of this solver.
Grammar - Class in io.github.cvc5: A Sygus Grammar.
Grammar(Grammar) - Constructor for class io.github.cvc5.Grammar
GROUND_TERM - io.github.cvc5.SkolemId: An arbitrary ground term of a given sort.
GT - io.github.cvc5.Kind: Greater than, chainable.

H

hashCode() - Method in class io.github.cvc5.Datatype: Get the hash value of a datatype.
hashCode() - Method in class io.github.cvc5.DatatypeConstructor: Get the hash value of a datatype constructor.
hashCode() - Method in class io.github.cvc5.DatatypeConstructorDecl: Get the hash value of a datatype constructor declaration.
hashCode() - Method in class io.github.cvc5.DatatypeDecl: Get the hash value of a datatype declaration.
hashCode() - Method in class io.github.cvc5.DatatypeSelector: Get the hash value of a datatype selector.
hashCode() - Method in class io.github.cvc5.Grammar: Get the hash value of a grammar.
hashCode() - Method in class io.github.cvc5.Op: Get the hash value of an operator.
hashCode() - Method in class io.github.cvc5.Proof: Get the hash value of a proof.
hashCode() - Method in class io.github.cvc5.Result: Get the hash value of a result.
hashCode() - Method in class io.github.cvc5.Sort: Get the hash value of a sort.
hashCode() - Method in class io.github.cvc5.SynthResult: Get the hash value of a synthesis result.
hashCode() - Method in class io.github.cvc5.Term: Get the hash value of a term.
hasNext() - Method in class io.github.cvc5.Datatype.ConstIterator
hasNext() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
hasNext() - Method in class io.github.cvc5.Statistics.ConstIterator
hasNext() - Method in class io.github.cvc5.Term.ConstIterator
hasNoSolution() - Method in class io.github.cvc5.SynthResult
hasOp() - Method in class io.github.cvc5.Term
hasSolution() - Method in class io.github.cvc5.SynthResult
hasSymbol() - Method in class io.github.cvc5.Sort
hasSymbol() - Method in class io.github.cvc5.Term
HO_APP_ENCODE - io.github.cvc5.ProofRule: Equality – Higher-order application encoding \[ \inferrule{-\mid t}{t=t'} \] where `t'` is the higher-order application that is equivalent to `t`, as implemented by uf.TheoryUfRewriter.getHoApplyForApplyUf.
HO_APPLY - io.github.cvc5.Kind: Higher-order applicative encoding of function application, left associative.
HO_CONG - io.github.cvc5.ProofRule: Equality – Higher-order congruence \[ \inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid k}{k(f, t_1,\dots, t_n) = k(g, s_1,\dots, s_n)} \] Notice that this rule is only used when the application kind $k$ is either `cvc5.Kind.APPLY_UF` or `cvc5.Kind.HO_APPLY`.
HO_DEQ_DIFF - io.github.cvc5.SkolemId: The higher-roder diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (A k1 ... kn) (B k1 ... kn)))).

I

IAND - io.github.cvc5.Kind: Integer and.
IMPLIES - io.github.cvc5.Kind: Logical implication.
IMPLIES_ELIM - io.github.cvc5.ProofRule: Boolean – Implication elimination \[ \inferrule{F_1 \rightarrow F_2 \mid -}{\neg F_1 \lor F_2} \]
impTerm(Term) - Method in class io.github.cvc5.Term: Boolean implication.
INCOMPLETE - io.github.cvc5.UnknownExplanation: Incomplete theory solver.
INPUT - io.github.cvc5.modes.LearnedLitType: A literal from the preprocessed set of input formulas that does not occur at top-level after preprocessing.
InputLanguage - Enum in io.github.cvc5.modes
InputParser - Class in io.github.cvc5: This class is the main interface for retrieving commands and expressions from an input using a parser.
InputParser(Solver) - Constructor for class io.github.cvc5.InputParser: Construct an input parser with an initially empty symbol manager.
InputParser(Solver, SymbolManager) - Constructor for class io.github.cvc5.InputParser: Construct an input parser
INST_ADD_TO_POOL - io.github.cvc5.Kind: A instantantiation-add-to-pool annotation.
INST_ATTRIBUTE - io.github.cvc5.Kind: Instantiation attribute.
INST_NO_PATTERN - io.github.cvc5.Kind: Instantiation no-pattern.
INST_PATTERN - io.github.cvc5.Kind: Instantiation pattern.
INST_PATTERN_LIST - io.github.cvc5.Kind: A list of instantiation patterns, attributes or annotations.
INST_POOL - io.github.cvc5.Kind: Instantiation pool annotation.
instantiate(Sort[]) - Method in class io.github.cvc5.Sort: Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
INSTANTIATE - io.github.cvc5.ProofRule: Quantifiers – Instantiation \[ \inferrule{\forall x_1\dots x_n.\> F\mid (t_1 \dots t_n), (id\, (t)?)?} {F\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The list of terms to instantiate $(t_1 \dots t_n)$ is provided as an s-expression as the first argument.
INT_DIV_BY_ZERO - io.github.cvc5.SkolemId: The function for integer division by zero.
INT_TIGHT_LB - io.github.cvc5.ProofRule: Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where $i$ has integer type.
INT_TIGHT_UB - io.github.cvc5.ProofRule: Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where $i$ has integer type.
INT_TO_BITVECTOR - io.github.cvc5.Kind: Conversion from Int to bit-vector.
INTEGER_SORT - io.github.cvc5.SortKind: The integer sort.
INTERNAL - io.github.cvc5.modes.LearnedLitType: Any internal literal that does not fall into the above categories.
INTERNAL - io.github.cvc5.SkolemId: The identifier of the skolem is not exported.
INTERNAL_KIND - io.github.cvc5.Kind: Internal kind.
INTERNAL_SORT_KIND - io.github.cvc5.SortKind: Internal kind.
INTERRUPTED - io.github.cvc5.UnknownExplanation: Solver was interrupted.
INTS_DIVISION - io.github.cvc5.Kind: Integer division, division by 0 undefined, left associative.
INTS_DIVISION_TOTAL - io.github.cvc5.Kind: Integer division, division by 0 defined to be 0, left associative.
INTS_MODULUS - io.github.cvc5.Kind: Integer modulus, modulus by 0 undefined.
INTS_MODULUS_TOTAL - io.github.cvc5.Kind: Integer modulus, t modulus by 0 defined to be t.
intValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as as int.
invoke(Solver, SymbolManager) - Method in class io.github.cvc5.Command: Invoke the command on the solver and symbol manager sm and return any resulting output as a string.
io.github.cvc5 - package io.github.cvc5
io.github.cvc5.modes - package io.github.cvc5.modes
IOracle - Interface in io.github.cvc5
IS_INTEGER - io.github.cvc5.Kind: Is-integer predicate.
isAbstract() - Method in class io.github.cvc5.Sort: Determine if this is an abstract sort.
isArray() - Method in class io.github.cvc5.Sort: Determine if this is an array sort.
isBag() - Method in class io.github.cvc5.Sort: Determine if this is a Bag sort.
isBitVector() - Method in class io.github.cvc5.Sort: Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).
isBitVectorValue() - Method in class io.github.cvc5.Term
isBoolean() - Method in class io.github.cvc5.Sort: Determine if this is the Boolean sort (SMT-LIB: Bool).
isBooleanValue() - Method in class io.github.cvc5.Term
isCardinalityConstraint() - Method in class io.github.cvc5.Term
isCodatatype() - Method in class io.github.cvc5.Datatype
isConstArray() - Method in class io.github.cvc5.Term
isDatatype() - Method in class io.github.cvc5.Sort: Determine if this is a datatype sort.
isDatatypeConstructor() - Method in class io.github.cvc5.Sort: Determine if this is a datatype constructor sort.
isDatatypeSelector() - Method in class io.github.cvc5.Sort: Determine if this is a datatype selector sort.
isDatatypeTester() - Method in class io.github.cvc5.Sort: Determine if this is a datatype tester sort.
isDatatypeUpdater() - Method in class io.github.cvc5.Sort: Determine if this is a datatype updater sort.
isDefault() - Method in class io.github.cvc5.Stat: Does this value hold the default value?
isDouble() - Method in class io.github.cvc5.Stat: Is this value a double?
isFinite() - Method in class io.github.cvc5.Datatype
isFiniteField() - Method in class io.github.cvc5.Sort: Determine if this is a finite field sort (SMT-LIB: (_ FiniteField i)).
isFiniteFieldValue() - Method in class io.github.cvc5.Term
isFloatingPoint() - Method in class io.github.cvc5.Sort: Determine if this is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)).
isFloatingPointNaN() - Method in class io.github.cvc5.Term
isFloatingPointNegInf() - Method in class io.github.cvc5.Term
isFloatingPointNegZero() - Method in class io.github.cvc5.Term
isFloatingPointPosInf() - Method in class io.github.cvc5.Term
isFloatingPointPosZero() - Method in class io.github.cvc5.Term
isFloatingPointValue() - Method in class io.github.cvc5.Term
isFunction() - Method in class io.github.cvc5.Sort: Determine if this is a function sort.
isHistogram() - Method in class io.github.cvc5.Stat: Is this value a histogram?
isIndexed() - Method in class io.github.cvc5.Op
isInstantiated() - Method in class io.github.cvc5.Sort: Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
isInt() - Method in class io.github.cvc5.Stat: Is this value an integer?
isInteger() - Method in class io.github.cvc5.Sort: Determine if this is the integer sort (SMT-LIB: Int).
isIntegerValue() - Method in class io.github.cvc5.Term
isInternal() - Method in class io.github.cvc5.Stat: Is this value intended for internal use only?
isLogicSet() - Method in class io.github.cvc5.Solver: Is logic set? Returns whether we called setLogic yet for this solver.
isLogicSet() - Method in class io.github.cvc5.SymbolManager
isModelCoreSymbol(Term) - Method in class io.github.cvc5.Solver: This returns false if the model value of free constant v was not essential for showing the satisfiability of the last call to Solver.checkSat() using the current model.
isNull() - Method in class io.github.cvc5.Command
isNull() - Method in class io.github.cvc5.Datatype
isNull() - Method in class io.github.cvc5.DatatypeConstructor
isNull() - Method in class io.github.cvc5.DatatypeConstructorDecl
isNull() - Method in class io.github.cvc5.DatatypeDecl
isNull() - Method in class io.github.cvc5.DatatypeSelector
isNull() - Method in class io.github.cvc5.Grammar: Determine if this is the null grammar.
isNull() - Method in class io.github.cvc5.Op
isNull() - Method in class io.github.cvc5.Result
isNull() - Method in class io.github.cvc5.Sort: Determine if this is the null sort.
isNull() - Method in class io.github.cvc5.SynthResult
isNull() - Method in class io.github.cvc5.Term
isNullable() - Method in class io.github.cvc5.Sort: Determine if this a nullable sort.
isParametric() - Method in class io.github.cvc5.Datatype
isParametric() - Method in class io.github.cvc5.DatatypeDecl: Determine if this datatype declaration is parametric.
isPredicate() - Method in class io.github.cvc5.Sort: Determine if this is a predicate sort.
isReal() - Method in class io.github.cvc5.Sort: Determine if this is the real sort (SMT-LIB: Real).
isRealAlgebraicNumber() - Method in class io.github.cvc5.Term
isRealValue() - Method in class io.github.cvc5.Term
isRecord() - Method in class io.github.cvc5.Datatype
isRecord() - Method in class io.github.cvc5.Sort: Determine if this is a record sort.
isRegExp() - Method in class io.github.cvc5.Sort: Determine if this is the regular expression sort (SMT-LIB: RegLan).
isRoundingMode() - Method in class io.github.cvc5.Sort: Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).
isRoundingModeValue() - Method in class io.github.cvc5.Term
isSat() - Method in class io.github.cvc5.Result
isSequence() - Method in class io.github.cvc5.Sort: Determine if this is a Sequence sort.
isSequenceValue() - Method in class io.github.cvc5.Term
isSet() - Method in class io.github.cvc5.Sort: Determine if this is a Set sort.
isSetValue() - Method in class io.github.cvc5.Term
isSkolem() - Method in class io.github.cvc5.Term
isString() - Method in class io.github.cvc5.Sort: Determine if this is the string sort (SMT-LIB: String)..
isString() - Method in class io.github.cvc5.Stat: Is this value a string?
isStringValue() - Method in class io.github.cvc5.Term
isTuple() - Method in class io.github.cvc5.Datatype
isTuple() - Method in class io.github.cvc5.Sort: Determine if this a tuple sort.
isTupleValue() - Method in class io.github.cvc5.Term
isUninterpretedSort() - Method in class io.github.cvc5.Sort: Determine if this is an uninterpreted sort.
isUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort: Determine if this is an uninterpreted sort constructor.
isUninterpretedSortValue() - Method in class io.github.cvc5.Term
isUnknown() - Method in class io.github.cvc5.Result
isUnknown() - Method in class io.github.cvc5.SynthResult
isUnsat() - Method in class io.github.cvc5.Result
isWellFounded() - Method in class io.github.cvc5.Datatype: Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
ITE - io.github.cvc5.Kind: If-then-else.
ITE_ELIM1 - io.github.cvc5.ProofRule: Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
ITE_ELIM2 - io.github.cvc5.ProofRule: Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
ITE_ELSE_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-else-false
ITE_ELSE_LOOKAHEAD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-else-lookahead
ITE_ELSE_LOOKAHEAD_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-else-lookahead-self
ITE_ELSE_NEG_LOOKAHEAD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-else-neg-lookahead
ITE_ELSE_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-else-true
ITE_EQ - io.github.cvc5.ProofRule: Processing rules – If-then-else equivalence \[ \inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}} \]
ITE_EQ_BRANCH - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-eq-branch
ITE_FALSE_COND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-false-cond
ITE_NEG_BRANCH - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-neg-branch
ITE_NOT_COND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-not-cond
ITE_THEN_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-then-false
ITE_THEN_LOOKAHEAD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-then-lookahead
ITE_THEN_LOOKAHEAD_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-then-lookahead-self
ITE_THEN_NEG_LOOKAHEAD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-then-neg-lookahead
ITE_THEN_TRUE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-then-true
ITE_TRUE_COND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule ite-true-cond
iterator() - Method in class io.github.cvc5.Datatype
iterator() - Method in class io.github.cvc5.DatatypeConstructor
iterator() - Method in class io.github.cvc5.Statistics
iterator() - Method in class io.github.cvc5.Term
iterator(boolean, boolean) - Method in class io.github.cvc5.Statistics
iteTerm(Term, Term) - Method in class io.github.cvc5.Term: If-then-else with this term as the Boolean condition.

K

Kind - Enum in io.github.cvc5

L

LAMBDA - io.github.cvc5.Kind: Lambda expression.
LAST_KIND - io.github.cvc5.Kind: Marks the upper-bound of this enumeration.
LAST_SORT_KIND - io.github.cvc5.SortKind: Marks the upper-bound of this enumeration.
LearnedLitType - Enum in io.github.cvc5.modes
LEQ - io.github.cvc5.Kind: Less than or equal, chainable.
LFSC - io.github.cvc5.modes.ProofFormat: Output LFSC proof.
LFSC_RULE - io.github.cvc5.ProofRule: External – LFSC Place holder for LFSC rules.
LITERALS - io.github.cvc5.modes.BlockModelsMode: Block models based on the SAT skeleton.
loadLibraries() - Static method in class io.github.cvc5.Utils: Load cvc5 jni library.
LT - io.github.cvc5.Kind: Less than, chainable.

M

MACRO_ARITH_SCALE_SUM_UB - io.github.cvc5.ProofRule: Arithmetic – Adding inequalities An arithmetic literal is a term of the form $p \diamond c$ where $\diamond \in \{ <, \leq, =, \geq, > \}$, $p$ a polynomial and $c$ a rational constant.
MACRO_ARITH_STRING_PRED_ENTAIL - io.github.cvc5.ProofRewriteRule: Arithmetic - strings predicate entailment \[ (= s t) = c \] \[ (>= s t) = c \] where $c$ is a Boolean constant.
MACRO_BOOL_NNF_NORM - io.github.cvc5.ProofRewriteRule: Booleans – Negation Normal Form with normalization \[ F = G \] where $G$ is the result of applying negation normal form to $F$ with additional normalizations, see TheoryBoolRewriter.computeNnfNorm.
MACRO_BV_BITBLAST - io.github.cvc5.ProofRule: Bit-vectors – (Macro) Bitblast \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] where $\texttt{bitblast}$ represents the result of the bit-blasted term as a bit-vector consisting of the output bits of the bit-blasted circuit representation of the term.
MACRO_QUANT_PARTITION_CONNECTED_FV - io.github.cvc5.ProofRewriteRule: Quantifiers – Macro connected free variable partitioning \[ \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_{1,1} \vee \ldots \vee F_{1,k_1}) \vee \ldots \vee (\forall X_m.\> F_{m,1} \vee \ldots \vee F_{m,k_m}) \] where $X_1, \ldots, X_m$ is a partition of $X$.
MACRO_RE_ELIM - io.github.cvc5.ProofRule: Strings – Regular expressions – Macro elimination \[ \inferrule{-\mid F,b}{F = F'} \] where $F'$ is the result of eliminating regular expressions from $F$ using the routine $\texttt{strings::RegExpElimination::eliminate}(F, b)$.
MACRO_RESOLUTION - io.github.cvc5.ProofRule: Boolean – N-ary Resolution + Factoring + Reordering \[ \inferrule{C_1 \dots C_n \mid C, pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C} \] where let $C_1 \dots C_n$ be nodes viewed as clauses, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let $C_1 \diamond_{L,\mathit{pol}} C_2$ represent the resolution of $C_1$ with $C_2$ with pivot $L$ and polarity $pol$, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let $C_1'$ be equal, in its set representation, to $C_1$, for each $i > 1$, let $C_i'$ be equal, in its set representation, to $C_{i-1} \diamond_{L_{i-1},\mathit{pol}_{i-1}} C_i'$ The result of the chain resolution is $C$, which is equal, in its set representation, to $C_n'$
MACRO_RESOLUTION_TRUST - io.github.cvc5.ProofRule: Boolean – N-ary Resolution + Factoring + Reordering unchecked Same as MACRO_RESOLUTION <cvc5.ProofRule.MACRO_RESOLUTION>, but not checked by the internal proof checker.
MACRO_REWRITE - io.github.cvc5.ProofRule: Builtin theory – Rewrite \[ \inferrule{- \mid t, idr}{t = \texttt{rewrite}_{idr}(t)} \] where $idr$ is a MethodId identifier, which determines the kind of rewriter to apply, e.g.
MACRO_SR_EQ_INTRO - io.github.cvc5.ProofRule: Builtin theory – Substitution + Rewriting equality introduction In this rule, we provide a term $t$ and conclude that it is equal to its rewritten form under a (proven) substitution.
MACRO_SR_PRED_ELIM - io.github.cvc5.ProofRule: Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid (ids (ida (idr)?)?)?}{\texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1))} \] where $ids$ and $idr$ are method identifiers.
MACRO_SR_PRED_INTRO - io.github.cvc5.ProofRule: Builtin theory – Substitution + Rewriting predicate introduction In this rule, we provide a formula $F$ and conclude it, under the condition that it rewrites to true under a proven substitution.
MACRO_SR_PRED_TRANSFORM - io.github.cvc5.ProofRule: Builtin theory – Substitution + Rewriting predicate elimination \[ \inferrule{F, F_1 \dots F_n \mid G, (ids (ida (idr)?)?)?}{G} \] where \[ \texttt{rewrite}_{idr}(F \circ \sigma_{ids, ida}(F_n) \circ\cdots \circ \sigma_{ids, ida}(F_1)) =\\ \texttt{rewrite}_{idr}(G \circ \sigma_{ids, ida}(F_n) \circ \cdots \circ \sigma_{ids, ida}(F_1)) \] More generally, this rule also holds when: $\texttt{Rewriter::rewrite}(\texttt{toOriginal}(F')) = \texttt{Rewriter::rewrite}(\texttt{toOriginal}(G'))$ where $F'$ and $G'$ are the result of each side of the equation above.
MACRO_STRING_INFERENCE - io.github.cvc5.ProofRule: Strings – (Macro) String inference \[ \inferrule{?\mid F,\mathit{id},\mathit{isRev},\mathit{exp}}{F} \] used to bookkeep an inference that has not yet been converted via $\texttt{strings::InferProofCons::convert}$.
MACRO_SUBSTR_STRIP_SYM_LENGTH - io.github.cvc5.ProofRewriteRule: Strings - strings substring strip symbolic length \[ str.substr(s, n, m) = t \] where $t$ is obtained by fully or partially stripping components of $s$ based on $n$ and $m$.
MATCH - io.github.cvc5.Kind: Match expression.
MATCH_BIND_CASE - io.github.cvc5.Kind: Match case with binders, for constructors with selectors and variable patterns.
MATCH_CASE - io.github.cvc5.Kind: Match case for nullary constructors.
MEMOUT - io.github.cvc5.UnknownExplanation: Memory limit reached.
mkAbstractSort(SortKind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkAbstractSort(SortKind). It will be removed in a future release.
mkAbstractSort(SortKind) - Method in class io.github.cvc5.TermManager: Create an abstract sort.
mkArraySort(Sort, Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkArraySort(Sort, Sort). It will be removed in a future release.
mkArraySort(Sort, Sort) - Method in class io.github.cvc5.TermManager: Create an array sort.
mkBagSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBagSort(Sort). It will be removed in a future release.
mkBagSort(Sort) - Method in class io.github.cvc5.TermManager: Create a bag sort.
mkBitVector(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int). It will be removed in a future release.
mkBitVector(int) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of given size and value = 0.
mkBitVector(int, long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int, long). It will be removed in a future release.
mkBitVector(int, long) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of given size and value.
mkBitVector(int, String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVector(int, String, int). It will be removed in a future release.
mkBitVector(int, String, int) - Method in class io.github.cvc5.TermManager: Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.
mkBitVectorSort(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBitVectorSort(int). It will be removed in a future release.
mkBitVectorSort(int) - Method in class io.github.cvc5.TermManager: Create a bit-vector sort.
mkBoolean(boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkBoolean(boolean). It will be removed in a future release.
mkBoolean(boolean) - Method in class io.github.cvc5.TermManager: Create a Boolean constant.
mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkCardinalityConstraint(Sort, int). It will be removed in a future release.
mkCardinalityConstraint(Sort, int) - Method in class io.github.cvc5.TermManager: Create a cardinality constraint for an uninterpreted sort.
mkConst(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConst(Sort). It will be removed in a future release.
mkConst(Sort) - Method in class io.github.cvc5.TermManager: Create a free constant with a default symbol name.
mkConst(Sort, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConst(Sort, String). It will be removed in a future release.
mkConst(Sort, String) - Method in class io.github.cvc5.TermManager: Create a free constant.
mkConstArray(Sort, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkConstArray(Sort, Term). It will be removed in a future release.
mkConstArray(Sort, Term) - Method in class io.github.cvc5.TermManager: Create a constant array with the provided constant value stored at every index
mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeConstructorDecl(String). It will be removed in a future release.
mkDatatypeConstructorDecl(String) - Method in class io.github.cvc5.TermManager: Create a datatype constructor declaration.
mkDatatypeDecl(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String). It will be removed in a future release.
mkDatatypeDecl(String) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, boolean). It will be removed in a future release.
mkDatatypeDecl(String, boolean) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
mkDatatypeDecl(String, Sort[]) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeDecl(String, Sort[]). It will be removed in a future release.
mkDatatypeDecl(String, Sort[], boolean) - Method in class io.github.cvc5.TermManager: Create a datatype declaration.
mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeSort(DatatypeDecl). It will be removed in a future release.
mkDatatypeSort(DatatypeDecl) - Method in class io.github.cvc5.TermManager: Create a datatype sort.
mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkDatatypeSorts(DatatypeDecl[]). It will be removed in a future release.
mkDatatypeSorts(DatatypeDecl[]) - Method in class io.github.cvc5.TermManager: Create a vector of datatype sorts.
mkEmptyBag(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptyBag(Sort). It will be removed in a future release.
mkEmptyBag(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing an empty bag of the given sort.
mkEmptySequence(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptySequence(Sort). It will be removed in a future release.
mkEmptySequence(Sort) - Method in class io.github.cvc5.TermManager: Create an empty sequence of the given element sort.
mkEmptySet(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkEmptySet(Sort). It will be removed in a future release.
mkEmptySet(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing an empty set of the given sort.
mkFalse() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFalse(). It will be removed in a future release.
mkFalse() - Method in class io.github.cvc5.TermManager: Create a Boolean false constant.
mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFiniteFieldElem(String, Sort, int). It will be removed in a future release.
mkFiniteFieldElem(String, Sort, int) - Method in class io.github.cvc5.TermManager: Create a finite field constant in a given field and for a given value.
mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFiniteFieldSort(String, int). It will be removed in a future release.
mkFiniteFieldSort(String, int) - Method in class io.github.cvc5.TermManager: Create a finite field sort.
mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPoint(int, int, Term). It will be removed in a future release.
mkFloatingPoint(int, int, Term) - Method in class io.github.cvc5.TermManager: Create a floating-point value from a bit-vector given in IEEE-754 format.
mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPoint(Term, Term, Term). It will be removed in a future release.
mkFloatingPoint(Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).
mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNaN(int, int). It will be removed in a future release.
mkFloatingPointNaN(int, int) - Method in class io.github.cvc5.TermManager: Create a not-a-number floating-point constant (SMT-LIB: NaN).
mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNegInf(int, int). It will be removed in a future release.
mkFloatingPointNegInf(int, int) - Method in class io.github.cvc5.TermManager: Create a negative infinity floating-point constant (SMT-LIB: -oo).
mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointNegZero(int, int). It will be removed in a future release.
mkFloatingPointNegZero(int, int) - Method in class io.github.cvc5.TermManager: Create a negative zero floating-point constant (SMT-LIB: -zero).
mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointPosInf(int, int). It will be removed in a future release.
mkFloatingPointPosInf(int, int) - Method in class io.github.cvc5.TermManager: Create a positive infinity floating-point constant (SMT-LIB: +oo).
mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointPosZero(int, int). It will be removed in a future release.
mkFloatingPointPosZero(int, int) - Method in class io.github.cvc5.TermManager: Create a positive zero floating-point constant (SMT-LIB: +zero).
mkFloatingPointSort(int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFloatingPointSort(int, int). It will be removed in a future release.
mkFloatingPointSort(int, int) - Method in class io.github.cvc5.TermManager: Create a floating-point sort.
mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFunctionSort(Sort[], Sort). It will be removed in a future release.
mkFunctionSort(Sort[], Sort) - Method in class io.github.cvc5.TermManager: Create function sort.
mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkFunctionSort(Sort, Sort). It will be removed in a future release.
mkFunctionSort(Sort, Sort) - Method in class io.github.cvc5.TermManager: Create function sort.
mkGrammar(Term[], Term[]) - Method in class io.github.cvc5.Solver: Create a Sygus grammar.
mkInteger(long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkInteger(long). It will be removed in a future release.
mkInteger(long) - Method in class io.github.cvc5.TermManager: Create an integer constant from a C++ int.
mkInteger(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkInteger(String). It will be removed in a future release.
mkInteger(String) - Method in class io.github.cvc5.TermManager: Create an integer constant from a string.
mkNullableIsNull(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableIsNull(Term). It will be removed in a future release.
mkNullableIsNull(Term) - Method in class io.github.cvc5.TermManager: Create a null tester for a nullable term.
mkNullableIsSome(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableIsSome(Term). It will be removed in a future release.
mkNullableIsSome(Term) - Method in class io.github.cvc5.TermManager: Create a some tester for a nullable term.
mkNullableLift(Kind, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableLift(Kind, Term[]). It will be removed in a future release.
mkNullableLift(Kind, Term[]) - Method in class io.github.cvc5.TermManager: Create a term that lifts kind to nullable terms.
mkNullableNull(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableNull(Sort). It will be removed in a future release.
mkNullableNull(Sort) - Method in class io.github.cvc5.TermManager: Create a constant representing a null value of the given sort.
mkNullableSome(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableSome(Term). It will be removed in a future release.
mkNullableSome(Term) - Method in class io.github.cvc5.TermManager: Create a nullable some term.
mkNullableSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableSort(Sort). It will be removed in a future release.
mkNullableSort(Sort) - Method in class io.github.cvc5.TermManager: Create a nullable sort.
mkNullableVal(Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkNullableVal(Term). It will be removed in a future release.
mkNullableVal(Term) - Method in class io.github.cvc5.TermManager: Create a selector for nullable term.
mkOp(Kind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind). It will be removed in a future release.
mkOp(Kind) - Method in class io.github.cvc5.TermManager: Create an operator for a builtin Kind The Kind may not be the Kind for an indexed operator (e.g., Kind.BITVECTOR_EXTRACT).
mkOp(Kind, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int). It will be removed in a future release.
mkOp(Kind, int) - Method in class io.github.cvc5.TermManager: Create operator of kind: DIVISIBLE BITVECTOR_REPEAT BITVECTOR_ZERO_EXTEND BITVECTOR_SIGN_EXTEND BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_RIGHT INT_TO_BITVECTOR FLOATINGPOINT_TO_UBV FLOATINGPOINT_TO_UBV_TOTAL FLOATINGPOINT_TO_SBV FLOATINGPOINT_TO_SBV_TOTAL TUPLE_UPDATE See enum Kind for a description of the parameters.
mkOp(Kind, int[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int[]). It will be removed in a future release.
mkOp(Kind, int[]) - Method in class io.github.cvc5.TermManager: Create operator of Kind: TUPLE_PROJECT See enum Kind for a description of the parameters.
mkOp(Kind, int, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, int, int). It will be removed in a future release.
mkOp(Kind, int, int) - Method in class io.github.cvc5.TermManager: Create operator of Kind: BITVECTOR_EXTRACT FLOATINGPOINT_TO_FP_FROM_IEEE_BV FLOATINGPOINT_TO_FP_FROM_FP FLOATINGPOINT_TO_FP_FROM_REAL FLOATINGPOINT_TO_FP_FROM_SBV FLOATINGPOINT_TO_FP_FROM_UBV See enum Kind for a description of the parameters.
mkOp(Kind, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkOp(Kind, String). It will be removed in a future release.
mkOp(Kind, String) - Method in class io.github.cvc5.TermManager: Create operator of kind: Kind.DIVISIBLE (to support arbitrary precision integers) See enum Kind for a description of the parameters.
mkParamSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkParamSort(). It will be removed in a future release.
mkParamSort() - Method in class io.github.cvc5.TermManager: Create a sort parameter.
mkParamSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkParamSort(String). It will be removed in a future release.
mkParamSort(String) - Method in class io.github.cvc5.TermManager: Create a sort parameter.
mkPi() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkPi(). It will be removed in a future release.
mkPi() - Method in class io.github.cvc5.TermManager: Create a constant representing the number Pi.
mkPredicateSort(Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkPredicateSort(Sort[]). It will be removed in a future release.
mkPredicateSort(Sort[]) - Method in class io.github.cvc5.TermManager: Create a predicate sort.
mkReal(long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(long). It will be removed in a future release.
mkReal(long) - Method in class io.github.cvc5.TermManager: Create a real constant from an integer.
mkReal(long, long) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(long, long). It will be removed in a future release.
mkReal(long, long) - Method in class io.github.cvc5.TermManager: Create a real constant from a rational.
mkReal(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkReal(String). It will be removed in a future release.
mkReal(String) - Method in class io.github.cvc5.TermManager: Create a real constant from a string.
mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRecordSort(Pair[]). It will be removed in a future release.
mkRecordSort(Pair<String, Sort>[]) - Method in class io.github.cvc5.TermManager: Create a record sort
mkRegexpAll() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpAll(). It will be removed in a future release.
mkRegexpAll() - Method in class io.github.cvc5.TermManager: Create a regular expression all (re.all) term.
mkRegexpAllchar() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpAllchar(). It will be removed in a future release.
mkRegexpAllchar() - Method in class io.github.cvc5.TermManager: Create a regular expression allchar (re.allchar) term.
mkRegexpNone() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRegexpNone(). It will be removed in a future release.
mkRegexpNone() - Method in class io.github.cvc5.TermManager: Create a regular expression none (re.none) term.
mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkRoundingMode(RoundingMode). It will be removed in a future release.
mkRoundingMode(RoundingMode) - Method in class io.github.cvc5.TermManager: Create a rounding mode constant.
mkSepEmp() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSepEmp(). It will be removed in a future release.
mkSepEmp() - Method in class io.github.cvc5.TermManager: Create a separation logic empty term.
mkSepNil(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSepNil(Sort). It will be removed in a future release.
mkSepNil(Sort) - Method in class io.github.cvc5.TermManager: Create a separation logic nil term.
mkSequenceSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSequenceSort(Sort). It will be removed in a future release.
mkSequenceSort(Sort) - Method in class io.github.cvc5.TermManager: Create a sequence sort.
mkSetSort(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkSetSort(Sort). It will be removed in a future release.
mkSetSort(Sort) - Method in class io.github.cvc5.TermManager: Create a set sort.
mkSkolem(SkolemId, Term[]) - Method in class io.github.cvc5.TermManager: Create a skolem
mkString(int[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(int[]). It will be removed in a future release.
mkString(int[]) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkString(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(String). It will be removed in a future release.
mkString(String) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkString(String, boolean) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkString(String, boolean). It will be removed in a future release.
mkString(String, boolean) - Method in class io.github.cvc5.TermManager: Create a String constant.
mkTerm(Kind) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind). It will be removed in a future release.
mkTerm(Kind) - Method in class io.github.cvc5.TermManager: Create 0-ary term of given kind.
mkTerm(Kind, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term). It will be removed in a future release.
mkTerm(Kind, Term) - Method in class io.github.cvc5.TermManager: Create a unary term of given kind.
mkTerm(Kind, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term[]). It will be removed in a future release.
mkTerm(Kind, Term[]) - Method in class io.github.cvc5.TermManager: Create n-ary term of given kind.
mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term). It will be removed in a future release.
mkTerm(Kind, Term, Term) - Method in class io.github.cvc5.TermManager: Create binary term of given kind.
mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Kind, Term, Term, Term). It will be removed in a future release.
mkTerm(Kind, Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create ternary term of given kind.
mkTerm(Op) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op). It will be removed in a future release.
mkTerm(Op) - Method in class io.github.cvc5.TermManager: Create nullary term of given kind from a given operator.
mkTerm(Op, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term). It will be removed in a future release.
mkTerm(Op, Term) - Method in class io.github.cvc5.TermManager: Create unary term of given kind from a given operator.
mkTerm(Op, Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term[]). It will be removed in a future release.
mkTerm(Op, Term[]) - Method in class io.github.cvc5.TermManager: Create n-ary term of given kind from a given operator.
mkTerm(Op, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term). It will be removed in a future release.
mkTerm(Op, Term, Term) - Method in class io.github.cvc5.TermManager: Create binary term of given kind from a given operator.
mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTerm(Op, Term, Term, Term). It will be removed in a future release.
mkTerm(Op, Term, Term, Term) - Method in class io.github.cvc5.TermManager: Create ternary term of given kind from a given operator.
mkTrue() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTrue(). It will be removed in a future release.
mkTrue() - Method in class io.github.cvc5.TermManager: Create a Boolean true constant.
mkTuple(Term[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTuple(Term[]). It will be removed in a future release.
mkTuple(Term[]) - Method in class io.github.cvc5.TermManager: Create a tuple term.
mkTupleSort(Sort[]) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkTupleSort(Sort[]). It will be removed in a future release.
mkTupleSort(Sort[]) - Method in class io.github.cvc5.TermManager: Create a tuple sort.
mkUninterpretedSort() - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSort(). It will be removed in a future release.
mkUninterpretedSort() - Method in class io.github.cvc5.TermManager: Create an uninterpreted sort.
mkUninterpretedSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSort(String). It will be removed in a future release.
mkUninterpretedSort(String) - Method in class io.github.cvc5.TermManager: Create an uninterpreted sort.
mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int). It will be removed in a future release.
mkUninterpretedSortConstructorSort(int) - Method in class io.github.cvc5.TermManager: Create a sort constructor sort.
mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUninterpretedSortConstructorSort(int, String). It will be removed in a future release.
mkUninterpretedSortConstructorSort(int, String) - Method in class io.github.cvc5.TermManager: Create a sort constructor sort.
mkUniverseSet(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUniverseSet(Sort). It will be removed in a future release.
mkUniverseSet(Sort) - Method in class io.github.cvc5.TermManager: Create a universe set of the given sort.
mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String). It will be removed in a future release.
mkUnresolvedDatatypeSort(String) - Method in class io.github.cvc5.TermManager: Create an unresolved datatype sort.
mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkUnresolvedDatatypeSort(String, int). It will be removed in a future release.
mkUnresolvedDatatypeSort(String, int) - Method in class io.github.cvc5.TermManager: Create an unresolved datatype sort.
mkVar(Sort) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkVar(Sort). It will be removed in a future release.
mkVar(Sort) - Method in class io.github.cvc5.TermManager: Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
mkVar(Sort, String) - Method in class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by TermManager.mkVar(Sort, String). It will be removed in a future release.
mkVar(Sort, String) - Method in class io.github.cvc5.TermManager: Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
MOD_BY_ZERO - io.github.cvc5.SkolemId: The function for integer modulus by zero.
ModeInfo(String, String, String[]) - Constructor for class io.github.cvc5.OptionInfo.ModeInfo
MODUS_PONENS - io.github.cvc5.ProofRule: Boolean – Modus Ponens \[ \inferrule{F_1, (F_1 \rightarrow F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for IMPLIES_ELIM <cvc5.ProofRule.IMPLIES_ELIM> + RESOLUTION <cvc5.ProofRule.RESOLUTION>.
MULT - io.github.cvc5.Kind: Arithmetic multiplication.

N

NARY_CONG - io.github.cvc5.ProofRule: Equality – N-ary Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid k}{k(t_1,\dots, t_n) = k(s_1,\dots, s_n)} \] where $k$ is the application kind.
NEG - io.github.cvc5.Kind: Arithmetic negation.
next() - Method in class io.github.cvc5.Datatype.ConstIterator
next() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
next() - Method in class io.github.cvc5.Statistics.ConstIterator
next() - Method in class io.github.cvc5.Term.ConstIterator
nextCommand() - Method in class io.github.cvc5.InputParser: Parse and return the next command.
nextTerm() - Method in class io.github.cvc5.InputParser: Parse and return the next term.
NONE - io.github.cvc5.modes.ProofFormat: Do not translate proof output.
NONE - io.github.cvc5.ProofRewriteRule: This enumeration represents the rewrite rules used in a rewrite proof.
NONE - io.github.cvc5.SkolemId: Indicates this is not a skolem.
NOT - io.github.cvc5.Kind: Logical negation.
NOT_AND - io.github.cvc5.ProofRule: Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
NOT_EQUIV_ELIM1 - io.github.cvc5.ProofRule: Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
NOT_EQUIV_ELIM2 - io.github.cvc5.ProofRule: Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
NOT_IMPLIES_ELIM1 - io.github.cvc5.ProofRule: Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
NOT_IMPLIES_ELIM2 - io.github.cvc5.ProofRule: Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
NOT_ITE_ELIM1 - io.github.cvc5.ProofRule: Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
NOT_ITE_ELIM2 - io.github.cvc5.ProofRule: Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
NOT_NOT_ELIM - io.github.cvc5.ProofRule: Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
NOT_OR_ELIM - io.github.cvc5.ProofRule: Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
NOT_XOR_ELIM1 - io.github.cvc5.ProofRule: Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
NOT_XOR_ELIM2 - io.github.cvc5.ProofRule: Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
notifySatClause(Term) - Method in class io.github.cvc5.AbstractPlugin: Notify SAT clause, called when cl is a clause learned by the SAT solver.
notifyTheoryLemma(Term) - Method in class io.github.cvc5.AbstractPlugin: Notify theory lemma, called when lem is a theory lemma sent by a theory solver.
notTerm() - Method in class io.github.cvc5.Term: Boolean negation.
NULL_SORT - io.github.cvc5.SortKind: Null kind.
NULL_TERM - io.github.cvc5.Kind: Null kind.
NULLABLE_LIFT - io.github.cvc5.Kind: Lifting operator for nullable terms.
NULLABLE_SORT - io.github.cvc5.SortKind: A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.
NumberInfo(T, T, T, T) - Constructor for class io.github.cvc5.OptionInfo.NumberInfo

O

Op - Class in io.github.cvc5: A cvc5 operator.
Op() - Constructor for class io.github.cvc5.Op: Null op
OptionInfo - Class in io.github.cvc5: Holds some description about a particular option, including its name, its aliases, whether the option was explicitly set by the user, and information concerning its value.
OptionInfo.BaseInfo - Class in io.github.cvc5: Abstract class for OptionInfo values
OptionInfo.ModeInfo - Class in io.github.cvc5
OptionInfo.NumberInfo<T> - Class in io.github.cvc5: Default value, current value, minimum and maximum of a numeric value
OptionInfo.ValueInfo<T> - Class in io.github.cvc5: Has the current and the default value
OptionInfo.VoidInfo - Class in io.github.cvc5: Has no value information
OR - io.github.cvc5.Kind: Logical disjunction.
orTerm(Term) - Method in class io.github.cvc5.Term: Boolean or.
OTHER - io.github.cvc5.UnknownExplanation: Other reason.

P

Pair<K,V> - Class in io.github.cvc5
Pair(K, V) - Constructor for class io.github.cvc5.Pair
PI - io.github.cvc5.Kind: Pi constant.
pointer - Variable in class io.github.cvc5.Proof
pop() - Method in class io.github.cvc5.Solver: Pop a level from the assertion stack.
pop(int) - Method in class io.github.cvc5.Solver: Pop (a) level(s) from the assertion stack.
POW - io.github.cvc5.Kind: Arithmetic power.
POW2 - io.github.cvc5.Kind: Power of two.
PREPROCESS - io.github.cvc5.modes.LearnedLitType: A top-level literal (unit clause) from the preprocessed set of input formulas.
PREPROCESS - io.github.cvc5.modes.ProofComponent: Proofs of Gu1 ...
PREPROCESS_SOLVED - io.github.cvc5.modes.LearnedLitType: An equality that was turned into a substitution during preprocessing.
Proof - Class in io.github.cvc5: A cvc5 Proof.
Proof() - Constructor for class io.github.cvc5.Proof: Null proof
ProofComponent - Enum in io.github.cvc5.modes
ProofFormat - Enum in io.github.cvc5.modes
ProofRewriteRule - Enum in io.github.cvc5
ProofRule - Enum in io.github.cvc5
proofToString(Proof) - Method in class io.github.cvc5.Solver: Prints a proof into a string with a slected proof format mode.
proofToString(Proof, ProofFormat) - Method in class io.github.cvc5.Solver: Prints a proof into a string with a slected proof format mode.
PURIFY - io.github.cvc5.SkolemId: The purification skolem for a term.
push() - Method in class io.github.cvc5.Solver: Push a level to the assertion stack.
push(int) - Method in class io.github.cvc5.Solver: Push (a) level(s) to the assertion stack.

Q

QUANT_MERGE_PRENEX - io.github.cvc5.ProofRewriteRule: Quantifiers – Merge prenex \[ \forall X_1.\> \ldots \forall X_n.\> F = \forall X_1 \ldots X_n.\> F \] where $X_1 \ldots X_n$ are lists of variables.
QUANT_MINISCOPE - io.github.cvc5.ProofRewriteRule: Quantifiers – Miniscoping \[ \forall X.\> F_1 \wedge \ldots \wedge F_n = (\forall X.\> F_1) \wedge \ldots \wedge (\forall X.\> F_n) \]
QUANT_UNUSED_VARS - io.github.cvc5.ProofRewriteRule: Quantifiers – Unused variables \[ \forall X.\> F = \forall X_1.\> F \] where $X_1$ is the subset of $X$ that appear free in $F$.
QUANTIFIERS_SKOLEMIZE - io.github.cvc5.SkolemId: The n^th skolem for the negation of universally quantified formula Q.
QUERY - io.github.cvc5.modes.FindSynthTarget: Find a query over the given grammar.

R

RAW_PREPROCESS - io.github.cvc5.modes.ProofComponent: Proofs of G1 ...
RE_ALL_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-all-elim
RE_CONCAT_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-concat-emp
RE_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-concat-flatten
RE_CONCAT_MERGE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-concat-merge
RE_CONCAT_NONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-concat-none
RE_CONCAT_STAR_SWAP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-concat-star-swap
RE_DIFF_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-diff-elim
RE_FIRST_MATCH - io.github.cvc5.SkolemId: For string a and regular expression R, this skolem is the string that the first, shortest match of R was matched to in a.
RE_FIRST_MATCH_POST - io.github.cvc5.SkolemId: For string a and regular expression R, this skolem is the remainder of a after the first, shortest match of R in a.
RE_FIRST_MATCH_PRE - io.github.cvc5.SkolemId: The next three skolems are used to decompose the match of a regular expression in string.
RE_IN_COMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-in-comp
RE_IN_CSTRING - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-in-cstring
RE_IN_EMPTY - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-in-empty
RE_IN_SIGMA - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-in-sigma
RE_IN_SIGMA_STAR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-in-sigma-star
RE_INTER - io.github.cvc5.ProofRule: Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{re.inter}(R_1,R_2)} \]
RE_INTER_ALL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-all
RE_INTER_CSTRING - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-cstring
RE_INTER_CSTRING_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-cstring-neg
RE_INTER_DUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-dup
RE_INTER_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-flatten
RE_INTER_NONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-inter-none
RE_INTER_UNION_INCLUSION - io.github.cvc5.ProofRewriteRule: Strings - regular expression intersection/union inclusion \[ (re.inter\ R) = \mathit{re.inter}(\mathit{re.none}, R_0) \] where $R$ is a list of regular expressions containing `r_1`, `re.comp(r_2)` and the list $R_0$ where `r_2` is a superset of `r_1`.
RE_LOOP_ELIM - io.github.cvc5.ProofRewriteRule: Strings - regular expression loop elimination \[ re.loop_{l,u}(R) = re.union(R^l, \ldots, R^u) \] where $u \geq l$.
RE_LOOP_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-loop-neg
RE_OPT_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-opt-elim
RE_UNFOLD_NEG - io.github.cvc5.ProofRule: Strings – Regular expressions – Negative Unfold \[ \inferrule{t \not \in \mathit{re}.\text{*}(R) \mid -}{t \neq \ \epsilon \ \wedge \forall L.
RE_UNFOLD_NEG_CONCAT_FIXED - io.github.cvc5.ProofRule: Strings – Regular expressions – Unfold negative concatenation, fixed ..
RE_UNFOLD_POS - io.github.cvc5.ProofRule: Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{F} \] where $F$ corresponds to the one-step unfolding of the premise.
RE_UNFOLD_POS_COMPONENT - io.github.cvc5.SkolemId: Regular expression unfold component: if (str.in_re a R), where R is (re.++ R0 ... Rn), then the RE_UNFOLD_POS_COMPONENT for indices (a,R,i) is a string ki such that (= a (str.++ k0 ... kn)) and (str.in_re k0 R0) for i = 0, ..., n.
RE_UNION_ALL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-union-all
RE_UNION_DUP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-union-dup
RE_UNION_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-union-flatten
RE_UNION_NONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule re-union-none
REAL_SORT - io.github.cvc5.SortKind: The real sort.
REFL - io.github.cvc5.ProofRule: Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
REGEXP_ALL - io.github.cvc5.Kind: Regular expression all.
REGEXP_ALLCHAR - io.github.cvc5.Kind: Regular expression all characters.
REGEXP_COMPLEMENT - io.github.cvc5.Kind: Regular expression complement.
REGEXP_CONCAT - io.github.cvc5.Kind: Regular expression concatenation.
REGEXP_DIFF - io.github.cvc5.Kind: Regular expression difference.
REGEXP_INTER - io.github.cvc5.Kind: Regular expression intersection.
REGEXP_LOOP - io.github.cvc5.Kind: Regular expression loop.
REGEXP_NONE - io.github.cvc5.Kind: Regular expression none.
REGEXP_OPT - io.github.cvc5.Kind: Regular expression ?.
REGEXP_PLUS - io.github.cvc5.Kind: Regular expression +.
REGEXP_RANGE - io.github.cvc5.Kind: Regular expression range.
REGEXP_REPEAT - io.github.cvc5.Kind: Operator for regular expression repeat.
REGEXP_STAR - io.github.cvc5.Kind: Regular expression \*.
REGEXP_UNION - io.github.cvc5.Kind: Regular expression union.
REGLAN_SORT - io.github.cvc5.SortKind: The regular language sort.
RELATION_AGGREGATE - io.github.cvc5.Kind: Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ...
RELATION_GROUP - io.github.cvc5.Kind: Relation group $((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A)$ partitions tuples of relation $A$ such that tuples that have the same projection with indices $n_1 \; \dots \; n_k$ are in the same part.
RELATION_IDEN - io.github.cvc5.Kind: Relation identity.
RELATION_JOIN - io.github.cvc5.Kind: Relation join.
RELATION_JOIN_IMAGE - io.github.cvc5.Kind: Relation join image.
RELATION_PRODUCT - io.github.cvc5.Kind: Relation cartesian product.
RELATION_PROJECT - io.github.cvc5.Kind: Relation projection operator extends tuple projection operator to sets.
RELATION_TABLE_JOIN - io.github.cvc5.Kind: Table join operator for relations has the form $((\_ \; rel.table\_join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)$ where $m_1 \; n_1 \; \dots \; m_k \; n_k$ are natural numbers, and $A, B$ are relations.
RELATION_TCLOSURE - io.github.cvc5.Kind: Relation transitive closure.
RELATION_TRANSPOSE - io.github.cvc5.Kind: Relation transpose.
RELATIONS_GROUP_PART - io.github.cvc5.SkolemId: Given a group term ((_ rel.group n1 ... nk) A) of type (Set (Relation T)) this skolem maps elements of A to their parts in the resulting partition.
RELATIONS_GROUP_PART_ELEMENT - io.github.cvc5.SkolemId: Given a group term ((_ rel.group n1 ...
REORDERING - io.github.cvc5.ProofRule: Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the set representations of $C_1$ and $C_2$ are the same and the number of literals in $C_2$ is the same of that of $C_1$.
REQUIRES_CHECK_AGAIN - io.github.cvc5.UnknownExplanation: Requires another satisfiability check
REQUIRES_FULL_CHECK - io.github.cvc5.UnknownExplanation: Full satisfiability check required (e.g., if only preprocessing was performed).
resetAssertions() - Method in class io.github.cvc5.Solver: Remove all assertions.
RESOLUTION - io.github.cvc5.ProofRule: Boolean – Resolution \[ \inferrule{C_1, C_2 \mid pol, L}{C} \] where $C_1$ and $C_2$ are nodes viewed as clauses, i.e., either an OR node with each children viewed as a literal or a node viewed as a literal.
RESOURCEOUT - io.github.cvc5.UnknownExplanation: Resource limit reached.
Result - Class in io.github.cvc5: Encapsulation of a three-valued solver result, with explanations.
Result() - Constructor for class io.github.cvc5.Result: Null result
REWRITE - io.github.cvc5.modes.FindSynthTarget: Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
REWRITE_INPUT - io.github.cvc5.modes.FindSynthTarget: Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
REWRITE_UNSOUND - io.github.cvc5.modes.FindSynthTarget: Find a term t in the target grammar which rewrites to a term s that is not equivalent to it.
ROUND_NEAREST_TIES_TO_AWAY - io.github.cvc5.RoundingMode: Round to the nearest number away from zero.
ROUND_NEAREST_TIES_TO_EVEN - io.github.cvc5.RoundingMode: Round to the nearest even number.
ROUND_TOWARD_NEGATIVE - io.github.cvc5.RoundingMode: Round towards negative infinity (-oo).
ROUND_TOWARD_POSITIVE - io.github.cvc5.RoundingMode: Round towards positive infinity (SMT-LIB: +oo).
ROUND_TOWARD_ZERO - io.github.cvc5.RoundingMode: Round towards zero.
RoundingMode - Enum in io.github.cvc5
ROUNDINGMODE_SORT - io.github.cvc5.SortKind: The rounding mode sort.

S

SAT - io.github.cvc5.modes.ProofComponent: A proof of false whose free assumptions are Gu1, ...
SAT_EXTERNAL_PROVE - io.github.cvc5.ProofRule: SAT external prove Refutation \[ \inferrule{F_1 \dots F_n \mid D}{\bot} \] where $F_1 \dots F_n$ correspond to the input clauses in the DIMACS file `D`.
SAT_REFUTATION - io.github.cvc5.ProofRule: SAT Refutation for assumption-based unsat cores \[ \inferrule{F_1 \dots F_n \mid -}{\bot} \] where $F_1 \dots F_n$ correspond to the unsat core determined by the SAT solver.
SCOPE - io.github.cvc5.ProofRule: Scope (a binder for assumptions) \[ \inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$} \] This rule has a dual purpose with ASSUME <cvc5.ProofRule.ASSUME>.
SECANT - io.github.cvc5.Kind: Secant function.
second - Variable in class io.github.cvc5.Pair
second - Variable in class io.github.cvc5.Triplet
SELECT - io.github.cvc5.Kind: Array select.
SEP_EMP - io.github.cvc5.Kind: Separation logic empty heap.
SEP_NIL - io.github.cvc5.Kind: Separation logic nil.
SEP_PTO - io.github.cvc5.Kind: Separation logic points-to relation.
SEP_STAR - io.github.cvc5.Kind: Separation logic star.
SEP_WAND - io.github.cvc5.Kind: Separation logic magic wand.
SEQ_AT - io.github.cvc5.Kind: Sequence element at.
SEQ_CONCAT - io.github.cvc5.Kind: Sequence concat.
SEQ_CONTAINS - io.github.cvc5.Kind: Sequence contains.
SEQ_EXTRACT - io.github.cvc5.Kind: Sequence extract.
SEQ_INDEXOF - io.github.cvc5.Kind: Sequence index-of.
SEQ_LEN_UNIT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule seq-len-unit
SEQ_LENGTH - io.github.cvc5.Kind: Sequence length.
SEQ_NTH - io.github.cvc5.Kind: Sequence nth.
SEQ_NTH_UNIT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule seq-nth-unit
SEQ_PREFIX - io.github.cvc5.Kind: Sequence prefix-of.
SEQ_REPLACE - io.github.cvc5.Kind: Sequence replace.
SEQ_REPLACE_ALL - io.github.cvc5.Kind: Sequence replace all.
SEQ_REV - io.github.cvc5.Kind: Sequence reverse.
SEQ_REV_CONCAT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule seq-rev-concat
SEQ_REV_UNIT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule seq-rev-unit
SEQ_SUFFIX - io.github.cvc5.Kind: Sequence suffix-of.
SEQ_UNIT - io.github.cvc5.Kind: Sequence unit.
SEQ_UPDATE - io.github.cvc5.Kind: Sequence update.
SEQUENCE_SORT - io.github.cvc5.SortKind: A sequence sort, whose argument sort is the element sort of the sequence.
SET_CARD - io.github.cvc5.Kind: Set cardinality.
SET_CHOOSE - io.github.cvc5.Kind: Set choose.
SET_COMPLEMENT - io.github.cvc5.Kind: Set complement with respect to finite universe.
SET_COMPREHENSION - io.github.cvc5.Kind: Set comprehension A set comprehension is specified by a variable list \(x_1 ...
SET_EMPTY - io.github.cvc5.Kind: Empty set.
SET_FILTER - io.github.cvc5.Kind: Set filter.
SET_FOLD - io.github.cvc5.Kind: Set fold.
SET_INSERT - io.github.cvc5.Kind: The set obtained by inserting elements; Arity: n > 0 1..n-1: Terms of any Sort (must match the element sort of the given set Term) n: Term of set Sort Create Term of this Kind with: Solver.mkTerm(Kind, Term[]) Solver.mkTerm(Op, Term[]) Create Op of this kind with: Solver.mkOp(Kind, int[])
SET_INTER - io.github.cvc5.Kind: Set intersection.
SET_IS_EMPTY - io.github.cvc5.Kind: Set is empty tester.
SET_IS_SINGLETON - io.github.cvc5.Kind: Set is singleton tester.
SET_MAP - io.github.cvc5.Kind: Set map.
SET_MEMBER - io.github.cvc5.Kind: Set membership predicate.
SET_MINUS - io.github.cvc5.Kind: Set subtraction.
SET_SINGLETON - io.github.cvc5.Kind: Singleton set.
SET_SORT - io.github.cvc5.SortKind: A set sort, whose argument sort is the element sort of the set.
SET_SUBSET - io.github.cvc5.Kind: Subset predicate.
SET_UNION - io.github.cvc5.Kind: Set union.
SET_UNIVERSE - io.github.cvc5.Kind: Finite universe set.
setFileInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser: Set the input for the given file.
setIncrementalStringInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser: Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
setInfo(String, String) - Method in class io.github.cvc5.Solver: Set info.
setLogic(String) - Method in class io.github.cvc5.Solver: Set logic.
setOption(String, String) - Method in class io.github.cvc5.Solver: Set option.
SETS_CARD_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-card-emp
SETS_CARD_MINUS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-card-minus
SETS_CARD_SINGLETON - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-card-singleton
SETS_CARD_UNION - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-card-union
SETS_CHOOSE - io.github.cvc5.SkolemId: An interpreted function for set.choose operator, where (set.choose A) is expanded to (uf A) along with the inference (set.member (uf A) A)) when A is non-empty, where uf: (-> (Set E) E) is this skolem function, and E is the type of elements of A.
SETS_CHOOSE_SINGLETON - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-choose-singleton
SETS_DEQ_DIFF - io.github.cvc5.SkolemId: The set diff skolem, which is the witness k for the inference (=> (not (= A B)) (not (= (set.member k A) (set.member k B)))).
SETS_EQ_SINGLETON_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-eq-singleton-emp
SETS_EXT - io.github.cvc5.ProofRule: Sets – Sets extensionality \[ \inferrule{a \neq b\mid -} {\mathit{set.member}(k,a)\neq\mathit{set.member}(k,b)} \] where $k$ is the $\texttt{SETS_DEQ_DIFF}$ skolem for `(a, b)`.
SETS_FOLD_CARD - io.github.cvc5.SkolemId: An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need to guess the cardinality n of set A using a skolem function with SETS_FOLD_CARD id.
SETS_FOLD_COMBINE - io.github.cvc5.SkolemId: An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function that accumulates intermidiate values.
SETS_FOLD_ELEMENTS - io.github.cvc5.SkolemId: An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function for elements of A.
SETS_FOLD_UNION - io.github.cvc5.SkolemId: An uninterpreted function for set.fold operator: To compute (set.fold f t A), we need a function for elements of A which is given by elements defined in SETS_FOLD_ELEMENTS.
SETS_INTER_COMM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-inter-comm
SETS_INTER_EMP1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-inter-emp1
SETS_INTER_EMP2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-inter-emp2
SETS_INTER_MEMBER - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-inter-member
SETS_IS_EMPTY_EVAL - io.github.cvc5.ProofRewriteRule: Sets - empty tester evaluation \[ \mathit{sets.is\_empty}(\epsilon) = \top \] where $\epsilon$ is the empty set, or alternatively: \[ \mathit{sets.is\_empty}(c) = \bot \] where $c$ is a constant set that is not the empty set.
SETS_MAP_DOWN_ELEMENT - io.github.cvc5.SkolemId: A skolem variable that is unique per terms (set.map f A), y which is an element in (set.map f A).
SETS_MEMBER_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-member-emp
SETS_MEMBER_SINGLETON - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-member-singleton
SETS_MINUS_EMP1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-minus-emp1
SETS_MINUS_EMP2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-minus-emp2
SETS_MINUS_MEMBER - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-minus-member
SETS_SINGLETON_INJ - io.github.cvc5.ProofRule: Sets – Singleton injectivity \[ \inferrule{\mathit{set.singleton}(t) = \mathit{set.singleton}(s)\mid -}{t=s} \]
SETS_SUBSET_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-subset-elim
SETS_UNION_COMM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-union-comm
SETS_UNION_EMP1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-union-emp1
SETS_UNION_EMP2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-union-emp2
SETS_UNION_MEMBER - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule sets-union-member
setStringInput(InputLanguage, String, String) - Method in class io.github.cvc5.InputParser: Set the input to the given concrete input string.
SEXPR - io.github.cvc5.Kind: Symbolic expression.
SHARED_SELECTOR - io.github.cvc5.SkolemId: A shared datatype selector, see Reynolds et.
simplify(Term) - Method in class io.github.cvc5.Solver: Simplify a term or formula based on rewriting.
simplify(Term, boolean) - Method in class io.github.cvc5.Solver: Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.
SINE - io.github.cvc5.Kind: Sine function.
SKOLEM - io.github.cvc5.Kind: A Skolem.
SKOLEM_ADD_TO_POOL - io.github.cvc5.Kind: A skolemization-add-to-pool annotation.
SKOLEM_INTRO - io.github.cvc5.ProofRule: Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where $t$ is the unpurified form of skolem $k$.
SkolemId - Enum in io.github.cvc5
SKOLEMIZE - io.github.cvc5.ProofRule: Quantifiers – Skolemization \[ \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} \] where $\sigma$ maps $x_1,\dots,x_n$ to their representative skolems, which are skolems $k_1,\dots,k_n$.
SMT_LIB_2_6 - io.github.cvc5.modes.InputLanguage: The SMT-LIB version 2.6 language
SOLVABLE - io.github.cvc5.modes.LearnedLitType: An internal literal that is solvable for an input variable.
Solver - Class in io.github.cvc5: A cvc5 solver.
Solver() - Constructor for class io.github.cvc5.Solver: Deprecated.
This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
Solver(TermManager) - Constructor for class io.github.cvc5.Solver: Create solver instance.
Sort - Class in io.github.cvc5: The sort of a cvc5 term.
Sort() - Constructor for class io.github.cvc5.Sort: Null sort
SortKind - Enum in io.github.cvc5
SPLIT - io.github.cvc5.ProofRule: Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
SQRT - io.github.cvc5.Kind: Square root.
Stat - Class in io.github.cvc5: Represents a snapshot of a single statistic value.
Statistics - Class in io.github.cvc5
Statistics.ConstIterator - Class in io.github.cvc5
STORE - io.github.cvc5.Kind: Array store.
STR_AT_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-at-elim
STR_CONCAT_CLASH - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash
STR_CONCAT_CLASH_CHAR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash-char
STR_CONCAT_CLASH_CHAR_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash-char-rev
STR_CONCAT_CLASH_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash-rev
STR_CONCAT_CLASH2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash2
STR_CONCAT_CLASH2_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-clash2-rev
STR_CONCAT_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-emp
STR_CONCAT_FLATTEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-flatten
STR_CONCAT_FLATTEN_EQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-flatten-eq
STR_CONCAT_FLATTEN_EQ_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-flatten-eq-rev
STR_CONCAT_UNIFY - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-unify
STR_CONCAT_UNIFY_BASE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-unify-base
STR_CONCAT_UNIFY_BASE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-unify-base-rev
STR_CONCAT_UNIFY_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-concat-unify-rev
STR_CONTAINS_CONCAT_FIND - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-concat-find
STR_CONTAINS_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-emp
STR_CONTAINS_IS_EMP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-is-emp
STR_CONTAINS_LEQ_LEN_EQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-leq-len-eq
STR_CONTAINS_LT_LEN - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-lt-len
STR_CONTAINS_REFL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-refl
STR_CONTAINS_SPLIT_CHAR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-contains-split-char
STR_EQ_CTN_FALSE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-eq-ctn-false
STR_EQ_CTN_FULL_FALSE1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-eq-ctn-full-false1
STR_EQ_CTN_FULL_FALSE2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-eq-ctn-full-false2
STR_IN_RE_CONCAT_STAR_CHAR - io.github.cvc5.ProofRewriteRule: Strings - string in regular expression concatenation star character \[ \mathit{str.in\_re}(\mathit{str}.\text{++}(s_1, \ldots, s_n), \mathit{re}.\text{*}(R)) =\\ \mathit{str.in\_re}(s_1, \mathit{re}.\text{*}(R)) \wedge \ldots \wedge \mathit{str.in\_re}(s_n, \mathit{re}.\text{*}(R)) \] where all strings in $R$ have length one.
STR_IN_RE_CONSUME - io.github.cvc5.ProofRewriteRule: Strings - regular expression membership consume \[ \mathit{str.in_re}(s, R) = b \] where $b$ is either $false$ or the result of stripping entailed prefixes and suffixes off of $s$ and $R$.
STR_IN_RE_CONTAINS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-contains
STR_IN_RE_EVAL - io.github.cvc5.ProofRewriteRule: Strings - regular expression membership evaluation \[ \mathit{str.in\_re}(s, R) = c \] where $s$ is a constant string, $R$ is a constant regular expression and $c$ is true or false.
STR_IN_RE_INTER_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-inter-elim
STR_IN_RE_RANGE_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-range-elim
STR_IN_RE_REQ_UNFOLD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-req-unfold
STR_IN_RE_REQ_UNFOLD_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-req-unfold-rev
STR_IN_RE_SIGMA - io.github.cvc5.ProofRewriteRule: Strings - string in regular expression sigma \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar})) = (\mathit{str.len}(s) = n) \] or alternatively: \[ \mathit{str.in\_re}(s, \mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}, \mathit{re}.\text{*}(\mathit{re.allchar}))) = (\mathit{str.len}(s) \ge n) \]
STR_IN_RE_SIGMA_STAR - io.github.cvc5.ProofRewriteRule: Strings - string in regular expression sigma star \[ \mathit{str.in\_re}(s, \mathit{re}.\text{*}(\mathit{re}.\text{++}(\mathit{re.allchar}, \ldots, \mathit{re.allchar}))) = (\mathit{str.len}(s) \ \% \ n = 0) \] where $n$ is the number of $\mathit{re.allchar}$ arguments to $\mathit{re}.\text{++}$.
STR_IN_RE_SKIP_UNFOLD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-skip-unfold
STR_IN_RE_SKIP_UNFOLD_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-skip-unfold-rev
STR_IN_RE_STRIP_CHAR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-char
STR_IN_RE_STRIP_CHAR_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-char-rev
STR_IN_RE_STRIP_CHAR_S_SINGLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-char-s-single
STR_IN_RE_STRIP_CHAR_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-char-s-single-rev
STR_IN_RE_STRIP_PREFIX - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix
STR_IN_RE_STRIP_PREFIX_BASE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base
STR_IN_RE_STRIP_PREFIX_BASE_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-neg
STR_IN_RE_STRIP_PREFIX_BASE_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-neg-rev
STR_IN_RE_STRIP_PREFIX_BASE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-rev
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-neg-rev
STR_IN_RE_STRIP_PREFIX_BASE_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-base-s-single-rev
STR_IN_RE_STRIP_PREFIX_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-neg
STR_IN_RE_STRIP_PREFIX_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-neg-rev
STR_IN_RE_STRIP_PREFIX_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-rev
STR_IN_RE_STRIP_PREFIX_S_SINGLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-s-single
STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg
STR_IN_RE_STRIP_PREFIX_S_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-s-single-neg-rev
STR_IN_RE_STRIP_PREFIX_S_SINGLE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-s-single-rev
STR_IN_RE_STRIP_PREFIX_SR_SINGLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-sr-single
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-neg-rev
STR_IN_RE_STRIP_PREFIX_SR_SINGLE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-sr-single-rev
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-srs-single
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_NEG_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-neg-rev
STR_IN_RE_STRIP_PREFIX_SRS_SINGLE_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-strip-prefix-srs-single-rev
STR_IN_RE_TEST_UNFOLD - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-test-unfold
STR_IN_RE_TEST_UNFOLD_REV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-test-unfold-rev
STR_IN_RE_UNION_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-in-re-union-elim
STR_INDEXOF_NO_CONTAINS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-indexof-no-contains
STR_INDEXOF_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-indexof-self
STR_LEN_CONCAT_REC - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-concat-rec
STR_LEN_REPLACE_INV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-replace-inv
STR_LEN_SUBSTR_IN_RANGE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-substr-in-range
STR_LEN_SUBSTR_UB1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-substr-ub1
STR_LEN_SUBSTR_UB2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-substr-ub2
STR_LEN_UPDATE_INV - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-len-update-inv
STR_NTH_ELIM_CODE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-nth-elim-code
STR_PREFIXOF_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-prefixof-elim
STR_PREFIXOF_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-prefixof-one
STR_REPLACE_EMPTY - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-replace-empty
STR_REPLACE_NO_CONTAINS - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-replace-no-contains
STR_REPLACE_SELF - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-replace-self
STR_SUBSTR_COMBINE1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-combine1
STR_SUBSTR_COMBINE2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-combine2
STR_SUBSTR_COMBINE3 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-combine3
STR_SUBSTR_COMBINE4 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-combine4
STR_SUBSTR_CONCAT1 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-concat1
STR_SUBSTR_CONCAT2 - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-concat2
STR_SUBSTR_EMPTY_RANGE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-empty-range
STR_SUBSTR_EMPTY_START - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-empty-start
STR_SUBSTR_EMPTY_START_NEG - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-empty-start-neg
STR_SUBSTR_EMPTY_STR - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-empty-str
STR_SUBSTR_EQ_EMPTY - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-eq-empty
STR_SUBSTR_FULL - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-full
STR_SUBSTR_FULL_EQ - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-full-eq
STR_SUBSTR_LEN_INCLUDE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-len-include
STR_SUBSTR_LEN_INCLUDE_PRE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-len-include-pre
STR_SUBSTR_LEN_SKIP - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-substr-len-skip
STR_SUFFIXOF_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-suffixof-elim
STR_SUFFIXOF_ONE - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-suffixof-one
STR_TO_LOWER_CONCAT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-to-lower-concat
STR_TO_LOWER_UPPER - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-to-lower-upper
STR_TO_UPPER_CONCAT - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-to-upper-concat
STR_TO_UPPER_LOWER - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule str-to-upper-lower
STRING_CHARAT - io.github.cvc5.Kind: String character at.
STRING_CODE_INJ - io.github.cvc5.ProofRule: Strings – Code points \[ \inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t = s} \]
STRING_CONCAT - io.github.cvc5.Kind: String concat.
STRING_CONTAINS - io.github.cvc5.Kind: String contains.
STRING_DECOMPOSE - io.github.cvc5.ProofRule: Strings – Core rules – String decomposition \[ \inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n} \] where $w_1$ is the purification skolem for $\mathit{pre}(t,n)$ and $w_2$ is the purification skolem for $\mathit{suf}(t,n)$.
STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule: Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where $R$ is $\texttt{TermRegistry::eagerReduce}(t)$.
STRING_FROM_CODE - io.github.cvc5.Kind: String from code.
STRING_FROM_INT - io.github.cvc5.Kind: Conversion from Int to String.
STRING_IN_REGEXP - io.github.cvc5.Kind: String membership.
STRING_INDEXOF - io.github.cvc5.Kind: String index-of.
STRING_INDEXOF_RE - io.github.cvc5.Kind: String index-of regular expression match.
STRING_IS_DIGIT - io.github.cvc5.Kind: String is-digit.
STRING_LENGTH - io.github.cvc5.Kind: String length.
STRING_LENGTH_NON_EMPTY - io.github.cvc5.ProofRule: Strings – Core rules – Length non-empty \[ \inferrule{t\neq \epsilon\mid -}{\mathit{len}(t) \neq 0} \]
STRING_LENGTH_POS - io.github.cvc5.ProofRule: Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= \epsilon)\vee \mathit{len}(t) > 0} \]
STRING_LEQ - io.github.cvc5.Kind: String less than or equal.
STRING_LT - io.github.cvc5.Kind: String less than.
STRING_PREFIX - io.github.cvc5.Kind: String prefix-of.
STRING_REDUCTION - io.github.cvc5.ProofRule: Strings – Extended functions – Reduction \[ \inferrule{-\mid t}{R\wedge t = w} \] where $w$ is $\texttt{StringsPreprocess::reduce}(t, R, \dots)$.
STRING_REPLACE - io.github.cvc5.Kind: String replace.
STRING_REPLACE_ALL - io.github.cvc5.Kind: String replace all.
STRING_REPLACE_RE - io.github.cvc5.Kind: String replace regular expression match.
STRING_REPLACE_RE_ALL - io.github.cvc5.Kind: String replace all regular expression matches.
STRING_REV - io.github.cvc5.Kind: String reverse.
STRING_SEQ_UNIT_INJ - io.github.cvc5.ProofRule: Strings – Sequence unit \[ \inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y} \] Also applies to the case where $\mathit{unit}(y)$ is a constant sequence of length one.
STRING_SORT - io.github.cvc5.SortKind: The string sort.
STRING_SUBSTR - io.github.cvc5.Kind: String substring.
STRING_SUFFIX - io.github.cvc5.Kind: String suffix-of.
STRING_TO_CODE - io.github.cvc5.Kind: String to code.
STRING_TO_INT - io.github.cvc5.Kind: String to integer (total function).
STRING_TO_LOWER - io.github.cvc5.Kind: String to lower case.
STRING_TO_REGEXP - io.github.cvc5.Kind: Conversion from string to regexp.
STRING_TO_UPPER - io.github.cvc5.Kind: String to upper case.
STRING_UPDATE - io.github.cvc5.Kind: String update.
STRINGS_DEQ_DIFF - io.github.cvc5.SkolemId: Difference index for string disequalities, such that k is the witness for the inference (=> (not (= a b)) (not (= (substr a k 1) (substr b k 1)))) where note that `k` may be out of bounds for at most of a,b.
STRINGS_ITOS_RESULT - io.github.cvc5.SkolemId: A function used to define intermediate results of str.from_int applications.
STRINGS_NUM_OCCUR - io.github.cvc5.SkolemId: An integer corresponding to the number of times a string occurs in another string.
STRINGS_NUM_OCCUR_RE - io.github.cvc5.SkolemId: Analogous to STRINGS_NUM_OCCUR, but for regular expressions.
STRINGS_OCCUR_INDEX - io.github.cvc5.SkolemId: A function k such that for x = 0...n, (k x) is the end index of the x^th occurrence of a string b in string a, where n is the number of occurrences of b in a, and (= (k 0) 0).
STRINGS_OCCUR_INDEX_RE - io.github.cvc5.SkolemId: Analogous to STRINGS_OCCUR_INDEX, but for regular expressions.
STRINGS_OCCUR_LEN_RE - io.github.cvc5.SkolemId: A function k where for x = 0...n, (k x) is the length of the x^th occurrence of R in a (excluding matches of empty strings) where R is a regular expression, n is the number of occurrences of R in a, and (= (k 0) 0).
STRINGS_REPLACE_ALL_RESULT - io.github.cvc5.SkolemId: A function used to define intermediate results of str.replace_all and str.replace_re_all applications.
STRINGS_STOI_NON_DIGIT - io.github.cvc5.SkolemId: A position containing a non-digit in a string, used when (str.to_int a) is equal to -1.
STRINGS_STOI_RESULT - io.github.cvc5.SkolemId: A function used to define intermediate results of str.from_int applications.
stringValue() - Method in class io.github.cvc5.OptionInfo: Obtain the current value as a string.
SUB - io.github.cvc5.Kind: Arithmetic subtraction, left associative.
SUBS - io.github.cvc5.ProofRule: Builtin theory – Substitution \[ \inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)} \] where $\sigma_{ids}(F_i)$ are substitutions, which notice are applied in reverse order.
substitute(Sort[], Sort[]) - Method in class io.github.cvc5.Sort: Simultaneous substitution of Sorts.
substitute(Sort, Sort) - Method in class io.github.cvc5.Sort: Substitution of Sorts.
substitute(Term[], Term[]) - Method in class io.github.cvc5.Term: Simultaneously replace terms with replacements in this term.
substitute(Term, Term) - Method in class io.github.cvc5.Term: Replace term with replacement in this term.
SYGUS_2_1 - io.github.cvc5.modes.InputLanguage: The SyGuS version 2.1 language.
SymbolManager - Class in io.github.cvc5
SymbolManager(Solver) - Constructor for class io.github.cvc5.SymbolManager: Deprecated.
This function is deprecated and replaced by Solver(TermManager). It will be removed in a future release.
SymbolManager(TermManager) - Constructor for class io.github.cvc5.SymbolManager: Create symbol manager instance.
SYMM - io.github.cvc5.ProofRule: Equality – Symmetry \[ \inferrule{t_1 = t_2\mid -}{t_2 = t_1} \] or \[ \inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1} \]
synthFun(String, Term[], Sort) - Method in class io.github.cvc5.Solver: Synthesize n-ary function.
synthFun(String, Term[], Sort, Grammar) - Method in class io.github.cvc5.Solver: Synthesize n-ary function following specified syntactic constraints.
SynthResult - Class in io.github.cvc5: Encapsulation of a solver synth result.
SynthResult() - Constructor for class io.github.cvc5.SynthResult: Null synthResult

T

TABLE_AGGREGATE - io.github.cvc5.Kind: Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ...
TABLE_GROUP - io.github.cvc5.Kind: Table group $((\_ \; table.group \; n_1 \; \dots \; n_k) \; A)$ partitions tuples of table $A$ such that tuples that have the same projection with indices $n_1 \; \dots \; n_k$ are in the same part.
TABLE_JOIN - io.github.cvc5.Kind: Table join operator has the form $((\_ \; table.join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)$ where $m_1 \; n_1 \; \dots \; m_k \; n_k$ are natural numbers, and $A, B$ are tables.
TABLE_PRODUCT - io.github.cvc5.Kind: Table cross product.
TABLE_PROJECT - io.github.cvc5.Kind: Table projection operator extends tuple projection operator to tables.
TABLES_GROUP_PART - io.github.cvc5.SkolemId: Given a group term ((_ table.group n1 ... nk) A) of type (Bag (Table T)), this skolem maps elements of A to their parts in the resulting partition.
TABLES_GROUP_PART_ELEMENT - io.github.cvc5.SkolemId: Given a group term ((_ table.group n1 ... nk) A) of type (Bag (Table T)) and a part B of type (Table T), this function returns a skolem element that is a member of B if B is not empty.
TANGENT - io.github.cvc5.Kind: Tangent function.
Term - Class in io.github.cvc5: A cvc5 Term.
Term() - Constructor for class io.github.cvc5.Term: Null term
Term.ConstIterator - Class in io.github.cvc5
termManager - Variable in class io.github.cvc5.AbstractPlugin
TermManager - Class in io.github.cvc5: A cvc5 term manager.
TermManager() - Constructor for class io.github.cvc5.TermManager: Create a term manager instance.
THEORY_LEMMAS - io.github.cvc5.modes.ProofComponent: Proofs of L1 ...
THEORY_REWRITE - io.github.cvc5.ProofRule: Other theory rewrite rules \[ \inferrule{- \mid id, t = t'}{t = t'} \] where `id` is the ProofRewriteRule of the theory rewrite rule which transforms $t$ to $t'$.
third - Variable in class io.github.cvc5.Triplet
TIMEOUT - io.github.cvc5.UnknownExplanation: Time limit reached.
TO_INTEGER - io.github.cvc5.Kind: Convert Term of sort Int or Real to Int via the floor function.
TO_REAL - io.github.cvc5.Kind: Convert Term of Sort Int or Real to Real.
toString() - Method in class io.github.cvc5.OptionInfo
toString(long) - Method in class io.github.cvc5.Command
toString(long) - Method in class io.github.cvc5.Datatype
toString(long) - Method in class io.github.cvc5.DatatypeConstructor
toString(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
toString(long) - Method in class io.github.cvc5.DatatypeDecl
toString(long) - Method in class io.github.cvc5.DatatypeSelector
toString(long) - Method in class io.github.cvc5.Grammar
toString(long) - Method in class io.github.cvc5.InputParser
toString(long) - Method in class io.github.cvc5.Op
toString(long) - Method in class io.github.cvc5.OptionInfo
toString(long) - Method in class io.github.cvc5.Result
toString(long) - Method in class io.github.cvc5.Solver
toString(long) - Method in class io.github.cvc5.Sort
toString(long) - Method in class io.github.cvc5.Stat
toString(long) - Method in class io.github.cvc5.Statistics
toString(long) - Method in class io.github.cvc5.SymbolManager
toString(long) - Method in class io.github.cvc5.SynthResult
toString(long) - Method in class io.github.cvc5.Term
toString(long) - Method in class io.github.cvc5.TermManager
TRANS - io.github.cvc5.ProofRule: Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
TRANSCENDENTAL_PURIFY - io.github.cvc5.SkolemId: A function introduced to eliminate extended trancendental functions.
TRANSCENDENTAL_PURIFY_ARG - io.github.cvc5.SkolemId: Argument used to purify trancendental function app (f x).
TRANSCENDENTAL_SINE_PHASE_SHIFT - io.github.cvc5.SkolemId: Argument used to reason about the phase shift of arguments to sine.
Triplet<A,B,C> - Class in io.github.cvc5
Triplet(A, B, C) - Constructor for class io.github.cvc5.Triplet
TRUE_ELIM - io.github.cvc5.ProofRule: Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
TRUE_INTRO - io.github.cvc5.ProofRule: Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
TRUST - io.github.cvc5.ProofRule: Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where $tid$ is an identifier and $F$ is a formula.
TRUST_THEORY_REWRITE - io.github.cvc5.ProofRule: Trusted rules – Theory rewrite \[ \inferrule{- \mid F, tid, rid}{F} \] where $F$ is an equality of the form $t = t'$ where $t'$ is obtained by applying the kind of rewriting given by the method identifier $rid$, which is one of: RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT.
TUPLE_PROJECT - io.github.cvc5.Kind: Tuple projection.
TUPLE_SORT - io.github.cvc5.SortKind: A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.

U

UF_BV2NAT_GEQ_ELIM - io.github.cvc5.ProofRewriteRule: Auto-generated from RARE rule uf-bv2nat-geq-elim
UNDEFINED_KIND - io.github.cvc5.Kind: Undefined kind.
UNDEFINED_SORT_KIND - io.github.cvc5.SortKind: Undefined kind.
UNINTERPRETED_SORT - io.github.cvc5.SortKind: An uninterpreted sort.
UNINTERPRETED_SORT_VALUE - io.github.cvc5.Kind: The value of an uninterpreted constant.
UNKNOWN - io.github.cvc5.modes.InputLanguage: No language given.
UNKNOWN - io.github.cvc5.modes.LearnedLitType: Special case for when produce-learned-literals is not set.
UNKNOWN - io.github.cvc5.ProofRule: External – Alethe Place holder for Alethe rules.
UNKNOWN_REASON - io.github.cvc5.UnknownExplanation: No specific reason given.
UnknownExplanation - Enum in io.github.cvc5
UNSUPPORTED - io.github.cvc5.UnknownExplanation: Unsupported feature encountered.
Utils - Class in io.github.cvc5
Utils() - Constructor for class io.github.cvc5.Utils

V

validateUnsigned(int[], String) - Static method in class io.github.cvc5.Utils
validateUnsigned(int, String) - Static method in class io.github.cvc5.Utils
validateUnsigned(long[], String) - Static method in class io.github.cvc5.Utils
validateUnsigned(long, String) - Static method in class io.github.cvc5.Utils
ValueInfo(T, T) - Constructor for class io.github.cvc5.OptionInfo.ValueInfo
valueOf(String) - Static method in enum io.github.cvc5.Kind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.BlockModelsMode: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.FindSynthTarget: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.InputLanguage: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.LearnedLitType: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.ProofComponent: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.modes.ProofFormat: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.ProofRewriteRule: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.ProofRule: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.RoundingMode: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.SkolemId: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.SortKind: Returns the enum constant of this type with the specified name.
valueOf(String) - Static method in enum io.github.cvc5.UnknownExplanation: Returns the enum constant of this type with the specified name.
values() - Static method in enum io.github.cvc5.Kind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.BlockModelsMode: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.FindSynthTarget: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.InputLanguage: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.LearnedLitType: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.ProofComponent: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.modes.ProofFormat: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.ProofRewriteRule: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.ProofRule: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.RoundingMode: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.SkolemId: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.SortKind: Returns an array containing the constants of this enum type, in the order they are declared.
values() - Static method in enum io.github.cvc5.UnknownExplanation: Returns an array containing the constants of this enum type, in the order they are declared.
VALUES - io.github.cvc5.modes.BlockModelsMode: Block models based on the concrete model values for the free variables.
VARIABLE - io.github.cvc5.Kind: (Bound) variable.
VARIABLE_LIST - io.github.cvc5.Kind: Variable list.
VoidInfo() - Constructor for class io.github.cvc5.OptionInfo.VoidInfo

W

WITNESS - io.github.cvc5.Kind: Witness.

X

XOR - io.github.cvc5.Kind: Logical exclusive disjunction, left associative.
XOR_ELIM1 - io.github.cvc5.ProofRule: Boolean – XOR elimination version 1 \[ \inferrule{F_1 \xor F_2 \mid -}{F_1 \lor F_2} \]
XOR_ELIM2 - io.github.cvc5.ProofRule: Boolean – XOR elimination version 2 \[ \inferrule{F_1 \xor F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
xorTerm(Term) - Method in class io.github.cvc5.Term: Boolean exclusive or.

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