what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

- A
- B
- C
- D
- E
- F
- G
- H
- I
- J
- K
- L
- M
- N
- O
- P
- Q
- R
- S
- T
- U
- V
- W
- X
- Y
- Z
- :
- *
- +
- .
- <
- =
- -
- _
- All

Index - C

cache | What4.Expr.App
cacheLookupFnNameBimap | What4.Protocol.SMTWriter
cacheOptDesc | What4.Expr.Allocator
cacheStartSize | What4.Expr.Builder, What4.Expr
cacheStartSizeDesc | What4.Expr.Allocator
cacheStartSizeOption | What4.Expr.Allocator, What4.Expr.Builder
cacheTerms | What4.Expr.Allocator, What4.Expr.Builder
carrylessMultiply | What4.Interface
CeilReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
cExprLookup | What4.Serialize.Parser
cfgAllowFreeSymFns | What4.Serialize.Printer
cfgAllowFreeVars | What4.Serialize.Printer
Char16 | What4.BaseTypes, What4.Interface
Char16Literal | What4.Utils.StringLiteral, What4.Interface
Char16Repr | What4.BaseTypes, What4.Interface
Char8 | What4.BaseTypes, What4.Interface
Char8Literal | What4.Utils.StringLiteral, What4.Interface
Char8Repr | What4.BaseTypes, What4.Interface
check | What4.Protocol.Online
checkAndGetModel | What4.Protocol.Online
checkCommands | What4.Protocol.SMTWriter
checkOptSetResult | What4.Config
checkSat | What4.Protocol.SMTLib2.Syntax
checkSatAssuming | What4.Protocol.SMTLib2.Syntax
CheckSatError | What4.Protocol.SMTLib2.Parse
checkSatisfiable | What4.Protocol.Online
checkSatisfiableWithModel | What4.Protocol.Online
CheckSatResponse | What4.Protocol.SMTLib2.Parse
CheckSatUnsupported | What4.Protocol.SMTLib2.Parse
checkSatWithAssumptions | What4.Protocol.SMTLib2.Syntax
checkSolverVersion | What4.Protocol.SMTLib2
checkSolverVersion' | What4.Protocol.SMTLib2
checkSynth | What4.Protocol.SMTLib2.Syntax
checkWithAssumptions | What4.Protocol.Online
checkWithAssumptionsAndModel | What4.Protocol.Online
checkWithAssumptionsCommands | What4.Protocol.SMTWriter
chooseBool | Test.Verification
chooseInt | Test.Verification
chooseInteger | Test.Verification
clampedIntAbs | What4.Expr.MATLAB
ClampedIntAbsFn | What4.Expr.MATLAB
clampedIntAdd | What4.Expr.MATLAB
ClampedIntAddFn | What4.Expr.MATLAB
clampedIntMul | What4.Expr.MATLAB
ClampedIntMulFn | What4.Expr.MATLAB
clampedIntNeg | What4.Expr.MATLAB
ClampedIntNegFn | What4.Expr.MATLAB
clampedIntSub | What4.Expr.MATLAB
ClampedIntSubFn | What4.Expr.MATLAB
clampedIntToBV | What4.Interface
clampedIntToSBV | What4.Interface
clampedUIntAdd | What4.Expr.MATLAB
ClampedUIntAddFn | What4.Expr.MATLAB
clampedUIntMul | What4.Expr.MATLAB
ClampedUIntMulFn | What4.Expr.MATLAB
clampedUIntSub | What4.Expr.MATLAB
ClampedUIntSubFn | What4.Expr.MATLAB
cleanupProcess | What4.Utils.Process
clearIdxCache | What4.Expr.Builder
clz |
1 (Function) | What4.Utils.Arithmetic
2 (Function) | What4.Utils.BVDomain
Cmd | What4.Protocol.SMTLib2.Syntax
Coefficient | What4.SemiRing, What4.Expr
CollectedVarInfo | What4.Expr.VarIdentification
CollectorResults |
1 (Type/Class) | What4.Protocol.SMTWriter
2 (Data Constructor) | What4.Protocol.SMTWriter
collectVarInfo | What4.Expr.VarIdentification
combine | What4.Expr.BoolMap
Command |
1 (Type/Class) | What4.Protocol.SMTLib2.Syntax
2 (Type/Class) | What4.Protocol.SMTWriter
commentCommand | What4.Protocol.SMTWriter
compareExpr | What4.Expr.App
compareNat | What4.BaseTypes, What4.Interface
Complex | What4.Utils.Complex
complexAdd | What4.Utils.Complex
complexAsRational | What4.Utils.Complex
complexDiv | What4.Utils.Complex
complexMul | What4.Utils.Complex
complexNegate | What4.Utils.Complex
complexRecip | What4.Utils.Complex
complexSub | What4.Utils.Complex
ComplexToArrayTypeMap | What4.Protocol.SMTWriter
ComplexToStructTypeMap | What4.Protocol.SMTWriter
ComputableArithTheory | What4.Expr.AppTheory, What4.Expr
computeDefaultSolverBounds | What4.Utils.Versions
Concat | What4.Protocol.VerilogWriter.AST
concat |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain
concat2 | What4.Protocol.VerilogWriter.AST
ConcreteArray | What4.Concrete
ConcreteBool | What4.Concrete
ConcreteBV | What4.Concrete
ConcreteComplex | What4.Concrete
ConcreteFloat | What4.Concrete
ConcreteInteger | What4.Concrete
concreteRange | What4.Utils.AbstractDomains
ConcreteReal | What4.Concrete
ConcreteString | What4.Concrete
ConcreteStruct | What4.Concrete
concreteToSym | What4.Interface
concreteType | What4.Concrete
ConcreteVal | What4.Concrete
ConcreteValue | What4.Utils.AbstractDomains
ConcreteValueWrapper |
1 (Type/Class) | What4.Utils.AbstractDomains
2 (Data Constructor) | What4.Utils.AbstractDomains
Config |
1 (Type/Class) | What4.Config
2 (Type/Class) | What4.Serialize.Printer
3 (Data Constructor) | What4.Serialize.Printer
4 (Type/Class) | What4.Serialize.Parser
5 (Data Constructor) | What4.Serialize.Parser
ConfigDesc | What4.Config
configHelp | What4.Config
ConfigOption | What4.Config
configOption | What4.Config
configOptionName | What4.Config
configOptionNameParts | What4.Config
configOptionText | What4.Config
configOptionType | What4.Config
ConfigValue |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
ConjPred | What4.Expr.App, What4.Expr.Builder, What4.Expr
Connection | What4.Solver.Yices
connHandle | What4.Protocol.SMTWriter
connInputHandle | What4.Protocol.SMTWriter
connState | What4.Protocol.SMTWriter
constant |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Expr.UnaryBV
ConstantArray | What4.Expr.App, What4.Expr.Builder, What4.Expr
constantArray | What4.Interface
constraint | What4.Protocol.SMTLib2.Syntax
constraintCommand | What4.Protocol.SMTWriter
consumeUntilEnd | What4.Serialize.Log
contains | What4.Expr.BoolMap
ContinueOnError | What4.Protocol.Online
convertBaseTypes | What4.Serialize.Printer
CopyArray | What4.Expr.App, What4.Expr.Builder, What4.Expr
copyOpt | What4.Config
correct_add |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_and |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain.XOR
3 (Function) | What4.Utils.BVDomain
correct_and_scalar | What4.Utils.BVDomain.XOR
correct_any |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_arithToBitwise | What4.Utils.BVDomain
correct_arithToXorDomain | What4.Utils.BVDomain
correct_ashr |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_asXorDomain | What4.Utils.BVDomain
correct_bitbounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.XOR
correct_bitwiseToArith | What4.Utils.BVDomain
correct_bitwiseToXorDomain | What4.Utils.BVDomain
correct_bra1 | What4.Utils.BVDomain
correct_bra2 | What4.Utils.BVDomain
correct_brb1 | What4.Utils.BVDomain
correct_brb2 | What4.Utils.BVDomain
correct_clz | What4.Utils.BVDomain
correct_concat |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_ctz | What4.Utils.BVDomain
correct_eq |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_fromXorDomain | What4.Utils.BVDomain
correct_intersection | What4.Utils.BVDomain.Bitwise
correct_isUltSumCommonEquiv | What4.Utils.BVDomain.Arith
correct_lshr |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_mul |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_neg |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_not |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_or |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
correct_overlap |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_popcnt | What4.Utils.BVDomain
correct_rol |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
correct_ror |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
correct_sbounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_scale |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_scale_eq | What4.Utils.BVDomain.Arith
correct_sdiv |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_sdivRange | What4.Utils.BVDomain.Arith
correct_select |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_shl |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_shrink |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
correct_sign_ext |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_singleton |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
correct_slt |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_srem |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_testBit |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
correct_trunc |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
correct_ubounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_udiv |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_ult |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_union |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
correct_unknowns | What4.Utils.BVDomain.Arith
correct_urem |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
correct_xor |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain.XOR
3 (Function) | What4.Utils.BVDomain
correct_xorToBitwiseDomain | What4.Utils.BVDomain
correct_zero_ext |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
Cos | What4.SpecialFunctions
Cosh | What4.SpecialFunctions
countOccurrences | What4.Expr.App
countOccurrences' | What4.Expr.App
count_subterms | What4.Expr.Simplify
Cplx | What4.Expr.App, What4.Expr.Builder, What4.Expr
cplxAdd | What4.Interface
CplxAddFn | What4.Expr.MATLAB
cplxCeil | What4.Interface
CplxCeilFn | What4.Expr.MATLAB
cplxConj | What4.Interface
cplxCos | What4.Interface
CplxCosFn | What4.Expr.MATLAB
cplxDiv | What4.Interface
cplxEq | What4.Interface
cplxExp | What4.Interface
CplxExpFn | What4.Expr.MATLAB
CplxExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
cplxExprAsInteger | What4.Interface
cplxExprAsRational | What4.Interface
cplxFloor | What4.Interface
CplxFloorFn | What4.Expr.MATLAB
cplxFromReal | What4.Interface
cplxGetParts | What4.Interface
cplxHypot | What4.Interface
CplxIsNonZeroFn | What4.Expr.MATLAB
CplxIsRealFn | What4.Expr.MATLAB
cplxIte | What4.Interface
cplxLog | What4.Interface
cplxLogBase | What4.Interface
CplxLogBaseFn | What4.Expr.MATLAB
CplxLogFn | What4.Expr.MATLAB
cplxMag | What4.Interface
CplxMagFn | What4.Expr.MATLAB
cplxMul | What4.Interface
CplxMulFn | What4.Expr.MATLAB
cplxNe | What4.Interface
cplxNeg | What4.Interface
CplxNegFn | What4.Expr.MATLAB
cplxRound | What4.Interface
CplxRoundFn | What4.Expr.MATLAB
cplxSin | What4.Interface
CplxSinFn | What4.Expr.MATLAB
cplxSqrt | What4.Interface
CplxSqrtFn | What4.Expr.MATLAB
cplxSub | What4.Interface
CplxSubFn | What4.Expr.MATLAB
cplxTan | What4.Interface
CplxTanFn | What4.Expr.MATLAB
crBindings | What4.Protocol.SMTWriter
crFreeConstants | What4.Protocol.SMTWriter
crResult | What4.Protocol.SMTWriter
crSideConds | What4.Protocol.SMTWriter
cSymFnLookup | What4.Serialize.Parser
ctz |
1 (Function) | What4.Utils.Arithmetic
2 (Function) | What4.Utils.BVDomain
curProgramLoc | What4.Expr.Builder, What4.Expr
CVC4 |
1 (Type/Class) | What4.Solver.CVC4, What4.Solver
2 (Data Constructor) | What4.Solver.CVC4, What4.Solver
cvc4Adapter | What4.Solver.CVC4, What4.Solver
cvc4Features | What4.Solver.CVC4, What4.Solver
cvc4Options | What4.Solver.CVC4, What4.Solver
cvc4Path | What4.Solver.CVC4, What4.Solver
cvc4Timeout | What4.Solver.CVC4, What4.Solver
CVC5 |
1 (Type/Class) | What4.Solver.CVC5, What4.Solver
2 (Data Constructor) | What4.Solver.CVC5, What4.Solver
cvc5Adapter | What4.Solver.CVC5, What4.Solver
cvc5Features | What4.Solver.CVC5, What4.Solver
cvc5Options | What4.Solver.CVC5, What4.Solver
cvc5Path | What4.Solver.CVC5, What4.Solver
cvc5Timeout | What4.Solver.CVC5, What4.Solver