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

A

ABS - io.github.cvc5.Kind
Absolute value.
ABSTRACT_SORT - io.github.cvc5.SortKind
An abstract sort.
ADD - io.github.cvc5.Kind
Arithmetic addition.
addAnyConstant(Term) - Method in class io.github.cvc5.Grammar
Allow ntSymbol to be an arbitrary constant.
addAnyVariable(Term) - Method in class io.github.cvc5.Grammar
Allow ntSymbol to be any input variable to corresponding synth-fun or synth-inv with the same sort as ntSymbol.
addConstructor(DatatypeConstructorDecl) - Method in class io.github.cvc5.DatatypeDecl
Add datatype constructor declaration.
addRule(Term, Term) - Method in class io.github.cvc5.Grammar
Add rule to the set of rules corresponding to ntSymbol.
addRules(long, long, long[]) - Method in class io.github.cvc5.Grammar
 
addRules(Term, Term[]) - Method in class io.github.cvc5.Grammar
Add rules to the set of rules corresponding to ntSymbol.
addSelector(String, Sort) - Method in class io.github.cvc5.DatatypeConstructorDecl
Add datatype selector declaration.
addSelectorSelf(String) - Method in class io.github.cvc5.DatatypeConstructorDecl
Add datatype selector declaration whose codomain type is the datatype itself.
addSelectorUnresolved(String, String) - Method in class io.github.cvc5.DatatypeConstructorDecl
Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.
addSygusAssume(Term) - Method in class io.github.cvc5.Solver
Add a forumla to the set of Sygus assumptions.
addSygusConstraint(Term) - Method in class io.github.cvc5.Solver
Add a forumla to the set of Sygus constraints.
addSygusInvConstraint(Term, Term, Term, Term) - Method in class io.github.cvc5.Solver
Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.
ALETHE - io.github.cvc5.modes.ProofFormat
Output Alethe proof.
ALETHE_RULE - io.github.cvc5.ProofRule
External – Alethe Place holder for Alethe rules.
ALF_RULE - io.github.cvc5.ProofRule
External – AletheLF Place holder for AletheLF rules.
ALPHA_EQUIV - io.github.cvc5.ProofRule
Quantifiers – Alpha equivalence \[ \inferruleSC{-\mid F, y_1=z_1,\dots, y_n=z_n} {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} \] Notice that this rule is correct only when \(z_1,\dots,z_n\) are not contained in \(FV(F) \setminus \{ y_1,\dots, y_n \}\), where \(FV(\varphi)\) are the free variables of \(\varphi\).
AND - io.github.cvc5.Kind
Logical conjunction.
AND_ELIM - io.github.cvc5.ProofRule
Boolean – And elimination \[ \inferrule{(F_1 \land \dots \land F_n) \mid i}{F_i} \]
AND_INTRO - io.github.cvc5.ProofRule
Boolean – And introduction \[ \inferrule{F_1 \dots F_n \mid -}{(F_1 \land \dots \land F_n)} \]
andTerm(Term) - Method in class io.github.cvc5.Term
Boolean and.
ANNOTATION - io.github.cvc5.ProofRule
Builtin theory – Annotation \[ \inferrule{F \mid a_1 \dots a_n}{F} \] The terms \(a_1 \dots a_n\) can be anything used to annotate the proof node, one example is where \(a_1\) is a theory.InferenceId.
appendIncrementalStringInput(String) - Method in class io.github.cvc5.InputParser
Append string to the input being parsed by this parser.
apply(Term[]) - Method in interface io.github.cvc5.IOracle
 
APPLY_CONSTRUCTOR - io.github.cvc5.Kind
Datatype constructor application.
APPLY_SELECTOR - io.github.cvc5.Kind
Datatype selector application.
APPLY_TESTER - io.github.cvc5.Kind
Datatype tester application.
APPLY_UF - io.github.cvc5.Kind
Application of an uninterpreted function.
APPLY_UPDATER - io.github.cvc5.Kind
Datatype update application.
ARCCOSECANT - io.github.cvc5.Kind
Arc cosecant function.
ARCCOSINE - io.github.cvc5.Kind
Arc cosine function.
ARCCOTANGENT - io.github.cvc5.Kind
Arc cotangent function.
ARCSECANT - io.github.cvc5.Kind
Arc secant function.
ARCSINE - io.github.cvc5.Kind
Arc sine function.
ARCTANGENT - io.github.cvc5.Kind
Arc tangent function.
ARITH_MULT_NEG - io.github.cvc5.ProofRule
Arithmetic – Multiplication with negative factor \[ \inferrule{- \mid m, l \diamond r}{(m < 0 \land l \diamond r) \rightarrow m \cdot l \diamond_{inv} m \cdot r} \] where \(\diamond\) is a relation symbol and \(\diamond_{inv}\) the inverted relation symbol.
ARITH_MULT_POS - io.github.cvc5.ProofRule
Arithmetic – Multiplication with positive factor \[ \inferrule{- \mid m, l \diamond r}{(m > 0 \land l \diamond r) \rightarrow m \cdot l \diamond m \cdot r} \] where \(\diamond\) is a relation symbol.
ARITH_MULT_SIGN - io.github.cvc5.ProofRule
Arithmetic – Sign inference \[ \inferrule{- \mid f_1 \dots f_k, m}{(f_1 \land \dots \land f_k) \rightarrow m \diamond 0} \] where \(f_1 \dots f_k\) are variables compared to zero (less, greater or not equal), \(m\) is a monomial from these variables and \(\diamond\) is the comparison (less or equal) that results from the signs of the variables.
ARITH_MULT_TANGENT - io.github.cvc5.ProofRule
Arithmetic – Multiplication tangent plane \[ \inferruleSC{- \mid t, x, y, a, b, \sigma}{(t \leq tplane) \leftrightarrow ((x \leq a \land y \geq b) \lor (x \geq a \land y \leq b))}{if $\sigma = -1$} \inferruleSC{- \mid t, x, y, a, b, \sigma}{(t \geq tplane) \leftrightarrow ((x \leq a \land y \leq b) \lor (x \geq a \land y \geq b))}{if $\sigma = 1$} \] where \(x,y\) are real terms (variables or extended terms), \(t = x \cdot y\) (possibly under rewriting), \(a,b\) are real constants, \(\sigma \in \{ 1, -1\}\) and \(tplane := b \cdot x + a \cdot y - a \cdot b\) is the tangent plane of \(x \cdot y\) at \((a,b)\).
ARITH_NL_COVERING_DIRECT - io.github.cvc5.ProofRule
Arithmetic – Coverings – Direct conflict We use \(\texttt{IRP}_k(poly)\) for an IndexedRootPredicate that is defined as the \(k\)'th root of the polynomial \(poly\).
ARITH_NL_COVERING_RECURSIVE - io.github.cvc5.ProofRule
Arithmetic – Coverings – Recursive interval See ARITH_NL_COVERING_DIRECT <cvc5.ProofRule.ARITH_NL_COVERING_DIRECT> for the necessary definitions.
ARITH_OP_ELIM_AXIOM - io.github.cvc5.ProofRule
Arithmetic – Operator elimination \[ \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}} \]
ARITH_POLY_NORM - io.github.cvc5.ProofRule
Arithmetic – Polynomial normalization \[ \inferrule{- \mid t = s}{t = s} \] where \(\texttt{arith::PolyNorm::isArithPolyNorm(t, s)} = \top\).
ARITH_SUM_UB - io.github.cvc5.ProofRule
Arithmetic – Sum upper bounds \[ \inferrule{P_1 \dots P_n \mid -}{L \diamond R} \] where \(P_i\) has the form \(L_i \diamond_i R_i\) and \(\diamond_i \in \{<, \leq, =\}\).
ARITH_TRANS_EXP_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is approximated from above for negative values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant}(\exp, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\).
ARITH_TRANS_EXP_APPROX_ABOVE_POS - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is approximated from above for positive values \[ \inferrule{- \mid d,t,l,u}{(t \geq l \land t \leq u) \rightarrow exp(t) \leq \texttt{secant-pos}(\exp, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term and \(l,u\) are lower and upper bounds on \(t\).
ARITH_TRANS_EXP_APPROX_BELOW - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is approximated from below \[ \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)} \] where \(d\) is an odd positive number, \(t\) an arithmetic term and \(\texttt{maclaurin}(\exp, d, c)\) is the \(d\)'th taylor polynomial at zero (also called the Maclaurin series) of the exponential function evaluated at \(c\).
ARITH_TRANS_EXP_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp at negative values \[ \inferrule{- \mid t}{(t < 0) \leftrightarrow (\exp(t) < 1)} \]
ARITH_TRANS_EXP_POSITIVITY - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is always positive \[ \inferrule{- \mid t}{\exp(t) > 0} \]
ARITH_TRANS_EXP_SUPER_LIN - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp grows super-linearly for positive values \[ \inferrule{- \mid t}{t \leq 0 \lor \exp(t) > t+1} \]
ARITH_TRANS_EXP_ZERO - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp at zero \[ \inferrule{- \mid t}{(t=0) \leftrightarrow (\exp(t) = 1)} \]
ARITH_TRANS_PI - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Assert bounds on Pi \[ \inferrule{- \mid l, u}{\texttt{real.pi} \geq l \land \texttt{real.pi} \leq u} \] where \(l,u\) are valid lower and upper bounds on \(\pi\).
ARITH_TRANS_SINE_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from above for negative values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{secant}(\sin, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\).
ARITH_TRANS_SINE_APPROX_ABOVE_POS - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from above for positive values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \leq \texttt{upper}(\sin, c)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)).
ARITH_TRANS_SINE_APPROX_BELOW_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from below for negative values \[ \inferrule{- \mid d,t,c,lb,ub}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{lower}(\sin, c)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(c\) an arithmetic constant and \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)).
ARITH_TRANS_SINE_APPROX_BELOW_POS - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from below for positive values \[ \inferrule{- \mid d,t,lb,ub,l,u}{(t \geq lb land t \leq ub) \rightarrow \sin(t) \geq \texttt{secant}(\sin, l, u, t)} \] where \(d\) is an even positive number, \(t\) an arithmetic term, \(lb,ub\) are symbolic lower and upper bounds on \(t\) (possibly containing \(\pi\)) and \(l,u\) the evaluated lower and upper bounds on \(t\).
ARITH_TRANS_SINE_BOUNDS - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is always between -1 and 1 \[ \inferrule{- \mid t}{\sin(t) \leq 1 \land \sin(t) \geq -1} \]
ARITH_TRANS_SINE_SHIFT - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is shifted to -pi...pi \[ \inferrule{- \mid x, y, s}{-\pi \leq y \leq \pi \land \sin(y) = \sin(x) \land (\ite{-\pi \leq x \leq \pi}{x = y}{x = y + 2 \pi s})} \] where \(x\) is the argument to sine, \(y\) is a new real skolem that is \(x\) shifted into \(-\pi \dots \pi\) and \(s\) is a new integer slolem that is the number of phases \(y\) is shifted.
ARITH_TRANS_SINE_SYMMETRY - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is symmetric with respect to negation of the argument \[ \inferrule{- \mid t}{\sin(t) - \sin(-t) = 0} \]
ARITH_TRANS_SINE_TANGENT_PI - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is bounded by the tangents at -pi and pi ..
ARITH_TRANS_SINE_TANGENT_ZERO - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is bounded by the tangent at zero ..
ARITH_TRICHOTOMY - io.github.cvc5.ProofRule
Arithmetic – Trichotomy of the reals \[ \inferrule{A, B \mid C}{C} \] where \(\neg A, \neg B, C\) are \(x < c, x = c, x > c\) in some order.
ARRAY_SORT - io.github.cvc5.SortKind
An array sort, whose argument sorts are the index and element sorts of the array.
ARRAYS_EQ_RANGE_EXPAND - io.github.cvc5.ProofRule
Arrays – Expansion of array range equality \[ \inferrule{-\mid \mathit{eqrange}(a,b,i,j)} {\mathit{eqrange}(a,b,i,j)= \forall x.\> i \leq x \leq j \rightarrow \mathit{select}(a,x)=\mathit{select}(b,x)} \]
ARRAYS_EXT - io.github.cvc5.ProofRule
Arrays – Arrays extensionality \[ \inferrule{a \neq b\mid -} {\mathit{select}(a,k)\neq\mathit{select}(b,k)} \] where \(k\) is \(\texttt{arrays::SkolemCache::getExtIndexSkolem}(a\neq b)\).
ARRAYS_READ_OVER_WRITE - io.github.cvc5.ProofRule
Arrays – Read over write \[ \inferrule{i_1 \neq i_2\mid \mathit{select}(\mathit{store}(a,i_1,e),i_2)} {\mathit{select}(\mathit{store}(a,i_1,e),i_2) = \mathit{select}(a,i_2)} \]
ARRAYS_READ_OVER_WRITE_1 - io.github.cvc5.ProofRule
Arrays – Read over write 1 \[ \inferrule{-\mid \mathit{select}(\mathit{store}(a,i,e),i)} {\mathit{select}(\mathit{store}(a,i,e),i)=e} \]
ARRAYS_READ_OVER_WRITE_CONTRA - io.github.cvc5.ProofRule
Arrays – Read over write, contrapositive \[ \inferrule{\mathit{select}(\mathit{store}(a,i_2,e),i_1) \neq \mathit{select}(a,i_1)\mid -}{i_1=i_2} \]
assertFormula(Term) - Method in class io.github.cvc5.Solver
Assert a formula.
ASSUME - io.github.cvc5.ProofRule
Assumption (a leaf) \[ \inferrule{- \mid F}{F} \] This rule has special status, in that an application of assume is an open leaf in a proof that is not (yet) justified.

