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 F,y1=z1,,yn=znF=F{y1z1,,ynzn}~if y1,,yn,z1,,zn are unique bound variables Notice that this rule is correct only when z1,,zn are not contained in FV(F){y1,,yn}, where FV(φ) are the free variables of φ.
AND - io.github.cvc5.Kind
Logical conjunction.
AND_ELIM - io.github.cvc5.ProofRule
Boolean – And elimination (F1Fn)iFi
AND_INTRO - io.github.cvc5.ProofRule
Boolean – And introduction F1Fn(F1Fn)
andTerm(Term) - Method in class io.github.cvc5.Term
Boolean and.
ANNOTATION - io.github.cvc5.ProofRule
Builtin theory – Annotation Fa1anF The terms a1an can be anything used to annotate the proof node, one example is where a1 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 m,lr(m<0lr)mlinvmr where is a relation symbol and inv the inverted relation symbol.
ARITH_MULT_POS - io.github.cvc5.ProofRule
Arithmetic – Multiplication with positive factor m,lr(m>0lr)mlmr where is a relation symbol.
ARITH_MULT_SIGN - io.github.cvc5.ProofRule
Arithmetic – Sign inference f1fk,m(f1fk)m0 where f1fk are variables compared to zero (less, greater or not equal), m is a monomial from these variables and 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 t,x,y,a,b,σ(ttplane)((xayb)(xayb))~if σ=1t,x,y,a,b,σ(ttplane)((xayb)(xayb))~if σ=1 where x,y are real terms (variables or extended terms), t=xy (possibly under rewriting), a,b are real constants, σ{1,1} and tplane:=bx+ayab is the tangent plane of xy at (a,b).
ARITH_NL_COVERING_DIRECT - io.github.cvc5.ProofRule
Arithmetic – Coverings – Direct conflict We use IRPk(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 tarith::OperatorElim::getAxiomFor(t)
ARITH_POLY_NORM - io.github.cvc5.ProofRule
Arithmetic – Polynomial normalization t=st=s where arith::PolyNorm::isArithPolyNorm(t, s)=.
ARITH_SUM_UB - io.github.cvc5.ProofRule
Arithmetic – Sum upper bounds P1PnLR where Pi has the form LiiRi and i{<,,=}.
ARITH_TRANS_EXP_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is approximated from above for negative values d,t,l,u(tltu)exp(t)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 d,t,l,u(tltu)exp(t)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 d,c,ttcexp(t)maclaurin(exp,d,c) where d is an odd positive number, t an arithmetic term and 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 t(t<0)(exp(t)<1)
ARITH_TRANS_EXP_POSITIVITY - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp is always positive texp(t)>0
ARITH_TRANS_EXP_SUPER_LIN - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp grows super-linearly for positive values tt0exp(t)>t+1
ARITH_TRANS_EXP_ZERO - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Exp at zero t(t=0)(exp(t)=1)
ARITH_TRANS_PI - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Assert bounds on Pi l,ureal.pilreal.piu where l,u are valid lower and upper bounds on π.
ARITH_TRANS_SINE_APPROX_ABOVE_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from above for negative values d,t,lb,ub,l,u(tlblandtub)sin(t)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 π) 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 d,t,c,lb,ub(tlblandtub)sin(t)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 π).
ARITH_TRANS_SINE_APPROX_BELOW_NEG - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from below for negative values d,t,c,lb,ub(tlblandtub)sin(t)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 π).
ARITH_TRANS_SINE_APPROX_BELOW_POS - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is approximated from below for positive values d,t,lb,ub,l,u(tlblandtub)sin(t)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 π) 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 tsin(t)1sin(t)1
ARITH_TRANS_SINE_SHIFT - io.github.cvc5.ProofRule
Arithmetic – Transcendentals – Sine is shifted to -pi...pi x,y,sπyπsin(y)=sin(x)(πxπ ? x=y : x=y+2πs) where x is the argument to sine, y is a new real skolem that is x shifted into ππ 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 tsin(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 A,BCC where ¬A,¬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 eqrange(a,b,i,j)eqrange(a,b,i,j)=x.ixjselect(a,x)=select(b,x)
ARRAYS_EXT - io.github.cvc5.ProofRule
Arrays – Arrays extensionality abselect(a,k)select(b,k) where k is arrays::SkolemCache::getExtIndexSkolem(ab).
ARRAYS_READ_OVER_WRITE - io.github.cvc5.ProofRule
Arrays – Read over write i1i2select(store(a,i1,e),i2)select(store(a,i1,e),i2)=select(a,i2)
ARRAYS_READ_OVER_WRITE_1 - io.github.cvc5.ProofRule
Arrays – Read over write 1 select(store(a,i,e),i)select(store(a,i,e),i)=e
ARRAYS_READ_OVER_WRITE_CONTRA - io.github.cvc5.ProofRule
Arrays – Read over write, contrapositive select(store(a,i2,e),i1)select(a,i1)i1=i2
assertFormula(Term) - Method in class io.github.cvc5.Solver
Assert a formula.
ASSUME - io.github.cvc5.ProofRule
Assumption (a leaf) FF 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 λx1xn.t,t1,,tn((λx1xn.t)t1tn)=t{x1t1,,xntn} 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: tt=bitblast(t) For terms: k(bitblast(t1),,bitblast(tn))k(bitblast(t1),,bitblast(tn))=bitblast(t) where t is k(t1,,tn).
BV_EAGER_ATOM - io.github.cvc5.ProofRule
Bit-vectors – Bit-vector eager atom FF=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 C1Cnpol1,L1poln1,Ln1C where let C1Cn be nodes viewed as clauses, as defined above let C1L,polC2 represent the resolution of C1 with C2 with pivot L and polarity pol, as defined above let C1=C1, for each i>1, let Ci=Ci1Li1,poli1Ci The result of the chain resolution is C=Cn
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 (F1Fn)(F1Fn)¬F1¬Fn
CNF_AND_POS - io.github.cvc5.ProofRule
Boolean – CNF – And Positive (F1Fn),i¬(F1Fn)Fi
CNF_EQUIV_NEG1 - io.github.cvc5.ProofRule
Boolean – CNF – Equiv Negative 1 F1=F2(F1=F2)F1F2
CNF_EQUIV_NEG2 - io.github.cvc5.ProofRule
Boolean – CNF – Equiv Negative 2 F1=F2(F1=F2)¬F1¬F2
CNF_EQUIV_POS1 - io.github.cvc5.ProofRule
Boolean – CNF – Equiv Positive 1 F1=F2F1F2¬F1F2
CNF_EQUIV_POS2 - io.github.cvc5.ProofRule
Boolean – CNF – Equiv Positive 2 F1=F2F1F2F1¬F2
CNF_IMPLIES_NEG1 - io.github.cvc5.ProofRule
Boolean – CNF – Implies Negative 1 F1F2(F1F2)F1
CNF_IMPLIES_NEG2 - io.github.cvc5.ProofRule
Boolean – CNF – Implies Negative 2 F1F2(F1F2)¬F2
CNF_IMPLIES_POS - io.github.cvc5.ProofRule
Boolean – CNF – Implies Positive F1F2¬(F1F2)¬F1F2
CNF_ITE_NEG1 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Negative 1 (C ? F1 : F2)(C ? F1 : F2)¬C¬F1
CNF_ITE_NEG2 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Negative 2 (C ? F1 : F2)(C ? F1 : F2)C¬F2
CNF_ITE_NEG3 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Negative 3 (C ? F1 : F2)(C ? F1 : F2)¬F1¬F2
CNF_ITE_POS1 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Positive 1 (C ? F1 : F2)¬(C ? F1 : F2)¬CF1
CNF_ITE_POS2 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Positive 2 (C ? F1 : F2)¬(C ? F1 : F2)CF2
CNF_ITE_POS3 - io.github.cvc5.ProofRule
Boolean – CNF – ITE Positive 3 (C ? F1 : F2)¬(C ? F1 : F2)F1F2
CNF_OR_NEG - io.github.cvc5.ProofRule
Boolean – CNF – Or Negative (F1Fn),i(F1Fn)¬Fi
CNF_OR_POS - io.github.cvc5.ProofRule
Boolean – CNF – Or Positive (F1Fn)¬(F1Fn)F1Fn
CNF_XOR_NEG1 - io.github.cvc5.ProofRule
Boolean – CNF – XOR Negative 1 F1xorF2(F1xorF2)¬F1F2
CNF_XOR_NEG2 - io.github.cvc5.ProofRule
Boolean – CNF – XOR Negative 2 F1xorF2(F1xorF2)F1¬F2
CNF_XOR_POS1 - io.github.cvc5.ProofRule
Boolean – CNF – XOR Positive 1 F1xorF2¬(F1xorF2)F1F2
CNF_XOR_POS2 - io.github.cvc5.ProofRule
Boolean – CNF – XOR Positive 2 F1xorF2¬(F1xorF2)¬F1¬F2
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 (c1t)=(c2s)b where b indicates if the direction is reversed, c1,c2 are constants such that Word::splitConstant(c1,c2,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 (t1w1t2)=(w2s),len(t1)0(t1=w3r) where w1,w2,w3 are words, w3 is pre(w2,p), p is Word::overlap(suf(w2,1),w1), and r is skolem(suf(t1,len(w3))).
CONCAT_CSPLIT - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation split for constants (t1t2)=(cs2),len(t1)0(t1=cr) where r is skolem(suf(t1,1)).
CONCAT_EQ - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation equality (t1tnt)=(t1tns)bt=s where stands for string concatenation and b indicates if the direction is reversed.
CONCAT_LPROP - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation length propagation (t1t2)=(s1s2),len(t1)>len(s1)(t1=s1rt) where rt is skolem(suf(t1,len(s1))).
CONCAT_SPLIT - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation split (t1t2)=(s1s2),len(t1)len(s1)b(t1=s1rt)(s1=t1rs)~if b= where rt is skolem(suf(t1,len(s1))) and rs is skolem(suf(s1,len(t1))).
CONCAT_UNIFY - io.github.cvc5.ProofRule
Strings – Core rules – Concatenation unification (t1t2)=(s1s2),len(t1)=len(s1)bt1=s1 where b indicates if the direction is reversed.
CONG - io.github.cvc5.ProofRule
Equality – Congruence t1=s1,,tn=snk,f?k(f?)(t1,,tn)=k(f?)(s1,,sn) 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 F,¬F
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 F1Fnidt1tnF where the DSL rewrite rule with the given identifier is \(\forall x_1 \dots x_n.
DT_CLASH - io.github.cvc5.ProofRule
Datatypes – Clash isCi(t),isCj(t)~if ij
DT_COLLAPSE - io.github.cvc5.ProofRule
Datatypes – Collapse seli(Cj(t1,,tn))seli(Cj(t1,,tn))=r where Cj is a constructor, r is ti if seli is a correctly applied selector, or {@link TypeNode#mkGroundTerm()} of the proper type otherwise.
DT_INST - io.github.cvc5.ProofRule
Datatypes – Instantiation t,nisC(t)=(t=C(sel1(t),,seln(t))) where C is the nth constructor of the type of t, and isC is the discriminator (tester) for C.
DT_SPLIT - io.github.cvc5.ProofRule
Datatypes – Split tisC1(t)isCn(t) where C1,,Cn are all the constructors of the type of t.
DT_UNIF - io.github.cvc5.ProofRule
Datatypes – Unification C(t1,,tn)=C(s1,,sn)it1=si where C is a constructor.

E

ENCODE_PRED_TRANSFORM - io.github.cvc5.ProofRule
Builtin theory – Encode predicate transformation FGG 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 F1,(F1=F2)F2 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 F1=F2¬F1F2
EQUIV_ELIM2 - io.github.cvc5.ProofRule
Boolean – Equivalence elimination version 2 F1=F2F1¬F2
EVALUATE - io.github.cvc5.ProofRule
Builtin theory – Evaluate tt=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 C1C2 where C2 is the clause C1, but every occurence of a literal after its first occurence is omitted.
FALSE_ELIM - io.github.cvc5.ProofRule
Equality – False elim F=¬F
FALSE_INTRO - io.github.cvc5.ProofRule
Equality – False intro ¬FF=
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 tt=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 f=g,t1=s1,,tn=snf(t1,,tn)=g(s1,,sn) 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 F1F2¬F1F2
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 x1xn.Ft1,,tn,(id(t)?)?F{x1t1,,xntn} 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 i>cic where i has integer type.
INT_TIGHT_UB - io.github.cvc5.ProofRule
Arithmetic – Tighten strict integer upper bounds i<cic 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 (C ? F1 : F2)¬CF1
ITE_ELIM2 - io.github.cvc5.ProofRule
Boolean – ITE elimination version 2 (C ? F1 : F2)CF2
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 pc where {<,,=,,>}, p a polynomial and c a rational constant.
MACRO_BV_BITBLAST - io.github.cvc5.ProofRule
Bit-vectors – (Macro) Bitblast tt=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 C1CnC,pol1,L1poln1,Ln1C where let C1Cn be nodes viewed as clauses, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let C1L,polC2 represent the resolution of C1 with C2 with pivot L and polarity pol, as defined in RESOLUTION <cvc5.ProofRule.RESOLUTION> let C1 be equal, in its set representation, to C1, for each i>1, let Ci be equal, in its set representation, to Ci1Li1,poli1Ci The result of the chain resolution is C, which is equal, in its set representation, to Cn
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 t,idrt=Rewriteridr(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 F,F1Fn(ids(ida(idr)?)?)?Rewriteridr(Fσids,ida(Fn)σids,ida(F1)) 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 F,F1FnG,(ids(ida(idr)?)?)?G where Rewriteridr(Fσids,ida(Fn)σids,ida(F1))=Rewriteridr(Gσids,ida(Fn)σids,ida(F1)).
MACRO_STRING_INFERENCE - io.github.cvc5.ProofRule
Strings – (Macro) String inference ?F,id,isRev,expF used to bookkeep an inference that has not yet been converted via 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 F1,(F1F2)F2 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 ¬(F1Fn)¬F1¬Fn
NOT_EQUIV_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not Equivalence elimination version 1 F1F2F1F2
NOT_EQUIV_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not Equivalence elimination version 2 F1F2¬F1¬F2
NOT_IMPLIES_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not Implication elimination version 1 ¬(F1F2)F1
NOT_IMPLIES_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not Implication elimination version 2 ¬(F1F2)¬F2
NOT_ITE_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not ITE elimination version 1 ¬(C ? F1 : F2)¬C¬F1
NOT_ITE_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not ITE elimination version 2 ¬(C ? F1 : F2)C¬F2
NOT_NOT_ELIM - io.github.cvc5.ProofRule
Boolean – Double negation elimination ¬(¬F)F
NOT_OR_ELIM - io.github.cvc5.ProofRule
Boolean – Not Or elimination ¬(F1Fn)i¬Fi
NOT_XOR_ELIM1 - io.github.cvc5.ProofRule
Boolean – Not XOR elimination version 1 ¬(F1xorF2)F1¬F2
NOT_XOR_ELIM2 - io.github.cvc5.ProofRule
Boolean – Not XOR elimination version 2 ¬(F1xorF2)¬F1F2
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 F,bF=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 tR1,tR2tinter(R1,R2)
RE_UNFOLD_NEG - io.github.cvc5.ProofRule
Strings – Regular expressions – Negative Unfold tRRegExpOpr::reduceRegExpNeg(tR) 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 tRRegExpOpr::reduceRegExpNegConcatFixed(tR,L,i) where RegExpOpr::getRegExpConcatFixed(tR,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 tRRegExpOpr::reduceRegExpPos(tR) 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 tt=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.groupn1nk)A) partitions tuples of relation A such that tuples that have the same projection with indices n1nk 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 tRemoveTermFormulas::getAxiomFor(t)
REORDERING - io.github.cvc5.ProofRule
Boolean – Reordering C1C2C2 where the set representations of C1 and C2 are the same and the number of literals in C2 is the same of that of C1.
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 C1,C2pol,LC where C1 and C2 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 F1Fn where F1Fn correspond to the unsat core determined by the SAT solver.
SCOPE - io.github.cvc5.ProofRule
Scope (a binder for assumptions) FF1Fn(F1Fn)F~if F or FF1Fn¬(F1Fn)~if F= 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 kk=t where t is the unpurified form of skolem k.
SKOLEMIZE - io.github.cvc5.ProofRule
Quantifiers – Skolemization x1xn.FFσ or ¬(x1xn.F)¬Fσ where σ maps x1,,xn 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 FF¬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 t,sto_code(t)=1to_code(t)to_code(s)ts
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 len(t)nt=w1w2len(w1)=n or alternatively for the reverse: len(t)nt=w1w2len(w2)=n where w1 is skolem(pre(t,n) and w2 is skolem(suf(t,n).
STRING_EAGER_REDUCTION - io.github.cvc5.ProofRule
Strings – Extended functions – Eager reduction tR where R is 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 tlen(t)0
STRING_LENGTH_POS - io.github.cvc5.ProofRule
Strings – Core rules – Length positive t(len(t)=0t=)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 tRt=w where w is strings::StringsPreprocess::reduce(t,R,).
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 unit(x)=unit(y)x=y Also applies to the case where 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 F1Fnt,ids?t=tσids(Fn)σids(F1) where σids(Fi) 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 t1=t2t2=t1 or t1t2t2t1
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.groupn1nk)A) partitions tuples of table A such that tuples that have the same projection with indices n1nk are in the same part.
TABLE_JOIN - io.github.cvc5.Kind
Table join operator has the form ((_table.joinm1n1mknk)AB) where m1n1mknk 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 t1=t2,,tn1=tnt1=tn
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 F=F
TRUE_INTRO - io.github.cvc5.ProofRule
Equality – True intro FF=
TRUST - io.github.cvc5.ProofRule
Trusted rule F1Fntid,F,...F where tid is an identifier and F is a formula.
TRUST_THEORY_REWRITE - io.github.cvc5.ProofRule
Trusted rules – Theory rewrite F,tid,ridF 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 F1xorF2F1F2
XOR_ELIM2 - io.github.cvc5.ProofRule
Boolean – XOR elimination version 2 F1xorF2¬F1¬F2
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