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

Index

* | What4.BaseTypes, What4.Interface
+ | What4.BaseTypes, What4.Interface
- | What4.BaseTypes, What4.Interface
.&& | What4.Protocol.SMTWriter
./ | What4.Protocol.SMTLib2.Syntax
./= | What4.Protocol.SMTWriter
.< | What4.Protocol.SMTWriter
.<= | What4.Protocol.SMTWriter
.== | What4.Protocol.SMTWriter
.> | What4.Protocol.SMTWriter
.>= | What4.Protocol.SMTWriter
.|| | What4.Protocol.SMTWriter
:+ | What4.Utils.Complex
:~: | What4.BaseTypes, What4.Interface
<= | What4.BaseTypes, What4.Interface
==> | Test.Verification
A | What4.Serialize.Printer
abcOptions | What4.Solver.ExternalABC, What4.Solver
abcPath | What4.Solver.ExternalABC, What4.Solver
ABool | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
abs | What4.Protocol.SMTLib2.Syntax
absAnd | What4.Utils.AbstractDomains
absOr | What4.Utils.AbstractDomains
Abstractable | What4.Utils.AbstractDomains
abstractEval | What4.Expr.App
AbstractValue | What4.Utils.AbstractDomains
AbstractValueWrapper |
1 (Type/Class) | What4.Utils.AbstractDomains
2 (Data Constructor) | What4.Utils.AbstractDomains
ABV | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AckAction | What4.Protocol.SMTWriter
AckError | What4.Protocol.SMTLib2.Response
AckFail | What4.Protocol.SMTLib2.Response
AckInfeasible | What4.Protocol.SMTLib2.Response
AcknowledgementAction | What4.Protocol.SMTWriter
AckSat | What4.Protocol.SMTLib2.Response
AckSkipped | What4.Protocol.SMTLib2.Response
AckSuccess | What4.Protocol.SMTLib2.Response
AckSuccessSExp | What4.Protocol.SMTLib2.Response
AckUnknown | What4.Protocol.SMTLib2.Response
AckUnsat | What4.Protocol.SMTLib2.Response
AckUnsupported | What4.Protocol.SMTLib2.Response
add |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
3 (Function) | What4.Utils.BVDomain.Arith
4 (Function) | What4.Utils.BVDomain
5 (Function) | What4.Expr.WeightedSum
6 (Function) | What4.Expr.UnaryBV
addBoundInput | What4.Protocol.VerilogWriter.AST
addCommand | What4.Protocol.SMTWriter, What4.Solver.Yices
addCommandNoAck | What4.Protocol.SMTWriter
addCommands | What4.Protocol.SMTWriter
addCondition | What4.Partial
addConstant | What4.Expr.WeightedSum
addConstraint | What4.Protocol.SMTWriter
addDeclareVar | What4.Protocol.SMTWriter
addFreshInput | What4.Protocol.VerilogWriter.AST
addFreshWire | What4.Protocol.VerilogWriter.AST
addIsLeq | What4.BaseTypes, What4.Interface
addIsLeqLeft1 | What4.BaseTypes, What4.Interface
addMulDistribRight | What4.BaseTypes, What4.Interface
addNat | What4.BaseTypes, What4.Interface
addOutput | What4.Protocol.VerilogWriter.AST
addPrefixIsLeq | What4.BaseTypes, What4.Interface
addRange | What4.Utils.AbstractDomains
addSignedOF | What4.Interface
addSynthFun | What4.Protocol.SMTWriter
addUnsignedOF | What4.Interface
addVar |
1 (Function) | What4.Expr.BoolMap
2 (Function) | What4.Expr.WeightedSum
addVars | What4.Expr.WeightedSum
addWire | What4.Protocol.VerilogWriter.AST
AFloat | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AId | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AInt | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
allLogic | What4.Protocol.SMTLib2.Syntax
allSupported | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
allTrueEntries | What4.Interface
all_supported | What4.Protocol.SMTLib2
alter | What4.Utils.AnnotatedMap
alterF | What4.Utils.AnnotatedMap
AlwaysUnfold | What4.Interface
ANat | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
And | What4.Protocol.VerilogWriter.AST
and |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
andAll | What4.Protocol.SMTWriter
andAllOf | What4.Interface
andPred | What4.Interface
and_scalar | What4.Utils.BVDomain.XOR
AnnotatedMap | What4.Utils.AnnotatedMap
annotateTerm | What4.Interface
Annotation | What4.Expr.App, What4.Expr.Builder, What4.Expr
annotation | What4.Utils.AnnotatedMap
AnOnlineSolver |
1 (Type/Class) | What4.Protocol.Online
2 (Data Constructor) | What4.Protocol.Online
any |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
APE | What4.Expr.App
apeDoc | What4.Expr.App
apeExprs | What4.Expr.App
apeIndex | What4.Expr.App
apeLength | What4.Expr.App
apeLoc | What4.Expr.App
apeName | What4.Expr.App
App | What4.Expr.App, What4.Expr.Builder, What4.Expr
app | What4.Protocol.SMTWriter
append |
1 (Function) | What4.Utils.Word16String
2 (Function) | What4.Expr.StringSeq
appEqF | What4.Expr.App
AppExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
appExpr | What4.Expr.Allocator
appExprAbsValue | What4.Expr.App
appExprApp | What4.Expr.App, What4.Expr.Builder, What4.Expr
AppExprCtor | What4.Expr.App
appExprId | What4.Expr.App, What4.Expr.Builder, What4.Expr
appExprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
applySymFn | What4.Interface
AppPPExpr |
1 (Data Constructor) | What4.Expr.App
2 (Type/Class) | What4.Expr.App
approximate | What4.Protocol.PolyRoot
AppTheory | What4.Expr.AppTheory, What4.Expr
appTheory | What4.Expr.AppTheory, What4.Expr
appType | What4.Expr.App, What4.Expr.Builder
app_list | What4.Protocol.SMTWriter
Arccos | What4.SpecialFunctions
Arccosh | What4.SpecialFunctions
Arcsin | What4.SpecialFunctions
Arcsinh | What4.SpecialFunctions
Arctan | What4.SpecialFunctions
Arctan2 | What4.SpecialFunctions
Arctanh | What4.SpecialFunctions
AReal | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
arithDomainData | What4.Utils.BVDomain.Arith, What4.Utils.BVDomain
arithToXorDomain | What4.Utils.BVDomain
Array | What4.Protocol.SMTLib2.Parse
ArrayConcrete | What4.Expr.GroundEval, What4.Expr
arrayConst |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
arrayConstant | What4.Protocol.SMTWriter
ArrayConstantFn | What4.Protocol.SMTWriter
arrayCopy | What4.Interface
arrayEq | What4.Interface
ArrayFromFn | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayFromFn | What4.Interface
arrayFromMap | What4.Interface
arrayIte | What4.Interface
arrayLookup | What4.Interface
ArrayMap | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayMap | What4.Interface
ArrayMapping | What4.Expr.GroundEval, What4.Expr
arrayRangeEq | What4.Interface
ArrayResultWrapper |
1 (Type/Class) | What4.Interface, What4.Expr.Builder
2 (Data Constructor) | What4.Interface, What4.Expr.Builder
arraySelect |
1 (Function) | What4.Protocol.SMTWriter
2 (Function) | What4.Protocol.SMTLib2
arraySet | What4.Interface
arraySort | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
arrayStore | What4.Protocol.SMTLib2
ArrayTheory | What4.Expr.AppTheory, What4.Expr
ArrayTrueOnEntries | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayTrueOnEntries | What4.Interface
arrayTypeIndices | What4.BaseTypes, What4.Interface
arrayTypeResult | What4.BaseTypes, What4.Interface
arrayUpdate |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
arrayUpdateAbs | What4.Expr.ArrayUpdateMap
arrayUpdateAtIdxLits | What4.Interface
ArrayUpdateMap | What4.Expr.ArrayUpdateMap
asAffineVar |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Interface
asApp | What4.Expr.App, What4.Expr.Builder
asArithDomain | What4.Utils.BVDomain
asAtomList | What4.Protocol.SExp
asBitwiseDomain | What4.Utils.BVDomain
asBV | What4.Interface
asComplex | What4.Interface
asConcrete | What4.Interface
asConjunction | What4.Expr.App, What4.Expr.Builder
AsConst | What4.Protocol.SMTLib2.Parse
asConstant |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Expr.UnaryBV
asConstantArray | What4.Interface
asConstantPred | What4.Interface
asDisjunction | What4.Expr.App, What4.Expr.Builder
asFloat | What4.Interface
ashr |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
asInteger | What4.Interface
asMatlabSolverFn | What4.Expr.App
asNat | What4.Interface
asNegAtom | What4.Expr.App
asNegAtomList | What4.Protocol.SExp
asNonceApp | What4.Expr.App, What4.Expr.Builder
asPosAtom | What4.Expr.App
asProdVar | What4.Expr.WeightedSum
asRational | What4.Interface
asSemiRingLit | What4.Expr.App
asSemiRingProd | What4.Expr.App
asSemiRingSum | What4.Expr.App
assert | What4.Protocol.SMTLib2.Syntax
assertCommand | What4.Protocol.SMTWriter
assertForall | What4.Solver.Yices
assertNamed | What4.Protocol.SMTLib2.Syntax
assertNamedCommand | What4.Protocol.SMTWriter
Assign | What4.Protocol.VerilogWriter.AST
asSingleRange | What4.Utils.AbstractDomains
asSingleton |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
asSMT2Type | What4.Protocol.SMTLib2
asString | What4.Interface
asStruct | What4.Interface
assume | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2, What4.Solver.Yices
assumedProp | Test.Verification
assumeFormula | What4.Protocol.SMTWriter
assumeFormulaWithFreshName | What4.Protocol.SMTWriter
assumeFormulaWithName | What4.Protocol.SMTWriter
Assuming | Test.Verification
assuming | Test.Verification
Assumption | Test.Verification
AssumptionProp | Test.Verification
AStr | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
asVar | What4.Expr.WeightedSum
asWeightedSum | What4.Expr.App
asWeightedVar | What4.Expr.WeightedSum
asXorDomain | What4.Utils.BVDomain
asyncLinked | What4.Utils.Serialize
Atom | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
avCheckEq | What4.Utils.AbstractDomains
avContains | What4.Utils.AbstractDomains
avJoin | What4.Utils.AbstractDomains
avOverlap | What4.Utils.AbstractDomains
avSingle | What4.Utils.AbstractDomains
avTop | What4.Utils.AbstractDomains
backendPred | What4.Interface
BaseArrayRepr | What4.BaseTypes, What4.Interface
BaseArrayType | What4.BaseTypes, What4.Interface
BaseBoolRepr | What4.BaseTypes, What4.Interface
BaseBoolType | What4.BaseTypes, What4.Interface
BaseBVRepr | What4.BaseTypes, What4.Interface
BaseBVType | What4.BaseTypes, What4.Interface
BaseComplexRepr | What4.BaseTypes, What4.Interface
BaseComplexType | What4.BaseTypes, What4.Interface
baseDefaultValue | What4.Interface
BaseEq | What4.Expr.App, What4.Expr.Builder, What4.Expr
BaseFloatRepr | What4.BaseTypes, What4.Interface
BaseFloatType | What4.BaseTypes, What4.Interface
BaseIntegerRepr | What4.BaseTypes, What4.Interface
BaseIntegerType | What4.BaseTypes, What4.Interface
baseIsConcrete | What4.Interface
BaseIte | What4.Expr.App, What4.Expr.Builder, What4.Expr
BaseRealRepr | What4.BaseTypes, What4.Interface
BaseRealType | What4.BaseTypes, What4.Interface
BaseStringRepr | What4.BaseTypes, What4.Interface
BaseStringType | What4.BaseTypes, What4.Interface
BaseStructRepr | What4.BaseTypes, What4.Interface
BaseStructType | What4.BaseTypes, What4.Interface
BaseType | What4.BaseTypes, What4.Interface
baseTypeIte | What4.Interface
BaseTypeRepr | What4.BaseTypes, What4.Interface
bfStatus | What4.Utils.FloatHelpers
BigEndian | What4.Utils.Endian
BinaryPos | What4.ProgramLoc
BinarySearch | What4.Utils.ResolveBounds.BV
bindVarAsFree | What4.Protocol.SMTWriter
Binop |
1 (Data Constructor) | What4.Protocol.VerilogWriter.AST
2 (Type/Class) | What4.Protocol.VerilogWriter.AST
binop | What4.Protocol.VerilogWriter.AST
binopDoc | What4.Protocol.VerilogWriter.ABCVerilog
binopType | What4.Protocol.VerilogWriter.AST
bin_app | What4.Protocol.SMTLib2.Syntax
Bit | What4.Protocol.VerilogWriter.AST
bit | What4.Protocol.VerilogWriter.AST
bit0 | What4.Protocol.SMTLib2.Syntax
bit1 | What4.Protocol.SMTLib2.Syntax
bitbounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise, What4.Utils.BVDomain
3 (Function) | What4.Utils.BVDomain.XOR
bitle | What4.Utils.BVDomain.Bitwise
BitSelect | What4.Protocol.VerilogWriter.AST
bitSelect | What4.Protocol.VerilogWriter.AST
BitVec | What4.Protocol.SMTLib2.Parse
bitvec | What4.Serialize.SETokens, What4.Serialize.Printer
BitvectorTheory | What4.Expr.AppTheory, What4.Expr
bitwiseRoundAbove | What4.Utils.BVDomain
bitwiseRoundBetween | What4.Utils.BVDomain
bitwiseToXorDomain | What4.Utils.BVDomain
Bitwuzla |
1 (Type/Class) | What4.Solver.Bitwuzla, What4.Solver
2 (Data Constructor) | What4.Solver.Bitwuzla, What4.Solver
bitwuzlaAdapter | What4.Solver.Bitwuzla, What4.Solver
bitwuzlaFeatures | What4.Solver.Bitwuzla, What4.Solver
bitwuzlaOptions | What4.Solver.Bitwuzla, What4.Solver
bitwuzlaPath | What4.Solver.Bitwuzla, What4.Solver
bitwuzlaTimeout | What4.Solver.Bitwuzla, What4.Solver
Bool | What4.Protocol.SMTLib2.Parse
bool | What4.Serialize.SETokens, What4.Serialize.Printer
Boolector |
1 (Type/Class) | What4.Solver.Boolector, What4.Solver
2 (Data Constructor) | What4.Solver.Boolector, What4.Solver
boolectorAdapter | What4.Solver.Boolector, What4.Solver
boolectorFeatures | What4.Solver.Boolector, What4.Solver
boolectorOptions | What4.Solver.Boolector, What4.Solver
boolectorPath | What4.Solver.Boolector, What4.Solver
boolectorTimeout | What4.Solver.Boolector, What4.Solver
BoolExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
boolExpr | What4.Protocol.SMTWriter
BoolLit | What4.Protocol.VerilogWriter.AST
BoolMap | What4.Expr.BoolMap
BoolMapDualUnit | What4.Expr.BoolMap
BoolMapTerms | What4.Expr.BoolMap
BoolMapUnit | What4.Expr.BoolMap
BoolMapView | What4.Expr.BoolMap
boolOptSty | What4.Config
BoolOrFn | What4.Expr.MATLAB
BoolProperty | Test.Verification
boolSort | What4.Protocol.SMTLib2.Syntax
BoolTheory | What4.Expr.AppTheory, What4.Expr
BoolTypeMap | What4.Protocol.SMTWriter
Bound | What4.Config
boundInnerTerm | What4.Expr.VarIdentification
BoundQuant | What4.Expr.VarIdentification
boundQuant | What4.Expr.VarIdentification
boundTopTerm | What4.Expr.VarIdentification
BoundVar | What4.Interface
boundVar | What4.Expr.VarIdentification
BoundVarExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
BoundVarMap | What4.Expr.App
boundVars | What4.Expr.App, What4.Expr.Builder, What4.Expr
boundVars' | What4.Expr.App
builder_list |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTWriter
BVAdd | What4.Protocol.VerilogWriter.AST
bvAdd |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvadd | What4.Protocol.SMTLib2.Syntax
BVAnd | What4.Protocol.VerilogWriter.AST
bvAnd |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvand | What4.Protocol.SMTLib2.Syntax
bvAndBits | What4.Interface
BVar | What4.Expr.App
bvarAbstractValue | What4.Expr.App, What4.Expr.Builder
bvarId | What4.Expr.App, What4.Expr.Builder, What4.Expr
BVArith | What4.SemiRing
BVArithRepr | What4.SemiRing, What4.Expr
bvarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvarLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvarName | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvarType | What4.Expr.App, What4.Expr.Builder
BVAshr | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvAshr |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvashr | What4.Protocol.SMTLib2.Syntax
bvAsSignedInteger | What4.SWord
bvAsUnsignedInteger | What4.SWord
bvAtBE | What4.SWord
bvAtLE | What4.SWord
bvbinary | What4.Protocol.SMTLib2.Syntax
BVBitInterval | What4.Utils.BVDomain.Bitwise
bvBitreverse | What4.Interface
BVBits | What4.SemiRing
BVBitsRepr | What4.SemiRing, What4.Expr
BVConcat | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvConcat |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
BVConcrete | What4.Utils.ResolveBounds.BV
BVConst |
1 (Type/Class) | What4.Protocol.VerilogWriter.AST
2 (Data Constructor) | What4.Protocol.VerilogWriter.AST
BVCountLeadingZeros | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvCountLeadingZeros |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVCountTrailingZeros | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvCountTrailingZeros |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVDAny | What4.Utils.BVDomain.Arith
BVDArith | What4.Utils.BVDomain
BVDBitwise | What4.Utils.BVDomain
bvdecimal | What4.Protocol.SMTLib2.Syntax
BVDInterval | What4.Utils.BVDomain.Arith
BVDiv | What4.Protocol.VerilogWriter.AST
bvdMask |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
BVDomain | What4.Utils.BVDomain
BVDXor | What4.Utils.BVDomain.XOR
bvEq |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvExtract | What4.Protocol.SMTWriter
BVFill | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvFill |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVFlavor | What4.SemiRing, What4.Expr
BVFlavorRepr | What4.SemiRing, What4.Expr
bvForall | What4.SWord
bvhexadecimal | What4.Protocol.SMTLib2.Syntax
BVI | What4.Expr.VarIdentification
BVIndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder
bvIsNeg | What4.Interface
bvIsNonzero |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVIsNonZeroFn | What4.Expr.MATLAB
bvIte |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
bvJoin | What4.SWord
bvJoinVector | What4.Interface
bvLg2 | What4.SWord
BVLit | What4.Protocol.VerilogWriter.AST
bvLit |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVLshr | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvLshr |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvlshr | What4.Protocol.SMTLib2.Syntax
BVMul | What4.Protocol.VerilogWriter.AST
bvMul |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvmul | What4.Protocol.SMTLib2.Syntax
bvNe | What4.Interface
bvNeg |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvneg | What4.Protocol.SMTLib2.Syntax
BVNot | What4.Protocol.VerilogWriter.AST
bvNot |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvnot | What4.Protocol.SMTLib2.Syntax
bvNotBits | What4.Interface
bvOne | What4.Interface
BVOr | What4.Protocol.VerilogWriter.AST
bvOr |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvor | What4.Protocol.SMTLib2.Syntax
bvOrAbs | What4.Expr.App, What4.Expr.Builder
BVOrBits | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvOrBits | What4.Interface
bvOrContains | What4.Expr.App
bvOrInsert | What4.Expr.App, What4.Expr.Builder
BVOrNote |
1 (Type/Class) | What4.Expr.App
2 (Data Constructor) | What4.Expr.App
BVOrSet |
1 (Type/Class) | What4.Expr.App, What4.Expr.Builder
2 (Data Constructor) | What4.Expr.App
bvOrSingleton | What4.Expr.App, What4.Expr.Builder
bvOrToList | What4.Expr.App, What4.Expr.Builder
bvOrUnion | What4.Expr.App, What4.Expr.Builder
bvPackBE | What4.SWord
bvPackLE | What4.SWord
BVPopcount | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvPopcount |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVPow | What4.Protocol.VerilogWriter.AST
BVRem | What4.Protocol.VerilogWriter.AST
BVRol | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvRol |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVRor | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvRor |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVRotateL | What4.Protocol.VerilogWriter.AST
BVRotateR | What4.Protocol.VerilogWriter.AST
BVSdiv | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvSDiv |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvSdiv | What4.Interface
bvsdiv | What4.Protocol.SMTLib2.Syntax
BVSelect | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvSelect | What4.Interface
bvSet | What4.Interface
bvSetBE | What4.SWord
bvSetLE | What4.SWord
BVSext | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvSext |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
bvSge | What4.Interface
bvsge |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvSgt | What4.Interface
bvsgt |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
BVShiftL | What4.Protocol.VerilogWriter.AST
BVShiftR | What4.Protocol.VerilogWriter.AST
BVShiftRA | What4.Protocol.VerilogWriter.AST
BVShl | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvShl |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvshl | What4.Protocol.SMTLib2.Syntax
bvsignExtend | What4.Protocol.SMTLib2.Syntax
bvSLe | What4.Protocol.SMTWriter
bvSle | What4.Interface
bvsle |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvSliceBE | What4.SWord
bvSliceLE | What4.SWord
BVSlt | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvSLt | What4.Protocol.SMTWriter
bvSlt | What4.Interface
bvslt |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvSort | What4.Protocol.SMTLib2.Syntax
bvSplitVector | What4.Interface
BVSrem | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvSRem |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvSrem | What4.Interface
bvsrem | What4.Protocol.SMTLib2.Syntax
BVSub | What4.Protocol.VerilogWriter.AST
bvSub |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
3 (Function) | What4.Protocol.SMTWriter
bvsub | What4.Protocol.SMTLib2.Syntax
bvSum | What4.Expr.Builder
bvSumExpr | What4.Protocol.SMTWriter
bvSwap | What4.Interface
BVSymbolic | What4.Utils.ResolveBounds.BV
BVTerm | What4.Protocol.SMTLib2.Parse
bvTerm | What4.Protocol.SMTWriter
BVTestBit | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvTestBit | What4.Protocol.SMTWriter
BVToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvToFloat |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
BVToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvToInteger |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
BVToIntegerFn | What4.Expr.MATLAB
bvToNat | What4.Interface
bvTrunc | What4.Interface
BVTypeMap | What4.Protocol.SMTWriter
BVUdiv | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvUDiv |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvUdiv | What4.Interface
bvudiv | What4.Protocol.SMTLib2.Syntax
bvUge | What4.Interface
bvuge |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvUgt | What4.Interface
bvugt |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvULe | What4.Protocol.SMTWriter
bvUle | What4.Interface
bvule |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
BVUlt | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvULt | What4.Protocol.SMTWriter
bvUlt | What4.Interface
bvult |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SWord
bvUnary | What4.Expr.Builder
BVUnaryTerm | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvUnpackBE | What4.SWord
bvUnpackLE | What4.SWord
BVUrem | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvURem |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvUrem | What4.Interface
bvurem | What4.Protocol.SMTLib2.Syntax
bvWidth |
1 (Function) | What4.Interface, What4.Expr.Builder
2 (Function) | What4.SWord
BVXor | What4.Protocol.VerilogWriter.AST
bvXor |
1 (Function) | What4.SWord
2 (Function) | What4.Protocol.SMTWriter
bvxor | What4.Protocol.SMTLib2.Syntax
bvXorBits | What4.Interface
bvZero | What4.Interface
bvzeroExtend | What4.Protocol.SMTLib2.Syntax
BVZext | What4.Expr.App, What4.Expr.Builder, What4.Expr
bvZext |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
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
dblPosIsPos | What4.BaseTypes, What4.Interface
DBV | What4.SWord
Debug | What4.Serialize.Log
decDoc | What4.Protocol.VerilogWriter.ABCVerilog
decideLeq | What4.BaseTypes, What4.Interface
decimal | What4.Protocol.SMTLib2.Syntax
declareCommand | What4.Protocol.SMTWriter
declareConst | What4.Protocol.SMTLib2.Syntax
declareFun | What4.Protocol.SMTLib2.Syntax
declareSort | What4.Protocol.SMTLib2.Syntax
DeclareSortResponse | What4.Protocol.SMTLib2.Parse
declareStructDatatype | What4.Protocol.SMTWriter
declareVar | What4.Protocol.SMTLib2.Syntax
declareVarCommand | What4.Protocol.SMTWriter
decNat | What4.BaseTypes, What4.Interface
defaultConfig |
1 (Function) | What4.Serialize.Printer
2 (Function) | What4.Serialize.Parser
defaultFeatures | What4.Protocol.SMTLib2
defaultFileWriter | What4.Protocol.SMTLib2
defaultLogData | What4.Solver.Adapter, What4.Solver
defaultPPExprOpts | What4.Expr.App
defaultSolverAdapter | What4.Solver.Adapter, What4.Solver
defaultSolverArgs | What4.Protocol.SMTLib2
defaultSolverBounds | What4.Protocol.SMTLib2
defaultSolverPath | What4.Protocol.SMTLib2
defaultValueForType | What4.Expr.GroundEval
defaultWriteSMTLIB2Features | What4.Solver.Adapter
defineCommand | What4.Protocol.SMTWriter
definedFn | What4.Interface
DefinedFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr
DefineFun |
1 (Type/Class) | What4.Protocol.SMTLib2.Parse
2 (Data Constructor) | What4.Protocol.SMTLib2.Parse
defineFun | What4.Protocol.SMTLib2.Syntax
DefineFunResponse | What4.Protocol.SMTLib2.Parse
defineSort | What4.Protocol.SMTLib2.Syntax
DefineStyle | What4.Protocol.SMTWriter
delete |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Expr.ArrayUpdateMap
deleteFindMax | What4.Utils.LeqMap
deleteFindMin | What4.Utils.LeqMap
deleteIdxValue | What4.Expr.Builder
demuxProcessHandles | What4.Utils.HandleReader
deprecatedOpt | What4.Config
deserializeBaseType | What4.Serialize.Parser
deserializeExpr | What4.Serialize.Parser
deserializeExprWithConfig | What4.Serialize.Parser
deserializeSymFn | What4.Serialize.Parser
deserializeSymFnWithConfig | What4.Serialize.Parser
difference | What4.Utils.AnnotatedMap
distinct | What4.Protocol.SMTLib2.Syntax
div | What4.Protocol.SMTLib2.Syntax
divNat | What4.BaseTypes, What4.Interface
Domain |
1 (Type/Class) | What4.Utils.BVDomain.Arith
2 (Type/Class) | What4.Utils.BVDomain.Bitwise
3 (Type/Class) | What4.Utils.BVDomain.XOR
domain | What4.Expr.UnaryBV
domainsOverlap |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
DoubleDoubleFloat | What4.InterpretedFloatingPoint
DoubleDoubleFloatRepr | What4.InterpretedFloatingPoint
DoubleFloat | What4.InterpretedFloatingPoint
DoubleFloatRepr | What4.InterpretedFloatingPoint
DReal |
1 (Type/Class) | What4.Solver.DReal, What4.Solver
2 (Data Constructor) | What4.Solver.DReal, What4.Solver
drealAdapter | What4.Solver.DReal, What4.Solver
DRealBindings | What4.Solver.DReal, What4.Solver
drealOptions | What4.Solver.DReal
drealPath | What4.Solver.DReal, What4.Solver
drop | What4.Utils.Word16String
Dummy | What4.Expr.App
E | What4.SpecialFunctions
efSolveCommand | What4.Solver.Yices
empty |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.LeqMap
3 (Function) | What4.Utils.Word16String
4 (Function) | What4.Expr.ArrayUpdateMap
EmptyExprBuilderState |
1 (Type/Class) | What4.Expr
2 (Data Constructor) | What4.Expr
emptySolverBounds | What4.Utils.Versions
emptySymbol | What4.Symbol, What4.Interface
emptySymbolVarBimap | What4.Expr.Builder
emptyWordMap | What4.WordMap
Endian | What4.Utils.Endian
entryStackHeight | What4.Protocol.SMTWriter
enumOptSty | What4.Config
Eq | What4.Protocol.VerilogWriter.AST
eq |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
3 (Function) | What4.Utils.BVDomain.Arith
4 (Function) | What4.Utils.BVDomain.Bitwise
5 (Function) | What4.Utils.BVDomain
6 (Function) | What4.Expr.UnaryBV
eqBy | What4.Utils.AnnotatedMap
eqPred | What4.Interface
EqualArrayRange | What4.Expr.App, What4.Expr.Builder, What4.Expr
EqualityDefinition | What4.Protocol.SMTWriter
Err | What4.Partial
Error | What4.Serialize.Log
ErrorBehavior |
1 (Data Constructor) | What4.Protocol.SMTLib2.Syntax
2 (Type/Class) | What4.Protocol.Online
eval |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Solver.Yices
evalBoundVars | What4.Expr.Builder
evalGroundApp | What4.Expr.GroundEval
evalGroundExpr | What4.Expr.GroundEval
evalGroundNonceApp | What4.Expr.GroundEval
evalM | What4.Expr.WeightedSum
evalMatlabSolverFn | What4.Expr.MATLAB
evaluate | What4.Expr.UnaryBV
EvenFunction | What4.SpecialFunctions
Excl | What4.SpecialFunctions
Exclusive | What4.Config
executablePathOptSty | What4.Config
execVerilogM | What4.Protocol.VerilogWriter.AST
ExistBound | What4.Expr.VarIdentification
existQuantifiers | What4.Expr.VarIdentification
Exists | What4.Expr.App, What4.Expr.Builder, What4.Expr
existsExpr | What4.Protocol.SMTWriter
ExistsForall | What4.Expr.VarIdentification
ExistsOnly | What4.Expr.VarIdentification
existsPred | What4.Interface
exists_ | What4.Protocol.SMTLib2.Syntax
exit | What4.Protocol.SMTLib2.Syntax
Exp |
1 (Data Constructor) | What4.SpecialFunctions
2 (Type/Class) | What4.Protocol.VerilogWriter.AST
Exp10 | What4.SpecialFunctions
Exp2 | What4.SpecialFunctions
expandEnvironmentPath | What4.Utils.Environment
expDoc | What4.Protocol.VerilogWriter.ABCVerilog
Expm1 | What4.SpecialFunctions
exponentBits | What4.SFloat
ExponentialSearch | What4.Utils.ResolveBounds.BV
Expr | What4.Expr.App, What4.Expr.Builder, What4.Expr
exprAbsValue | What4.Expr.App
ExprAllocator |
1 (Type/Class) | What4.Expr.Allocator
2 (Data Constructor) | What4.Expr.Allocator
ExprBoundVar | What4.Expr.App, What4.Expr.Builder, What4.Expr
ExprBuilder | What4.Expr.Builder, What4.Expr
exprBuilderFreshConfig | What4.Expr.Builder, What4.Expr
exprBuilderSplitConfig | What4.Expr.Builder, What4.Expr
exprCounter | What4.Expr.Builder, What4.Expr
ExprEquivalent | What4.Serialize.Normalize
ExprEquivResult | What4.Serialize.Normalize
exprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
exprMaybeId | What4.Expr.Builder
ExprNormEquivalent | What4.Serialize.Normalize
ExprPPIndex | What4.Expr.App
exprPrettyArg | What4.Expr.App
exprPrettyIndices | What4.Expr.App
ExprRangeBindings | What4.Expr.GroundEval, What4.Expr, What4.Solver.DReal, What4.Solver
exprsToModule | What4.Protocol.VerilogWriter
exprsVerilog | What4.Protocol.VerilogWriter
ExprSymFn |
1 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
ExprSymFnWrapper |
1 (Type/Class) | What4.Expr.Builder
2 (Data Constructor) | What4.Expr.Builder
exprToVerilogExpr | What4.Protocol.VerilogWriter.Backend
exprType | What4.Interface, What4.Expr.Builder
ExprUnequal | What4.Serialize.Normalize
exprUninterpConstants | What4.Interface
expType | What4.Protocol.VerilogWriter.AST
extendConfig | What4.Config
ExternalABC |
1 (Type/Class) | What4.Solver.ExternalABC, What4.Solver
2 (Data Constructor) | What4.Solver.ExternalABC, What4.Solver
externalABCAdapter | What4.Solver.ExternalABC, What4.Solver
extract | What4.Protocol.SMTLib2.Syntax
extractCommon | What4.Expr.WeightedSum
false | What4.Protocol.SMTLib2.Syntax
falsePred | What4.Interface
fileLogEventConsumer | What4.Serialize.Log
fillright | What4.Utils.BVDomain.Arith
filter |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Expr.ArrayUpdateMap
filterAsync | What4.Utils.Process
filterGt | What4.Utils.LeqMap
filterLt | What4.Utils.LeqMap
findExecutable | What4.Utils.Environment
findExprToRemove | What4.Expr.App
findMax | What4.Utils.LeqMap
findMin | What4.Utils.LeqMap
findSolverPath | What4.Utils.Process
findSubstring | What4.Utils.Word16String
FixedPPExpr | What4.Expr.App
Flags | What4.Expr.Builder, What4.Expr
float | What4.Serialize.SETokens
FloatAbs | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatAbs |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatAdd | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatAdd |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatCast | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatCast |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatDiv |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatEq |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder
FloatFMA | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatFMA |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatFpApart | What4.Interface
FloatFpEq | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatFpEq |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatFpUnordered | What4.Interface
FloatFromBinary | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatFromBinary |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatFromInteger | What4.Utils.FloatHelpers
floatFromRational | What4.Utils.FloatHelpers
floatGe | What4.Interface
floatGt | What4.Interface
FloatIEEE | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatIEEERepr | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatInfo | What4.InterpretedFloatingPoint
FloatInfoRepr | What4.InterpretedFloatingPoint
FloatInfoToBitWidth | What4.InterpretedFloatingPoint
floatInfoToBVTypeRepr | What4.InterpretedFloatingPoint
FloatInfoToPrecision | What4.InterpretedFloatingPoint
floatInfoToPrecisionRepr | What4.InterpretedFloatingPoint
FloatingPoint | What4.Protocol.SMTLib2.Parse
FloatingPointPrecision | What4.BaseTypes, What4.Interface
FloatingPointPrecisionRepr | What4.BaseTypes, What4.Interface
FloatingPointTheory | What4.Expr.AppTheory, What4.Expr
FloatIsInf | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsInf |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsNaN | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNaN |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsNeg | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNeg |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsNorm | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNorm |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsPos | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsPos |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsSubnorm | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsSubnorm |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatIsZero | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsZero |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatIte | What4.Interface
FloatLe | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatLe |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatLit | What4.Interface
floatLitRational | What4.Interface
FloatLt | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatLt |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatMax | What4.Interface
floatMin | What4.Interface
FloatMode | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatModeRepr | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatMul | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatMul |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatNaN | What4.Interface
floatNe | What4.Interface
FloatNeg | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatNeg |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatNInf | What4.Interface
floatNZero | What4.Interface
floatPInf | What4.Interface
FloatPrecision | What4.BaseTypes, What4.Interface
floatPrecision | What4.Interface
FloatPrecisionBits | What4.BaseTypes, What4.Interface
FloatPrecisionRepr | What4.BaseTypes, What4.Interface
floatPrecisionToBVType | What4.BaseTypes, What4.Interface
FloatPrecisionToInfo | What4.InterpretedFloatingPoint
floatPrecisionToInfoRepr | What4.InterpretedFloatingPoint
floatPZero | What4.Interface
FloatReal | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatRealRepr | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatRem | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatRem |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatRound | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatRound |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatRoundToInt | What4.Utils.FloatHelpers
FloatSpecialFunction | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatSpecialFunction | What4.Interface
FloatSqrt | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatSqrt |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatSub | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatSub |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatTerm | What4.Protocol.SMTWriter
FloatToBinary | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatToBinary | What4.Interface
FloatToBV | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatToBV |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
floatToInteger | What4.Utils.FloatHelpers
floatToRational | What4.Utils.FloatHelpers
FloatToReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatToReal |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatToSBV | What4.Expr.App, What4.Expr.Builder, What4.Expr
floatToSBV |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
FloatTypeMap | What4.Protocol.SMTWriter
FloatUninterpreted | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloatUninterpretedRepr | What4.FloatMode, What4.Expr.Builder, What4.Expr
FloorReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
FnApp | What4.Expr.App, What4.Expr.Builder, What4.Expr
fnArgTypes | What4.Interface
FnArrayTypeMap | What4.Protocol.SMTWriter
fnCompare | What4.Interface
fnReturnType | What4.Interface
FnSymbolBinding | What4.Expr.Builder
fnTestEquality | What4.Interface
FnTheory | What4.Expr.AppTheory, What4.Expr
foldl' | What4.Utils.Word16String
foldlWithKey' | What4.Utils.LeqMap
Forall | What4.Expr.App, What4.Expr.Builder, What4.Expr
ForallBound | What4.Expr.VarIdentification
forallExpr | What4.Protocol.SMTWriter
forallPred | What4.Interface
forallQuantifiers | What4.Expr.VarIdentification
forall_ | What4.Protocol.SMTLib2.Syntax
forgetModelAndCore | What4.SatResult, What4.Solver
fp80ToBits | What4.InterpretedFloatingPoint
fp80ToRational | What4.InterpretedFloatingPoint
fpAbs | What4.SFloat
fpActual | What4.SFloat
fpAdd | What4.SFloat
fpAsLit | What4.SFloat
fpDiv | What4.SFloat
fpEq | What4.SFloat
fpEqIEEE | What4.SFloat
fpExpected | What4.SFloat
fpFMA | What4.SFloat
fpFresh | What4.SFloat
fpFromBinary | What4.SFloat
fpFromInteger | What4.SFloat
fpFromLit | What4.SFloat
fpFromRational | What4.SFloat
fpFromRationalLit | What4.SFloat
fpFromReal | What4.SFloat
fpGtIEEE | What4.SFloat
fpIsInf | What4.SFloat
fpIsNaN | What4.SFloat
fpIsNeg | What4.SFloat
fpIsNorm | What4.SFloat
fpIsSubnorm | What4.SFloat
fpIsZero | What4.SFloat
fpIte | What4.SFloat
fpLtIEEE | What4.SFloat
fpMax | What4.SFloat
fpMin | What4.SFloat
fpMul | What4.SFloat
fpNaN | What4.SFloat
fpNeg | What4.SFloat
fpNegInf | What4.SFloat
fpOpts | What4.Utils.FloatHelpers
fppOpts | What4.Utils.FloatHelpers
fpPosInf | What4.SFloat
fpRepr | What4.SFloat
fpReprOf | What4.SFloat
fpRound | What4.SFloat
fpSize | What4.SFloat
fpSqrt | What4.SFloat
fpSub | What4.SFloat
fpToBinary | What4.SFloat
fpToRational | What4.SFloat
fpToReal | What4.SFloat
FPTypeError |
1 (Type/Class) | What4.SFloat
2 (Data Constructor) | What4.SFloat
fpWho | What4.SFloat
freshBoundedBV | What4.Interface
freshBoundedInt | What4.Interface
freshBoundedNat | What4.Interface
freshBoundedReal | What4.Interface
freshBoundedSBV | What4.Interface
freshBoundVar | What4.Interface
freshBoundVarName | What4.Protocol.SMTWriter
freshBV | What4.SWord
freshConstant | What4.Interface
freshFloatBoundVar | What4.InterpretedFloatingPoint
freshFloatConstant | What4.InterpretedFloatingPoint
freshFloatLatch | What4.InterpretedFloatingPoint
freshIdentifier | What4.Protocol.VerilogWriter.AST
freshLatch | What4.Interface
freshNat | What4.Interface
freshTotalUninterpFn | What4.Interface
fromAscEltList |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
fromAscList |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Expr.ArrayUpdateMap
fromChar16Lit | What4.Utils.StringLiteral
fromChar8Lit | What4.Utils.StringLiteral
fromConcreteBool | What4.Concrete
fromConcreteBV | What4.Concrete
fromConcreteComplex | What4.Concrete
fromConcreteInteger | What4.Concrete
fromConcreteReal | What4.Concrete
fromConcreteString | What4.Concrete
fromDistinctAscList | What4.Utils.LeqMap
fromDistinctDescList | What4.Utils.LeqMap
fromLEByteString | What4.Utils.Word16String
fromTerms | What4.Expr.WeightedSum
fromText | What4.Protocol.SMTWriter
fromUnicodeLit | What4.Utils.StringLiteral
fromVars | What4.Expr.BoolMap
fromXorDomain | What4.Utils.BVDomain
fromYicesText | What4.Protocol.PolyRoot
funArgs | What4.Protocol.SMTLib2.Parse
FunctionDefinition | What4.Protocol.SMTWriter
FunctionName | What4.FunctionName
functionName | What4.FunctionName
functionNameFromText | What4.FunctionName
FunctionSymmetry | What4.SpecialFunctions
funDef | What4.Protocol.SMTLib2.Parse
funResultSort | What4.Protocol.SMTLib2.Parse
funSymbol | What4.Protocol.SMTLib2.Parse
ge | What4.Protocol.SMTLib2.Syntax
Gen | Test.Verification
genChooseBool | Test.Verification
genChooseInt | Test.Verification
genChooseInteger | Test.Verification
genDomain |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
genElement |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
GenEnv |
1 (Type/Class) | Test.Verification
2 (Data Constructor) | Test.Verification
genGetSize | Test.Verification
genPair |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
getAbduct | What4.Protocol.SMTLib2.Syntax
getAbductCommand | What4.Protocol.SMTWriter
getAbductNext | What4.Protocol.SMTLib2.Syntax
getAbductNextCommand | What4.Protocol.SMTWriter
getAbducts | What4.Protocol.Online
getAbsValue | What4.Utils.AbstractDomains
getAnnotation | What4.Interface
getAvgBindings | What4.Solver.DReal
getBoundBindings | What4.Solver.DReal
getConfiguration | What4.Interface
getConfigValues | What4.Config
getCurrentProgramLoc | What4.Interface
getErrorBehavior |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
getGoalTimeoutInMilliSeconds | What4.Protocol.Online
getGoalTimeoutInSeconds | What4.Protocol.Online
getImagPart | What4.Interface
getInfo | What4.Protocol.SMTLib2.Syntax
getLimitedSolverResponse | What4.Protocol.SMTLib2.Response
getLogCfg | What4.Serialize.Log
getLogCfgM | What4.Serialize.Log
getMaybeOpt | What4.Config
getModel |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.Online
GetModelResponse | What4.Protocol.SMTLib2.Parse
getName |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
getOpt | What4.Config
getOption | What4.Config
getOptionSetting | What4.Config
getOptionSettingFromText | What4.Config
getRealPart | What4.Interface
getSatResult | What4.Protocol.Online
getSize | Test.Verification
getSolverLogListener | What4.Interface
getSolverResponse | What4.Protocol.SMTLib2.Response
getStatistics | What4.Interface
getSymbolVarBimap | What4.Expr.Builder
getUnannotatedTerm | What4.Interface
getUnsatAssumptions |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.Online
getUnsatAssumptionsCommand | What4.Protocol.SMTWriter
getUnsatCore |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.Online
getUnsatCoreCommand | What4.Protocol.SMTWriter
getValue | What4.Protocol.SMTLib2.Syntax
getVersion |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
GroundArray | What4.Expr.GroundEval, What4.Expr
groundEq | What4.Expr.GroundEval
groundEval | What4.Expr.GroundEval, What4.Expr
GroundEvalFn |
1 (Type/Class) | What4.Expr.GroundEval, What4.Expr
2 (Data Constructor) | What4.Expr.GroundEval, What4.Expr
groundToSym | What4.Expr.GroundEval
GroundValue | What4.Expr.GroundEval, What4.Expr
GroundValueWrapper | What4.Expr.GroundEval, What4.Expr
gt | What4.Protocol.SMTLib2.Syntax
GVW | What4.Expr.GroundEval, What4.Expr
HalfFloat | What4.InterpretedFloatingPoint
HalfFloatRepr | What4.InterpretedFloatingPoint
halfNat | What4.BaseTypes, What4.Interface
HalfPi | What4.SpecialFunctions
HandleReader |
1 (Type/Class) | What4.Utils.HandleReader, What4.Solver.Yices
2 (Data Constructor) | What4.Utils.HandleReader
HasAbsValue | What4.Utils.AbstractDomains, What4.Interface
HasCallStack | What4.Panic, What4.Serialize.Log
hashApp | What4.Expr.App
hashIndexLit | What4.IndexLit
HasLogCfg | What4.Serialize.Log
hasProblemFeature | What4.ProblemFeatures
HasProgramLoc | What4.ProgramLoc
hexDoc | What4.Protocol.VerilogWriter.ABCVerilog
hornLogic | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
hrChan | What4.Utils.HandleReader
hrHandle | What4.Utils.HandleReader
hrThreadId | What4.Utils.HandleReader
Hypot | What4.SpecialFunctions
iBVToFloat | What4.InterpretedFloatingPoint
Ident | What4.Protocol.VerilogWriter.AST
ident | What4.Serialize.SETokens, What4.Serialize.Printer
ident' | What4.Serialize.SETokens
identDoc | What4.Protocol.VerilogWriter.ABCVerilog
Identifier | What4.Protocol.VerilogWriter.AST
IdxCache | What4.Expr.Builder
idxCacheEval | What4.Expr.Builder
idxCacheEval' | What4.Expr.Builder
IExp |
1 (Data Constructor) | What4.Protocol.VerilogWriter.AST
2 (Type/Class) | What4.Protocol.VerilogWriter.AST
iexpDoc | What4.Protocol.VerilogWriter.ABCVerilog
iexpType | What4.Protocol.VerilogWriter.AST
IfEqTerm | What4.Protocol.SMTLib2.Parse
iFloatAbs | What4.InterpretedFloatingPoint
iFloatAdd | What4.InterpretedFloatingPoint
iFloatBaseTypeRepr | What4.InterpretedFloatingPoint
iFloatCast | What4.InterpretedFloatingPoint
iFloatDiv | What4.InterpretedFloatingPoint
iFloatEq | What4.InterpretedFloatingPoint
iFloatFMA | What4.InterpretedFloatingPoint
iFloatFpApart | What4.InterpretedFloatingPoint
iFloatFpEq | What4.InterpretedFloatingPoint
iFloatFromBinary | What4.InterpretedFloatingPoint
iFloatGe | What4.InterpretedFloatingPoint
iFloatGt | What4.InterpretedFloatingPoint
iFloatIsInf | What4.InterpretedFloatingPoint
iFloatIsNaN | What4.InterpretedFloatingPoint
iFloatIsNeg | What4.InterpretedFloatingPoint
iFloatIsNorm | What4.InterpretedFloatingPoint
iFloatIsPos | What4.InterpretedFloatingPoint
iFloatIsSubnorm | What4.InterpretedFloatingPoint
iFloatIsZero | What4.InterpretedFloatingPoint
iFloatIte | What4.InterpretedFloatingPoint
iFloatLe | What4.InterpretedFloatingPoint
iFloatLitDouble | What4.InterpretedFloatingPoint
iFloatLitLongDouble | What4.InterpretedFloatingPoint
iFloatLitRational | What4.InterpretedFloatingPoint
iFloatLitSingle | What4.InterpretedFloatingPoint
iFloatLt | What4.InterpretedFloatingPoint
iFloatMax | What4.InterpretedFloatingPoint
iFloatMin | What4.InterpretedFloatingPoint
iFloatMul | What4.InterpretedFloatingPoint
iFloatNaN | What4.InterpretedFloatingPoint
iFloatNe | What4.InterpretedFloatingPoint
iFloatNeg | What4.InterpretedFloatingPoint
iFloatNInf | What4.InterpretedFloatingPoint
iFloatNZero | What4.InterpretedFloatingPoint
iFloatPInf | What4.InterpretedFloatingPoint
iFloatPZero | What4.InterpretedFloatingPoint
iFloatRem | What4.InterpretedFloatingPoint
iFloatRound | What4.InterpretedFloatingPoint
iFloatSpecialFunction | What4.InterpretedFloatingPoint
iFloatSpecialFunction0 | What4.InterpretedFloatingPoint
iFloatSpecialFunction1 | What4.InterpretedFloatingPoint
iFloatSpecialFunction2 | What4.InterpretedFloatingPoint
iFloatSqrt | What4.InterpretedFloatingPoint
iFloatSub | What4.InterpretedFloatingPoint
iFloatToBinary | What4.InterpretedFloatingPoint
iFloatToBV | What4.InterpretedFloatingPoint
iFloatToReal | What4.InterpretedFloatingPoint
iFloatToSBV | What4.InterpretedFloatingPoint
ImagPart | What4.Expr.App, What4.Expr.Builder, What4.Expr
imagPart | What4.Utils.Complex
ImagPartOfCplxFn | What4.Expr.MATLAB
ImmediateExit | What4.Protocol.Online
implies | What4.Protocol.SMTLib2.Syntax
impliesExpr | What4.Protocol.SMTWriter
impliesPred | What4.Interface
Incl | What4.SpecialFunctions
Inclusive |
1 (Data Constructor) | What4.Utils.AbstractDomains
2 (Data Constructor) | What4.Config
incNat | What4.BaseTypes, What4.Interface
incOccurrence | What4.Expr.App
IncrHash | What4.Utils.IncrHash
index | What4.Utils.Word16String
IndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder
indexLit | What4.Interface
IndicesInRange | What4.Expr.MATLAB
Info | What4.Serialize.Log
InfoKeyword | What4.Protocol.SMTLib2.Syntax
initialConfig | What4.Config
initializationLoc | What4.ProgramLoc
initModuleState | What4.Protocol.VerilogWriter.AST
inlineDefineFun | What4.Interface
inNewFrame | What4.Protocol.Online, What4.Solver.Yices
inNewFrame2Close | What4.Protocol.Online
inNewFrame2Open | What4.Protocol.Online
inNewFrameWithVars | What4.Protocol.Online
Input | What4.Protocol.VerilogWriter.AST
inputDoc | What4.Protocol.VerilogWriter.ABCVerilog
insert |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.LeqMap
3 (Function) | What4.Expr.ArrayUpdateMap
insertIdxValue | What4.Expr.Builder
insertWordMap | What4.WordMap
instantiate | What4.Expr.UnaryBV
Int | What4.Protocol.SMTLib2.Parse
int | What4.Serialize.SETokens, What4.Serialize.Printer
IntAbs | What4.Expr.App, What4.Expr.Builder, What4.Expr
intAbs |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
intAbsRange | What4.Utils.AbstractDomains
intAdd | What4.Interface
IntDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr
intDiv |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
IntDivisible | What4.Expr.App, What4.Expr.Builder, What4.Expr
intDivisible |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
intDivRange | What4.Utils.AbstractDomains
integerBounds | What4.Interface
IntegerExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
integerOptSty | What4.Config
integerTerm | What4.Protocol.SMTWriter
IntegerToBV | What4.Expr.App, What4.Expr.Builder, What4.Expr
integerToBV |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
integerToNat | What4.Interface
IntegerToReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
integerToReal | What4.Interface
IntegerToRealFn | What4.Expr.MATLAB
IntegerTypeMap | What4.Protocol.SMTWriter
integerWithMaxOptSty | What4.Config
integerWithMinOptSty | What4.Config
integerWithRangeOptSty | What4.Config
intEq | What4.Interface
InternalPos | What4.ProgramLoc
intersection | What4.Utils.BVDomain.Bitwise
interval |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
IntervalRange | What4.Utils.AbstractDomains, What4.Interface
IntIndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder
intIte | What4.Interface
intLe | What4.Interface
IntLeFn | What4.Expr.MATLAB
intLit | What4.Interface
intLt | What4.Interface
intMax | What4.Interface
intMin | What4.Interface
IntMod | What4.Expr.App, What4.Expr.Builder, What4.Expr
intMod |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
intModRange | What4.Utils.AbstractDomains
intMul | What4.Interface
intNeg | What4.Interface
IntSeqFn | What4.Expr.MATLAB
intSetWidth | What4.Interface
IntSetWidthFn | What4.Expr.MATLAB
intSort | What4.Protocol.SMTLib2.Syntax
intSub | What4.Interface
intSum | What4.Expr.Builder
IntTerm | What4.Protocol.SMTLib2.Parse
intToUInt | What4.Interface
IntToUIntFn | What4.Expr.MATLAB
intValue | What4.BaseTypes, What4.Interface
InvalidRange |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
iRealToFloat | What4.InterpretedFloatingPoint
iSBVToFloat | What4.InterpretedFloatingPoint
isEq | What4.Interface
IsEqFn | What4.Expr.MATLAB
IsExpr | What4.Interface
IsExprBuilder | What4.Interface
isInconsistent | What4.Expr.BoolMap
isInfixOf | What4.Utils.Word16String
isInt | What4.Protocol.SMTLib2.Syntax
isInteger | What4.Interface
IsIntegerFn | What4.Expr.MATLAB
IsInterpretedFloatExprBuilder | What4.InterpretedFloatingPoint
IsInterpretedFloatSymExprBuilder | What4.InterpretedFloatingPoint
isNonLinearApp | What4.Expr.App
isNonZero | What4.Interface
isNull | What4.Expr.BoolMap
isPosNat | What4.BaseTypes, What4.Interface
isPow2 | What4.Utils.Arithmetic
isPrefixOf | What4.Utils.Word16String
isReal | What4.Interface
isSat | What4.SatResult, What4.Solver
isSuffixOf | What4.Utils.Word16String
IsSymExprBuilder | What4.Interface
IsSymFn | What4.Interface
isUltSumCommonEquiv |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
isUnknown | What4.SatResult, What4.Solver
isUnsat | What4.SatResult, What4.Solver
isZero | What4.Expr.WeightedSum
IsZeroNat | What4.BaseTypes, What4.Interface
isZeroNat | What4.BaseTypes, What4.Interface
isZeroOrGT1 | What4.BaseTypes, What4.Interface
ite |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTWriter
iteList | What4.Interface
Item | What4.Protocol.VerilogWriter.AST
iteM | What4.Interface
itePred | What4.Interface
itePredM | What4.Interface
iteSize | What4.Expr.App, What4.Expr.Builder
joinMaybePE | What4.Partial
joinRange | What4.Utils.AbstractDomains
justPartExpr | What4.Partial
keys | What4.Utils.LeqMap
keysSet | What4.Expr.ArrayUpdateMap
killSolver | What4.Protocol.Online
KnownCtx | What4.BaseTypes, What4.Interface
knownNat | What4.BaseTypes, What4.Interface
KnownRepr | What4.BaseTypes, What4.Interface
knownRepr | What4.BaseTypes, What4.Interface
L | What4.Serialize.Printer
LabeledPred |
1 (Type/Class) | What4.LabeledPred
2 (Data Constructor) | What4.LabeledPred
labeledPred | What4.LabeledPred
labeledPredMsg | What4.LabeledPred
lambdaTerm | What4.Protocol.SMTWriter
latches | What4.Expr.VarIdentification
LatchVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr
Le | What4.Protocol.VerilogWriter.AST
le |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
leCallSite | What4.Serialize.Log
leLevel | What4.Serialize.Log
lemmaFloatPrecisionIsPos | What4.BaseTypes, What4.Interface
lemmaMul | What4.BaseTypes, What4.Interface
leMsg | What4.Serialize.Log
length | What4.Utils.Word16String
Lenient | What4.Protocol.SMTWriter
leqAdd | What4.BaseTypes, What4.Interface
leqAdd2 | What4.BaseTypes, What4.Interface
leqAddPos | What4.BaseTypes, What4.Interface
LeqMap | What4.Utils.LeqMap
leqMulCongr | What4.BaseTypes, What4.Interface
leqMulMono | What4.BaseTypes, What4.Interface
leqMulPos | What4.BaseTypes, What4.Interface
LeqProof |
1 (Type/Class) | What4.BaseTypes, What4.Interface
2 (Data Constructor) | What4.BaseTypes, What4.Interface
leqProof | What4.BaseTypes, What4.Interface
leqRefl | What4.BaseTypes, What4.Interface
leqSub | What4.BaseTypes, What4.Interface
leqSub2 | What4.BaseTypes, What4.Interface
leqSucc | What4.BaseTypes, What4.Interface
leqTrans | What4.BaseTypes, What4.Interface
leqZero | What4.BaseTypes, What4.Interface
lessThanAsymmetric | What4.BaseTypes, What4.Interface
lessThanIrreflexive | What4.BaseTypes, What4.Interface
letBinder | What4.Protocol.SMTLib2.Syntax
letExpr | What4.Protocol.SMTWriter
leThreadId | What4.Serialize.Log
leTime | What4.Serialize.Log
lg | What4.Utils.Arithmetic
lgCeil | What4.Utils.Arithmetic
LHS |
1 (Type/Class) | What4.Protocol.VerilogWriter.AST
2 (Data Constructor) | What4.Protocol.VerilogWriter.AST
LHSBit | What4.Protocol.VerilogWriter.AST
lhsDoc | What4.Protocol.VerilogWriter.ABCVerilog
liftST | What4.Utils.MonadST
LinearArithTheory | What4.Expr.AppTheory, What4.Expr
lineBufferedOutputStream | What4.Utils.HandleReader
listOptSty | What4.Config
litBool | What4.Protocol.VerilogWriter.AST
litBV | What4.Protocol.VerilogWriter.AST
LittleEndian | What4.Utils.Endian
Ln_10 | What4.SpecialFunctions
Ln_2 | What4.SpecialFunctions
Log | What4.SpecialFunctions
Log10 | What4.SpecialFunctions
Log10_E | What4.SpecialFunctions
Log1p | What4.SpecialFunctions
Log2 | What4.SpecialFunctions
Log2_E | What4.SpecialFunctions
logCallback | What4.Solver.Adapter, What4.Solver
logCallbackVerbose | What4.Solver.Adapter, What4.Solver
LogCfg | What4.Serialize.Log
LogData |
1 (Type/Class) | What4.Solver.Adapter, What4.Solver
2 (Data Constructor) | What4.Solver.Adapter, What4.Solver
logEndWith | What4.Serialize.Log
logErrorStream | What4.Utils.Streams
LogEvent |
1 (Type/Class) | What4.Serialize.Log
2 (Data Constructor) | What4.Serialize.Log
logHandle | What4.Solver.Adapter, What4.Solver
Logic |
1 (Type/Class) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
2 (Data Constructor) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
logIO | What4.Serialize.Log
logIOWith | What4.Serialize.Log
LogLevel | What4.Serialize.Log
logM | What4.Serialize.Log
LogMsg | What4.Serialize.Log
logReason | What4.Solver.Adapter, What4.Solver
logSolverEvent | What4.Interface
logTrace | What4.Serialize.Log
logVerbosity | What4.Solver.Adapter, What4.Solver
lookup |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Expr.ArrayUpdateMap
lookupArray | What4.Expr.GroundEval, What4.Expr
lookupBindingOfSymbol | What4.Expr.Builder
lookupGE | What4.Utils.LeqMap
lookupGT | What4.Utils.LeqMap
lookupIdx | What4.Expr.Builder
lookupIdxValue | What4.Expr.Builder
lookupLE | What4.Utils.LeqMap
lookupLT | What4.Utils.LeqMap
lookupSymbolOfBinding | What4.Expr.Builder
lookupWordMap | What4.WordMap
lower | What4.Utils.Versions
lshr |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
Lt | What4.Protocol.VerilogWriter.AST
lt |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
magnitude | What4.Utils.Complex
magnitudeSq | What4.Utils.Complex
makeSymbol | What4.Utils.Serialize
mapKeysMonotonic | What4.Utils.LeqMap
mapMaybe | What4.Utils.AnnotatedMap
mapMaybeWithKey | What4.Utils.AnnotatedMap
MapOverArrays | What4.Expr.App, What4.Expr.Builder, What4.Expr
mapRange | What4.Utils.AbstractDomains
matlabSolverArgTypes | What4.Expr.MATLAB
MatlabSolverFn | What4.Expr.MATLAB
MatlabSolverFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr
matlabSolverReturnType | What4.Expr.MATLAB
MatlabSymbolicArrayBuilder | What4.Expr.MATLAB
maxNat | What4.BaseTypes, What4.Interface
MaxRange | What4.Utils.AbstractDomains, What4.Interface
maxSigned | What4.BaseTypes, What4.Interface
maxSignedBV | What4.Interface
maxUnsigned | What4.BaseTypes, What4.Interface
maxUnsignedBV | What4.Interface
maxValueBound | What4.Utils.AbstractDomains
maybePartExpr | What4.Partial
member |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
mergeA | What4.Utils.AnnotatedMap
mergeM | What4.Expr.ArrayUpdateMap
mergePartial | What4.Partial
mergePartials | What4.Partial
mergeWithKey |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.LeqMap
mergeWithKeyM | What4.Utils.AnnotatedMap
MinRange | What4.Utils.AbstractDomains, What4.Interface
minSigned | What4.BaseTypes, What4.Interface
minSignedBV | What4.Interface
minUnsigned | What4.BaseTypes, What4.Interface
minUnsignedBV | What4.Interface
minusPlusCancel | What4.BaseTypes, What4.Interface
minValueBound | What4.Utils.AbstractDomains
minViewWithKey | What4.Utils.LeqMap
mkAtomicFormula | What4.Protocol.SMTWriter
mkBaseExpr | What4.Protocol.SMTWriter
mkComplex | What4.Interface
mkComplexLit | What4.Interface
mkExpr | What4.Expr.App
mkFormula | What4.Protocol.SMTWriter
mkFreeVar | What4.Protocol.SMTWriter
mkIncrHash | What4.Utils.IncrHash
mkLet | What4.Protocol.VerilogWriter.AST
mkLogCfg | What4.Serialize.Log
mkMatlabSolverFn | What4.Expr.MATLAB
mkModule | What4.Protocol.VerilogWriter.AST
mkNatRepr | What4.BaseTypes, What4.Interface
mkNonLogCfg | What4.Serialize.Log
mkOpt | What4.Config
mkPE | What4.Partial
mkProgramLoc | What4.ProgramLoc
mkRational | What4.Interface
mkReal | What4.Interface
mkSMTTerm | What4.Protocol.SMTWriter
mkStruct | What4.Interface
mod | What4.Protocol.SMTLib2.Syntax
ModelResponse | What4.Protocol.SMTLib2.Parse
Module |
1 (Type/Class) | What4.Protocol.VerilogWriter.AST, What4.Protocol.VerilogWriter
2 (Data Constructor) | What4.Protocol.VerilogWriter.AST
moduleDoc | What4.Protocol.VerilogWriter.ABCVerilog
ModuleState |
1 (Type/Class) | What4.Protocol.VerilogWriter.AST
2 (Data Constructor) | What4.Protocol.VerilogWriter.AST
MonadHasLogCfg | What4.Serialize.Log
MonadST | What4.Utils.MonadST
mul |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
3 (Function) | What4.Utils.BVDomain.Arith
4 (Function) | What4.Utils.BVDomain
mul2Plus | What4.BaseTypes, What4.Interface
mulCancelR | What4.BaseTypes, What4.Interface
mulComm | What4.BaseTypes, What4.Interface
mulRange | What4.Utils.AbstractDomains
mulSignedOF | What4.Interface
MultiRange | What4.Utils.AbstractDomains
mulUnsignedOF | What4.Interface
Mux | What4.Protocol.VerilogWriter.AST
mux |
1 (Function) | What4.Expr.UnaryBV
2 (Function) | What4.Protocol.VerilogWriter.AST
muxRange | What4.Interface
muxWordMap | What4.WordMap
Name | What4.Protocol.SMTLib2.Syntax
named | What4.Serialize.Log
namedIO | What4.Serialize.Log
namedM | What4.Serialize.Log
namedTerm | What4.Protocol.SMTLib2.Syntax
nameResult | What4.Protocol.SMTLib2
nat | What4.Serialize.SETokens, What4.Serialize.Printer
natAdd | What4.Interface
NatCaseEQ | What4.BaseTypes, What4.Interface
NatCaseGT | What4.BaseTypes, What4.Interface
NatCaseLT | What4.BaseTypes, What4.Interface
NatCases | What4.BaseTypes, What4.Interface
NatComparison | What4.BaseTypes, What4.Interface
natDiv | What4.Interface
NatEQ | What4.BaseTypes, What4.Interface
natEq | What4.Interface
natForEach | What4.BaseTypes, What4.Interface
natFromZero | What4.BaseTypes, What4.Interface
NatGT | What4.BaseTypes, What4.Interface
natIte | What4.Interface
natLe | What4.Interface
natLit | What4.Interface
NatLT | What4.BaseTypes, What4.Interface
natLt | What4.Interface
natMod | What4.Interface
natMul | What4.Interface
natMultiply | What4.BaseTypes, What4.Interface
natRec | What4.BaseTypes, What4.Interface
natRecBounded | What4.BaseTypes, What4.Interface
natRecStrictlyBounded | What4.BaseTypes, What4.Interface
natRecStrong | What4.BaseTypes, What4.Interface
NatRepr | What4.BaseTypes, What4.Interface
natSub | What4.Interface
natToInteger | What4.Interface
natToIntegerPure | What4.Interface
natToReal | What4.Interface
natValue | What4.BaseTypes, What4.Interface
Ne | What4.Protocol.VerilogWriter.AST
neg | What4.Expr.UnaryBV
negate |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain
negatePolarity | What4.Expr.BoolMap, What4.Expr.Builder
negateRange | What4.Utils.AbstractDomains
Negative | What4.Expr.BoolMap, What4.Expr.VarIdentification, What4.Expr.Builder
NegHalfPi | What4.SpecialFunctions
NegInf | What4.SpecialFunctions
NegOne | What4.SpecialFunctions
NegPi | What4.SpecialFunctions
NeverUnfold | What4.Interface
newCachedStorage | What4.Expr.Allocator
newConnection | What4.Solver.Yices
newDefaultWriter | What4.Protocol.SMTLib2
newExprBuilder | What4.Expr.Builder, What4.Expr
newIdxCache | What4.Expr.Builder
newStorage | What4.Expr.Allocator
newWriter | What4.Protocol.SMTLib2
newWriterConn | What4.Protocol.SMTWriter
nextMultiple | What4.Utils.Arithmetic
nextPow2Multiple | What4.Utils.Arithmetic
NoErr | What4.Partial
noFeatures | What4.ProblemFeatures
NonceApp | What4.Expr.App, What4.Expr.Builder, What4.Expr
NonceAppExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
NonceAppExprCtor | What4.Expr.App
nonceAppType | What4.Expr.App, What4.Expr.Builder
nonceExpr | What4.Expr.Allocator
nonceExprAbsValue | What4.Expr.App
nonceExprApp | What4.Expr.App, What4.Expr.Builder, What4.Expr
nonceExprId | What4.Expr.App, What4.Expr.Builder, What4.Expr
nonceExprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
nonempty | What4.Utils.BVDomain.Bitwise
NonlinearArithTheory | What4.Expr.AppTheory, What4.Expr
NonZeroNat | What4.BaseTypes, What4.Interface
normExpr | What4.Serialize.Normalize
normSymFn | What4.Serialize.Normalize
NoSymmetry | What4.SpecialFunctions
Not | What4.Protocol.VerilogWriter.AST
not |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain
notExpr | What4.Protocol.SMTWriter
NotPred | What4.Expr.App, What4.Expr.Builder, What4.Expr
notPred | What4.Interface
null |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.LeqMap
3 (Function) | What4.Utils.Word16String
4 (Function) | What4.Expr.ArrayUpdateMap
nullAcknowledgementAction | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2
nullProd | What4.Expr.WeightedSum
numeral | What4.Protocol.SMTLib2.Syntax
Occurrence | What4.SemiRing
OccurrenceTable | What4.Expr.App
occ_add | What4.SemiRing
occ_compare | What4.SemiRing
occ_count | What4.SemiRing
occ_eq | What4.SemiRing
occ_hashWithSalt | What4.SemiRing
occ_one | What4.SemiRing
OddFunction | What4.SpecialFunctions
one | What4.SemiRing
OneOverPi | What4.SpecialFunctions
OnlineSolver | What4.Protocol.Online
OnlyIntRepr |
1 (Type/Class) | What4.Utils.OnlyIntRepr
2 (Data Constructor) | What4.Utils.OnlyIntRepr
Opt | What4.Config
opt | What4.Config
OptCreateFailure |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
optErr | What4.Config
OptGetFailure |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
optionSetError | What4.Config
OptionSetResult |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
OptionSetting |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
optionSettingName | What4.Config
optionSetWarnings | What4.Config
OptionStyle |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
optOK | What4.Config
OptSetFailure |
1 (Type/Class) | What4.Config
2 (Data Constructor) | What4.Config
optU | What4.Config
optUV | What4.Config
optV | What4.Config
optWarn | What4.Config
opt_default_value | What4.Config
opt_help | What4.Config
opt_onset | What4.Config
opt_type | What4.Config
Or | What4.Protocol.VerilogWriter.AST
or |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
orAll | What4.Protocol.SMTWriter
orderedSemiRing | What4.SemiRing
OrderedSemiRingIntegerRepr | What4.SemiRing, What4.Expr
OrderedSemiRingRealRepr | What4.SemiRing, What4.Expr
OrderedSemiRingRepr | What4.SemiRing, What4.Expr
orOneOf | What4.Interface
orPred | What4.Interface
OtherPos | What4.ProgramLoc
Output | What4.Protocol.VerilogWriter.AST
pairwise_app | What4.Protocol.SMTLib2.Syntax
Panic | What4.Panic
panic | What4.Panic
parenIf | What4.Expr.App
parseFnModel | What4.Protocol.SMTLib2
parseFnValues | What4.Protocol.SMTLib2
parseNextWord | What4.Protocol.SExp
parserStrictness | What4.Protocol.SMTWriter
parseSExp | What4.Protocol.SExp
parseSExpBody | What4.Protocol.SExp
parseSExpr |
1 (Function) | What4.Serialize.SETokens, What4.Serialize.Parser
2 (Function) | What4.Serialize.FastSExpr
parseSolverBounds | What4.Utils.Versions
parseYicesRoot | What4.Protocol.PolyRoot
PartExpr | What4.Partial
Partial |
1 (Type/Class) | What4.Partial
2 (Data Constructor) | What4.Partial
partialPred | What4.Partial
PartialT |
1 (Type/Class) | What4.Partial
2 (Data Constructor) | What4.Partial
partialValue | What4.Partial
PartialWithErr | What4.Partial
partitionByPreds | What4.LabeledPred
partitionByPredsM | What4.LabeledPred
partitionLabeledPreds | What4.LabeledPred
PE | What4.Partial
Pi | What4.SpecialFunctions
plFunction | What4.ProgramLoc
plSourceLoc | What4.ProgramLoc
plusAssoc | What4.BaseTypes, What4.Interface
plusComm | What4.BaseTypes, What4.Interface
plusMinusCancel | What4.BaseTypes, What4.Interface
pmember |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
Polarity | What4.Expr.BoolMap, What4.Expr.VarIdentification, What4.Expr.Builder
pop |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.Online, What4.Solver.Yices
pop2Command | What4.Protocol.SMTWriter
popcnt | What4.Utils.BVDomain
popCommand | What4.Protocol.SMTWriter
popEntryStack | What4.Protocol.SMTWriter
popEntryStackToTop | What4.Protocol.SMTWriter
popManyCommands | What4.Protocol.SMTWriter
pos | What4.ProgramLoc
Posd |
1 (Type/Class) | What4.ProgramLoc
2 (Data Constructor) | What4.ProgramLoc
PosHalfPi | What4.SpecialFunctions
PosInf | What4.SpecialFunctions
Position | What4.ProgramLoc
Positive | What4.Expr.BoolMap, What4.Expr.VarIdentification, What4.Expr.Builder
PosOne | What4.SpecialFunctions
PosPi | What4.SpecialFunctions
pos_val | What4.ProgramLoc
Pow | What4.SpecialFunctions
ppApp' | What4.Expr.App
ppBoundVar | What4.Expr.App, What4.Expr.Builder
ppConcrete | What4.Concrete
PPExpr | What4.Expr.App
ppExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
ppExpr' | What4.Expr.App
ppExprDoc | What4.Expr.App
ppExprLength | What4.Expr.App
PPExprOpts |
1 (Type/Class) | What4.Expr.App
2 (Data Constructor) | What4.Expr.App
ppExprTop | What4.Expr.App, What4.Expr.Builder
ppExpr_maxWidth | What4.Expr.App
ppExpr_useDecimal | What4.Expr.App
ppFreeSymFnEnv | What4.Serialize.Printer
ppFreeVarEnv | What4.Serialize.Printer
PPIndex | What4.Expr.App
ppMatlabSolverFn | What4.Expr.MATLAB
ppNoFileName | What4.ProgramLoc
ppNonceApp | What4.Expr.App
ppSolverSymbolError | What4.Symbol
ppSolverVersionCheckError | What4.Protocol.SMTLib2
ppSolverVersionError | What4.Protocol.SMTLib2
ppVar | What4.Expr.App
ppVarTypeCode | What4.Expr.App
Prec128 | What4.BaseTypes, What4.Interface
Prec16 | What4.BaseTypes, What4.Interface
Prec32 | What4.BaseTypes, What4.Interface
Prec64 | What4.BaseTypes, What4.Interface
Prec80 | What4.BaseTypes, What4.Interface
precise_overlap | What4.Utils.BVDomain
precisionBits | What4.SFloat
preCondition | Test.Verification
Pred | What4.Interface
predicateVarInfo | What4.Expr.VarIdentification
predNat | What4.BaseTypes, What4.Interface
predToBV | What4.Interface
PredToBVFn | What4.Expr.MATLAB
PredToIntegerFn | What4.Expr.MATLAB
predToReal | What4.Interface
PrettyApp | What4.Expr.App
prettyApp | What4.Expr.App
PrettyArg |
1 (Type/Class) | What4.Expr.App
2 (Data Constructor) | What4.Expr.App
PrettyFunc | What4.Expr.App
prettyLogEvent | What4.Serialize.Log
PrettyText | What4.Expr.App
PrimArrayTypeMap | What4.Protocol.SMTWriter
printAtom | What4.Serialize.SETokens
printSExpr | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
printSymExpr | What4.Interface
printSymNat | What4.Interface
ProblemFeatures | What4.ProblemFeatures
problemFeatures | What4.Expr.VarIdentification
prodAbsValue | What4.Expr.WeightedSum
prodContains | What4.Expr.WeightedSum
prodEval | What4.Expr.WeightedSum
prodEvalM | What4.Expr.WeightedSum
prodMul | What4.Expr.WeightedSum
prodRepr | What4.Expr.WeightedSum
prodVar | What4.Expr.WeightedSum
ProgramLoc | What4.ProgramLoc
programLoc | What4.ProgramLoc
proper |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
Property | Test.Verification
property | Test.Verification
push |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.Online, What4.Solver.Yices
push2Command | What4.Protocol.SMTWriter
pushCommand | What4.Protocol.SMTWriter
pushEntryStack | What4.Protocol.SMTWriter
pushMuxOps | What4.Expr.Builder, What4.Expr
pushMuxOpsOption | What4.Expr.Builder
qf_bv | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
QuadFloat | What4.InterpretedFloatingPoint
QuadFloatRepr | What4.InterpretedFloatingPoint
quantAbsEval | What4.Expr.App
QuantifierInfo | What4.Expr.VarIdentification
QuantifierInfoMap | What4.Expr.VarIdentification
QuantifierTheory | What4.Expr.AppTheory, What4.Expr
QuantifierVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr
quantTheory | What4.Expr.AppTheory, What4.Expr
QuarterPi | What4.SpecialFunctions
queryErrorBehavior | What4.Protocol.SMTLib2
R | What4.SpecialFunctions
range |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
rangeCheckEq | What4.Utils.AbstractDomains
rangeCheckLe | What4.Utils.AbstractDomains
rangeHiBound | What4.Utils.AbstractDomains
rangeLowBound | What4.Utils.AbstractDomains
rangeMax | What4.Utils.AbstractDomains
rangeMin | What4.Utils.AbstractDomains
rangeScalarMul | What4.Utils.AbstractDomains
rationalAsInteger | What4.Interface
rationalBounds | What4.Interface
rationalTerm | What4.Protocol.SMTWriter
RatPPIndex | What4.Expr.App
RatTerm | What4.Protocol.SMTLib2.Parse
RAV | What4.Utils.AbstractDomains
ravAdd | What4.Utils.AbstractDomains
ravCheckEq | What4.Utils.AbstractDomains
ravCheckLe | What4.Utils.AbstractDomains
ravConcreteRange | What4.Utils.AbstractDomains
ravIsInteger | What4.Utils.AbstractDomains
ravJoin | What4.Utils.AbstractDomains
ravMul | What4.Utils.AbstractDomains
ravRange | What4.Utils.AbstractDomains
ravScalarMul | What4.Utils.AbstractDomains
ravSingle | What4.Utils.AbstractDomains
ravUnbounded | What4.Utils.AbstractDomains
readAllLines | What4.Utils.HandleReader
readBaseTypes | What4.Serialize.Parser
readCheckSatResponse | What4.Protocol.SMTLib2.Parse
readDecimal | What4.Protocol.ReadDecimal
readGetModelResponse | What4.Protocol.SMTLib2.Parse
readNextLine | What4.Utils.HandleReader
Real | What4.Protocol.SMTLib2.Parse
real | What4.Serialize.SETokens, What4.Serialize.Printer
realAbs | What4.Interface
RealAbstractValue | What4.Utils.AbstractDomains
realAdd | What4.Interface
realATan2 | What4.Protocol.SMTWriter
realAtan2 | What4.Interface
RealBound | What4.SpecialFunctions
realCeil | What4.Interface
realCos |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
RealCosFn | What4.Expr.MATLAB
realCosh |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
RealDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr
realDiv |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
realEq | What4.Interface
realExp |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
RealExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr
realExprAsInteger | What4.Interface
realFloor | What4.Interface
realGe | What4.Interface
realGt | What4.Interface
realHypot | What4.Interface
RealInterval |
1 (Type/Class) | What4.SpecialFunctions
2 (Data Constructor) | What4.SpecialFunctions
RealIsInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr
realIsInteger | What4.Protocol.SMTWriter
realIsNonNeg | What4.Interface
RealIsNonZeroFn | What4.Expr.MATLAB
realIte | What4.Interface
realLe | What4.Interface
realLit | What4.Interface
realLog |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
realLt | What4.Interface
realMax | What4.Interface
realMin | What4.Interface
realMod | What4.Interface
realMul | What4.Interface
realNe | What4.Interface
realNeg | What4.Interface
realOptSty | What4.Config
RealPart | What4.Expr.App, What4.Expr.Builder, What4.Expr
realPart | What4.Utils.Complex
RealPartOfCplxFn | What4.Expr.MATLAB
realPi | What4.Interface
RealPoint |
1 (Data Constructor) | What4.SpecialFunctions
2 (Type/Class) | What4.SpecialFunctions
realRound | What4.Interface
realRoundEven | What4.Interface
RealSeqFn | What4.Expr.MATLAB
realSin |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
RealSinFn | What4.Expr.MATLAB
realSinh |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
realSort | What4.Protocol.SMTLib2.Syntax
RealSpecialFunction | What4.Expr.App, What4.Expr.Builder, What4.Expr
realSpecialFunction | What4.Interface
realSpecialFunction0 | What4.Interface
realSpecialFunction1 | What4.Interface
realSpecialFunction2 | What4.Interface
realSq | What4.Interface
RealSqrt | What4.Expr.App, What4.Expr.Builder, What4.Expr
realSqrt | What4.Interface
realSub | What4.Interface
realSum | What4.Expr.Builder
realTan |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
realTanh |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
realToBV | What4.Interface
RealToComplexFn | What4.Expr.MATLAB
RealToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr
realToFloat |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
RealToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr
realToInteger | What4.Interface
RealToIntegerFn | What4.Expr.MATLAB
realToNat | What4.Interface
realToSBV | What4.Interface
RealToSBVFn | What4.Expr.MATLAB
RealToUBVFn | What4.Expr.MATLAB
realTrunc | What4.Interface
RealTypeMap | What4.Protocol.SMTWriter
realWithMaxOptSty | What4.Config
realWithMinOptSty | What4.Config
realWithRangeOptSty | What4.Config
RealWorld | What4.Utils.MonadST
realZero | What4.Interface
recommended | What4.Utils.Versions
recordExprVars | What4.Expr.VarIdentification
reduceApp | What4.Expr.App
reduceIntSumMod | What4.Expr.WeightedSum
Refl | What4.BaseTypes, What4.Interface
removeVar | What4.Expr.BoolMap
renderTerm | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
reset | What4.Protocol.Online
resetAssertions | What4.Protocol.SMTLib2.Syntax
resetCommand | What4.Protocol.SMTWriter
resetDeclaredStructs | What4.Protocol.SMTWriter
resetEntryStack | What4.Protocol.SMTWriter
resFreeVarEnv | What4.Serialize.Printer
ResolvedSymBV | What4.Utils.ResolveBounds.BV
resolveSolverPath | What4.Utils.Process
resolveSymBV | What4.Utils.ResolveBounds.BV
ResponseStrictness | What4.Protocol.SMTWriter
resSExpr | What4.Serialize.Printer
resSymFnEnv | What4.Serialize.Printer
Result |
1 (Type/Class) | What4.Serialize.Printer
2 (Data Constructor) | What4.Serialize.Printer
returnMaybe | What4.Partial
returnPartial | What4.Partial
returnUnassigned | What4.Partial
reversePolarities | What4.Expr.BoolMap
RNA | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RNE | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
rol |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
Root | What4.Protocol.PolyRoot
ror |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
rotateDoc | What4.Protocol.VerilogWriter.ABCVerilog
rotateLeft | What4.Utils.Arithmetic
rotateRight | What4.Utils.Arithmetic
roundAway | What4.Utils.Arithmetic
RoundEvenReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
RoundingMode |
1 (Data Constructor) | What4.Protocol.SMTLib2.Parse
2 (Type/Class) | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RoundReal | What4.Expr.App, What4.Expr.Builder, What4.Expr
RspErrBehavior | What4.Protocol.SMTLib2.Response
RspName | What4.Protocol.SMTLib2.Response
RspOutOfMemory | What4.Protocol.SMTLib2.Response
RspRsnIncomplete | What4.Protocol.SMTLib2.Response
RspUnkReason | What4.Protocol.SMTLib2.Response
RspVersion | What4.Protocol.SMTLib2.Response
RTN | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RTP | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RTZ | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
runAckAction | What4.Protocol.SMTWriter
runBitwuzlaInOverride | What4.Solver.Bitwuzla, What4.Solver
runBoolectorInOverride | What4.Solver.Boolector, What4.Solver
runCheckSat | What4.Protocol.SMTLib2
runCVC4InOverride | What4.Solver.CVC4, What4.Solver
runCVC5InOverride | What4.Solver.CVC5, What4.Solver
runCVC5SyGuS | What4.Solver.CVC5
runDRealInOverride | What4.Solver.DReal, What4.Solver
runExternalABCInOverride | What4.Solver.ExternalABC, What4.Solver
runGetAbducts | What4.Protocol.SMTLib2
runInSandbox | What4.Protocol.SMTWriter
runPartialT | What4.Partial
runSolverInOverride | What4.Protocol.SMTLib2
runSTPInOverride | What4.Solver.STP, What4.Solver
runVerilogM | What4.Protocol.VerilogWriter.AST
runYicesInOverride | What4.Solver.Yices, What4.Solver
runZ3Horn | What4.Solver.Z3
runZ3InOverride | What4.Solver.Z3, What4.Solver
safeSymbol | What4.Symbol, What4.Interface
sameTerm | What4.Expr.App
SApp | What4.Protocol.SExp
Sat | What4.SatResult, What4.Solver
SAtom | What4.Protocol.SExp
satQueryError | What4.Interface
satQueryReason | What4.Interface
satQueryResult | What4.Interface
satQuerySolverName | What4.Interface
SatResponse | What4.Protocol.SMTLib2.Parse
SatResult | What4.SatResult, What4.Solver
sbMakeExpr | What4.Expr.Builder
sbNonceExpr | What4.Expr.Builder
sbounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
SBVToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr
sbvToFloat |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
SBVToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr
sbvToInteger |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
SBVToIntegerFn | What4.Expr.MATLAB
sbvToReal | What4.Interface
scalarMul | What4.Expr.Builder
scale |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
3 (Function) | What4.Expr.WeightedSum
scaledVar | What4.Expr.WeightedSum
scalMult | What4.Protocol.VerilogWriter.AST
sciLit | What4.Interface
Scope | What4.Expr.VarIdentification
sdiv |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
SearchStrategy | What4.Utils.ResolveBounds.BV
select |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain
SelectArray | What4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRing | What4.SemiRing, What4.Expr
SemiRingBase | What4.SemiRing
semiRingBase | What4.SemiRing
SemiRingBV | What4.SemiRing
SemiRingBVRepr | What4.SemiRing, What4.Expr
SemiRingInteger | What4.SemiRing
SemiRingIntegerRepr | What4.SemiRing, What4.Expr
SemiRingLe | What4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingLiteral | What4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingProd | What4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingProduct | What4.Expr.WeightedSum
SemiRingReal | What4.SemiRing
SemiRingRealRepr | What4.SemiRing, What4.Expr
SemiRingRepr | What4.SemiRing, What4.Expr
SemiRingSum | What4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingView | What4.Expr.App
sendCheck | What4.Solver.Yices
sendCheckExistsForall | What4.Solver.Yices
serializeBaseType | What4.Serialize.Printer
serializeExpr | What4.Serialize.Printer
serializeExprWithConfig | What4.Serialize.Printer
serializeSymFn | What4.Serialize.Printer
serializeSymFnWithConfig | What4.Serialize.Printer
Session |
1 (Type/Class) | What4.Protocol.SMTLib2
2 (Data Constructor) | What4.Protocol.SMTLib2
sessionResponse | What4.Protocol.SMTLib2
sessionWriter | What4.Protocol.SMTLib2
SetArray | What4.Expr.App, What4.Expr.Builder, What4.Expr
setBoolOpt | What4.Config
setCurrentProgramLoc | What4.Interface
setDefaultLogicAndOptions | What4.Protocol.SMTLib2
setIntegerOpt | What4.Config
setLogic |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
setOpt | What4.Config
setOptCommand | What4.Protocol.SMTWriter
setOption |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Config
3 (Function) | What4.Protocol.SMTLib2
setParam | What4.Solver.Yices
setProduceModels |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
setSolverLogListener | What4.Interface
setUnicodeOpt | What4.Config
setYicesParams | What4.Solver.Yices
set_opt_default | What4.Config
set_opt_onset | What4.Config
SExp | What4.Protocol.SExp
SExpr | What4.Serialize.Printer, What4.Serialize.Parser
sExpToString | What4.Protocol.SExp
sext |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
4 (Function) | What4.Expr.UnaryBV
SFloat |
1 (Type/Class) | What4.SFloat
2 (Data Constructor) | What4.SFloat
SFloatBinArith | What4.SFloat
SFloatRel | What4.SFloat
shl |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
shouldUnfold | What4.Interface
showPrettyArg | What4.Expr.App
shutdownSolver | What4.Protocol.SMTLib2
shutdownSolverProcess | What4.Protocol.Online
signed | What4.Protocol.VerilogWriter.AST
signedBVBounds |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
signedClamp | What4.BaseTypes, What4.Interface
signedWideMultiplyBV | What4.Interface
SimpleWordMap | What4.WordMap
simplify | What4.Expr.Simplify
Sin | What4.SpecialFunctions
SingleFloat | What4.InterpretedFloatingPoint
SingleFloatRepr | What4.InterpretedFloatingPoint
SingleRange | What4.Utils.AbstractDomains, What4.Interface
singleRange | What4.Utils.AbstractDomains
singleton |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain.XOR
5 (Function) | What4.Utils.BVDomain
6 (Function) | What4.Utils.LeqMap
7 (Function) | What4.Utils.Word16String
8 (Function) | What4.Expr.ArrayUpdateMap
9 (Function) | What4.Expr.StringSeq
Sinh | What4.SpecialFunctions
size |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain
5 (Function) | What4.Utils.LeqMap
6 (Function) | What4.Expr.UnaryBV
skipSpaceOrNewline | What4.Protocol.SExp
slt |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
3 (Function) | What4.Expr.UnaryBV
smokeTest | What4.Solver.Adapter, What4.Solver
smtAbductNextResult | What4.Protocol.SMTWriter
smtAbductResult | What4.Protocol.SMTWriter
smtAckResult | What4.Protocol.SMTLib2
smtEvalBool | What4.Protocol.SMTWriter
smtEvalBV | What4.Protocol.SMTWriter
smtEvalBvArray | What4.Protocol.SMTWriter
SMTEvalBVArrayFn | What4.Protocol.SMTWriter
SMTEvalBVArrayWrapper |
1 (Type/Class) | What4.Protocol.SMTWriter
2 (Data Constructor) | What4.Protocol.SMTWriter
smtEvalFloat | What4.Protocol.SMTWriter
SMTEvalFunctions |
1 (Type/Class) | What4.Protocol.SMTWriter
2 (Data Constructor) | What4.Protocol.SMTWriter
smtEvalFuns | What4.Protocol.SMTWriter
smtEvalReal | What4.Protocol.SMTWriter
smtEvalString | What4.Protocol.SMTWriter
smtExprGroundEvalFn | What4.Protocol.SMTWriter
smtFnApp | What4.Protocol.SMTWriter
smtFnUpdate | What4.Protocol.SMTWriter
SMTInfoFlag | What4.Protocol.SMTLib2.Syntax
smtlib2arrayConstant | What4.Protocol.SMTLib2
smtlib2arraySelect | What4.Protocol.SMTLib2
smtlib2arrayType | What4.Protocol.SMTLib2
smtlib2arrayUpdate | What4.Protocol.SMTLib2
smtlib2declareStructCmd | What4.Protocol.SMTLib2
SMTLib2Error | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
SMTLib2Exception | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
smtlib2exitCommand | What4.Protocol.SMTLib2
SMTLib2GenericSolver | What4.Protocol.SMTLib2
SMTLib2InvalidResponse | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
smtlib2Options | What4.Protocol.SMTLib2
SMTLib2ParseError | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
SMTLib2ResponseUnrecognized | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
smtlib2StringAppend | What4.Protocol.SMTLib2
smtlib2StringContains | What4.Protocol.SMTLib2
smtlib2StringIndexOf | What4.Protocol.SMTLib2
smtlib2StringIsPrefixOf | What4.Protocol.SMTLib2
smtlib2StringIsSuffixOf | What4.Protocol.SMTLib2
smtlib2StringLength | What4.Protocol.SMTLib2
smtlib2StringSort | What4.Protocol.SMTLib2
smtlib2StringSubstring | What4.Protocol.SMTLib2
smtlib2StringTerm | What4.Protocol.SMTLib2
smtlib2StructCtor | What4.Protocol.SMTLib2
smtlib2StructProj | What4.Protocol.SMTLib2
smtlib2StructSort | What4.Protocol.SMTLib2
SMTLib2Tweaks | What4.Protocol.SMTLib2
smtlib2tweaks | What4.Protocol.SMTLib2
SMTLib2Unsupported | What4.Protocol.SMTLib2.Response, What4.Protocol.SMTLib2
smtLibEvalFuns | What4.Protocol.SMTLib2
smtParseOptions | What4.Protocol.SMTLib2.Response
SMTReadWriter | What4.Protocol.SMTWriter
SMTResponse | What4.Protocol.SMTLib2.Response
smtSatResult | What4.Protocol.SMTWriter
smtUnsatAssumptionsResult | What4.Protocol.SMTWriter
smtUnsatCoreResult | What4.Protocol.SMTWriter
SMTWriter | What4.Protocol.SMTWriter
smtWriterName | What4.Protocol.SMTWriter
SolverAdapter |
1 (Type/Class) | What4.Solver.Adapter, What4.Solver
2 (Data Constructor) | What4.Solver.Adapter, What4.Solver
solverAdapterOptions | What4.Solver.Adapter, What4.Solver
SolverBounds |
1 (Type/Class) | What4.Utils.Versions
2 (Data Constructor) | What4.Utils.Versions
solverCleanupCallback | What4.Protocol.Online
solverConn | What4.Protocol.Online
solverEarlyUnsat | What4.Protocol.Online
SolverEndSATQuery |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
SolverEndSATQueryRec | What4.Interface
solverErrorBehavior | What4.Protocol.Online
solverEvalFuns | What4.Protocol.Online
SolverEvent | What4.Interface
SolverGoalTimeout |
1 (Type/Class) | What4.Protocol.Online
2 (Data Constructor) | What4.Protocol.Online
solverGoalTimeout | What4.Protocol.Online
solverHandle | What4.Protocol.Online
solverLogFn | What4.Protocol.Online
solverName | What4.Protocol.Online
SolverProcess |
1 (Type/Class) | What4.Protocol.Online
2 (Data Constructor) | What4.Protocol.Online
solverResponse | What4.Protocol.Online
SolverStartSATQuery |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
SolverStartSATQueryRec | What4.Interface
solverStderr | What4.Protocol.Online
solverStdin | What4.Protocol.Online
solverSupportsResetAssertions | What4.Protocol.Online
SolverSymbol | What4.Symbol, What4.Interface
solverSymbolAsText | What4.Symbol
SolverSymbolError | What4.Symbol
solver_adapter_check_sat | What4.Solver.Adapter, What4.Solver
solver_adapter_config_options | What4.Solver.Adapter, What4.Solver
solver_adapter_name | What4.Solver.Adapter, What4.Solver
solver_adapter_write_smt2 | What4.Solver.Adapter, What4.Solver
Some | What4.BaseTypes, What4.Interface
SomeExprSymFn |
1 (Type/Class) | What4.Expr.Builder
2 (Data Constructor) | What4.Expr.Builder
3 (Type/Class) | What4.Serialize.Printer
4 (Data Constructor) | What4.Serialize.Printer
someNat | What4.BaseTypes, What4.Interface
SomeSymFn |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
3 (Type/Class) | What4.Serialize.Parser
4 (Data Constructor) | What4.Serialize.Parser
Sort |
1 (Type/Class) | What4.Protocol.SMTLib2.Parse
2 (Data Constructor) | What4.Protocol.SMTLib2.Parse
3 (Type/Class) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
4 (Data Constructor) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
SourcePos | What4.ProgramLoc
sourcePos | What4.ProgramLoc
SpecialFnArg |
1 (Type/Class) | What4.SpecialFunctions
2 (Data Constructor) | What4.SpecialFunctions
SpecialFnArgs |
1 (Type/Class) | What4.SpecialFunctions
2 (Data Constructor) | What4.SpecialFunctions
specialFnDomain | What4.SpecialFunctions
specialFnRange | What4.SpecialFunctions
specialFnSymmetry | What4.SpecialFunctions
SpecialFunction | What4.SpecialFunctions
splitConfig | What4.Config
splitEntry | What4.Utils.LeqMap
splitLeq | What4.Utils.LeqMap
SplitPPExprList | What4.Expr.App
Sqrt_2 | What4.SpecialFunctions
Sqrt_OneHalf | What4.SpecialFunctions
srem |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
sr_compare | What4.SemiRing
SR_Constant | What4.Expr.App
SR_General | What4.Expr.App
sr_hashWithSalt | What4.SemiRing
SR_Prod | What4.Expr.App
SR_Sum | What4.Expr.App
SString | What4.Protocol.SExp
ST | What4.Utils.MonadST
startCaching | What4.Expr.Builder, What4.Expr
startFunctionName | What4.FunctionName
startHandleReader | What4.Utils.HandleReader, What4.Solver.Yices
startOfFile | What4.ProgramLoc
startProcess | What4.Utils.Process
startSolver | What4.Protocol.SMTLib2
startSolverProcess | What4.Protocol.Online
statAllocs | What4.Interface
Statistics |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
statNonLinearOps | What4.Interface
stdErrLogEventConsumer | What4.Serialize.Log
stopCaching | What4.Expr.Builder, What4.Expr
stopHandleReader | What4.Utils.HandleReader
store | What4.Protocol.SMTLib2.Syntax
StoreTerm | What4.Protocol.SMTLib2.Parse
STP |
1 (Type/Class) | What4.Solver.STP, What4.Solver
2 (Data Constructor) | What4.Solver.STP, What4.Solver
stpAdapter | What4.Solver.STP, What4.Solver
stpFeatures | What4.Solver.STP, What4.Solver
stpOptions | What4.Solver.STP, What4.Solver
stpPath | What4.Solver.STP, What4.Solver
stpTimeout | What4.Solver.STP, What4.Solver
streamLines | What4.Utils.HandleReader
Strict | What4.Protocol.SMTWriter
strictParsing | What4.Protocol.SMTWriter
strictSMTParseOpt | What4.Protocol.SMTLib2.Response
strictSMTParsing | What4.Protocol.SMTLib2.Response
string | What4.Serialize.SETokens, What4.Serialize.Printer
string' | What4.Serialize.SETokens
StringAbs | What4.Utils.AbstractDomains
stringAbsConcat | What4.Utils.AbstractDomains
stringAbsContains | What4.Utils.AbstractDomains
stringAbsEmpty | What4.Utils.AbstractDomains
stringAbsIndexOf | What4.Utils.AbstractDomains
stringAbsIsPrefixOf | What4.Utils.AbstractDomains
stringAbsIsSuffixOf | What4.Utils.AbstractDomains
stringAbsJoin | What4.Utils.AbstractDomains
stringAbsLength | What4.Utils.AbstractDomains
stringAbsOverlap | What4.Utils.AbstractDomains
stringAbsSingle | What4.Utils.AbstractDomains
stringAbsSubstring | What4.Utils.AbstractDomains
stringAbsTop | What4.Utils.AbstractDomains
StringAbstractValue | What4.Utils.AbstractDomains
StringAppend | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringAppend | What4.Protocol.SMTWriter
stringConcat | What4.Interface
StringContains | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringContains |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
stringEmpty | What4.Interface
stringEq | What4.Interface
StringExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
StringIndexOf | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringIndexOf |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
StringInfo | What4.BaseTypes, What4.Interface
stringInfo | What4.Interface
StringInfoRepr | What4.BaseTypes, What4.Interface
StringIsPrefixOf | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringIsPrefixOf |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
StringIsSuffixOf | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringIsSuffixOf |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
stringIte | What4.Interface
StringLength | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringLength |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
stringLit | What4.Interface
stringLitBounds | What4.Utils.StringLiteral
stringLitContains | What4.Utils.StringLiteral
stringLitEmpty | What4.Utils.StringLiteral
StringLiteral | What4.Utils.StringLiteral, What4.Interface
stringLiteralInfo | What4.Utils.StringLiteral, What4.Interface
stringLitIndexOf | What4.Utils.StringLiteral
stringLitIsPrefixOf | What4.Utils.StringLiteral
stringLitIsSuffixOf | What4.Utils.StringLiteral
stringLitLength | What4.Utils.StringLiteral
stringLitNull | What4.Utils.StringLiteral
stringLitSubstring | What4.Utils.StringLiteral
stringOptSty | What4.Config
stringPPExpr | What4.Expr.App
stringPrettyArg | What4.Expr.App
StringSeq | What4.Expr.StringSeq
stringSeqAbs | What4.Expr.StringSeq
StringSeqEntry | What4.Expr.StringSeq
StringSeqLiteral | What4.Expr.StringSeq
StringSeqTerm | What4.Expr.StringSeq
StringSubstring | What4.Expr.App, What4.Expr.Builder, What4.Expr
stringSubstring |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
stringTerm | What4.Protocol.SMTWriter
StringTheory | What4.Expr.AppTheory, What4.Expr
stringToSExp | What4.Protocol.SExp
StructCtor | What4.Expr.App, What4.Expr.Builder, What4.Expr
structCtor | What4.Protocol.SMTWriter
structEq | What4.Interface
StructField | What4.Expr.App, What4.Expr.Builder, What4.Expr
structField | What4.Interface
structIte | What4.Interface
structProj | What4.Protocol.SMTWriter
StructTheory | What4.Expr.AppTheory, What4.Expr
StructTypeMap | What4.Protocol.SMTWriter
sub | What4.Protocol.SMTLib2.Syntax
subNat | What4.BaseTypes, What4.Interface
subSignedOF | What4.Interface
substituteBoundVars | What4.Interface
substituteSymFns | What4.Interface
subUnsignedOF | What4.Interface
sumAbsValue | What4.Expr.WeightedSum
sumExpr | What4.Protocol.SMTWriter
sumOffset | What4.Expr.WeightedSum
sumRepr | What4.Expr.WeightedSum
supportedFeatures | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2
supportFunctionArguments | What4.Protocol.SMTWriter
supportFunctionDefs | What4.Protocol.SMTWriter
supportQuantifiers | What4.Protocol.SMTWriter
supportsResetAssertions | What4.Protocol.SMTLib2
SupportTermOps | What4.Protocol.SMTWriter
SWord | What4.SWord
SymAnnotation | What4.Interface
SymArray | What4.Interface
Symbol |
1 (Type/Class) | What4.Protocol.SMTLib2.Parse
2 (Type/Class) | What4.Protocol.SMTLib2.Syntax
SymbolBinding | What4.Expr.Builder
SymbolTerm | What4.Protocol.SMTLib2.Parse
SymbolVarBimap | What4.Expr.Builder
SymBV | What4.Interface
SymCplx | What4.Interface
SymEncoder |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
symEncoderType | What4.Interface
SymExpr | What4.Interface, What4.Expr.Builder
SymFloat | What4.Interface
SymFn | What4.Interface
symFnArgTypes | What4.Expr.App, What4.Expr.Builder, What4.Expr
symFnId | What4.Expr.App, What4.Expr.Builder, What4.Expr
SymFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr
symFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr
symFnLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
symFnName | What4.Expr.App, What4.Expr.Builder, What4.Expr
symFnReturnType | What4.Expr.App, What4.Expr.Builder, What4.Expr
SymFnWrapper |
1 (Type/Class) | What4.Interface
2 (Data Constructor) | What4.Interface
symFromExpr | What4.Interface
SymInteger | What4.Interface
SymInterpretedFloat | What4.InterpretedFloatingPoint
SymInterpretedFloatType | What4.InterpretedFloatingPoint
SymNat | What4.Interface
SymReal | What4.Interface
SymString | What4.Interface
SymStruct | What4.Interface
symToExpr | What4.Interface
sym_evaluate | What4.Expr.UnaryBV
synthFun | What4.Protocol.SMTLib2.Syntax
synthFunCommand | What4.Protocol.SMTWriter
systemSymbol | What4.Symbol
T | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
take | What4.Utils.Word16String
Tan | What4.SpecialFunctions
Tanh | What4.SpecialFunctions
teeInputStream | What4.Utils.HandleReader
teeOutputStream | What4.Utils.HandleReader
Term |
1 (Type/Class) | What4.Protocol.SMTLib2.Parse
2 (Type/Class) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
3 (Type/Class) | What4.Protocol.SMTWriter
termIntegerToReal | What4.Protocol.SMTWriter
termRealToInteger | What4.Protocol.SMTWriter
term_app | What4.Protocol.SMTLib2.Syntax
testBit |
1 (Function) | What4.Utils.BVDomain.Bitwise
2 (Function) | What4.Utils.BVDomain
testBitBV | What4.Interface
TestEquality | What4.BaseTypes, What4.Interface
testEquality | What4.BaseTypes, What4.Interface
testEquivExpr | What4.Serialize.Normalize
testEquivSymFn | What4.Serialize.Normalize
testExprSymFnEq | What4.Expr.App
testLeq | What4.BaseTypes, What4.Interface
testNatCases | What4.BaseTypes, What4.Interface
testSolverFnEq | What4.Expr.MATLAB
testStrictLeq | What4.BaseTypes, What4.Interface
textPPExpr | What4.Expr.App
Tm | What4.Expr.WeightedSum
tmpFileLogEventConsumer | What4.Serialize.Log
toBaseTypeRepr | What4.Utils.OnlyIntRepr
toDescList | What4.Utils.LeqMap
toIncrHash | What4.Utils.IncrHash
toIncrHashWithSalt | What4.Utils.IncrHash
toInt | What4.Protocol.SMTLib2.Syntax
toLEByteString | What4.Utils.Word16String
toList |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.LeqMap
3 (Function) | What4.Expr.ArrayUpdateMap
4 (Function) | What4.Expr.StringSeq
toMap | What4.Expr.ArrayUpdateMap
toNativeProperty | Test.Verification
toReal | What4.Protocol.SMTLib2.Syntax
toRoundMode | What4.Utils.FloatHelpers
toSigned | What4.BaseTypes, What4.Interface
toUnsigned | What4.BaseTypes, What4.Interface
transformPredBV2LIA | What4.Interface
transformSum | What4.Expr.WeightedSum
transformSymFnLIA2BV | What4.Interface
traverseApp | What4.Expr.App, What4.Expr.Builder
traverseArrayResultWrapper | What4.Expr.App
traverseArrayResultWrapperAssignment | What4.Expr.App
traverseArrayUpdateMap | What4.Expr.ArrayUpdateMap
traverseBVOrSet | What4.Expr.App, What4.Expr.Builder
traverseCoeffs | What4.Expr.WeightedSum
traverseMatlabSolverFn | What4.Expr.MATLAB
traverseMaybeWithKey | What4.Utils.AnnotatedMap
traversePreds | What4.Expr.UnaryBV
traverseProdVars | What4.Expr.WeightedSum
traverseSatResult | What4.SatResult, What4.Solver
traverseSpecialFnArg | What4.SpecialFunctions
traverseSpecialFnArgs | What4.SpecialFunctions
traverseStringSeq | What4.Expr.StringSeq
traverseVars |
1 (Function) | What4.Expr.BoolMap
2 (Function) | What4.Expr.WeightedSum
true | What4.Protocol.SMTLib2.Syntax
truePred | What4.Interface
trunc | What4.Expr.UnaryBV
tryComplexSqrt | What4.Utils.Complex
tryEvalGroundExpr | What4.Expr.GroundEval
tryExtendConfig | What4.Config
tryIntSqrt | What4.Utils.Arithmetic
tryMagnitude | What4.Utils.Complex
tryPop | What4.Protocol.Online
tryRationalSqrt | What4.Utils.Arithmetic
trySetOpt | What4.Config
TwoOverPi | What4.SpecialFunctions
TwoOverSqrt_Pi | What4.SpecialFunctions
typeDoc | What4.Protocol.VerilogWriter.ABCVerilog
TypeMap | What4.Protocol.SMTWriter
typeMap | What4.Protocol.SMTWriter
typeTheory | What4.Expr.AppTheory
ubounds |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
udiv |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
uext | What4.Expr.UnaryBV
uintSetWidth | What4.Interface
UIntSetWidthFn | What4.Expr.MATLAB
uintToInt | What4.Interface
UIntToIntFn | What4.Expr.MATLAB
uintToReal | What4.Interface
ult |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
3 (Function) | What4.Expr.UnaryBV
UnaryBV | What4.Expr.UnaryBV, What4.Expr
unaryThreshold | What4.Expr.Builder, What4.Expr
unaryThresholdOption | What4.Expr.Builder
Unassigned | What4.Partial
Unbounded |
1 (Data Constructor) | What4.Utils.AbstractDomains
2 (Data Constructor) | What4.Config
UnboundedRange | What4.Utils.AbstractDomains, What4.Interface
unboundedRange | What4.Utils.AbstractDomains
unconstrainedAbsValue | What4.Expr.App
unEvalBVArrayWrapper | What4.Protocol.SMTWriter
UnfoldConcrete | What4.Interface
UnfoldPolicy | What4.Interface
unGVW | What4.Expr.GroundEval, What4.Expr
Unicode | What4.BaseTypes, What4.Interface
UnicodeLiteral | What4.Utils.StringLiteral, What4.Interface
UnicodeRepr | What4.BaseTypes, What4.Interface
UnicodeTypeMap | What4.Protocol.SMTWriter
uninterpConstants | What4.Expr.VarIdentification
UninterpFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr
UninterpVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr
union |
1 (Function) | What4.Utils.AnnotatedMap
2 (Function) | What4.Utils.BVDomain.Arith
3 (Function) | What4.Utils.BVDomain.Bitwise
4 (Function) | What4.Utils.BVDomain
5 (Function) | What4.Utils.LeqMap
unionWith | What4.Utils.AnnotatedMap
unionWithKeyMaybe | What4.Utils.AnnotatedMap
Unknown | What4.SatResult, What4.Solver
UnknownResponse | What4.Protocol.SMTLib2.Parse
unknowns | What4.Utils.BVDomain.Arith
Unop |
1 (Data Constructor) | What4.Protocol.VerilogWriter.AST
2 (Type/Class) | What4.Protocol.VerilogWriter.AST
unop | What4.Protocol.VerilogWriter.AST
unopDoc | What4.Protocol.VerilogWriter.ABCVerilog
unPartial | What4.Partial
unsafeSetAbstractValue | What4.Interface
Unsat | What4.SatResult, What4.Solver
UnsatResponse | What4.Protocol.SMTLib2.Parse
unsignedBVBounds |
1 (Function) | What4.Interface
2 (Function) | What4.SWord
unsignedClamp | What4.BaseTypes, What4.Interface
unsignedEntries | What4.Expr.UnaryBV
unsignedRanges | What4.Expr.UnaryBV
unsignedWideMultiplyBV | What4.Interface
unSort | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
UnsupportedFloat |
1 (Type/Class) | What4.SFloat
2 (Data Constructor) | What4.SFloat
unWrap | What4.Expr.BoolMap
unwrapArrayResult | What4.Interface, What4.Expr.Builder
unwrapAV | What4.Utils.AbstractDomains
unwrapCV | What4.Utils.AbstractDomains
un_app | What4.Protocol.SMTLib2.Syntax
UpdateArray | What4.Expr.App, What4.Expr.Builder, What4.Expr
upper | What4.Utils.Versions
urem |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain
useBitvectors | What4.ProblemFeatures
useComputableReals | What4.ProblemFeatures
useDefinedFunctions | What4.ProblemFeatures
useExistForall | What4.ProblemFeatures
useFloatingPoint | What4.ProblemFeatures
useIntegerArithmetic | What4.ProblemFeatures
useLinearArithmetic | What4.ProblemFeatures
useNonlinearArithmetic | What4.ProblemFeatures
useProduceAbducts | What4.ProblemFeatures
useQuantifiers | What4.ProblemFeatures
userState | What4.Expr.Builder, What4.Expr
userSymbol | What4.Symbol, What4.Interface
useStrings | What4.ProblemFeatures
useStructs | What4.ProblemFeatures
useSymbolicArrays | What4.ProblemFeatures
useUninterpFunctions | What4.ProblemFeatures
useUnsatAssumptions | What4.ProblemFeatures
useUnsatCores | What4.ProblemFeatures
ValueBound | What4.Utils.AbstractDomains
ValueRange | What4.Utils.AbstractDomains, What4.Interface
valueRange | What4.Utils.AbstractDomains
var |
1 (Function) | What4.Expr.BoolMap
2 (Function) | What4.Expr.WeightedSum
varErrors | What4.Expr.VarIdentification
varExpr | What4.Interface
VarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr
VarRecorder | What4.Expr.VarIdentification
varSort | What4.Protocol.SMTLib2.Syntax
VarSymbolBinding | What4.Expr.Builder
ver | What4.Utils.Versions
verbosity | What4.Config
verbosityLogger | What4.Config
Verifiable | Test.Verification
verifying | Test.Verification
VerilogM |
1 (Type/Class) | What4.Protocol.VerilogWriter.AST
2 (Data Constructor) | What4.Protocol.VerilogWriter.AST
Version | What4.Protocol.SMTLib2.Syntax
versionResult | What4.Protocol.SMTLib2
viewBoolMap | What4.Expr.BoolMap
viewSemiRing | What4.Expr.App
vsBoolCache | What4.Protocol.VerilogWriter.AST
vsBVCache | What4.Protocol.VerilogWriter.AST
vsExpCache | What4.Protocol.VerilogWriter.AST
vsInputs | What4.Protocol.VerilogWriter.AST
vsOutputs | What4.Protocol.VerilogWriter.AST
vsSeenNonces | What4.Protocol.VerilogWriter.AST
vsSym | What4.Protocol.VerilogWriter.AST
vsUsedIdentifiers | What4.Protocol.VerilogWriter.AST
vsWires | What4.Protocol.VerilogWriter.AST
Warn | What4.Serialize.Log
WeightedSum | What4.Expr.WeightedSum, What4.Expr
WellFormedSExpr | What4.Serialize.Printer, What4.Serialize.Parser
WFSAtom | What4.Serialize.Printer, What4.Serialize.Parser
WFSList | What4.Serialize.Printer, What4.Serialize.Parser
What4 | What4.Panic
width | What4.Expr.UnaryBV
widthVal | What4.BaseTypes, What4.Interface
Wire | What4.Protocol.VerilogWriter.AST
wireDoc | What4.Protocol.VerilogWriter.ABCVerilog
withAbstractable | What4.Utils.AbstractDomains
withAddLeq | What4.BaseTypes, What4.Interface
withAddMulDistribRight | What4.BaseTypes, What4.Interface
withAddPrefixLeq | What4.BaseTypes, What4.Interface
withAsyncLinked | What4.Utils.Serialize
withBitwuzla | What4.Solver.Bitwuzla, What4.Solver
withBoolector | What4.Solver.Boolector, What4.Solver
withCVC4 | What4.Solver.CVC4, What4.Solver
withCVC5 | What4.Solver.CVC5, What4.Solver
withCVC5_SyGuS | What4.Solver.CVC5
withDivModNat | What4.BaseTypes, What4.Interface
withHandleReader | What4.Utils.HandleReader
withKnownNat | What4.BaseTypes, What4.Interface
withLeqProof | What4.BaseTypes, What4.Interface
withLocalGoalTimeout | What4.Protocol.Online
withLogCfg | What4.Serialize.Log
withLogging | What4.Serialize.Log
withProcessHandles | What4.Utils.Process
withRounding | What4.Utils.Serialize
withSolver | What4.Protocol.SMTLib2
withSTP | What4.Solver.STP, What4.Solver
withSubMulDistribRight | What4.BaseTypes, What4.Interface
withZ3 | What4.Solver.Z3, What4.Solver
Word16String | What4.Utils.Word16String
WordMap | What4.WordMap
Wrap |
1 (Type/Class) | What4.Expr.BoolMap
2 (Data Constructor) | What4.Expr.BoolMap
writeABCSMT2File | What4.Solver.ExternalABC, What4.Solver
writeCheckSat | What4.Protocol.SMTLib2
writeCheckSynth | What4.Protocol.SMTLib2
writeCommand | What4.Protocol.SMTWriter
writeCVC4SMT2File | What4.Solver.CVC4, What4.Solver
writeCVC5SMT2File | What4.Solver.CVC5, What4.Solver
writeCVC5SyFile | What4.Solver.CVC5
writeDefaultSMT2 | What4.Protocol.SMTLib2
writeDRealSMT2File | What4.Solver.DReal, What4.Solver
writeExit | What4.Protocol.SMTLib2
writeGetAbduct | What4.Protocol.SMTLib2
writeGetAbductNext | What4.Protocol.SMTLib2
writeGetValue | What4.Protocol.SMTLib2
writeLogEvent | What4.Serialize.Log
writeMultiAsmpCVC4SMT2File | What4.Solver.CVC4
writeMultiAsmpCVC5SMT2File | What4.Solver.CVC5
Writer | What4.Protocol.SMTLib2
WriterConn | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2
writeYicesFile | What4.Solver.Yices, What4.Solver
writeZ3HornSMT2File | What4.Solver.Z3
writeZ3SMT2File | What4.Solver.Z3
X86_80Float | What4.InterpretedFloatingPoint
X86_80FloatRepr | What4.InterpretedFloatingPoint
X86_80Val |
1 (Type/Class) | What4.InterpretedFloatingPoint
2 (Data Constructor) | What4.InterpretedFloatingPoint
Xor | What4.Protocol.VerilogWriter.AST
xor |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
xorPred | What4.Interface
xorToBitwiseDomain | What4.Utils.BVDomain
yicesAdapter | What4.Solver.Yices, What4.Solver
yicesDefaultFeatures | What4.Solver.Yices, What4.Solver
yicesEnableInteractive | What4.Solver.Yices, What4.Solver
yicesEnableMCSat | What4.Solver.Yices, What4.Solver
YicesError | What4.Solver.Yices
yicesEvalBool | What4.Solver.Yices
YicesException | What4.Solver.Yices
yicesGoalTimeout | What4.Solver.Yices, What4.Solver
yicesOptions | What4.Solver.Yices, What4.Solver
YicesParseError | What4.Solver.Yices
yicesPath | What4.Solver.Yices, What4.Solver
yicesType | What4.Solver.Yices
YicesUnsupported | What4.Solver.Yices
Z3 |
1 (Type/Class) | What4.Solver.Z3, What4.Solver
2 (Data Constructor) | What4.Solver.Z3, What4.Solver
z3Adapter | What4.Solver.Z3, What4.Solver
z3Features | What4.Solver.Z3, What4.Solver
z3Options | What4.Solver.Z3, What4.Solver
z3Path | What4.Solver.Z3, What4.Solver
z3Tactic | What4.Solver.Z3, What4.Solver
z3TacticDefault | What4.Solver.Z3, What4.Solver
z3Timeout | What4.Solver.Z3, What4.Solver
ZBV | What4.SWord
Zero | What4.SpecialFunctions
zero | What4.SemiRing
ZeroNat | What4.BaseTypes, What4.Interface
zeroStatistics | What4.Interface
zext |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
_labeledPred | What4.LabeledPred
_labeledPredMsg | What4.LabeledPred
_partialPred | What4.Partial
_partialValue | What4.Partial
_stringAbsLength | What4.Utils.AbstractDomains