B

BAG_CARD - io.github.cvc5.Kind
Bag cardinality.
BAG_CHOOSE - io.github.cvc5.Kind
Bag choose.
BAG_COUNT - io.github.cvc5.Kind
Bag element multiplicity.
BAG_DIFFERENCE_REMOVE - io.github.cvc5.Kind
Bag difference remove.
BAG_DIFFERENCE_SUBTRACT - io.github.cvc5.Kind
Bag difference subtract.
BAG_DUPLICATE_REMOVAL - io.github.cvc5.Kind
Bag duplicate removal.
BAG_EMPTY - io.github.cvc5.Kind
Empty bag.
BAG_FILTER - io.github.cvc5.Kind
Bag filter.
BAG_FOLD - io.github.cvc5.Kind
Bag fold.
BAG_FROM_SET - io.github.cvc5.Kind
Conversion from set to bag.
BAG_INTER_MIN - io.github.cvc5.Kind
Bag intersection (min).
BAG_IS_SINGLETON - io.github.cvc5.Kind
Bag is singleton tester.
BAG_MAKE - io.github.cvc5.Kind
Bag make.
BAG_MAP - io.github.cvc5.Kind
Bag map.
BAG_MEMBER - io.github.cvc5.Kind
Bag membership predicate.
BAG_PARTITION - io.github.cvc5.Kind
Bag partition.
BAG_SORT - io.github.cvc5.SortKind
A bag sort, whose argument sort is the element sort of the bag.
BAG_SUBBAG - io.github.cvc5.Kind
Bag inclusion predicate.
BAG_TO_SET - io.github.cvc5.Kind
Conversion from bag to set.
BAG_UNION_DISJOINT - io.github.cvc5.Kind
Bag disjoint union (sum).
BAG_UNION_MAX - io.github.cvc5.Kind
Bag max union.
BaseInfo() - Constructor for class io.github.cvc5.OptionInfo.BaseInfo
 
BETA_REDUCE - io.github.cvc5.ProofRule
Equality – Beta reduction \[ \inferrule{\mid \lambda x_1\dots x_n.\> t, t_1,\dots,t_n} {((\lambda x_1\dots x_n.\> t) t_1 \ldots t_n)=t\{x_1\mapsto t_1,\dots,x_n\mapsto t_n\}} \] The right hand side of the equality in the conclusion is computed using standard substitution via Node.substitute.
BITVECTOR_ADD - io.github.cvc5.Kind
Addition of two or more bit-vectors.
BITVECTOR_AND - io.github.cvc5.Kind
Bit-wise and.
BITVECTOR_ASHR - io.github.cvc5.Kind
Bit-vector arithmetic shift right.
BITVECTOR_COMP - io.github.cvc5.Kind
Equality comparison (returns bit-vector of size 1).
BITVECTOR_CONCAT - io.github.cvc5.Kind
Concatenation of two or more bit-vectors.
BITVECTOR_EXTRACT - io.github.cvc5.Kind
Bit-vector extract.
BITVECTOR_ITE - io.github.cvc5.Kind
Bit-vector if-then-else.
BITVECTOR_LSHR - io.github.cvc5.Kind
Bit-vector logical shift right.
BITVECTOR_MULT - io.github.cvc5.Kind
Multiplication of two or more bit-vectors.
BITVECTOR_NAND - io.github.cvc5.Kind
Bit-wise nand.
BITVECTOR_NEG - io.github.cvc5.Kind
Negation of a bit-vector (two's complement).
BITVECTOR_NEGO - io.github.cvc5.Kind
Bit-vector negation overflow detection.
BITVECTOR_NOR - io.github.cvc5.Kind
Bit-wise nor.
BITVECTOR_NOT - io.github.cvc5.Kind
Bit-wise negation.
BITVECTOR_OR - io.github.cvc5.Kind
Bit-wise or.
BITVECTOR_REDAND - io.github.cvc5.Kind
Bit-vector redand.
BITVECTOR_REDOR - io.github.cvc5.Kind
Bit-vector redor.
BITVECTOR_REPEAT - io.github.cvc5.Kind
Bit-vector repeat.
BITVECTOR_ROTATE_LEFT - io.github.cvc5.Kind
Bit-vector rotate left.
BITVECTOR_ROTATE_RIGHT - io.github.cvc5.Kind
Bit-vector rotate right.
BITVECTOR_SADDO - io.github.cvc5.Kind
Bit-vector signed addition overflow detection.
BITVECTOR_SDIV - io.github.cvc5.Kind
Signed bit-vector division.
BITVECTOR_SDIVO - io.github.cvc5.Kind
Bit-vector signed division overflow detection.
BITVECTOR_SGE - io.github.cvc5.Kind
Bit-vector signed greater than or equal.
BITVECTOR_SGT - io.github.cvc5.Kind
Bit-vector signed greater than.
BITVECTOR_SHL - io.github.cvc5.Kind
Bit-vector shift left.
BITVECTOR_SIGN_EXTEND - io.github.cvc5.Kind
Bit-vector sign extension.
BITVECTOR_SLE - io.github.cvc5.Kind
Bit-vector signed less than or equal.
BITVECTOR_SLT - io.github.cvc5.Kind
Bit-vector signed less than.
BITVECTOR_SLTBV - io.github.cvc5.Kind
Bit-vector signed less than returning a bit-vector of size 1.
BITVECTOR_SMOD - io.github.cvc5.Kind
Signed bit-vector remainder (sign follows divisor).
BITVECTOR_SMULO - io.github.cvc5.Kind
Bit-vector signed multiplication overflow detection.
BITVECTOR_SORT - io.github.cvc5.SortKind
A bit-vector sort, parameterized by an integer denoting its bit-width.
BITVECTOR_SREM - io.github.cvc5.Kind
Signed bit-vector remainder (sign follows dividend).
BITVECTOR_SSUBO - io.github.cvc5.Kind
Bit-vector signed subtraction overflow detection.
BITVECTOR_SUB - io.github.cvc5.Kind
Subtraction of two bit-vectors.
BITVECTOR_TO_NAT - io.github.cvc5.Kind
Bit-vector conversion to (non-negative) integer.
BITVECTOR_UADDO - io.github.cvc5.Kind
Bit-vector unsigned addition overflow detection.
BITVECTOR_UDIV - io.github.cvc5.Kind
Unsigned bit-vector division.
BITVECTOR_UGE - io.github.cvc5.Kind
Bit-vector unsigned greater than or equal.
BITVECTOR_UGT - io.github.cvc5.Kind
Bit-vector unsigned greater than.
BITVECTOR_ULE - io.github.cvc5.Kind
Bit-vector unsigned less than or equal.
BITVECTOR_ULT - io.github.cvc5.Kind
Bit-vector unsigned less than.
BITVECTOR_ULTBV - io.github.cvc5.Kind
Bit-vector unsigned less than returning a bit-vector of size 1.
BITVECTOR_UMULO - io.github.cvc5.Kind
Bit-vector unsigned multiplication overflow detection.
BITVECTOR_UREM - io.github.cvc5.Kind
Unsigned bit-vector remainder.
BITVECTOR_USUBO - io.github.cvc5.Kind
Bit-vector unsigned subtraction overflow detection.
BITVECTOR_XNOR - io.github.cvc5.Kind
Bit-wise xnor, left associative.
BITVECTOR_XOR - io.github.cvc5.Kind
Bit-wise xor.
BITVECTOR_ZERO_EXTEND - io.github.cvc5.Kind
Bit-vector zero extension.
blockModel(BlockModelsMode) - Method in class io.github.cvc5.Solver
Block the current model.
BlockModelsMode - Enum in io.github.cvc5.modes
 
blockModelValues(Term[]) - Method in class io.github.cvc5.Solver
Block the current model values of (at least) the values in terms.
BOOLEAN_SORT - io.github.cvc5.SortKind
The Boolean sort.
booleanValue() - Method in class io.github.cvc5.OptionInfo
Obtain the current value as a Boolean.
BV_BITBLAST_STEP - io.github.cvc5.ProofRule
Bit-vectors – Bitblast bit-vector constant, variable, and terms For constant and variables: \[ \inferrule{-\mid t}{t = \texttt{bitblast}(t)} \] For terms: \[ \inferrule{-\mid k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n))} {k(\texttt{bitblast}(t_1),\dots,\texttt{bitblast}(t_n)) = \texttt{bitblast}(t)} \] where \(t\) is \(k(t_1,\dots,t_n)\).
BV_EAGER_ATOM - io.github.cvc5.ProofRule
Bit-vectors – Bit-vector eager atom \[ \inferrule{-\mid F}{F = F[0]} \] where \(F\) is of kind BITVECTOR_EAGER_ATOM.

C

CARDINALITY_CONSTRAINT - io.github.cvc5.Kind
Cardinality constraint on uninterpreted sort.
CHAIN_RESOLUTION - io.github.cvc5.ProofRule
Boolean – N-ary Resolution \[ \inferrule{C_1 \dots C_n \mid pol_1,L_1 \dots pol_{n-1},L_{n-1}}{C} \] where let \(C_1 \dots C_n\) be nodes viewed as clauses, as defined above let \(C_1 \diamond_{L,\mathit{pol}} C_2\) represent the resolution of \(C_1\) with \(C_2\) with pivot \(L\) and polarity \(pol\), as defined above let \(C_1' = C_1\), for each \(i > 1\), let \(C_i' = C_{i-1} \diamond{L_{i-1}, \mathit{pol}_{i-1}} C_i'\) The result of the chain resolution is \(C = C_n'\)
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_CPROP - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation constant propagation \[ \inferrule{(t_1\cdot w_1\cdot t_2) = (w_2 \cdot s),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = w_3\cdot r)} \] where \(w_1,\,w_2,\,w_3\) are words, \(w_3\) is \(\mathit{pre}(w_2,p)\), \(p\) is \(\texttt{Word::overlap}(\mathit{suf}(w_2,1), w_1)\), and \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(w_3)))\).
CONCAT_CSPLIT - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation split for constants \[ \inferrule{(t_1\cdot t_2) = (c \cdot s_2),\, \mathit{len}(t_1) \neq 0\mid \bot}{(t_1 = c\cdot r)} \] where \(r\) is \(\mathit{skolem}(\mathit{suf}(t_1,1))\).
CONCAT_EQ - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation equality \[ \inferrule{(t_1\cdot\ldots \cdot t_n \cdot t) = (t_1 \cdot\ldots \cdot t_n\cdot s)\mid b}{t = s} \] where \(\cdot\) stands for string concatenation and \(b\) indicates if the direction is reversed.
CONCAT_LPROP - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation length propagation \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) > \mathit{len}(s_1)\mid \bot}{(t_1 = s_1\cdot r_t)} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\).
CONCAT_SPLIT - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation split \[ \inferruleSC{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) \neq \mathit{len}(s_1)\mid b}{(t_1 = s_1\cdot r_t) \vee (s_1 = t_1\cdot r_s)}{if $b=\bot$} \] where \(r_t\) is \(\mathit{skolem}(\mathit{suf}(t_1,\mathit{len}(s_1)))\) and \(r_s\) is \(\mathit{skolem}(\mathit{suf}(s_1,\mathit{len}(t_1)))\).
CONCAT_UNIFY - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation unification \[ \inferrule{(t_1\cdot t_2) = (s_1 \cdot s_2),\, \mathit{len}(t_1) = \mathit{len}(s_1)\mid b}{t_1 = s_1} \] where \(b\) indicates if the direction is reversed.
CONG - io.github.cvc5.ProofRule
Equality – Congruence \[ \inferrule{t_1=s_1,\dots,t_n=s_n\mid k, f?}{k(f?)(t_1,\dots, t_n) = k(f?)(s_1,\dots, s_n)} \] where \(k\) is the application kind.
CONST_ARRAY - io.github.cvc5.Kind
Constant array.
CONST_BITVECTOR - io.github.cvc5.Kind
Fixed-size bit-vector constant.
CONST_BOOLEAN - io.github.cvc5.Kind
Boolean constant.
CONST_FINITE_FIELD - io.github.cvc5.Kind
Finite field constant.
CONST_FLOATINGPOINT - io.github.cvc5.Kind
Floating-point constant, created from IEEE-754 bit-vector representation of the floating-point value.
CONST_INTEGER - io.github.cvc5.Kind
Arbitrary-precision integer constant.
CONST_RATIONAL - io.github.cvc5.Kind
Arbitrary-precision rational constant.
CONST_ROUNDINGMODE - io.github.cvc5.Kind
RoundingMode constant.
CONST_SEQUENCE - io.github.cvc5.Kind
Constant sequence.
CONST_STRING - io.github.cvc5.Kind
Constant string.
CONSTANT - io.github.cvc5.Kind
Free constant symbol.
CONSTANT_PROP - io.github.cvc5.modes.LearnedLitType
An internal literal that can be made into a constant propagation for an input term.
ConstIterator() - Constructor for class io.github.cvc5.Datatype.ConstIterator
 
ConstIterator() - Constructor for class io.github.cvc5.DatatypeConstructor.ConstIterator
 
ConstIterator() - Constructor for class io.github.cvc5.Statistics.ConstIterator
 
ConstIterator() - Constructor for class io.github.cvc5.Term.ConstIterator
 
ConstIterator(boolean, boolean) - Constructor for class io.github.cvc5.Statistics.ConstIterator
 
Context - Class in io.github.cvc5
 
Context() - Constructor for class io.github.cvc5.Context
 
CONTRA - io.github.cvc5.ProofRule
Boolean – Contradiction \[ \inferrule{F, \neg F \mid -}{\bot} \]
COSECANT - io.github.cvc5.Kind
Cosecant function.
COSINE - io.github.cvc5.Kind
Cosine function.
COTANGENT - io.github.cvc5.Kind
Cotangent function.
CVC5ApiException - Exception in io.github.cvc5
 
CVC5ApiException(String) - Constructor for exception io.github.cvc5.CVC5ApiException
 
CVC5ApiOptionException - Exception in io.github.cvc5
 
CVC5ApiOptionException(String) - Constructor for exception io.github.cvc5.CVC5ApiOptionException
 
CVC5ApiRecoverableException - Exception in io.github.cvc5
 
CVC5ApiRecoverableException(String) - Constructor for exception io.github.cvc5.CVC5ApiRecoverableException
 
CVC5ParserException - Exception in io.github.cvc5
 
CVC5ParserException(String) - Constructor for exception io.github.cvc5.CVC5ParserException
 

D

Datatype - Class in io.github.cvc5
A cvc5 datatype.
DATATYPE_SORT - io.github.cvc5.SortKind
A datatype sort.
Datatype.ConstIterator - Class in io.github.cvc5
 
DatatypeConstructor - Class in io.github.cvc5
A cvc5 datatype constructor.
DatatypeConstructor.ConstIterator - Class in io.github.cvc5
 
DatatypeConstructorDecl - Class in io.github.cvc5
A cvc5 datatype constructor declaration.
DatatypeDecl - Class in io.github.cvc5
A cvc5 datatype declaration.
DatatypeDecl() - Constructor for class io.github.cvc5.DatatypeDecl
Null datatypeDecl
DatatypeSelector - Class in io.github.cvc5
A cvc5 datatype selector.
declareDatatype(String, DatatypeConstructorDecl[]) - Method in class io.github.cvc5.Solver
Create datatype sort.
declareFun(String, Sort[], Sort) - Method in class io.github.cvc5.Solver
Declare n-ary function symbol.
declareFun(String, Sort[], Sort, boolean) - Method in class io.github.cvc5.Solver
Declare n-ary function symbol.
declareOracleFun(String, Sort[], Sort, IOracle) - Method in class io.github.cvc5.Solver
Declare an oracle function with reference to an implementation.
declarePool(String, Sort, Term[]) - Method in class io.github.cvc5.Solver
Declare a symbolic pool of terms with the given initial value.
declareSepHeap(Sort, Sort) - Method in class io.github.cvc5.Solver
When using separation logic, this sets the location sort and the datatype sort to the given ones.
declareSort(String, int) - Method in class io.github.cvc5.Solver
Declare uninterpreted sort.
declareSort(String, int, boolean) - Method in class io.github.cvc5.Solver
Declare uninterpreted sort.
declareSygusVar(String, Sort) - Method in class io.github.cvc5.Solver
Append symbol to the current list of universal variables.
DEFAULT - io.github.cvc5.modes.ProofFormat
Use the proof format mode set in the solver options.
defineFun(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver
Define n-ary function in the current context.
defineFun(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver
Define n-ary function.
defineFunRec(Term, Term[], Term) - Method in class io.github.cvc5.Solver
Define recursive function in the current context.
defineFunRec(Term, Term[], Term, boolean) - Method in class io.github.cvc5.Solver
Define recursive function.
defineFunRec(String, Term[], Sort, Term) - Method in class io.github.cvc5.Solver
Define recursive function in the current context.
defineFunRec(String, Term[], Sort, Term, boolean) - Method in class io.github.cvc5.Solver
Define recursive function.
defineFunsRec(Term[], Term[][], Term[]) - Method in class io.github.cvc5.Solver
Define recursive functions in the current context.
defineFunsRec(Term[], Term[][], Term[], boolean) - Method in class io.github.cvc5.Solver
Define recursive functions.
deletePointer() - Method in class io.github.cvc5.Proof
 
deletePointer(long) - Method in class io.github.cvc5.Command
 
deletePointer(long) - Method in class io.github.cvc5.Datatype
 
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructor
 
deletePointer(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
 
deletePointer(long) - Method in class io.github.cvc5.DatatypeDecl
 
deletePointer(long) - Method in class io.github.cvc5.DatatypeSelector
 
deletePointer(long) - Method in class io.github.cvc5.Grammar
 
deletePointer(long) - Method in class io.github.cvc5.InputParser
 
deletePointer(long) - Method in class io.github.cvc5.Op
 
deletePointer(long) - Method in class io.github.cvc5.OptionInfo
 
deletePointer(long) - Method in class io.github.cvc5.Proof
 
deletePointer(long) - Method in class io.github.cvc5.Result
 
deletePointer(long) - Method in class io.github.cvc5.Solver
 
deletePointer(long) - Method in class io.github.cvc5.Sort
 
deletePointer(long) - Method in class io.github.cvc5.Stat
 
deletePointer(long) - Method in class io.github.cvc5.Statistics
 
deletePointer(long) - Method in class io.github.cvc5.SymbolManager
 
deletePointer(long) - Method in class io.github.cvc5.SynthResult
 
deletePointer(long) - Method in class io.github.cvc5.Term
 
deletePointers() - Static method in class io.github.cvc5.Context
Delete all cpp pointers for terms, sorts, etc
DISTINCT - io.github.cvc5.Kind
Disequality.
DIVISIBLE - io.github.cvc5.Kind
Operator for the divisibility-by-\(k\) predicate.
DIVISION - io.github.cvc5.Kind
Real division, division by 0 undefined, left associative.
done() - Method in class io.github.cvc5.InputParser
 
DOT - io.github.cvc5.modes.ProofFormat
Output DOT proof.
doubleValue() - Method in class io.github.cvc5.OptionInfo
Obtain the current value as a double.
DSL_REWRITE - io.github.cvc5.ProofRule
Builtin theory – DSL rewrite \[ \inferrule{F_1 \dots F_n \mid id t_1 \dots t_n}{F} \] where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n.
DT_CLASH - io.github.cvc5.ProofRule
Datatypes – Clash \[ \inferruleSC{\mathit{is}_{C_i}(t), \mathit{is}_{C_j}(t)\mid -}{\bot} {if $i\neq j$} \]
DT_COLLAPSE - io.github.cvc5.ProofRule
Datatypes – Collapse \[ \inferrule{-\mid \mathit{sel}_i(C_j(t_1,\dots,t_n))}{ \mathit{sel}_i(C_j(t_1,\dots,t_n)) = r} \] where \(C_j\) is a constructor, \(r\) is \(t_i\) if \(\mathit{sel}_i\) is a correctly applied selector, or {@link TypeNode#mkGroundTerm()} of the proper type otherwise.
DT_INST - io.github.cvc5.ProofRule
Datatypes – Instantiation \[ \inferrule{-\mid t,n}{\mathit{is}_C(t) = (t = C(\mathit{sel}_1(t),\dots,\mathit{sel}_n(t)))} \] where \(C\) is the \(n^{\mathit{th}}\) constructor of the type of t, and \(\mathit{is}_C\) is the discriminator (tester) for \(C\).
DT_SPLIT - io.github.cvc5.ProofRule
Datatypes – Split \[ \inferrule{-\mid t}{\mathit{is}_{C_1}(t)\vee\cdots\vee\mathit{is}_{C_n}(t)} \] where \(C_1,\dots,C_n\) are all the constructors of the type of \(t\).
DT_UNIF - io.github.cvc5.ProofRule
Datatypes – Unification \[ \inferrule{C(t_1,\dots,t_n)= C(s_1,\dots,s_n)\mid i}{t_1 = s_i} \] where \(C\) is a constructor.

E

ENCODE_PRED_TRANSFORM - io.github.cvc5.ProofRule
Builtin theory – Encode predicate transformation \[ \inferrule{F \mid G}{G} \] where \(F\) and \(G\) are equivalent up to their encoding in an external proof format.
ENUM - io.github.cvc5.modes.FindSynthTarget
Find the next term in the enumeration of the target grammar.
EQ_RANGE - io.github.cvc5.Kind
Equality over arrays \(a\) and \(b\) over a given range \([i,j]\), i.e., \[ \forall k .
EQ_RESOLVE - io.github.cvc5.ProofRule
Boolean – Equality resolution \[ \inferrule{F_1, (F_1 = F_2) \mid -}{F_2} \] Note this can optionally be seen as a macro for EQUIV_ELIM1 <cvc5.ProofRule.EQUIV_ELIM1> + RESOLUTION <cvc5.ProofRule.RESOLUTION>.
eqTerm(Term) - Method in class io.github.cvc5.Term
Equality.
EQUAL - io.github.cvc5.Kind
Equality, chainable.
equals(Object) - Method in class io.github.cvc5.Op
Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Pair
 
equals(Object) - Method in class io.github.cvc5.Result
Operator overloading for equality of two results.
equals(Object) - Method in class io.github.cvc5.Solver
 
equals(Object) - Method in class io.github.cvc5.Sort
Comparison for structural equality.
equals(Object) - Method in class io.github.cvc5.SymbolManager
 
equals(Object) - Method in class io.github.cvc5.Term
Syntactic equality operator.
equals(Object) - Method in class io.github.cvc5.Triplet
 
EQUIV_ELIM1 - io.github.cvc5.ProofRule
Boolean – Equivalence elimination version 1 \[ \inferrule{F_1 = F_2 \mid -}{\neg F_1 \lor F_2} \]
EQUIV_ELIM2 - io.github.cvc5.ProofRule
Boolean – Equivalence elimination version 2 \[ \inferrule{F_1 = F_2 \mid -}{F_1 \lor \neg F_2} \]
EVALUATE - io.github.cvc5.ProofRule
Builtin theory – Evaluate \[ \inferrule{- \mid t}{t = \texttt{Evaluator::evaluate}(t)} \] Note this is equivalent to: (REWRITE t {@link MethodId#RW_EVALUATE)}.
EXISTS - io.github.cvc5.Kind
Existentially quantified formula.
EXPONENTIAL - io.github.cvc5.Kind
Exponential function.

F

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

G

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

H

hasNext() - Method in class io.github.cvc5.Datatype.ConstIterator
 
hasNext() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
 
hasNext() - Method in class io.github.cvc5.Statistics.ConstIterator
 
hasNext() - Method in class io.github.cvc5.Term.ConstIterator
 
hasNoSolution() - Method in class io.github.cvc5.SynthResult
 
hasOp() - Method in class io.github.cvc5.Term
 
hasSolution() - Method in class io.github.cvc5.SynthResult
 
hasSymbol() - Method in class io.github.cvc5.Sort
 
hasSymbol() - Method in class io.github.cvc5.Term
 
HO_APP_ENCODE - io.github.cvc5.ProofRule
Equality – Higher-order application encoding \[ \inferrule{-\mid t}{t= \texttt{TheoryUfRewriter::getHoApplyForApplyUf}(t)} \] For example, this rule concludes \(f(x,y) = @(@(f,x),y)\), where \(@\) isthe HO_APPLY kind.
HO_APPLY - io.github.cvc5.Kind
Higher-order applicative encoding of function application, left associative.
HO_CONG - io.github.cvc5.ProofRule
Equality – Higher-order congruence \[ \inferrule{f=g, t_1=s_1,\dots,t_n=s_n\mid -}{f(t_1,\dots, t_n) = g(s_1,\dots, s_n)} \] Notice that this rule is only used when the application kinds are APPLY_UF.

I

IAND - io.github.cvc5.Kind
Integer and.
IMPLIES - io.github.cvc5.Kind
Logical implication.
IMPLIES_ELIM - io.github.cvc5.ProofRule
Boolean – Implication elimination \[ \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 optional argument \(id\) indicates the inference id that caused the instantiation.
INT_TIGHT_LB - io.github.cvc5.ProofRule
Arithmetic – Tighten strict integer lower bounds \[ \inferrule{i > c \mid -}{i \geq \lceil c \rceil} \] where \(i\) has integer type.
INT_TIGHT_UB - io.github.cvc5.ProofRule
Arithmetic – Tighten strict integer upper bounds \[ \inferrule{i < c \mid -}{i \leq \lfloor c \rfloor} \] where \(i\) has integer type.
INT_TO_BITVECTOR - io.github.cvc5.Kind
Conversion from Int to bit-vector.
INTEGER_SORT - io.github.cvc5.SortKind
The integer sort.
INTERNAL - io.github.cvc5.modes.LearnedLitType
Any internal literal that does not fall into the above categories.
INTERNAL_KIND - io.github.cvc5.Kind
Internal kind.
INTERNAL_SORT_KIND - io.github.cvc5.SortKind
Internal kind.
INTERRUPTED - io.github.cvc5.UnknownExplanation
Solver was interrupted.
INTS_DIVISION - io.github.cvc5.Kind
Integer division, division by 0 undefined, left associative.
INTS_MODULUS - io.github.cvc5.Kind
Integer modulus, modulus by 0 undefined.
intValue() - Method in class io.github.cvc5.OptionInfo
Obtain the current value as as int.
invoke(Solver, SymbolManager) - Method in class io.github.cvc5.Command
Invoke the command on the solver and symbol manager sm, prints the result to output stream out.
io.github.cvc5 - package io.github.cvc5
 
io.github.cvc5.modes - package io.github.cvc5.modes
 
IOracle - Interface in io.github.cvc5
 
IS_INTEGER - io.github.cvc5.Kind
Is-integer predicate.
isAbstract() - Method in class io.github.cvc5.Sort
Determine if this is an abstract sort.
isArray() - Method in class io.github.cvc5.Sort
Determine if this is an array sort.
isBag() - Method in class io.github.cvc5.Sort
Determine if this is a Bag sort.
isBitVector() - Method in class io.github.cvc5.Sort
Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).
isBitVectorValue() - Method in class io.github.cvc5.Term
 
isBoolean() - Method in class io.github.cvc5.Sort
Determine if this is the Boolean sort (SMT-LIB: Bool).
isBooleanValue() - Method in class io.github.cvc5.Term
 
isCardinalityConstraint() - Method in class io.github.cvc5.Term
 
isCodatatype() - Method in class io.github.cvc5.Datatype
 
isConstArray() - Method in class io.github.cvc5.Term
 
isDatatype() - Method in class io.github.cvc5.Sort
Determine if this is a datatype sort.
isDatatypeConstructor() - Method in class io.github.cvc5.Sort
Determine if this is a datatype constructor sort.
isDatatypeSelector() - Method in class io.github.cvc5.Sort
Determine if this is a datatype selector sort.
isDatatypeTester() - Method in class io.github.cvc5.Sort
Determine if this is a datatype tester sort.
isDatatypeUpdater() - Method in class io.github.cvc5.Sort
Determine if this is a datatype updater sort.
isDefault() - Method in class io.github.cvc5.Stat
Does this value hold the default value?
isDouble() - Method in class io.github.cvc5.Stat
Is this value a double?
isFinite() - Method in class io.github.cvc5.Datatype
 
isFiniteField() - Method in class io.github.cvc5.Sort
Determine if this is a finite field sort (SMT-LIB: (_ FiniteField i)).
isFiniteFieldValue() - Method in class io.github.cvc5.Term
 
isFloatingPoint() - Method in class io.github.cvc5.Sort
Determine if this is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)).
isFloatingPointNaN() - Method in class io.github.cvc5.Term
 
isFloatingPointNegInf() - Method in class io.github.cvc5.Term
 
isFloatingPointNegZero() - Method in class io.github.cvc5.Term
 
isFloatingPointPosInf() - Method in class io.github.cvc5.Term
 
isFloatingPointPosZero() - Method in class io.github.cvc5.Term
 
isFloatingPointValue() - Method in class io.github.cvc5.Term
 
isFunction() - Method in class io.github.cvc5.Sort
Determine if this is a function sort.
isHistogram() - Method in class io.github.cvc5.Stat
Is this value a histogram?
isIndexed() - Method in class io.github.cvc5.Op
 
isInstantiated() - Method in class io.github.cvc5.Sort
Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
isInt() - Method in class io.github.cvc5.Stat
Is this value an integer?
isInteger() - Method in class io.github.cvc5.Sort
Determine if this is the integer sort (SMT-LIB: Int).
isIntegerValue() - Method in class io.github.cvc5.Term
 
isInternal() - Method in class io.github.cvc5.Stat
Is this value intended for internal use only?
isLogicSet() - Method in class io.github.cvc5.Solver
Is logic set? Returns whether we called setLogic yet for this solver.
isLogicSet() - Method in class io.github.cvc5.SymbolManager
 
isModelCoreSymbol(Term) - Method in class io.github.cvc5.Solver
This returns false if the model value of free constant v was not essential for showing the satisfiability of the last call to Solver.checkSat() using the current model.
isNull() - Method in class io.github.cvc5.Command
 
isNull() - Method in class io.github.cvc5.Datatype
 
isNull() - Method in class io.github.cvc5.DatatypeConstructor
 
isNull() - Method in class io.github.cvc5.DatatypeConstructorDecl
 
isNull() - Method in class io.github.cvc5.DatatypeDecl
 
isNull() - Method in class io.github.cvc5.DatatypeSelector
 
isNull() - Method in class io.github.cvc5.Op
 
isNull() - Method in class io.github.cvc5.Result
 
isNull() - Method in class io.github.cvc5.Sort
Determine if this is the null sort.
isNull() - Method in class io.github.cvc5.SynthResult
 
isNull() - Method in class io.github.cvc5.Term
 
isParametric() - Method in class io.github.cvc5.Datatype
 
isParametric() - Method in class io.github.cvc5.DatatypeDecl
Determine if this datatype declaration is parametric.
isPredicate() - Method in class io.github.cvc5.Sort
Determine if this is a predicate sort.
isReal() - Method in class io.github.cvc5.Sort
Determine if this is the real sort (SMT-LIB: Real).
isRealAlgebraicNumber() - Method in class io.github.cvc5.Term
 
isRealValue() - Method in class io.github.cvc5.Term
 
isRecord() - Method in class io.github.cvc5.Datatype
 
isRecord() - Method in class io.github.cvc5.Sort
Determine if this is a record sort.
isRegExp() - Method in class io.github.cvc5.Sort
Determine if this is the regular expression sort (SMT-LIB: RegLan).
isRoundingMode() - Method in class io.github.cvc5.Sort
Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).
isRoundingModeValue() - Method in class io.github.cvc5.Term
 
isSat() - Method in class io.github.cvc5.Result
 
isSequence() - Method in class io.github.cvc5.Sort
Determine if this is a Sequence sort.
isSequenceValue() - Method in class io.github.cvc5.Term
 
isSet() - Method in class io.github.cvc5.Sort
Determine if this is a Set sort.
isSetValue() - Method in class io.github.cvc5.Term
 
isString() - Method in class io.github.cvc5.Sort
Determine if this is the string sort (SMT-LIB: String)..
isString() - Method in class io.github.cvc5.Stat
Is this value a string?
isStringValue() - Method in class io.github.cvc5.Term
 
isTuple() - Method in class io.github.cvc5.Datatype
 
isTuple() - Method in class io.github.cvc5.Sort
Determine if this a tuple sort.
isTupleValue() - Method in class io.github.cvc5.Term
 
isUninterpretedSort() - Method in class io.github.cvc5.Sort
Determine if this is an uninterpreted sort.
isUninterpretedSortConstructor() - Method in class io.github.cvc5.Sort
Determine if this is an uninterpreted sort constructor.
isUninterpretedSortValue() - Method in class io.github.cvc5.Term
 
isUnknown() - Method in class io.github.cvc5.Result
 
isUnknown() - Method in class io.github.cvc5.SynthResult
 
isUnsat() - Method in class io.github.cvc5.Result
 
isWellFounded() - Method in class io.github.cvc5.Datatype
Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
ITE - io.github.cvc5.Kind
If-then-else.
ITE_ELIM1 - io.github.cvc5.ProofRule
Boolean – ITE elimination version 1 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor F_1} \]
ITE_ELIM2 - io.github.cvc5.ProofRule
Boolean – ITE elimination version 2 \[ \inferrule{(\ite{C}{F_1}{F_2}) \mid -}{C \lor F_2} \]
iterator() - Method in class io.github.cvc5.Datatype
 
iterator() - Method in class io.github.cvc5.DatatypeConstructor
 
iterator() - Method in class io.github.cvc5.Statistics
 
iterator() - Method in class io.github.cvc5.Term
 
iterator(boolean, boolean) - Method in class io.github.cvc5.Statistics
 
iteTerm(Term, Term) - Method in class io.github.cvc5.Term
If-then-else with this term as the Boolean condition.

K

Kind - Enum in io.github.cvc5
 

L

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

M

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

N

NEG - io.github.cvc5.Kind
Arithmetic negation.
next() - Method in class io.github.cvc5.Datatype.ConstIterator
 
next() - Method in class io.github.cvc5.DatatypeConstructor.ConstIterator
 
next() - Method in class io.github.cvc5.Statistics.ConstIterator
 
next() - Method in class io.github.cvc5.Term.ConstIterator
 
nextCommand() - Method in class io.github.cvc5.InputParser
Parse and return the next command.
nextTerm() - Method in class io.github.cvc5.InputParser
Parse and return the next term.
NONE - io.github.cvc5.modes.ProofFormat
Do not translate proof output.
NOT - io.github.cvc5.Kind
Logical negation.
NOT_AND - io.github.cvc5.ProofRule
Boolean – De Morgan – Not And \[ \inferrule{\neg(F_1 \land \dots \land F_n) \mid -}{\neg F_1 \lor \dots \lor \neg F_n} \]
NOT_EQUIV_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not Equivalence elimination version 1 \[ \inferrule{F_1 \neq F_2 \mid -}{F_1 \lor F_2} \]
NOT_EQUIV_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not Equivalence elimination version 2 \[ \inferrule{F_1 \neq F_2 \mid -}{\neg F_1 \lor \neg F_2} \]
NOT_IMPLIES_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not Implication elimination version 1 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{F_1} \]
NOT_IMPLIES_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not Implication elimination version 2 \[ \inferrule{\neg(F_1 \rightarrow F_2) \mid -}{\neg F_2} \]
NOT_ITE_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not ITE elimination version 1 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{\neg C \lor \neg F_1} \]
NOT_ITE_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not ITE elimination version 2 \[ \inferrule{\neg(\ite{C}{F_1}{F_2}) \mid -}{C \lor \neg F_2} \]
NOT_NOT_ELIM - io.github.cvc5.ProofRule
Boolean – Double negation elimination \[ \inferrule{\neg (\neg F) \mid -}{F} \]
NOT_OR_ELIM - io.github.cvc5.ProofRule
Boolean – Not Or elimination \[ \inferrule{\neg(F_1 \lor \dots \lor F_n) \mid i}{\neg F_i} \]
NOT_XOR_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not XOR elimination version 1 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{F_1 \lor \neg F_2} \]
NOT_XOR_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not XOR elimination version 2 \[ \inferrule{\neg(F_1 \xor F_2) \mid -}{\neg F_1 \lor F_2} \]
notTerm() - Method in class io.github.cvc5.Term
Boolean negation.
NULL_SORT - io.github.cvc5.SortKind
Null kind.
NULL_TERM - io.github.cvc5.Kind
Null kind.
NumberInfo(T, T, T, T) - Constructor for class io.github.cvc5.OptionInfo.NumberInfo
 

O

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

P

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

Q

QUERY - io.github.cvc5.modes.FindSynthTarget
Find a query over the given grammar.

R

RAW_PREPROCESS - io.github.cvc5.modes.ProofComponent
Proofs of G1 ...
RE_ELIM - io.github.cvc5.ProofRule
Strings – Regular expressions – Elimination \[ \inferrule{-\mid F,b}{F = \texttt{strings::RegExpElimination::eliminate}(F, b)} \] where \(b\) is a Boolean indicating whether we are using aggressive eliminations.
RE_INTER - io.github.cvc5.ProofRule
Strings – Regular expressions – Intersection \[ \inferrule{t\in R_1,\,t\in R_2\mid -}{t\in \mathit{inter}(R_1,R_2)} \]
RE_UNFOLD_NEG - io.github.cvc5.ProofRule
Strings – Regular expressions – Negative Unfold \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNeg}(t\not\in R)} \] corresponding to the one-step unfolding of the premise.
RE_UNFOLD_NEG_CONCAT_FIXED - io.github.cvc5.ProofRule
Strings – Regular expressions – Unfold negative concatenation, fixed \[ \inferrule{t\not\in R\mid -}{\texttt{RegExpOpr::reduceRegExpNegConcatFixed}(t\not\in R,L,i)} \] where \(\texttt{RegExpOpr::getRegExpConcatFixed}(t\not\in R, i) = L\), corresponding to the one-step unfolding of the premise, optimized for fixed length of component \(i\) of the regular expression concatenation \(R\).
RE_UNFOLD_POS - io.github.cvc5.ProofRule
Strings – Regular expressions – Positive Unfold \[ \inferrule{t\in R\mid -}{\texttt{RegExpOpr::reduceRegExpPos}(t\in R)} \] corresponding to the one-step unfolding of the premise.
REAL_SORT - io.github.cvc5.SortKind
The real sort.
REFL - io.github.cvc5.ProofRule
Equality – Reflexivity \[ \inferrule{-\mid t}{t = t} \]
REGEXP_ALL - io.github.cvc5.Kind
Regular expression all.
REGEXP_ALLCHAR - io.github.cvc5.Kind
Regular expression all characters.
REGEXP_COMPLEMENT - io.github.cvc5.Kind
Regular expression complement.
REGEXP_CONCAT - io.github.cvc5.Kind
Regular expression concatenation.
REGEXP_DIFF - io.github.cvc5.Kind
Regular expression difference.
REGEXP_INTER - io.github.cvc5.Kind
Regular expression intersection.
REGEXP_LOOP - io.github.cvc5.Kind
Regular expression loop.
REGEXP_NONE - io.github.cvc5.Kind
Regular expression none.
REGEXP_OPT - io.github.cvc5.Kind
Regular expression ?.
REGEXP_PLUS - io.github.cvc5.Kind
Regular expression +.
REGEXP_RANGE - io.github.cvc5.Kind
Regular expression range.
REGEXP_REPEAT - io.github.cvc5.Kind
Operator for regular expression repeat.
REGEXP_STAR - io.github.cvc5.Kind
Regular expression \*.
REGEXP_UNION - io.github.cvc5.Kind
Regular expression union.
REGLAN_SORT - io.github.cvc5.SortKind
The regular language sort.
RELATION_AGGREGATE - io.github.cvc5.Kind
Relation aggregate operator has the form \(((\_ \; rel.aggr \; n_1 ...
RELATION_GROUP - io.github.cvc5.Kind
Relation group \(((\_ \; rel.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of relation \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part.
RELATION_IDEN - io.github.cvc5.Kind
Relation identity.
RELATION_JOIN - io.github.cvc5.Kind
Relation join.
RELATION_JOIN_IMAGE - io.github.cvc5.Kind
Relation join image.
RELATION_PRODUCT - io.github.cvc5.Kind
Relation cartesian product.
RELATION_PROJECT - io.github.cvc5.Kind
Relation projection operator extends tuple projection operator to sets.
RELATION_TCLOSURE - io.github.cvc5.Kind
Relation transitive closure.
RELATION_TRANSPOSE - io.github.cvc5.Kind
Relation transpose.
REMOVE_TERM_FORMULA_AXIOM - io.github.cvc5.ProofRule
Processing rules – Remove Term Formulas Axiom \[ \inferrule{- \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)} \]
REORDERING - io.github.cvc5.ProofRule
Boolean – Reordering \[ \inferrule{C_1 \mid C_2}{C_2} \] where the set representations of \(C_1\) and \(C_2\) are the same and the number of literals in \(C_2\) is the same of that of \(C_1\).
REQUIRES_CHECK_AGAIN - io.github.cvc5.UnknownExplanation
Requires another satisfiability check
REQUIRES_FULL_CHECK - io.github.cvc5.UnknownExplanation
Full satisfiability check required (e.g., if only preprocessing was performed).
resetAssertions() - Method in class io.github.cvc5.Solver
Remove all assertions.
RESOLUTION - io.github.cvc5.ProofRule
Boolean – Resolution \[ \inferrule{C_1, C_2 \mid pol, L}{C} \] where \(C_1\) and \(C_2\) are nodes viewed as clauses, i.e., either an OR node with each children viewed as a literal or a node viewed as a literal.
RESOURCEOUT - io.github.cvc5.UnknownExplanation
Resource limit reached.
Result - Class in io.github.cvc5
Encapsulation of a three-valued solver result, with explanations.
Result() - Constructor for class io.github.cvc5.Result
Null result
REWRITE - io.github.cvc5.modes.FindSynthTarget
Find a pair of terms (t,s) in the target grammar which are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
REWRITE_INPUT - io.github.cvc5.modes.FindSynthTarget
Find a rewrite between pairs of terms (t,s) that are matchable with terms in the input assertions where t and s are equivalent but do not rewrite to the same term in the given rewriter (--sygus-rewrite=MODE).
REWRITE_UNSOUND - io.github.cvc5.modes.FindSynthTarget
Find a term t in the target grammar which rewrites to a term s that is not equivalent to it.
ROUND_NEAREST_TIES_TO_AWAY - io.github.cvc5.RoundingMode
Round to the nearest number away from zero.
ROUND_NEAREST_TIES_TO_EVEN - io.github.cvc5.RoundingMode
Round to the nearest even number.
ROUND_TOWARD_NEGATIVE - io.github.cvc5.RoundingMode
Round towards negative infinity (-oo).
ROUND_TOWARD_POSITIVE - io.github.cvc5.RoundingMode
Round towards positive infinity (SMT-LIB: +oo).
ROUND_TOWARD_ZERO - io.github.cvc5.RoundingMode
Round towards zero.
RoundingMode - Enum in io.github.cvc5
 
ROUNDINGMODE_SORT - io.github.cvc5.SortKind
The rounding mode sort.

S

SAT - io.github.cvc5.modes.ProofComponent
A proof of false whose free assumptions are Gu1, ...
SAT_REFUTATION - io.github.cvc5.ProofRule
SAT Refutation for assumption-based unsat cores \[ \inferrule{F_1 \dots F_n \mid -}{\bot} \] where \(F_1 \dots F_n\) correspond to the unsat core determined by the SAT solver.
SCOPE - io.github.cvc5.ProofRule
Scope (a binder for assumptions) \[ \inferruleSC{F \mid F_1 \dots F_n}{(F_1 \land \dots \land F_n) \Rightarrow F}{if $F\neq\bot$} \textrm{ or } \inferruleSC{F \mid F_1 \dots F_n}{\neg (F_1 \land \dots \land F_n)}{if $F=\bot$} \] This rule has a dual purpose with :cpp:enumerator:`ASSUME <cvc5.ProofRule.ASSUME>`.
SECANT - io.github.cvc5.Kind
Secant function.
second - Variable in class io.github.cvc5.Pair
 
second - Variable in class io.github.cvc5.Triplet
 
SELECT - io.github.cvc5.Kind
Array select.
SEP_EMP - io.github.cvc5.Kind
Separation logic empty heap.
SEP_NIL - io.github.cvc5.Kind
Separation logic nil.
SEP_PTO - io.github.cvc5.Kind
Separation logic points-to relation.
SEP_STAR - io.github.cvc5.Kind
Separation logic star.
SEP_WAND - io.github.cvc5.Kind
Separation logic magic wand.
SEQ_AT - io.github.cvc5.Kind
Sequence element at.
SEQ_CONCAT - io.github.cvc5.Kind
Sequence concat.
SEQ_CONTAINS - io.github.cvc5.Kind
Sequence contains.
SEQ_EXTRACT - io.github.cvc5.Kind
Sequence extract.
SEQ_INDEXOF - io.github.cvc5.Kind
Sequence index-of.
SEQ_LENGTH - io.github.cvc5.Kind
Sequence length.
SEQ_NTH - io.github.cvc5.Kind
Sequence nth.
SEQ_PREFIX - io.github.cvc5.Kind
Sequence prefix-of.
SEQ_REPLACE - io.github.cvc5.Kind
Sequence replace.
SEQ_REPLACE_ALL - io.github.cvc5.Kind
Sequence replace all.
SEQ_REV - io.github.cvc5.Kind
Sequence reverse.
SEQ_SUFFIX - io.github.cvc5.Kind
Sequence suffix-of.
SEQ_UNIT - io.github.cvc5.Kind
Sequence unit.
SEQ_UPDATE - io.github.cvc5.Kind
Sequence update.
SEQUENCE_SORT - io.github.cvc5.SortKind
A sequence sort, whose argument sort is the element sort of the sequence.
SET_CARD - io.github.cvc5.Kind
Set cardinality.
SET_CHOOSE - io.github.cvc5.Kind
Set choose.
SET_COMPLEMENT - io.github.cvc5.Kind
Set complement with respect to finite universe.
SET_COMPREHENSION - io.github.cvc5.Kind
Set comprehension A set comprehension is specified by a variable list \(x_1 ...
SET_EMPTY - io.github.cvc5.Kind
Empty set.
SET_FILTER - io.github.cvc5.Kind
Set filter.
SET_FOLD - io.github.cvc5.Kind
Set fold.
SET_INSERT - io.github.cvc5.Kind
The set obtained by inserting elements; Arity: n > 0 1..n-1: Terms of any Sort (must match the element sort of the given set Term) n: Term of set Sort Create Term of this Kind with: Solver.mkTerm(Kind, Term[]) Solver.mkTerm(Op, Term[]) Create Op of this kind with: Solver.mkOp(Kind, int[])
SET_INTER - io.github.cvc5.Kind
Set intersection.
SET_IS_SINGLETON - io.github.cvc5.Kind
Set is singleton tester.
SET_MAP - io.github.cvc5.Kind
Set map.
SET_MEMBER - io.github.cvc5.Kind
Set membership predicate.
SET_MINUS - io.github.cvc5.Kind
Set subtraction.
SET_SINGLETON - io.github.cvc5.Kind
Singleton set.
SET_SORT - io.github.cvc5.SortKind
A set sort, whose argument sort is the element sort of the set.
SET_SUBSET - io.github.cvc5.Kind
Subset predicate.
SET_UNION - io.github.cvc5.Kind
Set union.
SET_UNIVERSE - io.github.cvc5.Kind
Finite universe set.
setFileInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser
Set the input for the given file.
setIncrementalStringInput(InputLanguage, String) - Method in class io.github.cvc5.InputParser
Set that we will be feeding strings to this parser via appendIncrementalStringInput below.
setInfo(String, String) - Method in class io.github.cvc5.Solver
Set info.
setLogic(String) - Method in class io.github.cvc5.Solver
Set logic.
setOption(String, String) - Method in class io.github.cvc5.Solver
Set option.
setStringInput(InputLanguage, String, String) - Method in class io.github.cvc5.InputParser
Set the input to the given concrete input string.
SEXPR - io.github.cvc5.Kind
Symbolic expression.
simplify(Term) - Method in class io.github.cvc5.Solver
Simplify a formula without doing "much" work.
SINE - io.github.cvc5.Kind
Sine function.
SKOLEM_ADD_TO_POOL - io.github.cvc5.Kind
A skolemization-add-to-pool annotation.
SKOLEM_INTRO - io.github.cvc5.ProofRule
Quantifiers – Skolem introduction \[ \inferrule{-\mid k}{k = t} \] where \(t\) is the unpurified form of skolem \(k\).
SKOLEMIZE - io.github.cvc5.ProofRule
Quantifiers – Skolemization \[ \inferrule{\exists x_1\dots x_n.\> F\mid -}{F\sigma} \] or \[ \inferrule{\neg (\forall x_1\dots x_n.\> F)\mid -}{\neg F\sigma} \] where \(\sigma\) maps \(x_1,\dots,x_n\) to their representative skolems obtained by SkolemManager.mkSkolemize, returned in the skolems argument of that method.
SMT_LIB_2_6 - io.github.cvc5.modes.InputLanguage
The SMT-LIB version 2.6 language
SOLVABLE - io.github.cvc5.modes.LearnedLitType
An internal literal that is solvable for an input variable.
Solver - Class in io.github.cvc5
A cvc5 solver.
Solver() - Constructor for class io.github.cvc5.Solver
 
Sort - Class in io.github.cvc5
The sort of a cvc5 term.
Sort() - Constructor for class io.github.cvc5.Sort
Null sort
SortKind - Enum in io.github.cvc5
 
SPLIT - io.github.cvc5.ProofRule
Boolean – Split \[ \inferrule{- \mid F}{F \lor \neg F} \]
SQRT - io.github.cvc5.Kind
Square root.
Stat - Class in io.github.cvc5
Represents a snapshot of a single statistic value.
Statistics - Class in io.github.cvc5
 
Statistics.ConstIterator - Class in io.github.cvc5
 
STORE - io.github.cvc5.Kind
Array store.
STRING_CHARAT - io.github.cvc5.Kind
String character at.
STRING_CODE_INJ - io.github.cvc5.ProofRule
Strings – Code points \[ \inferrule{-\mid t,s}{\mathit{to\_code}(t) = -1 \vee \mathit{to\_code}(t) \neq \mathit{to\_code}(s) \vee t\neq s} \]
STRING_CONCAT - io.github.cvc5.Kind
String concat.
STRING_CONTAINS - io.github.cvc5.Kind
String contains.
STRING_DECOMPOSE - io.github.cvc5.ProofRule
Strings – Core rules – String decomposition \[ \inferrule{\mathit{len}(t) \geq n\mid \bot}{t = w_1\cdot w_2 \wedge \mathit{len}(w_1) = n} \] or alternatively for the reverse: \[ \inferrule{\mathit{len}(t) \geq n\mid \top}{t = w_1\cdot w_2 \wedge \mathit{len}(w_2) = n} \] where \(w_1\) is \(\mathit{skolem}(\mathit{pre}(t,n)\) and \(w_2\) is \(\mathit{skolem}(\mathit{suf}(t,n)\).
STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule
Strings – Extended functions – Eager reduction \[ \inferrule{-\mid t}{R} \] where \(R\) is \(\texttt{strings::TermRegistry::eagerReduce}(t)\).
STRING_FROM_CODE - io.github.cvc5.Kind
String from code.
STRING_FROM_INT - io.github.cvc5.Kind
Conversion from Int to String.
STRING_IN_REGEXP - io.github.cvc5.Kind
String membership.
STRING_INDEXOF - io.github.cvc5.Kind
String index-of.
STRING_INDEXOF_RE - io.github.cvc5.Kind
String index-of regular expression match.
STRING_IS_DIGIT - io.github.cvc5.Kind
String is-digit.
STRING_LENGTH - io.github.cvc5.Kind
String length.
STRING_LENGTH_NON_EMPTY - io.github.cvc5.ProofRule
Strings – Core rules – Length non-empty \[ \inferrule{t\neq ''\mid -}{\mathit{len}(t) \neq 0} \]
STRING_LENGTH_POS - io.github.cvc5.ProofRule
Strings – Core rules – Length positive \[ \inferrule{-\mid t}{(\mathit{len}(t) = 0\wedge t= '')\vee \mathit{len}(t) > 0} \]
STRING_LEQ - io.github.cvc5.Kind
String less than or equal.
STRING_LT - io.github.cvc5.Kind
String less than.
STRING_PREFIX - io.github.cvc5.Kind
String prefix-of.
STRING_REDUCTION - io.github.cvc5.ProofRule
Strings – Extended functions – Reduction \[ \inferrule{-\mid t}{R\wedge t = w} \] where \(w\) is \(\texttt{strings::StringsPreprocess::reduce}(t, R, \dots)\).
STRING_REPLACE - io.github.cvc5.Kind
String replace.
STRING_REPLACE_ALL - io.github.cvc5.Kind
String replace all.
STRING_REPLACE_RE - io.github.cvc5.Kind
String replace regular expression match.
STRING_REPLACE_RE_ALL - io.github.cvc5.Kind
String replace all regular expression matches.
STRING_REV - io.github.cvc5.Kind
String reverse.
STRING_SEQ_UNIT_INJ - io.github.cvc5.ProofRule
Strings – Sequence unit \[ \inferrule{\mathit{unit}(x) = \mathit{unit}(y)\mid -}{x = y} \] Also applies to the case where \(\mathit{unit}(y)\) is a constant sequence of length one.
STRING_SORT - io.github.cvc5.SortKind
The string sort.
STRING_SUBSTR - io.github.cvc5.Kind
String substring.
STRING_SUFFIX - io.github.cvc5.Kind
String suffix-of.
STRING_TO_CODE - io.github.cvc5.Kind
String to code.
STRING_TO_INT - io.github.cvc5.Kind
String to integer (total function).
STRING_TO_LOWER - io.github.cvc5.Kind
String to lower case.
STRING_TO_REGEXP - io.github.cvc5.Kind
Conversion from string to regexp.
STRING_TO_UPPER - io.github.cvc5.Kind
String to upper case.
STRING_UPDATE - io.github.cvc5.Kind
String update.
stringValue() - Method in class io.github.cvc5.OptionInfo
Obtain the current value as a string.
SUB - io.github.cvc5.Kind
Arithmetic subtraction, left associative.
SUBS - io.github.cvc5.ProofRule
Builtin theory – Substitution \[ \inferrule{F_1 \dots F_n \mid t, ids?}{t = t \circ \sigma_{ids}(F_n) \circ \cdots \circ \sigma_{ids}(F_1)} \] where \(\sigma_{ids}(F_i)\) are substitutions, which notice are applied in reverse order.
substitute(Sort[], Sort[]) - Method in class io.github.cvc5.Sort
Simultaneous substitution of Sorts.
substitute(Sort, Sort) - Method in class io.github.cvc5.Sort
Substitution of Sorts.
substitute(Term[], Term[]) - Method in class io.github.cvc5.Term
Simultaneously replace terms with replacements in this term.
substitute(Term, Term) - Method in class io.github.cvc5.Term
Replace term with replacement in this term.
SYGUS_2_1 - io.github.cvc5.modes.InputLanguage
The SyGuS version 2.1 language.
SymbolManager - Class in io.github.cvc5
 
SymbolManager(Solver) - Constructor for class io.github.cvc5.SymbolManager
 
SYMM - io.github.cvc5.ProofRule
Equality – Symmetry \[ \inferrule{t_1 = t_2\mid -}{t_2 = t_1} \] or \[ \inferrule{t_1 \neq t_2\mid -}{t_2 \neq t_1} \]
synthFun(String, Term[], Sort) - Method in class io.github.cvc5.Solver
Synthesize n-ary function.
synthFun(String, Term[], Sort, Grammar) - Method in class io.github.cvc5.Solver
Synthesize n-ary function following specified syntactic constraints.
SynthResult - Class in io.github.cvc5
Encapsulation of a solver synth result.
SynthResult() - Constructor for class io.github.cvc5.SynthResult
Null synthResult

T

TABLE_AGGREGATE - io.github.cvc5.Kind
Table aggregate operator has the form \(((\_ \; table.aggr \; n_1 ...
TABLE_GROUP - io.github.cvc5.Kind
Table group \(((\_ \; table.group \; n_1 \; \dots \; n_k) \; A)\) partitions tuples of table \(A\) such that tuples that have the same projection with indices \(n_1 \; \dots \; n_k\) are in the same part.
TABLE_JOIN - io.github.cvc5.Kind
Table join operator has the form \(((\_ \; table.join \; m_1 \; n_1 \; \dots \; m_k \; n_k) \; A \; B)\) where \(m_1 \; n_1 \; \dots \; m_k \; n_k\) are natural numbers, and \(A, B\) are tables.
TABLE_PRODUCT - io.github.cvc5.Kind
Table cross product.
TABLE_PROJECT - io.github.cvc5.Kind
Table projection operator extends tuple projection operator to tables.
TANGENT - io.github.cvc5.Kind
Tangent function.
Term - Class in io.github.cvc5
A cvc5 Term.
Term() - Constructor for class io.github.cvc5.Term
Null term
Term.ConstIterator - Class in io.github.cvc5
 
THEORY_LEMMAS - io.github.cvc5.modes.ProofComponent
Proofs of L1 ...
third - Variable in class io.github.cvc5.Triplet
 
TIMEOUT - io.github.cvc5.UnknownExplanation
Time limit reached.
TO_INTEGER - io.github.cvc5.Kind
Convert Term of sort Int or Real to Int via the floor function.
TO_REAL - io.github.cvc5.Kind
Convert Term of Sort Int or Real to Real.
toString() - Method in class io.github.cvc5.OptionInfo
 
toString(long) - Method in class io.github.cvc5.Command
 
toString(long) - Method in class io.github.cvc5.Datatype
 
toString(long) - Method in class io.github.cvc5.DatatypeConstructor
 
toString(long) - Method in class io.github.cvc5.DatatypeConstructorDecl
 
toString(long) - Method in class io.github.cvc5.DatatypeDecl
 
toString(long) - Method in class io.github.cvc5.DatatypeSelector
 
toString(long) - Method in class io.github.cvc5.Grammar
 
toString(long) - Method in class io.github.cvc5.InputParser
 
toString(long) - Method in class io.github.cvc5.Op
 
toString(long) - Method in class io.github.cvc5.OptionInfo
 
toString(long) - Method in class io.github.cvc5.Result
 
toString(long) - Method in class io.github.cvc5.Solver
 
toString(long) - Method in class io.github.cvc5.Sort
 
toString(long) - Method in class io.github.cvc5.Stat
 
toString(long) - Method in class io.github.cvc5.Statistics
 
toString(long) - Method in class io.github.cvc5.SymbolManager
 
toString(long) - Method in class io.github.cvc5.SynthResult
 
toString(long) - Method in class io.github.cvc5.Term
 
TRANS - io.github.cvc5.ProofRule
Equality – Transitivity \[ \inferrule{t_1=t_2,\dots,t_{n-1}=t_n\mid -}{t_1 = t_n} \]
Triplet<A,​B,​C> - Class in io.github.cvc5
 
Triplet(A, B, C) - Constructor for class io.github.cvc5.Triplet
 
TRUE_ELIM - io.github.cvc5.ProofRule
Equality – True elim \[ \inferrule{F=\top\mid -}{F} \]
TRUE_INTRO - io.github.cvc5.ProofRule
Equality – True intro \[ \inferrule{F\mid -}{F = \top} \]
TRUST - io.github.cvc5.ProofRule
Trusted rule \[ \inferrule{F_1 \dots F_n \mid tid, F, ...}{F} \] where \(tid\) is an identifier and \(F\) is a formula.
TRUST_THEORY_REWRITE - io.github.cvc5.ProofRule
Trusted rules – Theory rewrite \[ \inferrule{- \mid F, tid, rid}{F} \] where \(F\) is an equality of the form \(t = t'\) where \(t'\) is obtained by applying the kind of rewriting given by the method identifier \(rid\), which is one of: RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT.
TUPLE_PROJECT - io.github.cvc5.Kind
Tuple projection.
TUPLE_SORT - io.github.cvc5.SortKind
A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.

U

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

V

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

W

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