what4-1.1: 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
abcOptionsWhat4.Solver.ExternalABC, What4.Solver
abcPathWhat4.Solver.ExternalABC, What4.Solver
absWhat4.Protocol.SMTLib2.Syntax
absAndWhat4.Utils.AbstractDomains
absOrWhat4.Utils.AbstractDomains
AbstractableWhat4.Utils.AbstractDomains
abstractEvalWhat4.Expr.App
AbstractValueWhat4.Utils.AbstractDomains
AbstractValueWrapper 
1 (Type/Class)What4.Utils.AbstractDomains
2 (Data Constructor)What4.Utils.AbstractDomains
AckActionWhat4.Protocol.SMTWriter
AcknowledgementActionWhat4.Protocol.SMTWriter
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
addCommandWhat4.Protocol.SMTWriter, What4.Solver.Yices
addCommandNoAckWhat4.Protocol.SMTWriter
addCommandsWhat4.Protocol.SMTWriter
addConditionWhat4.Partial
addConstantWhat4.Expr.WeightedSum
addFreshInputWhat4.Protocol.VerilogWriter.AST
addFreshWireWhat4.Protocol.VerilogWriter.AST
addIsLeqWhat4.BaseTypes, What4.Interface
addIsLeqLeft1What4.BaseTypes, What4.Interface
addMulDistribRightWhat4.BaseTypes, What4.Interface
addNatWhat4.BaseTypes, What4.Interface
addOutputWhat4.Protocol.VerilogWriter.AST
addPrefixIsLeqWhat4.BaseTypes, What4.Interface
addRangeWhat4.Utils.AbstractDomains
addSignedOFWhat4.Interface
addUnsignedOFWhat4.Interface
addVar 
1 (Function)What4.Expr.BoolMap
2 (Function)What4.Expr.WeightedSum
addVarsWhat4.Expr.WeightedSum
addWireWhat4.Protocol.VerilogWriter.AST
allSupportedWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
allTrueEntriesWhat4.Interface
all_supportedWhat4.Protocol.SMTLib2
alterWhat4.Utils.AnnotatedMap
alterFWhat4.Utils.AnnotatedMap
AlwaysUnfoldWhat4.Interface
AndWhat4.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
andAllWhat4.Protocol.SMTWriter
andAllOfWhat4.Interface
andPredWhat4.Interface
and_scalarWhat4.Utils.BVDomain.XOR
AnnotatedMapWhat4.Utils.AnnotatedMap
annotateTermWhat4.Interface
AnnotationWhat4.Expr.App, What4.Expr.Builder, What4.Expr
annotationWhat4.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
APEWhat4.Expr.App
apeDocWhat4.Expr.App
apeExprsWhat4.Expr.App
apeIndexWhat4.Expr.App
apeLengthWhat4.Expr.App
apeLocWhat4.Expr.App
apeNameWhat4.Expr.App
AppWhat4.Expr.App, What4.Expr.Builder, What4.Expr
appWhat4.Protocol.SMTWriter
append 
1 (Function)What4.Utils.Word16String
2 (Function)What4.Expr.StringSeq
appEqFWhat4.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
appExprAbsValueWhat4.Expr.App
appExprAppWhat4.Expr.App, What4.Expr.Builder, What4.Expr
AppExprCtorWhat4.Expr.App
appExprIdWhat4.Expr.App, What4.Expr.Builder, What4.Expr
appExprLocWhat4.Expr.App, What4.Expr.Builder, What4.Expr
applySymFnWhat4.Interface
AppPPExpr 
1 (Data Constructor)What4.Expr.App
2 (Type/Class)What4.Expr.App
approximateWhat4.Protocol.PolyRoot
AppTheoryWhat4.Expr.AppTheory, What4.Expr
appTheoryWhat4.Expr.AppTheory, What4.Expr
appTypeWhat4.Expr.App, What4.Expr.Builder
app_listWhat4.Protocol.SMTWriter
arithDomainDataWhat4.Utils.BVDomain.Arith, What4.Utils.BVDomain
arithToXorDomainWhat4.Utils.BVDomain
ArrayWhat4.Protocol.SMTLib2.Parse
ArrayConcreteWhat4.Expr.GroundEval, What4.Expr
arrayConst 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
arrayConstantWhat4.Protocol.SMTWriter
ArrayConstantFnWhat4.Protocol.SMTWriter
arrayEqWhat4.Interface
ArrayFromFnWhat4.Expr.App, What4.Expr.Builder, What4.Expr
arrayFromFnWhat4.Interface
arrayFromMapWhat4.Interface
arrayIteWhat4.Interface
arrayLookupWhat4.Interface
ArrayMapWhat4.Expr.App, What4.Expr.Builder, What4.Expr
arrayMapWhat4.Interface
ArrayMappingWhat4.Expr.GroundEval, What4.Expr
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
arraySortWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
arrayStoreWhat4.Protocol.SMTLib2
ArrayTheoryWhat4.Expr.AppTheory, What4.Expr
ArrayTrueOnEntriesWhat4.Expr.App, What4.Expr.Builder, What4.Expr
arrayTrueOnEntriesWhat4.Interface
arrayTypeIndicesWhat4.BaseTypes, What4.Interface
arrayTypeResultWhat4.BaseTypes, What4.Interface
arrayUpdate 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
arrayUpdateAbsWhat4.Expr.ArrayUpdateMap
arrayUpdateAtIdxLitsWhat4.Interface
ArrayUpdateMapWhat4.Expr.ArrayUpdateMap
asAffineVar 
1 (Function)What4.Expr.WeightedSum
2 (Function)What4.Interface
asAppWhat4.Expr.App, What4.Expr.Builder
asArithDomainWhat4.Utils.BVDomain
asAtomListWhat4.Protocol.SExp
asBitwiseDomainWhat4.Utils.BVDomain
asBVWhat4.Interface
asComplexWhat4.Interface
asConcreteWhat4.Interface
asConjunctionWhat4.Expr.App, What4.Expr.Builder
AsConstWhat4.Protocol.SMTLib2.Parse
asConstant 
1 (Function)What4.Expr.WeightedSum
2 (Function)What4.Expr.UnaryBV
asConstantArrayWhat4.Interface
asConstantPredWhat4.Interface
asDisjunctionWhat4.Expr.App, What4.Expr.Builder
asFloatWhat4.Interface
ashr 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
asIntegerWhat4.Interface
asMatlabSolverFnWhat4.Expr.App
asNatWhat4.Interface
asNegAtomWhat4.Expr.App
asNegAtomListWhat4.Protocol.SExp
asNonceAppWhat4.Expr.App, What4.Expr.Builder
asPosAtomWhat4.Expr.App
asProdVarWhat4.Expr.WeightedSum
asRationalWhat4.Interface
asSemiRingLitWhat4.Expr.App
asSemiRingProdWhat4.Expr.App
asSemiRingSumWhat4.Expr.App
assertWhat4.Protocol.SMTLib2.Syntax
assertCommandWhat4.Protocol.SMTWriter
assertForallWhat4.Solver.Yices
assertNamedWhat4.Protocol.SMTLib2.Syntax
assertNamedCommandWhat4.Protocol.SMTWriter
AssignWhat4.Protocol.VerilogWriter.AST
asSingleRangeWhat4.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
asSMT2TypeWhat4.Protocol.SMTLib2
asStringWhat4.Interface
asStructWhat4.Interface
assumeWhat4.Protocol.SMTWriter, What4.Protocol.SMTLib2, What4.Solver.Yices
assumedPropTest.Verification
assumeFormulaWhat4.Protocol.SMTWriter
assumeFormulaWithFreshNameWhat4.Protocol.SMTWriter
assumeFormulaWithNameWhat4.Protocol.SMTWriter
AssumingTest.Verification
assumingTest.Verification
AssumptionTest.Verification
AssumptionPropTest.Verification
asVarWhat4.Expr.WeightedSum
asWeightedSumWhat4.Expr.App
asWeightedVarWhat4.Expr.WeightedSum
asXorDomainWhat4.Utils.BVDomain
avCheckEqWhat4.Utils.AbstractDomains
avContainsWhat4.Utils.AbstractDomains
avJoinWhat4.Utils.AbstractDomains
avOverlapWhat4.Utils.AbstractDomains
avSingleWhat4.Utils.AbstractDomains
avTopWhat4.Utils.AbstractDomains
backendPredWhat4.Interface
BaseArrayReprWhat4.BaseTypes, What4.Interface
BaseArrayTypeWhat4.BaseTypes, What4.Interface
BaseBoolReprWhat4.BaseTypes, What4.Interface
BaseBoolTypeWhat4.BaseTypes, What4.Interface
BaseBVReprWhat4.BaseTypes, What4.Interface
BaseBVTypeWhat4.BaseTypes, What4.Interface
BaseComplexReprWhat4.BaseTypes, What4.Interface
BaseComplexTypeWhat4.BaseTypes, What4.Interface
baseDefaultValueWhat4.Interface
BaseEqWhat4.Expr.App, What4.Expr.Builder, What4.Expr
BaseFloatReprWhat4.BaseTypes, What4.Interface
BaseFloatTypeWhat4.BaseTypes, What4.Interface
BaseIntegerReprWhat4.BaseTypes, What4.Interface
BaseIntegerTypeWhat4.BaseTypes, What4.Interface
baseIsConcreteWhat4.Interface
BaseIteWhat4.Expr.App, What4.Expr.Builder, What4.Expr
BaseRealReprWhat4.BaseTypes, What4.Interface
BaseRealTypeWhat4.BaseTypes, What4.Interface
BaseStringReprWhat4.BaseTypes, What4.Interface
BaseStringTypeWhat4.BaseTypes, What4.Interface
BaseStructReprWhat4.BaseTypes, What4.Interface
BaseStructTypeWhat4.BaseTypes, What4.Interface
BaseTypeWhat4.BaseTypes, What4.Interface
baseTypeIteWhat4.Interface
BaseTypeReprWhat4.BaseTypes, What4.Interface
bfStatusWhat4.Utils.FloatHelpers
BigEndianWhat4.Utils.Endian
BinaryPosWhat4.ProgramLoc
bindVarAsFreeWhat4.Protocol.SMTWriter
Binop 
1 (Data Constructor)What4.Protocol.VerilogWriter.AST
2 (Type/Class)What4.Protocol.VerilogWriter.AST
binopWhat4.Protocol.VerilogWriter.AST
binopDocWhat4.Protocol.VerilogWriter.ABCVerilog
binopTypeWhat4.Protocol.VerilogWriter.AST
bin_appWhat4.Protocol.SMTLib2.Syntax
BitWhat4.Protocol.VerilogWriter.AST
bitWhat4.Protocol.VerilogWriter.AST
bit0What4.Protocol.SMTLib2.Syntax
bit1What4.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
bitleWhat4.Utils.BVDomain.Bitwise
BitSelectWhat4.Protocol.VerilogWriter.AST
bitSelectWhat4.Protocol.VerilogWriter.AST
BitVecWhat4.Protocol.SMTLib2.Parse
BitvectorTheoryWhat4.Expr.AppTheory, What4.Expr
bitwiseRoundAboveWhat4.Utils.BVDomain
bitwiseRoundBetweenWhat4.Utils.BVDomain
bitwiseToXorDomainWhat4.Utils.BVDomain
BoolWhat4.Protocol.SMTLib2.Parse
Boolector 
1 (Type/Class)What4.Solver.Boolector, What4.Solver
2 (Data Constructor)What4.Solver.Boolector, What4.Solver
boolectorAdapterWhat4.Solver.Boolector, What4.Solver
boolectorFeaturesWhat4.Solver.Boolector, What4.Solver
boolectorOptionsWhat4.Solver.Boolector, What4.Solver
boolectorPathWhat4.Solver.Boolector, What4.Solver
BoolExpr 
1 (Type/Class)What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Data Constructor)What4.Expr.App, What4.Expr.Builder, What4.Expr
boolExprWhat4.Protocol.SMTWriter
BoolLitWhat4.Protocol.VerilogWriter.AST
BoolMapWhat4.Expr.BoolMap
BoolMapDualUnitWhat4.Expr.BoolMap
BoolMapTermsWhat4.Expr.BoolMap
BoolMapUnitWhat4.Expr.BoolMap
BoolMapViewWhat4.Expr.BoolMap
boolOptStyWhat4.Config
BoolOrFnWhat4.Expr.MATLAB
BoolPropertyTest.Verification
boolSortWhat4.Protocol.SMTLib2.Syntax
BoolTheoryWhat4.Expr.AppTheory, What4.Expr
BoolTypeMapWhat4.Protocol.SMTWriter
BoundWhat4.Config
boundInnerTermWhat4.Expr.VarIdentification
BoundQuantWhat4.Expr.VarIdentification
boundQuantWhat4.Expr.VarIdentification
boundTopTermWhat4.Expr.VarIdentification
BoundVarWhat4.Interface
boundVarWhat4.Expr.VarIdentification
BoundVarExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
BoundVarMapWhat4.Expr.App
boundVarsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
boundVars'What4.Expr.App
builder_list 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTWriter
BVAddWhat4.Protocol.VerilogWriter.AST
bvAdd 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvaddWhat4.Protocol.SMTLib2.Syntax
BVAndWhat4.Protocol.VerilogWriter.AST
bvAnd 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvandWhat4.Protocol.SMTLib2.Syntax
bvAndBitsWhat4.Interface
BVarWhat4.Expr.App
bvarAbstractValueWhat4.Expr.App, What4.Expr.Builder
bvarIdWhat4.Expr.App, What4.Expr.Builder, What4.Expr
BVArithWhat4.SemiRing
BVArithReprWhat4.SemiRing, What4.Expr
bvarKindWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvarLocWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvarNameWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvarTypeWhat4.Expr.App, What4.Expr.Builder
BVAshrWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvAshr 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvashrWhat4.Protocol.SMTLib2.Syntax
bvAsSignedIntegerWhat4.SWord
bvAsUnsignedIntegerWhat4.SWord
bvAtBEWhat4.SWord
bvAtLEWhat4.SWord
bvbinaryWhat4.Protocol.SMTLib2.Syntax
BVBitIntervalWhat4.Utils.BVDomain.Bitwise
bvBitreverseWhat4.Interface
BVBitsWhat4.SemiRing
BVBitsReprWhat4.SemiRing, What4.Expr
BVConcatWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvConcat 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
BVConst 
1 (Type/Class)What4.Protocol.VerilogWriter.AST
2 (Data Constructor)What4.Protocol.VerilogWriter.AST
BVCountLeadingZerosWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvCountLeadingZeros 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVCountTrailingZerosWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvCountTrailingZeros 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVDAnyWhat4.Utils.BVDomain.Arith
BVDArithWhat4.Utils.BVDomain
BVDBitwiseWhat4.Utils.BVDomain
bvdecimalWhat4.Protocol.SMTLib2.Syntax
BVDIntervalWhat4.Utils.BVDomain.Arith
BVDivWhat4.Protocol.VerilogWriter.AST
bvdMask 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain.XOR
BVDomainWhat4.Utils.BVDomain
bvdomainRangeLimitOptionWhat4.Expr.Builder
BVDXorWhat4.Utils.BVDomain.XOR
bvEq 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvExtractWhat4.Protocol.SMTWriter
BVFillWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvFill 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVFlavorWhat4.SemiRing, What4.Expr
BVFlavorReprWhat4.SemiRing, What4.Expr
bvForallWhat4.SWord
bvhexadecimalWhat4.Protocol.SMTLib2.Syntax
BVIWhat4.Expr.VarIdentification
BVIndexLitWhat4.IndexLit, What4.Interface, What4.Expr.Builder
bvIsNegWhat4.Interface
bvIsNonzero 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVIsNonZeroFnWhat4.Expr.MATLAB
bvIte 
1 (Function)What4.Interface
2 (Function)What4.SWord
bvJoinWhat4.SWord
bvJoinVectorWhat4.Interface
bvLg2What4.SWord
BVLitWhat4.Protocol.VerilogWriter.AST
bvLit 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVLshrWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvLshr 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvlshrWhat4.Protocol.SMTLib2.Syntax
BVMulWhat4.Protocol.VerilogWriter.AST
bvMul 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvmulWhat4.Protocol.SMTLib2.Syntax
bvNeWhat4.Interface
bvNeg 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvnegWhat4.Protocol.SMTLib2.Syntax
BVNotWhat4.Protocol.VerilogWriter.AST
bvNot 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvnotWhat4.Protocol.SMTLib2.Syntax
bvNotBitsWhat4.Interface
BVOrWhat4.Protocol.VerilogWriter.AST
bvOr 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvorWhat4.Protocol.SMTLib2.Syntax
bvOrAbsWhat4.Expr.App, What4.Expr.Builder
BVOrBitsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvOrBitsWhat4.Interface
bvOrContainsWhat4.Expr.App
bvOrInsertWhat4.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
bvOrSingletonWhat4.Expr.App, What4.Expr.Builder
bvOrToListWhat4.Expr.App, What4.Expr.Builder
bvOrUnionWhat4.Expr.App, What4.Expr.Builder
bvPackBEWhat4.SWord
bvPackLEWhat4.SWord
BVPopcountWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvPopcount 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVPowWhat4.Protocol.VerilogWriter.AST
BVRemWhat4.Protocol.VerilogWriter.AST
BVRolWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvRol 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVRorWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvRor 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVRotateLWhat4.Protocol.VerilogWriter.AST
BVRotateRWhat4.Protocol.VerilogWriter.AST
BVSdivWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvSDiv 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvSdivWhat4.Interface
bvsdivWhat4.Protocol.SMTLib2.Syntax
BVSelectWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvSelectWhat4.Interface
bvSetWhat4.Interface
bvSetBEWhat4.SWord
bvSetLEWhat4.SWord
BVSextWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvSext 
1 (Function)What4.Interface
2 (Function)What4.SWord
bvSgeWhat4.Interface
bvsge 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvSgtWhat4.Interface
bvsgt 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
BVShiftLWhat4.Protocol.VerilogWriter.AST
BVShiftRWhat4.Protocol.VerilogWriter.AST
BVShiftRAWhat4.Protocol.VerilogWriter.AST
BVShlWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvShl 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvshlWhat4.Protocol.SMTLib2.Syntax
bvsignExtendWhat4.Protocol.SMTLib2.Syntax
bvSLeWhat4.Protocol.SMTWriter
bvSleWhat4.Interface
bvsle 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvSliceBEWhat4.SWord
bvSliceLEWhat4.SWord
BVSltWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvSLtWhat4.Protocol.SMTWriter
bvSltWhat4.Interface
bvslt 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvSortWhat4.Protocol.SMTLib2.Syntax
bvSplitVectorWhat4.Interface
BVSremWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvSRem 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvSremWhat4.Interface
bvsremWhat4.Protocol.SMTLib2.Syntax
BVSubWhat4.Protocol.VerilogWriter.AST
bvSub 
1 (Function)What4.Interface
2 (Function)What4.SWord
3 (Function)What4.Protocol.SMTWriter
bvsubWhat4.Protocol.SMTLib2.Syntax
bvSumWhat4.Expr.Builder
bvSumExprWhat4.Protocol.SMTWriter
bvSwapWhat4.Interface
BVTermWhat4.Protocol.SMTLib2.Parse
bvTermWhat4.Protocol.SMTWriter
BVTestBitWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvTestBitWhat4.Protocol.SMTWriter
BVToFloatWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvToFloat 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
BVToIntegerWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvToInteger 
1 (Function)What4.Interface
2 (Function)What4.SWord
BVToIntegerFnWhat4.Expr.MATLAB
bvToNatWhat4.Interface
bvTruncWhat4.Interface
BVTypeMapWhat4.Protocol.SMTWriter
BVUdivWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvUDiv 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvUdivWhat4.Interface
bvudivWhat4.Protocol.SMTLib2.Syntax
bvUgeWhat4.Interface
bvuge 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvUgtWhat4.Interface
bvugt 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvULeWhat4.Protocol.SMTWriter
bvUleWhat4.Interface
bvule 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
BVUltWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvULtWhat4.Protocol.SMTWriter
bvUltWhat4.Interface
bvult 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SWord
bvUnaryWhat4.Expr.Builder
BVUnaryTermWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvUnpackBEWhat4.SWord
bvUnpackLEWhat4.SWord
BVUremWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvURem 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvUremWhat4.Interface
bvuremWhat4.Protocol.SMTLib2.Syntax
bvWidth 
1 (Function)What4.Interface, What4.Expr.Builder
2 (Function)What4.SWord
BVXorWhat4.Protocol.VerilogWriter.AST
bvXor 
1 (Function)What4.SWord
2 (Function)What4.Protocol.SMTWriter
bvxorWhat4.Protocol.SMTLib2.Syntax
bvXorBitsWhat4.Interface
bvzeroExtendWhat4.Protocol.SMTLib2.Syntax
BVZextWhat4.Expr.App, What4.Expr.Builder, What4.Expr
bvZext 
1 (Function)What4.Interface
2 (Function)What4.SWord
cacheWhat4.Expr.App
cacheStartSizeOptionWhat4.Expr.Builder
cacheTermsWhat4.Expr.Builder
carrylessMultiplyWhat4.Interface
CeilRealWhat4.Expr.App, What4.Expr.Builder, What4.Expr
Char16What4.BaseTypes, What4.Interface
Char16LiteralWhat4.Utils.StringLiteral, What4.Interface
Char16ReprWhat4.BaseTypes, What4.Interface
Char8What4.BaseTypes, What4.Interface
Char8LiteralWhat4.Utils.StringLiteral, What4.Interface
Char8ReprWhat4.BaseTypes, What4.Interface
Char8TypeMapWhat4.Protocol.SMTWriter
checkWhat4.Protocol.Online
checkAndGetModelWhat4.Protocol.Online
checkCommandsWhat4.Protocol.SMTWriter
checkOptSetResultWhat4.Config
checkSatWhat4.Protocol.SMTLib2.Syntax
checkSatAssumingWhat4.Protocol.SMTLib2.Syntax
CheckSatErrorWhat4.Protocol.SMTLib2.Parse
checkSatisfiableWhat4.Protocol.Online
checkSatisfiableWithModelWhat4.Protocol.Online
CheckSatResponseWhat4.Protocol.SMTLib2.Parse
CheckSatUnsupportedWhat4.Protocol.SMTLib2.Parse
checkSatWithAssumptionsWhat4.Protocol.SMTLib2.Syntax
checkSolverVersionWhat4.Protocol.SMTLib2
checkSolverVersion'What4.Protocol.SMTLib2
checkWithAssumptionsWhat4.Protocol.Online
checkWithAssumptionsAndModelWhat4.Protocol.Online
checkWithAssumptionsCommandsWhat4.Protocol.SMTWriter
chooseBoolTest.Verification
chooseIntTest.Verification
chooseIntegerTest.Verification
clampedIntAbsWhat4.Expr.MATLAB
ClampedIntAbsFnWhat4.Expr.MATLAB
clampedIntAddWhat4.Expr.MATLAB
ClampedIntAddFnWhat4.Expr.MATLAB
clampedIntMulWhat4.Expr.MATLAB
ClampedIntMulFnWhat4.Expr.MATLAB
clampedIntNegWhat4.Expr.MATLAB
ClampedIntNegFnWhat4.Expr.MATLAB
clampedIntSubWhat4.Expr.MATLAB
ClampedIntSubFnWhat4.Expr.MATLAB
clampedIntToBVWhat4.Interface
clampedIntToSBVWhat4.Interface
clampedUIntAddWhat4.Expr.MATLAB
ClampedUIntAddFnWhat4.Expr.MATLAB
clampedUIntMulWhat4.Expr.MATLAB
ClampedUIntMulFnWhat4.Expr.MATLAB
clampedUIntSubWhat4.Expr.MATLAB
ClampedUIntSubFnWhat4.Expr.MATLAB
cleanupProcessWhat4.Utils.Process
clearIdxCacheWhat4.Expr.Builder
clz 
1 (Function)What4.Utils.Arithmetic
2 (Function)What4.Utils.BVDomain
CmdWhat4.Protocol.SMTLib2.Syntax
CoefficientWhat4.SemiRing, What4.Expr
CollectedVarInfoWhat4.Expr.VarIdentification
CollectorResults 
1 (Type/Class)What4.Protocol.SMTWriter
2 (Data Constructor)What4.Protocol.SMTWriter
collectVarInfoWhat4.Expr.VarIdentification
combineWhat4.Expr.BoolMap
Command 
1 (Type/Class)What4.Protocol.SMTLib2.Syntax
2 (Type/Class)What4.Protocol.SMTWriter
commentCommandWhat4.Protocol.SMTWriter
compareExprWhat4.Expr.App
compareNatWhat4.BaseTypes, What4.Interface
ComplexWhat4.Utils.Complex
complexAddWhat4.Utils.Complex
complexAsRationalWhat4.Utils.Complex
complexDivWhat4.Utils.Complex
complexMulWhat4.Utils.Complex
complexNegateWhat4.Utils.Complex
complexRecipWhat4.Utils.Complex
complexSubWhat4.Utils.Complex
ComplexToArrayTypeMapWhat4.Protocol.SMTWriter
ComplexToStructTypeMapWhat4.Protocol.SMTWriter
ComputableArithTheoryWhat4.Expr.AppTheory, What4.Expr
computeDefaultSolverBoundsWhat4.Utils.Versions
ConcatWhat4.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
concat2What4.Protocol.VerilogWriter.AST
ConcreteArrayWhat4.Concrete
ConcreteBoolWhat4.Concrete
ConcreteBVWhat4.Concrete
ConcreteComplexWhat4.Concrete
ConcreteIntegerWhat4.Concrete
concreteRangeWhat4.Utils.AbstractDomains
ConcreteRealWhat4.Concrete
ConcreteStringWhat4.Concrete
ConcreteStructWhat4.Concrete
concreteToSymWhat4.Interface
concreteTypeWhat4.Concrete
ConcreteValWhat4.Concrete
ConcreteValueWhat4.Utils.AbstractDomains
ConcreteValueWrapper 
1 (Type/Class)What4.Utils.AbstractDomains
2 (Data Constructor)What4.Utils.AbstractDomains
ConfigWhat4.Config
ConfigDescWhat4.Config
configHelpWhat4.Config
ConfigOptionWhat4.Config
configOptionWhat4.Config
configOptionNameWhat4.Config
configOptionNamePartsWhat4.Config
configOptionTextWhat4.Config
configOptionTypeWhat4.Config
ConfigValue 
1 (Type/Class)What4.Config
2 (Data Constructor)What4.Config
ConjPredWhat4.Expr.App, What4.Expr.Builder, What4.Expr
ConnectionWhat4.Solver.Yices
connHandleWhat4.Protocol.SMTWriter
connInputHandleWhat4.Protocol.SMTWriter
connStateWhat4.Protocol.SMTWriter
constant 
1 (Function)What4.Expr.WeightedSum
2 (Function)What4.Expr.UnaryBV
ConstantArrayWhat4.Expr.App, What4.Expr.Builder, What4.Expr
constantArrayWhat4.Interface
containsWhat4.Expr.BoolMap
ContinueOnErrorWhat4.Protocol.Online
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_scalarWhat4.Utils.BVDomain.XOR
correct_any 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
correct_arithToBitwiseWhat4.Utils.BVDomain
correct_arithToXorDomainWhat4.Utils.BVDomain
correct_ashr 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
correct_asXorDomainWhat4.Utils.BVDomain
correct_bitbounds 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.XOR
correct_bitwiseToArithWhat4.Utils.BVDomain
correct_bitwiseToXorDomainWhat4.Utils.BVDomain
correct_bra1What4.Utils.BVDomain
correct_bra2What4.Utils.BVDomain
correct_brb1What4.Utils.BVDomain
correct_brb2What4.Utils.BVDomain
correct_clzWhat4.Utils.BVDomain
correct_concat 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
correct_ctzWhat4.Utils.BVDomain
correct_eq 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
correct_fromXorDomainWhat4.Utils.BVDomain
correct_intersectionWhat4.Utils.BVDomain.Bitwise
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_popcntWhat4.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_eqWhat4.Utils.BVDomain.Arith
correct_sdiv 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
correct_sdivRangeWhat4.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_unknownsWhat4.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_xorToBitwiseDomainWhat4.Utils.BVDomain
correct_zero_ext 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
countOccurrencesWhat4.Expr.App
countOccurrences'What4.Expr.App
count_subtermsWhat4.Expr.Simplify
CplxWhat4.Expr.App, What4.Expr.Builder, What4.Expr
cplxAddWhat4.Interface
CplxAddFnWhat4.Expr.MATLAB
cplxCeilWhat4.Interface
CplxCeilFnWhat4.Expr.MATLAB
cplxConjWhat4.Interface
cplxCosWhat4.Interface
CplxCosFnWhat4.Expr.MATLAB
cplxDivWhat4.Interface
cplxEqWhat4.Interface
cplxExpWhat4.Interface
CplxExpFnWhat4.Expr.MATLAB
CplxExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
cplxExprAsIntegerWhat4.Interface
cplxExprAsRationalWhat4.Interface
cplxFloorWhat4.Interface
CplxFloorFnWhat4.Expr.MATLAB
cplxFromRealWhat4.Interface
cplxGetPartsWhat4.Interface
cplxHypotWhat4.Interface
CplxIsNonZeroFnWhat4.Expr.MATLAB
CplxIsRealFnWhat4.Expr.MATLAB
cplxIteWhat4.Interface
cplxLogWhat4.Interface
cplxLogBaseWhat4.Interface
CplxLogBaseFnWhat4.Expr.MATLAB
CplxLogFnWhat4.Expr.MATLAB
cplxMagWhat4.Interface
CplxMagFnWhat4.Expr.MATLAB
cplxMulWhat4.Interface
CplxMulFnWhat4.Expr.MATLAB
cplxNeWhat4.Interface
cplxNegWhat4.Interface
CplxNegFnWhat4.Expr.MATLAB
cplxRoundWhat4.Interface
CplxRoundFnWhat4.Expr.MATLAB
cplxSinWhat4.Interface
CplxSinFnWhat4.Expr.MATLAB
cplxSqrtWhat4.Interface
CplxSqrtFnWhat4.Expr.MATLAB
cplxSubWhat4.Interface
CplxSubFnWhat4.Expr.MATLAB
cplxTanWhat4.Interface
CplxTanFnWhat4.Expr.MATLAB
crBindingsWhat4.Protocol.SMTWriter
crFreeConstantsWhat4.Protocol.SMTWriter
crResultWhat4.Protocol.SMTWriter
crSideCondsWhat4.Protocol.SMTWriter
ctz 
1 (Function)What4.Utils.Arithmetic
2 (Function)What4.Utils.BVDomain
curProgramLocWhat4.Expr.Builder
CVC4 
1 (Type/Class)What4.Solver.CVC4, What4.Solver
2 (Data Constructor)What4.Solver.CVC4, What4.Solver
cvc4AdapterWhat4.Solver.CVC4, What4.Solver
cvc4FeaturesWhat4.Solver.CVC4, What4.Solver
cvc4OptionsWhat4.Solver.CVC4, What4.Solver
cvc4PathWhat4.Solver.CVC4, What4.Solver
cvc4TimeoutWhat4.Solver.CVC4
dblPosIsPosWhat4.BaseTypes, What4.Interface
DBVWhat4.SWord
decDocWhat4.Protocol.VerilogWriter.ABCVerilog
decideLeqWhat4.BaseTypes, What4.Interface
decimalWhat4.Protocol.SMTLib2.Syntax
declareCommandWhat4.Protocol.SMTWriter
declareConstWhat4.Protocol.SMTLib2.Syntax
declareFunWhat4.Protocol.SMTLib2.Syntax
declareSortWhat4.Protocol.SMTLib2.Syntax
DeclareSortResponseWhat4.Protocol.SMTLib2.Parse
declareStructDatatypeWhat4.Protocol.SMTWriter
decNatWhat4.BaseTypes, What4.Interface
defaultFeaturesWhat4.Protocol.SMTLib2
defaultLogDataWhat4.Solver.Adapter, What4.Solver
defaultPPExprOptsWhat4.Expr.App
defaultSolverAdapterWhat4.Solver.Adapter, What4.Solver
defaultSolverArgsWhat4.Protocol.SMTLib2
defaultSolverBoundsWhat4.Protocol.SMTLib2
defaultSolverPathWhat4.Protocol.SMTLib2
defaultValueForTypeWhat4.Expr.GroundEval
defaultWriteSMTLIB2FeaturesWhat4.Solver.Adapter
defineCommandWhat4.Protocol.SMTWriter
definedFnWhat4.Interface
DefinedFnInfoWhat4.Expr.App, What4.Expr.Builder, What4.Expr
DefineFun 
1 (Type/Class)What4.Protocol.SMTLib2.Parse
2 (Data Constructor)What4.Protocol.SMTLib2.Parse
defineFunWhat4.Protocol.SMTLib2.Syntax
DefineFunResponseWhat4.Protocol.SMTLib2.Parse
defineSortWhat4.Protocol.SMTLib2.Syntax
DefineStyleWhat4.Protocol.SMTWriter
delete 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Expr.ArrayUpdateMap
deleteFindMaxWhat4.Utils.LeqMap
deleteFindMinWhat4.Utils.LeqMap
deleteIdxValueWhat4.Expr.Builder
demuxProcessHandlesWhat4.Utils.HandleReader
differenceWhat4.Utils.AnnotatedMap
distinctWhat4.Protocol.SMTLib2.Syntax
divWhat4.Protocol.SMTLib2.Syntax
divNatWhat4.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
domainWhat4.Expr.UnaryBV
domainsOverlap 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
DoubleDoubleFloatWhat4.InterpretedFloatingPoint
DoubleDoubleFloatReprWhat4.InterpretedFloatingPoint
DoubleFloatWhat4.InterpretedFloatingPoint
DoubleFloatReprWhat4.InterpretedFloatingPoint
DReal 
1 (Type/Class)What4.Solver.DReal, What4.Solver
2 (Data Constructor)What4.Solver.DReal, What4.Solver
drealAdapterWhat4.Solver.DReal, What4.Solver
DRealBindingsWhat4.Solver.DReal, What4.Solver
drealOptionsWhat4.Solver.DReal
drealPathWhat4.Solver.DReal, What4.Solver
dropWhat4.Utils.Word16String
DummyWhat4.Expr.App
efSolveCommandWhat4.Solver.Yices
empty 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Utils.LeqMap
3 (Function)What4.Utils.Word16String
4 (Function)What4.Expr.ArrayUpdateMap
emptySolverBoundsWhat4.Utils.Versions
emptySymbolWhat4.Symbol, What4.Interface
emptySymbolVarBimapWhat4.Expr.Builder
emptyWordMapWhat4.WordMap
EndianWhat4.Utils.Endian
entryStackHeightWhat4.Protocol.SMTWriter
enumOptStyWhat4.Config
EqWhat4.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
eqByWhat4.Utils.AnnotatedMap
eqPredWhat4.Interface
EqualityDefinitionWhat4.Protocol.SMTWriter
ErrWhat4.Partial
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
evalBoundVarsWhat4.Expr.Builder
evalGroundAppWhat4.Expr.GroundEval
evalGroundExprWhat4.Expr.GroundEval
evalGroundNonceAppWhat4.Expr.GroundEval
evalMWhat4.Expr.WeightedSum
evalMatlabSolverFnWhat4.Expr.MATLAB
evaluateWhat4.Expr.UnaryBV
ExclusiveWhat4.Config
executablePathOptStyWhat4.Config
execVerilogMWhat4.Protocol.VerilogWriter.AST
ExistBoundWhat4.Expr.VarIdentification
existQuantifiersWhat4.Expr.VarIdentification
ExistsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
existsWhat4.Protocol.SMTLib2.Syntax
existsExprWhat4.Protocol.SMTWriter
ExistsForallWhat4.Expr.VarIdentification
ExistsOnlyWhat4.Expr.VarIdentification
existsPredWhat4.Interface
exitWhat4.Protocol.SMTLib2.Syntax
ExpWhat4.Protocol.VerilogWriter.AST
expandEnvironmentPathWhat4.Utils.Environment
expDocWhat4.Protocol.VerilogWriter.ABCVerilog
exponentBitsWhat4.SFloat
ExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
exprAbsValueWhat4.Expr.App
ExprBoundVarWhat4.Expr.App, What4.Expr.Builder, What4.Expr
ExprBuilderWhat4.Expr.Builder, What4.Expr
exprCounterWhat4.Expr.Builder
exprLocWhat4.Expr.App, What4.Expr.Builder, What4.Expr
exprMaybeIdWhat4.Expr.Builder
ExprPPIndexWhat4.Expr.App
exprPrettyArgWhat4.Expr.App
exprPrettyIndicesWhat4.Expr.App
ExprRangeBindingsWhat4.Expr.GroundEval, What4.Expr, What4.Solver.DReal, What4.Solver
ExprSymFn 
1 (Type/Class)What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Data Constructor)What4.Expr.App, What4.Expr.Builder, What4.Expr
exprToModuleWhat4.Protocol.VerilogWriter
exprToVerilogExprWhat4.Protocol.VerilogWriter.Backend
exprTypeWhat4.Interface, What4.Expr.Builder
exprVerilogWhat4.Protocol.VerilogWriter
expTypeWhat4.Protocol.VerilogWriter.AST
extendConfigWhat4.Config
ExternalABC 
1 (Type/Class)What4.Solver.ExternalABC, What4.Solver
2 (Data Constructor)What4.Solver.ExternalABC, What4.Solver
externalABCAdapterWhat4.Solver.ExternalABC, What4.Solver
extractWhat4.Protocol.SMTLib2.Syntax
extractCommonWhat4.Expr.WeightedSum
falseWhat4.Protocol.SMTLib2.Syntax
falsePredWhat4.Interface
fillrightWhat4.Utils.BVDomain.Arith
filter 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Expr.ArrayUpdateMap
filterAsyncWhat4.Utils.Process
filterGtWhat4.Utils.LeqMap
filterLtWhat4.Utils.LeqMap
findExecutableWhat4.Utils.Environment
findExprToRemoveWhat4.Expr.App
findMaxWhat4.Utils.LeqMap
findMinWhat4.Utils.LeqMap
findSolverPathWhat4.Utils.Process
findSubstringWhat4.Utils.Word16String
FixedPPExprWhat4.Expr.App
FlagsWhat4.Expr.Builder, What4.Expr
FloatAbsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatAbs 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatAddWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatAdd 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatCastWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatCast 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatDivWhat4.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 (Type/Class)What4.Expr.App, What4.Expr.Builder
2 (Data Constructor)What4.Expr.App, What4.Expr.Builder, What4.Expr
FloatFMAWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatFMA 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatFpApartWhat4.Interface
FloatFpEqWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatFpEq 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatFpUnorderedWhat4.Interface
FloatFromBinaryWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatFromBinary 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatFromIntegerWhat4.Utils.FloatHelpers
floatFromRationalWhat4.Utils.FloatHelpers
floatGeWhat4.Interface
floatGtWhat4.Interface
FloatIEEEWhat4.Expr.Builder, What4.Expr
FloatIEEEReprWhat4.Expr.Builder, What4.Expr
FloatInfoWhat4.InterpretedFloatingPoint
FloatInfoReprWhat4.InterpretedFloatingPoint
FloatInfoToBitWidthWhat4.InterpretedFloatingPoint
floatInfoToBVTypeReprWhat4.InterpretedFloatingPoint
FloatInfoToPrecisionWhat4.InterpretedFloatingPoint
floatInfoToPrecisionReprWhat4.InterpretedFloatingPoint
FloatingPointWhat4.Protocol.SMTLib2.Parse
FloatingPointPrecisionWhat4.BaseTypes, What4.Interface
FloatingPointPrecisionReprWhat4.BaseTypes, What4.Interface
FloatingPointTheoryWhat4.Expr.AppTheory, What4.Expr
FloatIsInfWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsInf 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsNaNWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNaN 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsNegWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNeg 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsNormWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsNorm 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsPosWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsPos 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsSubnormWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsSubnorm 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatIsZeroWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatIsZero 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatIteWhat4.Interface
FloatLeWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatLe 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatLitWhat4.Interface
floatLitRationalWhat4.Interface
FloatLtWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatLt 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatMaxWhat4.Interface
floatMinWhat4.Interface
FloatModeWhat4.Expr.Builder, What4.Expr
FloatModeReprWhat4.Expr.Builder, What4.Expr
FloatMulWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatMul 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatNaNWhat4.Interface
floatNeWhat4.Interface
FloatNegWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatNeg 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatNInfWhat4.Interface
floatNZeroWhat4.Interface
floatPInfWhat4.Interface
FloatPrecisionWhat4.BaseTypes, What4.Interface
floatPrecisionWhat4.Interface
FloatPrecisionBitsWhat4.BaseTypes, What4.Interface
FloatPrecisionReprWhat4.BaseTypes, What4.Interface
floatPrecisionToBVTypeWhat4.BaseTypes, What4.Interface
FloatPrecisionToInfoWhat4.InterpretedFloatingPoint
floatPrecisionToInfoReprWhat4.InterpretedFloatingPoint
floatPZeroWhat4.Interface
FloatRealWhat4.Expr.Builder, What4.Expr
FloatRealReprWhat4.Expr.Builder, What4.Expr
FloatRemWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatRem 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatRoundWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatRound 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatRoundToIntWhat4.Utils.FloatHelpers
FloatSqrtWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatSqrt 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatSubWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatSub 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatTermWhat4.Protocol.SMTWriter
FloatToBinaryWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatToBinaryWhat4.Interface
FloatToBVWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatToBV 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
floatToIntegerWhat4.Utils.FloatHelpers
floatToRationalWhat4.Utils.FloatHelpers
FloatToRealWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatToReal 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatToSBVWhat4.Expr.App, What4.Expr.Builder, What4.Expr
floatToSBV 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
FloatTypeMapWhat4.Protocol.SMTWriter
FloatUninterpretedWhat4.Expr.Builder, What4.Expr
FloatUninterpretedReprWhat4.Expr.Builder, What4.Expr
FloorRealWhat4.Expr.App, What4.Expr.Builder, What4.Expr
FnAppWhat4.Expr.App, What4.Expr.Builder, What4.Expr
fnArgTypesWhat4.Interface
FnArrayTypeMapWhat4.Protocol.SMTWriter
fnReturnTypeWhat4.Interface
FnSymbolBindingWhat4.Expr.Builder
FnTheoryWhat4.Expr.AppTheory, What4.Expr
foldl'What4.Utils.Word16String
foldlWithKey'What4.Utils.LeqMap
ForallWhat4.Expr.App, What4.Expr.Builder, What4.Expr
forallWhat4.Protocol.SMTLib2.Syntax
ForallBoundWhat4.Expr.VarIdentification
forallExprWhat4.Protocol.SMTWriter
forallPredWhat4.Interface
forallQuantifiersWhat4.Expr.VarIdentification
forgetModelAndCoreWhat4.SatResult, What4.Solver
fp80ToBitsWhat4.InterpretedFloatingPoint
fp80ToRationalWhat4.InterpretedFloatingPoint
fpAbsWhat4.SFloat
fpActualWhat4.SFloat
fpAddWhat4.SFloat
fpAsLitWhat4.SFloat
fpDivWhat4.SFloat
fpEqWhat4.SFloat
fpEqIEEEWhat4.SFloat
fpExpectedWhat4.SFloat
fpFMAWhat4.SFloat
fpFreshWhat4.SFloat
fpFromBinaryWhat4.SFloat
fpFromIntegerWhat4.SFloat
fpFromLitWhat4.SFloat
fpFromRationalWhat4.SFloat
fpFromRationalLitWhat4.SFloat
fpFromRealWhat4.SFloat
fpGtIEEEWhat4.SFloat
fpIsInfWhat4.SFloat
fpIsNaNWhat4.SFloat
fpIsNegWhat4.SFloat
fpIsNormWhat4.SFloat
fpIsSubnormWhat4.SFloat
fpIsZeroWhat4.SFloat
fpIteWhat4.SFloat
fpLtIEEEWhat4.SFloat
fpMaxWhat4.SFloat
fpMinWhat4.SFloat
fpMulWhat4.SFloat
fpNaNWhat4.SFloat
fpNegWhat4.SFloat
fpNegInfWhat4.SFloat
fpOptsWhat4.Utils.FloatHelpers
fppOptsWhat4.Utils.FloatHelpers
fpPosInfWhat4.SFloat
fpReprWhat4.SFloat
fpReprOfWhat4.SFloat
fpRoundWhat4.SFloat
fpSizeWhat4.SFloat
fpSqrtWhat4.SFloat
fpSubWhat4.SFloat
fpToBinaryWhat4.SFloat
fpToRationalWhat4.SFloat
fpToRealWhat4.SFloat
FPTypeError 
1 (Type/Class)What4.SFloat
2 (Data Constructor)What4.SFloat
fpWhoWhat4.SFloat
freshBoundedBVWhat4.Interface
freshBoundedIntWhat4.Interface
freshBoundedNatWhat4.Interface
freshBoundedRealWhat4.Interface
freshBoundedSBVWhat4.Interface
freshBoundVarWhat4.Interface
freshBoundVarNameWhat4.Protocol.SMTWriter
freshBVWhat4.SWord
freshConstantWhat4.Interface
freshFloatBoundVarWhat4.InterpretedFloatingPoint
freshFloatConstantWhat4.InterpretedFloatingPoint
freshFloatLatchWhat4.InterpretedFloatingPoint
freshIdentifierWhat4.Protocol.VerilogWriter.AST
freshLatchWhat4.Interface
freshNatWhat4.Interface
freshTotalUninterpFnWhat4.Interface
fromAscEltList 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
fromAscList 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Expr.ArrayUpdateMap
fromChar16LitWhat4.Utils.StringLiteral
fromChar8LitWhat4.Utils.StringLiteral
fromConcreteBoolWhat4.Concrete
fromConcreteBVWhat4.Concrete
fromConcreteComplexWhat4.Concrete
fromConcreteIntegerWhat4.Concrete
fromConcreteRealWhat4.Concrete
fromConcreteStringWhat4.Concrete
fromDistinctAscListWhat4.Utils.LeqMap
fromDistinctDescListWhat4.Utils.LeqMap
fromLEByteStringWhat4.Utils.Word16String
fromTermsWhat4.Expr.WeightedSum
fromTextWhat4.Protocol.SMTWriter
fromUnicodeLitWhat4.Utils.StringLiteral
fromVarsWhat4.Expr.BoolMap
fromXorDomainWhat4.Utils.BVDomain
fromYicesTextWhat4.Protocol.PolyRoot
funArgsWhat4.Protocol.SMTLib2.Parse
FunctionDefinitionWhat4.Protocol.SMTWriter
FunctionNameWhat4.FunctionName
functionNameWhat4.FunctionName
functionNameFromTextWhat4.FunctionName
funDefWhat4.Protocol.SMTLib2.Parse
funResultSortWhat4.Protocol.SMTLib2.Parse
funSymbolWhat4.Protocol.SMTLib2.Parse
geWhat4.Protocol.SMTLib2.Syntax
GenTest.Verification
genChooseBoolTest.Verification
genChooseIntTest.Verification
genChooseIntegerTest.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
genGetSizeTest.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
getAbsValueWhat4.Utils.AbstractDomains
getAnnotationWhat4.Interface
getAvgBindingsWhat4.Solver.DReal
getBoundBindingsWhat4.Solver.DReal
getConfigurationWhat4.Interface
getConfigValuesWhat4.Config
getCurrentProgramLocWhat4.Interface
getErrorBehavior 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
getGoalTimeoutInMilliSecondsWhat4.Protocol.Online
getGoalTimeoutInSecondsWhat4.Protocol.Online
getImagPartWhat4.Interface
getInfoWhat4.Protocol.SMTLib2.Syntax
getMaybeOptWhat4.Config
getModel 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.Online
GetModelResponseWhat4.Protocol.SMTLib2.Parse
getName 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
getOptWhat4.Config
getOptionWhat4.Config
getOptionSettingWhat4.Config
getOptionSettingFromTextWhat4.Config
getRealPartWhat4.Interface
getSatResultWhat4.Protocol.Online
getSizeTest.Verification
getSolverLogListenerWhat4.Interface
getStatisticsWhat4.Interface
getSymbolVarBimapWhat4.Expr.Builder
getUnsatAssumptions 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.Online
getUnsatAssumptionsCommandWhat4.Protocol.SMTWriter
getUnsatCore 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.Online
getUnsatCoreCommandWhat4.Protocol.SMTWriter
getValueWhat4.Protocol.SMTLib2.Syntax
getVersion 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
GroundArrayWhat4.Expr.GroundEval, What4.Expr
groundEqWhat4.Expr.GroundEval
groundEvalWhat4.Expr.GroundEval, What4.Expr
GroundEvalFn 
1 (Type/Class)What4.Expr.GroundEval, What4.Expr
2 (Data Constructor)What4.Expr.GroundEval, What4.Expr
GroundValueWhat4.Expr.GroundEval, What4.Expr
GroundValueWrapperWhat4.Expr.GroundEval, What4.Expr
gtWhat4.Protocol.SMTLib2.Syntax
GVWWhat4.Expr.GroundEval, What4.Expr
HalfFloatWhat4.InterpretedFloatingPoint
HalfFloatReprWhat4.InterpretedFloatingPoint
halfNatWhat4.BaseTypes, What4.Interface
HandleReader 
1 (Type/Class)What4.Utils.HandleReader, What4.Solver.Yices
2 (Data Constructor)What4.Utils.HandleReader
HasAbsValueWhat4.Utils.AbstractDomains, What4.Interface
HasCallStackWhat4.Panic
hashAppWhat4.Expr.App
hashIndexLitWhat4.IndexLit
hasProblemFeatureWhat4.ProblemFeatures
HasProgramLocWhat4.ProgramLoc
hexDocWhat4.Protocol.VerilogWriter.ABCVerilog
hrChanWhat4.Utils.HandleReader
hrHandleWhat4.Utils.HandleReader
hrThreadIdWhat4.Utils.HandleReader
iBVToFloatWhat4.InterpretedFloatingPoint
IdentWhat4.Protocol.VerilogWriter.AST
identDocWhat4.Protocol.VerilogWriter.ABCVerilog
IdentifierWhat4.Protocol.VerilogWriter.AST
IdxCacheWhat4.Expr.Builder
idxCacheEvalWhat4.Expr.Builder
idxCacheEval'What4.Expr.Builder
IExp 
1 (Data Constructor)What4.Protocol.VerilogWriter.AST
2 (Type/Class)What4.Protocol.VerilogWriter.AST
iexpDocWhat4.Protocol.VerilogWriter.ABCVerilog
iexpTypeWhat4.Protocol.VerilogWriter.AST
IfEqTermWhat4.Protocol.SMTLib2.Parse
iFloatAbsWhat4.InterpretedFloatingPoint
iFloatAddWhat4.InterpretedFloatingPoint
iFloatBaseTypeReprWhat4.InterpretedFloatingPoint
iFloatCastWhat4.InterpretedFloatingPoint
iFloatDivWhat4.InterpretedFloatingPoint
iFloatEqWhat4.InterpretedFloatingPoint
iFloatFMAWhat4.InterpretedFloatingPoint
iFloatFpApartWhat4.InterpretedFloatingPoint
iFloatFpEqWhat4.InterpretedFloatingPoint
iFloatFromBinaryWhat4.InterpretedFloatingPoint
iFloatGeWhat4.InterpretedFloatingPoint
iFloatGtWhat4.InterpretedFloatingPoint
iFloatIsInfWhat4.InterpretedFloatingPoint
iFloatIsNaNWhat4.InterpretedFloatingPoint
iFloatIsNegWhat4.InterpretedFloatingPoint
iFloatIsNormWhat4.InterpretedFloatingPoint
iFloatIsPosWhat4.InterpretedFloatingPoint
iFloatIsSubnormWhat4.InterpretedFloatingPoint
iFloatIsZeroWhat4.InterpretedFloatingPoint
iFloatIteWhat4.InterpretedFloatingPoint
iFloatLeWhat4.InterpretedFloatingPoint
iFloatLitDoubleWhat4.InterpretedFloatingPoint
iFloatLitLongDoubleWhat4.InterpretedFloatingPoint
iFloatLitRationalWhat4.InterpretedFloatingPoint
iFloatLitSingleWhat4.InterpretedFloatingPoint
iFloatLtWhat4.InterpretedFloatingPoint
iFloatMaxWhat4.InterpretedFloatingPoint
iFloatMinWhat4.InterpretedFloatingPoint
iFloatMulWhat4.InterpretedFloatingPoint
iFloatNaNWhat4.InterpretedFloatingPoint
iFloatNeWhat4.InterpretedFloatingPoint
iFloatNegWhat4.InterpretedFloatingPoint
iFloatNInfWhat4.InterpretedFloatingPoint
iFloatNZeroWhat4.InterpretedFloatingPoint
iFloatPInfWhat4.InterpretedFloatingPoint
iFloatPZeroWhat4.InterpretedFloatingPoint
iFloatRemWhat4.InterpretedFloatingPoint
iFloatRoundWhat4.InterpretedFloatingPoint
iFloatSqrtWhat4.InterpretedFloatingPoint
iFloatSubWhat4.InterpretedFloatingPoint
iFloatToBinaryWhat4.InterpretedFloatingPoint
iFloatToBVWhat4.InterpretedFloatingPoint
iFloatToRealWhat4.InterpretedFloatingPoint
iFloatToSBVWhat4.InterpretedFloatingPoint
ImagPartWhat4.Expr.App, What4.Expr.Builder, What4.Expr
imagPartWhat4.Utils.Complex
ImagPartOfCplxFnWhat4.Expr.MATLAB
ImmediateExitWhat4.Protocol.Online
impliesWhat4.Protocol.SMTLib2.Syntax
impliesExprWhat4.Protocol.SMTWriter
impliesPredWhat4.Interface
Inclusive 
1 (Data Constructor)What4.Utils.AbstractDomains
2 (Data Constructor)What4.Config
incNatWhat4.BaseTypes, What4.Interface
incOccurrenceWhat4.Expr.App
IncrHashWhat4.Utils.IncrHash
indexWhat4.Utils.Word16String
IndexLitWhat4.IndexLit, What4.Interface, What4.Expr.Builder
indexLitWhat4.Interface
IndicesInRangeWhat4.Expr.MATLAB
InfoKeywordWhat4.Protocol.SMTLib2.Syntax
initialConfigWhat4.Config
initializationLocWhat4.ProgramLoc
initModuleStateWhat4.Protocol.VerilogWriter.AST
inlineDefineFunWhat4.Interface
inNewFrameWhat4.Protocol.Online, What4.Solver.Yices
inNewFrameWithVarsWhat4.Protocol.Online
InputWhat4.Protocol.VerilogWriter.AST
inputDocWhat4.Protocol.VerilogWriter.ABCVerilog
insert 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Utils.LeqMap
3 (Function)What4.Expr.ArrayUpdateMap
insertIdxValueWhat4.Expr.Builder
insertWordMapWhat4.WordMap
instantiateWhat4.Expr.UnaryBV
IntWhat4.Protocol.SMTLib2.Parse
IntAbsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
intAbs 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
intAbsRangeWhat4.Utils.AbstractDomains
intAddWhat4.Interface
IntDivWhat4.Expr.App, What4.Expr.Builder, What4.Expr
intDiv 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
IntDivisibleWhat4.Expr.App, What4.Expr.Builder, What4.Expr
intDivisible 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
intDivRangeWhat4.Utils.AbstractDomains
integerBoundsWhat4.Interface
IntegerExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
integerOptStyWhat4.Config
integerTermWhat4.Protocol.SMTWriter
IntegerToBVWhat4.Expr.App, What4.Expr.Builder, What4.Expr
integerToBV 
1 (Function)What4.Interface
2 (Function)What4.SWord
integerToNatWhat4.Interface
IntegerToRealWhat4.Expr.App, What4.Expr.Builder, What4.Expr
integerToRealWhat4.Interface
IntegerToRealFnWhat4.Expr.MATLAB
IntegerTypeMapWhat4.Protocol.SMTWriter
integerWithMaxOptStyWhat4.Config
integerWithMinOptStyWhat4.Config
integerWithRangeOptStyWhat4.Config
intEqWhat4.Interface
InternalPosWhat4.ProgramLoc
intersectionWhat4.Utils.BVDomain.Bitwise
interval 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain.XOR
IntIndexLitWhat4.IndexLit, What4.Interface, What4.Expr.Builder
intIteWhat4.Interface
intLeWhat4.Interface
IntLeFnWhat4.Expr.MATLAB
intLitWhat4.Interface
intLtWhat4.Interface
intMaxWhat4.Interface
intMinWhat4.Interface
IntModWhat4.Expr.App, What4.Expr.Builder, What4.Expr
intMod 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
intModRangeWhat4.Utils.AbstractDomains
intMulWhat4.Interface
intNegWhat4.Interface
IntSeqFnWhat4.Expr.MATLAB
intSetWidthWhat4.Interface
IntSetWidthFnWhat4.Expr.MATLAB
intSortWhat4.Protocol.SMTLib2.Syntax
intSubWhat4.Interface
intSumWhat4.Expr.Builder
IntTermWhat4.Protocol.SMTLib2.Parse
intToUIntWhat4.Interface
IntToUIntFnWhat4.Expr.MATLAB
intValueWhat4.BaseTypes, What4.Interface
InvalidRange 
1 (Type/Class)What4.Interface
2 (Data Constructor)What4.Interface
iRealToFloatWhat4.InterpretedFloatingPoint
iSBVToFloatWhat4.InterpretedFloatingPoint
isEqWhat4.Interface
IsEqFnWhat4.Expr.MATLAB
IsExprWhat4.Interface
IsExprBuilderWhat4.Interface
isInconsistentWhat4.Expr.BoolMap
isInfixOfWhat4.Utils.Word16String
isIntWhat4.Protocol.SMTLib2.Syntax
isIntegerWhat4.Interface
IsIntegerFnWhat4.Expr.MATLAB
IsInterpretedFloatExprBuilderWhat4.InterpretedFloatingPoint
IsInterpretedFloatSymExprBuilderWhat4.InterpretedFloatingPoint
isNonLinearAppWhat4.Expr.App
isNonZeroWhat4.Interface
isNullWhat4.Expr.BoolMap
isPosNatWhat4.BaseTypes, What4.Interface
isPow2What4.Utils.Arithmetic
isPrefixOfWhat4.Utils.Word16String
isRealWhat4.Interface
isSatWhat4.SatResult, What4.Solver
isSuffixOfWhat4.Utils.Word16String
IsSymExprBuilderWhat4.Interface
IsSymFnWhat4.Interface
isUnknownWhat4.SatResult, What4.Solver
isUnsatWhat4.SatResult, What4.Solver
isZeroWhat4.Expr.WeightedSum
IsZeroNatWhat4.BaseTypes, What4.Interface
isZeroNatWhat4.BaseTypes, What4.Interface
isZeroOrGT1What4.BaseTypes, What4.Interface
ite 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTWriter
iteListWhat4.Interface
ItemWhat4.Protocol.VerilogWriter.AST
iteMWhat4.Interface
itePredWhat4.Interface
itePredMWhat4.Interface
iteSizeWhat4.Expr.App, What4.Expr.Builder
joinMaybePEWhat4.Partial
joinRangeWhat4.Utils.AbstractDomains
justPartExprWhat4.Partial
keysWhat4.Utils.LeqMap
keysSetWhat4.Expr.ArrayUpdateMap
killSolverWhat4.Protocol.Online
KnownCtxWhat4.BaseTypes, What4.Interface
knownNatWhat4.BaseTypes, What4.Interface
KnownReprWhat4.BaseTypes, What4.Interface
knownReprWhat4.BaseTypes, What4.Interface
LabeledPred 
1 (Type/Class)What4.LabeledPred
2 (Data Constructor)What4.LabeledPred
labeledPredWhat4.LabeledPred
labeledPredMsgWhat4.LabeledPred
lambdaTermWhat4.Protocol.SMTWriter
latchesWhat4.Expr.VarIdentification
LatchVarKindWhat4.Expr.App, What4.Expr.Builder, What4.Expr
LeWhat4.Protocol.VerilogWriter.AST
le 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SemiRing
lemmaFloatPrecisionIsPosWhat4.BaseTypes, What4.Interface
lemmaMulWhat4.BaseTypes, What4.Interface
lengthWhat4.Utils.Word16String
leqAddWhat4.BaseTypes, What4.Interface
leqAdd2What4.BaseTypes, What4.Interface
leqAddPosWhat4.BaseTypes, What4.Interface
LeqMapWhat4.Utils.LeqMap
leqMulCongrWhat4.BaseTypes, What4.Interface
leqMulMonoWhat4.BaseTypes, What4.Interface
leqMulPosWhat4.BaseTypes, What4.Interface
LeqProof 
1 (Data Constructor)What4.BaseTypes, What4.Interface
2 (Type/Class)What4.BaseTypes, What4.Interface
leqProofWhat4.BaseTypes, What4.Interface
leqReflWhat4.BaseTypes, What4.Interface
leqSubWhat4.BaseTypes, What4.Interface
leqSub2What4.BaseTypes, What4.Interface
leqTransWhat4.BaseTypes, What4.Interface
lessThanAsymmetricWhat4.BaseTypes, What4.Interface
lessThanIrreflexiveWhat4.BaseTypes, What4.Interface
letBinderWhat4.Protocol.SMTLib2.Syntax
letExprWhat4.Protocol.SMTWriter
lgWhat4.Utils.Arithmetic
lgCeilWhat4.Utils.Arithmetic
LHS 
1 (Type/Class)What4.Protocol.VerilogWriter.AST
2 (Data Constructor)What4.Protocol.VerilogWriter.AST
LHSBitWhat4.Protocol.VerilogWriter.AST
lhsDocWhat4.Protocol.VerilogWriter.ABCVerilog
liftSTWhat4.Utils.MonadST
LinearArithTheoryWhat4.Expr.AppTheory, What4.Expr
lineBufferedOutputStreamWhat4.Utils.HandleReader
listOptStyWhat4.Config
litBoolWhat4.Protocol.VerilogWriter.AST
litBVWhat4.Protocol.VerilogWriter.AST
LittleEndianWhat4.Utils.Endian
logCallbackWhat4.Solver.Adapter, What4.Solver
logCallbackVerboseWhat4.Solver.Adapter, What4.Solver
LogData 
1 (Type/Class)What4.Solver.Adapter, What4.Solver
2 (Data Constructor)What4.Solver.Adapter, What4.Solver
logErrorStreamWhat4.Utils.Streams
logHandleWhat4.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
logReasonWhat4.Solver.Adapter, What4.Solver
logSolverEventWhat4.Interface
logVerbosityWhat4.Solver.Adapter, What4.Solver
lookup 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Expr.ArrayUpdateMap
lookupArrayWhat4.Expr.GroundEval, What4.Expr
lookupBindingOfSymbolWhat4.Expr.Builder
lookupGEWhat4.Utils.LeqMap
lookupGTWhat4.Utils.LeqMap
lookupIdxWhat4.Expr.Builder
lookupIdxValueWhat4.Expr.Builder
lookupLEWhat4.Utils.LeqMap
lookupLTWhat4.Utils.LeqMap
lookupSymbolOfBindingWhat4.Expr.Builder
lookupWordMapWhat4.WordMap
lowerWhat4.Utils.Versions
lshr 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
LtWhat4.Protocol.VerilogWriter.AST
lt 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SemiRing
magnitudeWhat4.Utils.Complex
magnitudeSqWhat4.Utils.Complex
mapKeysMonotonicWhat4.Utils.LeqMap
mapMaybeWhat4.Utils.AnnotatedMap
MapOverArraysWhat4.Expr.App, What4.Expr.Builder, What4.Expr
mapRangeWhat4.Utils.AbstractDomains
matlabSolverArgTypesWhat4.Expr.MATLAB
MatlabSolverFnWhat4.Expr.MATLAB
MatlabSolverFnInfoWhat4.Expr.App, What4.Expr.Builder, What4.Expr
matlabSolverReturnTypeWhat4.Expr.MATLAB
MatlabSymbolicArrayBuilderWhat4.Expr.MATLAB
maxNatWhat4.BaseTypes, What4.Interface
maxSignedWhat4.BaseTypes, What4.Interface
maxSignedBVWhat4.Interface
maxUnsignedWhat4.BaseTypes, What4.Interface
maxUnsignedBVWhat4.Interface
maxValueBoundWhat4.Utils.AbstractDomains
maybePartExprWhat4.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
mergeAWhat4.Utils.AnnotatedMap
mergeMWhat4.Expr.ArrayUpdateMap
mergePartialWhat4.Partial
mergePartialsWhat4.Partial
mergeWithKey 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Utils.LeqMap
mergeWithKeyMWhat4.Utils.AnnotatedMap
minSignedWhat4.BaseTypes, What4.Interface
minSignedBVWhat4.Interface
minUnsignedWhat4.BaseTypes, What4.Interface
minUnsignedBVWhat4.Interface
minusPlusCancelWhat4.BaseTypes, What4.Interface
minValueBoundWhat4.Utils.AbstractDomains
minViewWithKeyWhat4.Utils.LeqMap
mkAtomicFormulaWhat4.Protocol.SMTWriter
mkBaseExprWhat4.Protocol.SMTWriter
mkComplexWhat4.Interface
mkComplexLitWhat4.Interface
mkExprWhat4.Expr.App
mkFormulaWhat4.Protocol.SMTWriter
mkFreeVarWhat4.Protocol.SMTWriter
mkIncrHashWhat4.Utils.IncrHash
mkLetWhat4.Protocol.VerilogWriter.AST
mkMatlabSolverFnWhat4.Expr.MATLAB
mkModuleWhat4.Protocol.VerilogWriter.AST
mkNatReprWhat4.BaseTypes, What4.Interface
mkOptWhat4.Config
mkPEWhat4.Partial
mkProgramLocWhat4.ProgramLoc
mkRationalWhat4.Interface
mkRealWhat4.Interface
mkSMTTermWhat4.Protocol.SMTWriter
mkStructWhat4.Interface
modWhat4.Protocol.SMTLib2.Syntax
ModelResponseWhat4.Protocol.SMTLib2.Parse
Module 
1 (Type/Class)What4.Protocol.VerilogWriter.AST, What4.Protocol.VerilogWriter
2 (Data Constructor)What4.Protocol.VerilogWriter.AST
moduleDocWhat4.Protocol.VerilogWriter.ABCVerilog
ModuleState 
1 (Type/Class)What4.Protocol.VerilogWriter.AST
2 (Data Constructor)What4.Protocol.VerilogWriter.AST
MonadSTWhat4.Utils.MonadST
mul 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.SemiRing
3 (Function)What4.Utils.BVDomain.Arith
4 (Function)What4.Utils.BVDomain
mul2PlusWhat4.BaseTypes, What4.Interface
mulCancelRWhat4.BaseTypes, What4.Interface
mulCommWhat4.BaseTypes, What4.Interface
mulRangeWhat4.Utils.AbstractDomains
mulSignedOFWhat4.Interface
MultiRangeWhat4.Utils.AbstractDomains, What4.Interface
mulUnsignedOFWhat4.Interface
MuxWhat4.Protocol.VerilogWriter.AST
mux 
1 (Function)What4.Expr.UnaryBV
2 (Function)What4.Protocol.VerilogWriter.AST
muxRangeWhat4.Interface
muxWordMapWhat4.WordMap
NameWhat4.Protocol.SMTLib2.Syntax
namedTermWhat4.Protocol.SMTLib2.Syntax
nameResultWhat4.Protocol.SMTLib2
natAddWhat4.Interface
NatCaseEQWhat4.BaseTypes, What4.Interface
NatCaseGTWhat4.BaseTypes, What4.Interface
NatCaseLTWhat4.BaseTypes, What4.Interface
NatCasesWhat4.BaseTypes, What4.Interface
NatComparisonWhat4.BaseTypes, What4.Interface
natDivWhat4.Interface
NatEQWhat4.BaseTypes, What4.Interface
natEqWhat4.Interface
natForEachWhat4.BaseTypes, What4.Interface
natFromZeroWhat4.BaseTypes, What4.Interface
NatGTWhat4.BaseTypes, What4.Interface
natIteWhat4.Interface
natLeWhat4.Interface
natLitWhat4.Interface
NatLTWhat4.BaseTypes, What4.Interface
natLtWhat4.Interface
natModWhat4.Interface
natMulWhat4.Interface
natMultiplyWhat4.BaseTypes, What4.Interface
natRecWhat4.BaseTypes, What4.Interface
natRecBoundedWhat4.BaseTypes, What4.Interface
natRecStrongWhat4.BaseTypes, What4.Interface
NatReprWhat4.BaseTypes, What4.Interface
natSubWhat4.Interface
natToIntegerWhat4.Interface
natToRealWhat4.Interface
natValueWhat4.BaseTypes, What4.Interface
NeWhat4.Protocol.VerilogWriter.AST
negWhat4.Expr.UnaryBV
negate 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Utils.BVDomain.Arith
3 (Function)What4.Utils.BVDomain
negatePolarityWhat4.Expr.BoolMap, What4.Expr.Builder
negateRangeWhat4.Utils.AbstractDomains
NegativeWhat4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification
NeverUnfoldWhat4.Interface
newConnectionWhat4.Solver.Yices
newDefaultWriterWhat4.Protocol.SMTLib2
newExprBuilderWhat4.Expr.Builder, What4.Expr
newIdxCacheWhat4.Expr.Builder
newWriterWhat4.Protocol.SMTLib2
newWriterConnWhat4.Protocol.SMTWriter
nextMultipleWhat4.Utils.Arithmetic
nextPow2MultipleWhat4.Utils.Arithmetic
NoErrWhat4.Partial
noFeaturesWhat4.ProblemFeatures
NonceAppWhat4.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
NonceAppExprCtorWhat4.Expr.App
nonceAppTypeWhat4.Expr.App, What4.Expr.Builder
nonceExprAbsValueWhat4.Expr.App
nonceExprAppWhat4.Expr.App, What4.Expr.Builder, What4.Expr
nonceExprIdWhat4.Expr.App, What4.Expr.Builder, What4.Expr
nonceExprLocWhat4.Expr.App, What4.Expr.Builder, What4.Expr
nonemptyWhat4.Utils.BVDomain.Bitwise
NonlinearArithTheoryWhat4.Expr.AppTheory, What4.Expr
NonZeroNatWhat4.BaseTypes, What4.Interface
NotWhat4.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
notExprWhat4.Protocol.SMTWriter
NotPredWhat4.Expr.App, What4.Expr.Builder, What4.Expr
notPredWhat4.Interface
null 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Utils.LeqMap
3 (Function)What4.Utils.Word16String
4 (Function)What4.Expr.ArrayUpdateMap
nullAcknowledgementActionWhat4.Protocol.SMTWriter, What4.Protocol.SMTLib2
nullProdWhat4.Expr.WeightedSum
numeralWhat4.Protocol.SMTLib2.Syntax
OccurrenceWhat4.SemiRing
OccurrenceTableWhat4.Expr.App
occ_addWhat4.SemiRing
occ_compareWhat4.SemiRing
occ_countWhat4.SemiRing
occ_eqWhat4.SemiRing
occ_hashWithSaltWhat4.SemiRing
occ_oneWhat4.SemiRing
oneWhat4.SemiRing
OnlineSolverWhat4.Protocol.Online
OnlyIntRepr 
1 (Type/Class)What4.Utils.OnlyIntRepr
2 (Data Constructor)What4.Utils.OnlyIntRepr
OptWhat4.Config
optWhat4.Config
optErrWhat4.Config
optionSetErrorWhat4.Config
OptionSetResult 
1 (Type/Class)What4.Config
2 (Data Constructor)What4.Config
OptionSetting 
1 (Type/Class)What4.Config
2 (Data Constructor)What4.Config
optionSettingNameWhat4.Config
optionSetWarningsWhat4.Config
OptionStyle 
1 (Type/Class)What4.Config
2 (Data Constructor)What4.Config
optOKWhat4.Config
optUWhat4.Config
optUVWhat4.Config
optVWhat4.Config
optWarnWhat4.Config
opt_default_valueWhat4.Config
opt_helpWhat4.Config
opt_onsetWhat4.Config
opt_typeWhat4.Config
OrWhat4.Protocol.VerilogWriter.AST
or 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
orAllWhat4.Protocol.SMTWriter
orderedSemiRingWhat4.SemiRing
OrderedSemiRingIntegerReprWhat4.SemiRing, What4.Expr
OrderedSemiRingRealReprWhat4.SemiRing, What4.Expr
OrderedSemiRingReprWhat4.SemiRing, What4.Expr
orOneOfWhat4.Interface
orPredWhat4.Interface
OtherPosWhat4.ProgramLoc
OutputWhat4.Protocol.VerilogWriter.AST
pairwise_appWhat4.Protocol.SMTLib2.Syntax
PanicWhat4.Panic
panicWhat4.Panic
parenIfWhat4.Expr.App
parseNextWordWhat4.Protocol.SExp
parseSExpWhat4.Protocol.SExp
parseSolverBoundsWhat4.Utils.Versions
parseYicesRootWhat4.Protocol.PolyRoot
PartExprWhat4.Partial
Partial 
1 (Type/Class)What4.Partial
2 (Data Constructor)What4.Partial
partialPredWhat4.Partial
PartialT 
1 (Type/Class)What4.Partial
2 (Data Constructor)What4.Partial
partialValueWhat4.Partial
PartialWithErrWhat4.Partial
partitionByPredsWhat4.LabeledPred
partitionByPredsMWhat4.LabeledPred
partitionLabeledPredsWhat4.LabeledPred
PEWhat4.Partial
PiWhat4.Expr.App, What4.Expr.Builder, What4.Expr
plFunctionWhat4.ProgramLoc
plSourceLocWhat4.ProgramLoc
plusAssocWhat4.BaseTypes, What4.Interface
plusCommWhat4.BaseTypes, What4.Interface
plusMinusCancelWhat4.BaseTypes, What4.Interface
pmember 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain.XOR
PolarityWhat4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification
pop 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.Online, What4.Solver.Yices
popcntWhat4.Utils.BVDomain
popCommandWhat4.Protocol.SMTWriter
popEntryStackWhat4.Protocol.SMTWriter
popEntryStackToTopWhat4.Protocol.SMTWriter
popManyCommandsWhat4.Protocol.SMTWriter
posWhat4.ProgramLoc
Posd 
1 (Type/Class)What4.ProgramLoc
2 (Data Constructor)What4.ProgramLoc
PositionWhat4.ProgramLoc
PositiveWhat4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification
pos_valWhat4.ProgramLoc
ppApp'What4.Expr.App
ppBoundVarWhat4.Expr.App, What4.Expr.Builder
ppConcreteWhat4.Concrete
PPExprWhat4.Expr.App
ppExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
ppExpr'What4.Expr.App
ppExprDocWhat4.Expr.App
ppExprLengthWhat4.Expr.App
PPExprOpts 
1 (Type/Class)What4.Expr.App
2 (Data Constructor)What4.Expr.App
ppExprTopWhat4.Expr.App, What4.Expr.Builder
ppExpr_maxWidthWhat4.Expr.App
ppExpr_useDecimalWhat4.Expr.App
PPIndexWhat4.Expr.App
ppMatlabSolverFnWhat4.Expr.MATLAB
ppNoFileNameWhat4.ProgramLoc
ppNonceAppWhat4.Expr.App
ppSolverSymbolErrorWhat4.Symbol
ppSolverVersionCheckErrorWhat4.Protocol.SMTLib2
ppSolverVersionErrorWhat4.Protocol.SMTLib2
ppVarWhat4.Expr.App
ppVarTypeCodeWhat4.Expr.App
Prec128What4.BaseTypes, What4.Interface
Prec16What4.BaseTypes, What4.Interface
Prec32What4.BaseTypes, What4.Interface
Prec64What4.BaseTypes, What4.Interface
Prec80What4.BaseTypes, What4.Interface
precise_overlapWhat4.Utils.BVDomain
precisionBitsWhat4.SFloat
preConditionTest.Verification
PredWhat4.Interface
predicateVarInfoWhat4.Expr.VarIdentification
predNatWhat4.BaseTypes, What4.Interface
predToBVWhat4.Interface
PredToBVFnWhat4.Expr.MATLAB
PredToIntegerFnWhat4.Expr.MATLAB
predToRealWhat4.Interface
PrettyAppWhat4.Expr.App
prettyAppWhat4.Expr.App
PrettyArg 
1 (Type/Class)What4.Expr.App
2 (Data Constructor)What4.Expr.App
PrettyFuncWhat4.Expr.App
PrettyTextWhat4.Expr.App
PrimArrayTypeMapWhat4.Protocol.SMTWriter
printSymExprWhat4.Interface
printSymNatWhat4.Interface
ProblemFeaturesWhat4.ProblemFeatures
problemFeaturesWhat4.Expr.VarIdentification
prodAbsValueWhat4.Expr.WeightedSum
prodContainsWhat4.Expr.WeightedSum
prodEvalWhat4.Expr.WeightedSum
prodEvalMWhat4.Expr.WeightedSum
prodMulWhat4.Expr.WeightedSum
prodReprWhat4.Expr.WeightedSum
prodVarWhat4.Expr.WeightedSum
ProgramLocWhat4.ProgramLoc
programLocWhat4.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
PropertyTest.Verification
propertyTest.Verification
push 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.Online, What4.Solver.Yices
pushCommandWhat4.Protocol.SMTWriter
pushEntryStackWhat4.Protocol.SMTWriter
qf_bvWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
QuadFloatWhat4.InterpretedFloatingPoint
QuadFloatReprWhat4.InterpretedFloatingPoint
quantAbsEvalWhat4.Expr.App
QuantifierInfoWhat4.Expr.VarIdentification
QuantifierInfoMapWhat4.Expr.VarIdentification
QuantifierTheoryWhat4.Expr.AppTheory, What4.Expr
QuantifierVarKindWhat4.Expr.App, What4.Expr.Builder, What4.Expr
quantTheoryWhat4.Expr.AppTheory, What4.Expr
queryErrorBehaviorWhat4.Protocol.SMTLib2
range 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain.XOR
4 (Function)What4.Utils.BVDomain
rangeCheckEqWhat4.Utils.AbstractDomains
rangeCheckLeWhat4.Utils.AbstractDomains
rangeHiBoundWhat4.Utils.AbstractDomains
rangeLowBoundWhat4.Utils.AbstractDomains
rangeMaxWhat4.Utils.AbstractDomains
rangeMinWhat4.Utils.AbstractDomains
rangeScalarMulWhat4.Utils.AbstractDomains
rationalAsIntegerWhat4.Interface
rationalBoundsWhat4.Interface
rationalTermWhat4.Protocol.SMTWriter
RatPPIndexWhat4.Expr.App
RatTermWhat4.Protocol.SMTLib2.Parse
RAVWhat4.Utils.AbstractDomains
ravAddWhat4.Utils.AbstractDomains
ravCheckEqWhat4.Utils.AbstractDomains
ravCheckLeWhat4.Utils.AbstractDomains
ravConcreteRangeWhat4.Utils.AbstractDomains
ravIsIntegerWhat4.Utils.AbstractDomains
ravJoinWhat4.Utils.AbstractDomains
ravMulWhat4.Utils.AbstractDomains
ravRangeWhat4.Utils.AbstractDomains
ravScalarMulWhat4.Utils.AbstractDomains
ravSingleWhat4.Utils.AbstractDomains
ravUnboundedWhat4.Utils.AbstractDomains
readAllLinesWhat4.Utils.HandleReader
readCheckSatResponseWhat4.Protocol.SMTLib2.Parse
readDecimalWhat4.Protocol.ReadDecimal
readGetModelResponseWhat4.Protocol.SMTLib2.Parse
readNextLineWhat4.Utils.HandleReader
RealWhat4.Protocol.SMTLib2.Parse
realAbsWhat4.Interface
RealAbstractValueWhat4.Utils.AbstractDomains
realAddWhat4.Interface
RealATan2What4.Expr.App, What4.Expr.Builder, What4.Expr
realATan2What4.Protocol.SMTWriter
realAtan2What4.Interface
realCeilWhat4.Interface
RealCosWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realCos 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
RealCosFnWhat4.Expr.MATLAB
RealCoshWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realCosh 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
RealDivWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realDiv 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
realEqWhat4.Interface
RealExpWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realExp 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
RealExprWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realExprAsIntegerWhat4.Interface
realFloorWhat4.Interface
realGeWhat4.Interface
realGtWhat4.Interface
realHypotWhat4.Interface
RealIsIntegerWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realIsIntegerWhat4.Protocol.SMTWriter
realIsNonNegWhat4.Interface
RealIsNonZeroFnWhat4.Expr.MATLAB
realIteWhat4.Interface
realLeWhat4.Interface
realLitWhat4.Interface
RealLogWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realLog 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
realLtWhat4.Interface
realMaxWhat4.Interface
realMinWhat4.Interface
realModWhat4.Interface
realMulWhat4.Interface
realNeWhat4.Interface
realNegWhat4.Interface
realOptStyWhat4.Config
RealPartWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realPartWhat4.Utils.Complex
RealPartOfCplxFnWhat4.Expr.MATLAB
realPiWhat4.Interface
realRoundWhat4.Interface
realRoundEvenWhat4.Interface
RealSeqFnWhat4.Expr.MATLAB
RealSinWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realSin 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
RealSinFnWhat4.Expr.MATLAB
RealSinhWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realSinh 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
realSortWhat4.Protocol.SMTLib2.Syntax
realSqWhat4.Interface
RealSqrtWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realSqrtWhat4.Interface
realSubWhat4.Interface
realSumWhat4.Expr.Builder
realTanWhat4.Interface
realTanhWhat4.Interface
realToBVWhat4.Interface
RealToComplexFnWhat4.Expr.MATLAB
RealToFloatWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realToFloat 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
RealToIntegerWhat4.Expr.App, What4.Expr.Builder, What4.Expr
realToIntegerWhat4.Interface
RealToIntegerFnWhat4.Expr.MATLAB
realToNatWhat4.Interface
realToSBVWhat4.Interface
RealToSBVFnWhat4.Expr.MATLAB
RealToUBVFnWhat4.Expr.MATLAB
realTruncWhat4.Interface
RealTypeMapWhat4.Protocol.SMTWriter
realWithMaxOptStyWhat4.Config
realWithMinOptStyWhat4.Config
realWithRangeOptStyWhat4.Config
RealWorldWhat4.Utils.MonadST
realZeroWhat4.Interface
recommendedWhat4.Utils.Versions
recordExprVarsWhat4.Expr.VarIdentification
reduceAppWhat4.Expr.App
reduceIntSumModWhat4.Expr.WeightedSum
ReflWhat4.BaseTypes, What4.Interface
removeVarWhat4.Expr.BoolMap
renderTermWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
resetWhat4.Protocol.Online
resetAssertionsWhat4.Protocol.SMTLib2.Syntax
resetCommandWhat4.Protocol.SMTWriter
resetDeclaredStructsWhat4.Protocol.SMTWriter
resetEntryStackWhat4.Protocol.SMTWriter
resolveSolverPathWhat4.Utils.Process
returnMaybeWhat4.Partial
returnPartialWhat4.Partial
returnUnassignedWhat4.Partial
reversePolaritiesWhat4.Expr.BoolMap
RNAWhat4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RNEWhat4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
rol 
1 (Function)What4.Utils.BVDomain.Bitwise
2 (Function)What4.Utils.BVDomain
RootWhat4.Protocol.PolyRoot
ror 
1 (Function)What4.Utils.BVDomain.Bitwise
2 (Function)What4.Utils.BVDomain
rotateDocWhat4.Protocol.VerilogWriter.ABCVerilog
rotateLeftWhat4.Utils.Arithmetic
rotateRightWhat4.Utils.Arithmetic
roundAwayWhat4.Utils.Arithmetic
RoundEvenRealWhat4.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
RoundRealWhat4.Expr.App, What4.Expr.Builder, What4.Expr
RTNWhat4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RTPWhat4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
RTZWhat4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter
runAckActionWhat4.Protocol.SMTWriter
runBoolectorInOverrideWhat4.Solver.Boolector, What4.Solver
runCheckSatWhat4.Protocol.SMTLib2
runCVC4InOverrideWhat4.Solver.CVC4, What4.Solver
runDRealInOverrideWhat4.Solver.DReal, What4.Solver
runExternalABCInOverrideWhat4.Solver.ExternalABC, What4.Solver
runInSandboxWhat4.Protocol.SMTWriter
runPartialTWhat4.Partial
runSolverInOverrideWhat4.Protocol.SMTLib2
runSTPInOverrideWhat4.Solver.STP, What4.Solver
runVerilogMWhat4.Protocol.VerilogWriter.AST
runYicesInOverrideWhat4.Solver.Yices, What4.Solver
runZ3InOverrideWhat4.Solver.Z3, What4.Solver
safeSymbolWhat4.Symbol, What4.Interface
sameTermWhat4.Expr.App
SAppWhat4.Protocol.SExp
SatWhat4.SatResult, What4.Solver
SAtomWhat4.Protocol.SExp
satQueryErrorWhat4.Interface
satQueryReasonWhat4.Interface
satQueryResultWhat4.Interface
satQuerySolverNameWhat4.Interface
SatResponseWhat4.Protocol.SMTLib2.Parse
SatResultWhat4.SatResult, What4.Solver
sbBVDomainRangeLimitWhat4.Expr.Builder
sbCacheStartSizeWhat4.Expr.Builder
sbMakeExprWhat4.Expr.Builder
sbNonceExprWhat4.Expr.Builder
sbounds 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
sbUnaryThresholdWhat4.Expr.Builder
sbUserStateWhat4.Expr.Builder
SBVToFloatWhat4.Expr.App, What4.Expr.Builder, What4.Expr
sbvToFloat 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
SBVToIntegerWhat4.Expr.App, What4.Expr.Builder, What4.Expr
sbvToInteger 
1 (Function)What4.Interface
2 (Function)What4.SWord
SBVToIntegerFnWhat4.Expr.MATLAB
sbvToRealWhat4.Interface
scalarMulWhat4.Expr.Builder
scale 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
3 (Function)What4.Expr.WeightedSum
scaledVarWhat4.Expr.WeightedSum
scalMultWhat4.Protocol.VerilogWriter.AST
sciLitWhat4.Interface
ScopeWhat4.Expr.VarIdentification
sdiv 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
select 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Utils.BVDomain.Arith
3 (Function)What4.Utils.BVDomain.Bitwise
4 (Function)What4.Utils.BVDomain
SelectArrayWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingWhat4.SemiRing, What4.Expr
SemiRingBaseWhat4.SemiRing
semiRingBaseWhat4.SemiRing
SemiRingBVWhat4.SemiRing
SemiRingBVReprWhat4.SemiRing, What4.Expr
SemiRingIntegerWhat4.SemiRing
SemiRingIntegerReprWhat4.SemiRing, What4.Expr
SemiRingLeWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingLiteralWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingProdWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingProductWhat4.Expr.WeightedSum
SemiRingRealWhat4.SemiRing
SemiRingRealReprWhat4.SemiRing, What4.Expr
SemiRingReprWhat4.SemiRing, What4.Expr
SemiRingSumWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SemiRingViewWhat4.Expr.App
sendCheckWhat4.Solver.Yices
sendCheckExistsForallWhat4.Solver.Yices
Session 
1 (Type/Class)What4.Protocol.SMTLib2
2 (Data Constructor)What4.Protocol.SMTLib2
sessionResponseWhat4.Protocol.SMTLib2
sessionWriterWhat4.Protocol.SMTLib2
setCurrentProgramLocWhat4.Interface
setDefaultLogicAndOptionsWhat4.Protocol.SMTLib2
setLogic 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
setOptWhat4.Config
setOptCommandWhat4.Protocol.SMTWriter
setOption 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Config
3 (Function)What4.Protocol.SMTLib2
setParamWhat4.Solver.Yices
setProduceModels 
1 (Function)What4.Protocol.SMTLib2.Syntax
2 (Function)What4.Protocol.SMTLib2
setSolverLogListenerWhat4.Interface
setYicesParamsWhat4.Solver.Yices
set_opt_defaultWhat4.Config
set_opt_onsetWhat4.Config
SExpWhat4.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
SFloatBinArithWhat4.SFloat
SFloatRelWhat4.SFloat
shl 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
shouldUnfoldWhat4.Interface
showPrettyArgWhat4.Expr.App
shutdownSolverWhat4.Protocol.SMTLib2
shutdownSolverProcessWhat4.Protocol.Online
signedWhat4.Protocol.VerilogWriter.AST
signedBVBounds 
1 (Function)What4.Interface
2 (Function)What4.SWord
signedClampWhat4.BaseTypes, What4.Interface
signedWideMultiplyBVWhat4.Interface
SimpleWordMapWhat4.WordMap
simplifyWhat4.Expr.Simplify
SingleFloatWhat4.InterpretedFloatingPoint
SingleFloatReprWhat4.InterpretedFloatingPoint
SingleRangeWhat4.Utils.AbstractDomains, What4.Interface
singleRangeWhat4.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
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
skipSpaceOrNewlineWhat4.Protocol.SExp
slt 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
3 (Function)What4.Expr.UnaryBV
smokeTestWhat4.Solver.Adapter, What4.Solver
smtAckResultWhat4.Protocol.SMTLib2
smtEvalBoolWhat4.Protocol.SMTWriter
smtEvalBVWhat4.Protocol.SMTWriter
smtEvalBvArrayWhat4.Protocol.SMTWriter
SMTEvalBVArrayFnWhat4.Protocol.SMTWriter
SMTEvalBVArrayWrapper 
1 (Type/Class)What4.Protocol.SMTWriter
2 (Data Constructor)What4.Protocol.SMTWriter
smtEvalFloatWhat4.Protocol.SMTWriter
SMTEvalFunctions 
1 (Type/Class)What4.Protocol.SMTWriter
2 (Data Constructor)What4.Protocol.SMTWriter
smtEvalFunsWhat4.Protocol.SMTWriter
smtEvalRealWhat4.Protocol.SMTWriter
smtEvalStringWhat4.Protocol.SMTWriter
smtExprGroundEvalFnWhat4.Protocol.SMTWriter
smtFnAppWhat4.Protocol.SMTWriter
smtFnUpdateWhat4.Protocol.SMTWriter
SMTInfoFlagWhat4.Protocol.SMTLib2.Syntax
smtlib2arrayConstantWhat4.Protocol.SMTLib2
smtlib2arraySelectWhat4.Protocol.SMTLib2
smtlib2arrayTypeWhat4.Protocol.SMTLib2
smtlib2arrayUpdateWhat4.Protocol.SMTLib2
smtlib2declareStructCmdWhat4.Protocol.SMTLib2
SMTLib2ErrorWhat4.Protocol.SMTLib2
SMTLib2ExceptionWhat4.Protocol.SMTLib2
smtlib2exitCommandWhat4.Protocol.SMTLib2
SMTLib2GenericSolverWhat4.Protocol.SMTLib2
SMTLib2ParseErrorWhat4.Protocol.SMTLib2
smtlib2StringAppendWhat4.Protocol.SMTLib2
smtlib2StringContainsWhat4.Protocol.SMTLib2
smtlib2StringIndexOfWhat4.Protocol.SMTLib2
smtlib2StringIsPrefixOfWhat4.Protocol.SMTLib2
smtlib2StringIsSuffixOfWhat4.Protocol.SMTLib2
smtlib2StringLengthWhat4.Protocol.SMTLib2
smtlib2StringSortWhat4.Protocol.SMTLib2
smtlib2StringSubstringWhat4.Protocol.SMTLib2
smtlib2StringTermWhat4.Protocol.SMTLib2
smtlib2StructCtorWhat4.Protocol.SMTLib2
smtlib2StructProjWhat4.Protocol.SMTLib2
smtlib2StructSortWhat4.Protocol.SMTLib2
SMTLib2TweaksWhat4.Protocol.SMTLib2
smtlib2tweaksWhat4.Protocol.SMTLib2
SMTLib2UnsupportedWhat4.Protocol.SMTLib2
smtLibEvalFunsWhat4.Protocol.SMTLib2
SMTReadWriterWhat4.Protocol.SMTWriter
smtSatResultWhat4.Protocol.SMTWriter
smtUnsatAssumptionsResultWhat4.Protocol.SMTWriter
smtUnsatCoreResultWhat4.Protocol.SMTWriter
SMTWriterWhat4.Protocol.SMTWriter
smtWriterNameWhat4.Protocol.SMTWriter
SolverAdapter 
1 (Type/Class)What4.Solver.Adapter, What4.Solver
2 (Data Constructor)What4.Solver.Adapter, What4.Solver
solverAdapterOptionsWhat4.Solver.Adapter, What4.Solver
SolverBounds 
1 (Type/Class)What4.Utils.Versions
2 (Data Constructor)What4.Utils.Versions
solverCleanupCallbackWhat4.Protocol.Online
solverConnWhat4.Protocol.Online
solverEarlyUnsatWhat4.Protocol.Online
SolverEndSATQueryWhat4.Interface
solverErrorBehaviorWhat4.Protocol.Online
solverEvalFunsWhat4.Protocol.Online
SolverEventWhat4.Interface
SolverGoalTimeout 
1 (Type/Class)What4.Protocol.Online
2 (Data Constructor)What4.Protocol.Online
solverGoalTimeoutWhat4.Protocol.Online
solverHandleWhat4.Protocol.Online
solverLogFnWhat4.Protocol.Online
solverNameWhat4.Protocol.Online
SolverProcess 
1 (Type/Class)What4.Protocol.Online
2 (Data Constructor)What4.Protocol.Online
solverResponseWhat4.Protocol.Online
SolverStartSATQueryWhat4.Interface
solverStderrWhat4.Protocol.Online
solverStdinWhat4.Protocol.Online
solverSupportsResetAssertionsWhat4.Protocol.Online
SolverSymbolWhat4.Symbol, What4.Interface
solverSymbolAsTextWhat4.Symbol
SolverSymbolErrorWhat4.Symbol
solver_adapter_check_satWhat4.Solver.Adapter, What4.Solver
solver_adapter_config_optionsWhat4.Solver.Adapter, What4.Solver
solver_adapter_nameWhat4.Solver.Adapter, What4.Solver
solver_adapter_write_smt2What4.Solver.Adapter, What4.Solver
SomeWhat4.BaseTypes, What4.Interface
someNatWhat4.BaseTypes, What4.Interface
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
SourcePosWhat4.ProgramLoc
sourcePosWhat4.ProgramLoc
splitEntryWhat4.Utils.LeqMap
splitLeqWhat4.Utils.LeqMap
SplitPPExprListWhat4.Expr.App
srem 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
sr_compareWhat4.SemiRing
SR_ConstantWhat4.Expr.App
SR_GeneralWhat4.Expr.App
sr_hashWithSaltWhat4.SemiRing
SR_ProdWhat4.Expr.App
SR_SumWhat4.Expr.App
SStringWhat4.Protocol.SExp
STWhat4.Utils.MonadST
startCachingWhat4.Expr.Builder
startFunctionNameWhat4.FunctionName
startHandleReaderWhat4.Utils.HandleReader, What4.Solver.Yices
startOfFileWhat4.ProgramLoc
startProcessWhat4.Utils.Process
startSolverWhat4.Protocol.SMTLib2
startSolverProcessWhat4.Protocol.Online
statAllocsWhat4.Interface
Statistics 
1 (Type/Class)What4.Interface
2 (Data Constructor)What4.Interface
statNonLinearOpsWhat4.Interface
stopCachingWhat4.Expr.Builder
stopHandleReaderWhat4.Utils.HandleReader
storeWhat4.Protocol.SMTLib2.Syntax
StoreTermWhat4.Protocol.SMTLib2.Parse
STP 
1 (Type/Class)What4.Solver.STP, What4.Solver
2 (Data Constructor)What4.Solver.STP, What4.Solver
stpAdapterWhat4.Solver.STP, What4.Solver
stpFeaturesWhat4.Solver.STP, What4.Solver
stpOptionsWhat4.Solver.STP, What4.Solver
stpPathWhat4.Solver.STP, What4.Solver
streamLinesWhat4.Utils.HandleReader
StringAbsWhat4.Utils.AbstractDomains
stringAbsConcatWhat4.Utils.AbstractDomains
stringAbsContainsWhat4.Utils.AbstractDomains
stringAbsEmptyWhat4.Utils.AbstractDomains
stringAbsIndexOfWhat4.Utils.AbstractDomains
stringAbsIsPrefixOfWhat4.Utils.AbstractDomains
stringAbsIsSuffixOfWhat4.Utils.AbstractDomains
stringAbsJoinWhat4.Utils.AbstractDomains
stringAbsLengthWhat4.Utils.AbstractDomains
stringAbsOverlapWhat4.Utils.AbstractDomains
stringAbsSingleWhat4.Utils.AbstractDomains
stringAbsSubstringWhat4.Utils.AbstractDomains
stringAbsTopWhat4.Utils.AbstractDomains
StringAbstractValueWhat4.Utils.AbstractDomains
StringAppendWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringAppendWhat4.Protocol.SMTWriter
stringConcatWhat4.Interface
StringContainsWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringContains 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
stringEmptyWhat4.Interface
stringEqWhat4.Interface
StringExpr 
1 (Type/Class)What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Data Constructor)What4.Expr.App, What4.Expr.Builder, What4.Expr
StringIndexOfWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringIndexOf 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
StringInfoWhat4.BaseTypes, What4.Interface
stringInfoWhat4.Interface
StringInfoReprWhat4.BaseTypes, What4.Interface
StringIsPrefixOfWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringIsPrefixOf 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
StringIsSuffixOfWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringIsSuffixOf 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
stringIteWhat4.Interface
StringLengthWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringLength 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
stringLitWhat4.Interface
stringLitBoundsWhat4.Utils.StringLiteral
stringLitContainsWhat4.Utils.StringLiteral
stringLitEmptyWhat4.Utils.StringLiteral
StringLiteralWhat4.Utils.StringLiteral, What4.Interface
stringLiteralInfoWhat4.Utils.StringLiteral, What4.Interface
stringLitIndexOfWhat4.Utils.StringLiteral
stringLitIsPrefixOfWhat4.Utils.StringLiteral
stringLitIsSuffixOfWhat4.Utils.StringLiteral
stringLitLengthWhat4.Utils.StringLiteral
stringLitNullWhat4.Utils.StringLiteral
stringLitSubstringWhat4.Utils.StringLiteral
stringOptStyWhat4.Config
stringPPExprWhat4.Expr.App
stringPrettyArgWhat4.Expr.App
StringSeqWhat4.Expr.StringSeq
stringSeqAbsWhat4.Expr.StringSeq
StringSeqEntryWhat4.Expr.StringSeq
StringSeqLiteralWhat4.Expr.StringSeq
StringSeqTermWhat4.Expr.StringSeq
StringSubstringWhat4.Expr.App, What4.Expr.Builder, What4.Expr
stringSubstring 
1 (Function)What4.Interface
2 (Function)What4.Protocol.SMTWriter
stringTermWhat4.Protocol.SMTWriter
StringTheoryWhat4.Expr.AppTheory, What4.Expr
stringToSExpWhat4.Protocol.SExp
StructCtorWhat4.Expr.App, What4.Expr.Builder, What4.Expr
structCtorWhat4.Protocol.SMTWriter
structEqWhat4.Interface
StructFieldWhat4.Expr.App, What4.Expr.Builder, What4.Expr
structFieldWhat4.Interface
structIteWhat4.Interface
structProjWhat4.Protocol.SMTWriter
StructTheoryWhat4.Expr.AppTheory, What4.Expr
StructTypeMapWhat4.Protocol.SMTWriter
subWhat4.Protocol.SMTLib2.Syntax
subNatWhat4.BaseTypes, What4.Interface
subSignedOFWhat4.Interface
subUnsignedOFWhat4.Interface
sumAbsValueWhat4.Expr.WeightedSum
sumExprWhat4.Protocol.SMTWriter
sumOffsetWhat4.Expr.WeightedSum
sumReprWhat4.Expr.WeightedSum
supportedFeaturesWhat4.Protocol.SMTWriter, What4.Protocol.SMTLib2
supportFunctionArgumentsWhat4.Protocol.SMTWriter
supportFunctionDefsWhat4.Protocol.SMTWriter
supportQuantifiersWhat4.Protocol.SMTWriter
supportsResetAssertionsWhat4.Protocol.SMTLib2
SupportTermOpsWhat4.Protocol.SMTWriter
SWordWhat4.SWord
SymAnnotationWhat4.Interface
SymArrayWhat4.Interface
Symbol 
1 (Type/Class)What4.Protocol.SMTLib2.Parse
2 (Type/Class)What4.Protocol.SMTLib2.Syntax
SymbolBindingWhat4.Expr.Builder
SymbolTermWhat4.Protocol.SMTLib2.Parse
SymbolVarBimapWhat4.Expr.Builder
SymBVWhat4.Interface
SymCplxWhat4.Interface
SymEncoder 
1 (Type/Class)What4.Interface
2 (Data Constructor)What4.Interface
symEncoderTypeWhat4.Interface
SymExprWhat4.Interface, What4.Expr.Builder
SymFloatWhat4.Interface
SymFnWhat4.Interface
symFnArgTypesWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFnIdWhat4.Expr.App, What4.Expr.Builder, What4.Expr
SymFnInfoWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFnInfoWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFnLocWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFnNameWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFnReturnTypeWhat4.Expr.App, What4.Expr.Builder, What4.Expr
symFromExprWhat4.Interface
SymIntegerWhat4.Interface
SymInterpretedFloatWhat4.InterpretedFloatingPoint
SymInterpretedFloatTypeWhat4.InterpretedFloatingPoint
SymNatWhat4.Interface
SymRealWhat4.Interface
SymStringWhat4.Interface
SymStructWhat4.Interface
symToExprWhat4.Interface
sym_evaluateWhat4.Expr.UnaryBV
systemSymbolWhat4.Symbol
TWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
takeWhat4.Utils.Word16String
teeInputStreamWhat4.Utils.HandleReader
teeOutputStreamWhat4.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
termIntegerToRealWhat4.Protocol.SMTWriter
termRealToIntegerWhat4.Protocol.SMTWriter
term_appWhat4.Protocol.SMTLib2.Syntax
testBit 
1 (Function)What4.Utils.BVDomain.Bitwise
2 (Function)What4.Utils.BVDomain
testBitBVWhat4.Interface
TestEqualityWhat4.BaseTypes, What4.Interface
testEqualityWhat4.BaseTypes, What4.Interface
testExprSymFnEqWhat4.Expr.App
testLeqWhat4.BaseTypes, What4.Interface
testNatCasesWhat4.BaseTypes, What4.Interface
testSolverFnEqWhat4.Expr.MATLAB
testStrictLeqWhat4.BaseTypes, What4.Interface
textPPExprWhat4.Expr.App
TmWhat4.Expr.WeightedSum
toBaseTypeReprWhat4.Utils.OnlyIntRepr
toDescListWhat4.Utils.LeqMap
toIncrHashWhat4.Utils.IncrHash
toIncrHashWithSaltWhat4.Utils.IncrHash
toIntWhat4.Protocol.SMTLib2.Syntax
toLEByteStringWhat4.Utils.Word16String
toList 
1 (Function)What4.Utils.AnnotatedMap
2 (Function)What4.Utils.LeqMap
3 (Function)What4.Expr.ArrayUpdateMap
4 (Function)What4.Expr.StringSeq
toMapWhat4.Expr.ArrayUpdateMap
toNativePropertyTest.Verification
toRealWhat4.Protocol.SMTLib2.Syntax
toRoundModeWhat4.Utils.FloatHelpers
toSignedWhat4.BaseTypes, What4.Interface
toUnsignedWhat4.BaseTypes, What4.Interface
transformSumWhat4.Expr.WeightedSum
traverseAppWhat4.Expr.App, What4.Expr.Builder
traverseArrayResultWrapperWhat4.Expr.App
traverseArrayResultWrapperAssignmentWhat4.Expr.App
traverseArrayUpdateMapWhat4.Expr.ArrayUpdateMap
traverseBVOrSetWhat4.Expr.App, What4.Expr.Builder
traverseCoeffsWhat4.Expr.WeightedSum
traverseMatlabSolverFnWhat4.Expr.MATLAB
traverseMaybeWithKeyWhat4.Utils.AnnotatedMap
traversePredsWhat4.Expr.UnaryBV
traverseProdVarsWhat4.Expr.WeightedSum
traverseSatResultWhat4.SatResult, What4.Solver
traverseStringSeqWhat4.Expr.StringSeq
traverseVars 
1 (Function)What4.Expr.BoolMap
2 (Function)What4.Expr.WeightedSum
trueWhat4.Protocol.SMTLib2.Syntax
truePredWhat4.Interface
truncWhat4.Expr.UnaryBV
tryComplexSqrtWhat4.Utils.Complex
tryEvalGroundExprWhat4.Expr.GroundEval
tryIntSqrtWhat4.Utils.Arithmetic
tryMagnitudeWhat4.Utils.Complex
tryRationalSqrtWhat4.Utils.Arithmetic
trySetOptWhat4.Config
typeDocWhat4.Protocol.VerilogWriter.ABCVerilog
TypeMapWhat4.Protocol.SMTWriter
typeMapWhat4.Protocol.SMTWriter
typeTheoryWhat4.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
uextWhat4.Expr.UnaryBV
uintSetWidthWhat4.Interface
UIntSetWidthFnWhat4.Expr.MATLAB
uintToIntWhat4.Interface
UIntToIntFnWhat4.Expr.MATLAB
uintToRealWhat4.Interface
ult 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
3 (Function)What4.Expr.UnaryBV
UnaryBVWhat4.Expr.UnaryBV, What4.Expr
unaryThresholdOptionWhat4.Expr.Builder
UnassignedWhat4.Partial
Unbounded 
1 (Data Constructor)What4.Utils.AbstractDomains
2 (Data Constructor)What4.Config
unboundedRangeWhat4.Utils.AbstractDomains
unconstrainedAbsValueWhat4.Expr.App
unEvalBVArrayWrapperWhat4.Protocol.SMTWriter
UnfoldConcreteWhat4.Interface
UnfoldPolicyWhat4.Interface
unGVWWhat4.Expr.GroundEval, What4.Expr
UnicodeWhat4.BaseTypes, What4.Interface
UnicodeLiteralWhat4.Utils.StringLiteral, What4.Interface
UnicodeReprWhat4.BaseTypes, What4.Interface
uninterpConstantsWhat4.Expr.VarIdentification
UninterpFnInfoWhat4.Expr.App, What4.Expr.Builder, What4.Expr
UninterpVarKindWhat4.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
unionWithWhat4.Utils.AnnotatedMap
unionWithKeyMaybeWhat4.Utils.AnnotatedMap
UnknownWhat4.SatResult, What4.Solver
UnknownResponseWhat4.Protocol.SMTLib2.Parse
unknownsWhat4.Utils.BVDomain.Arith
Unop 
1 (Data Constructor)What4.Protocol.VerilogWriter.AST
2 (Type/Class)What4.Protocol.VerilogWriter.AST
unopWhat4.Protocol.VerilogWriter.AST
unopDocWhat4.Protocol.VerilogWriter.ABCVerilog
unPartialWhat4.Partial
UnsatWhat4.SatResult, What4.Solver
UnsatResponseWhat4.Protocol.SMTLib2.Parse
unsignedBVBounds 
1 (Function)What4.Interface
2 (Function)What4.SWord
unsignedClampWhat4.BaseTypes, What4.Interface
unsignedEntriesWhat4.Expr.UnaryBV
unsignedRangesWhat4.Expr.UnaryBV
unsignedWideMultiplyBVWhat4.Interface
unSortWhat4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
UnsupportedFloat 
1 (Type/Class)What4.SFloat
2 (Data Constructor)What4.SFloat
unWrapWhat4.Expr.BoolMap
unwrapArrayResultWhat4.Interface, What4.Expr.Builder
unwrapAVWhat4.Utils.AbstractDomains
unwrapCVWhat4.Utils.AbstractDomains
un_appWhat4.Protocol.SMTLib2.Syntax
UpdateArrayWhat4.Expr.App, What4.Expr.Builder, What4.Expr
upperWhat4.Utils.Versions
urem 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain
useBitvectorsWhat4.ProblemFeatures
useComputableRealsWhat4.ProblemFeatures
useExistForallWhat4.ProblemFeatures
useFloatingPointWhat4.ProblemFeatures
useIntegerArithmeticWhat4.ProblemFeatures
useLinearArithmeticWhat4.ProblemFeatures
useNonlinearArithmeticWhat4.ProblemFeatures
useQuantifiersWhat4.ProblemFeatures
userSymbolWhat4.Symbol, What4.Interface
useStringsWhat4.ProblemFeatures
useStructsWhat4.ProblemFeatures
useSymbolicArraysWhat4.ProblemFeatures
useUnsatAssumptionsWhat4.ProblemFeatures
useUnsatCoresWhat4.ProblemFeatures
ValueBoundWhat4.Utils.AbstractDomains
ValueRangeWhat4.Utils.AbstractDomains, What4.Interface
valueRangeWhat4.Utils.AbstractDomains
var 
1 (Function)What4.Expr.BoolMap
2 (Function)What4.Expr.WeightedSum
varErrorsWhat4.Expr.VarIdentification
varExprWhat4.Interface
VarKindWhat4.Expr.App, What4.Expr.Builder, What4.Expr
VarRecorderWhat4.Expr.VarIdentification
varSortWhat4.Protocol.SMTLib2.Syntax
VarSymbolBindingWhat4.Expr.Builder
verWhat4.Utils.Versions
verbosityWhat4.Config
verbosityLoggerWhat4.Config
VerifiableTest.Verification
verifyingTest.Verification
VerilogM 
1 (Type/Class)What4.Protocol.VerilogWriter.AST
2 (Data Constructor)What4.Protocol.VerilogWriter.AST
VersionWhat4.Protocol.SMTLib2.Syntax
versionResultWhat4.Protocol.SMTLib2
viewBoolMapWhat4.Expr.BoolMap
viewSemiRingWhat4.Expr.App
vsBoolCacheWhat4.Protocol.VerilogWriter.AST
vsBVCacheWhat4.Protocol.VerilogWriter.AST
vsExpCacheWhat4.Protocol.VerilogWriter.AST
vsFreshIdentWhat4.Protocol.VerilogWriter.AST
vsInputsWhat4.Protocol.VerilogWriter.AST
vsOutputsWhat4.Protocol.VerilogWriter.AST
vsSymWhat4.Protocol.VerilogWriter.AST
vsWiresWhat4.Protocol.VerilogWriter.AST
WeightedSumWhat4.Expr.WeightedSum, What4.Expr
What4What4.Panic
widthWhat4.Expr.UnaryBV
widthValWhat4.BaseTypes, What4.Interface
WireWhat4.Protocol.VerilogWriter.AST
wireDocWhat4.Protocol.VerilogWriter.ABCVerilog
withAbstractableWhat4.Utils.AbstractDomains
withAddLeqWhat4.BaseTypes, What4.Interface
withAddMulDistribRightWhat4.BaseTypes, What4.Interface
withAddPrefixLeqWhat4.BaseTypes, What4.Interface
withBoolectorWhat4.Solver.Boolector, What4.Solver
withCVC4What4.Solver.CVC4, What4.Solver
withDivModNatWhat4.BaseTypes, What4.Interface
withHandleReaderWhat4.Utils.HandleReader
withKnownNatWhat4.BaseTypes, What4.Interface
withLeqProofWhat4.BaseTypes, What4.Interface
withProcessHandlesWhat4.Utils.Process
withSolverWhat4.Protocol.SMTLib2
withSTPWhat4.Solver.STP, What4.Solver
withSubMulDistribRightWhat4.BaseTypes, What4.Interface
withZ3What4.Solver.Z3, What4.Solver
Word16StringWhat4.Utils.Word16String
WordMapWhat4.WordMap
Wrap 
1 (Type/Class)What4.Expr.BoolMap
2 (Data Constructor)What4.Expr.BoolMap
writeABCSMT2FileWhat4.Solver.ExternalABC, What4.Solver
writeCheckSatWhat4.Protocol.SMTLib2
writeCommandWhat4.Protocol.SMTWriter
writeCVC4SMT2FileWhat4.Solver.CVC4, What4.Solver
writeDefaultSMT2What4.Protocol.SMTLib2
writeDRealSMT2FileWhat4.Solver.DReal, What4.Solver
writeExitWhat4.Protocol.SMTLib2
writeGetValueWhat4.Protocol.SMTLib2
writeMultiAsmpCVC4SMT2FileWhat4.Solver.CVC4
WriterWhat4.Protocol.SMTLib2
WriterConnWhat4.Protocol.SMTWriter, What4.Protocol.SMTLib2
writeYicesFileWhat4.Solver.Yices, What4.Solver
writeZ3SMT2FileWhat4.Solver.Z3
X86_80FloatWhat4.InterpretedFloatingPoint
X86_80FloatReprWhat4.InterpretedFloatingPoint
X86_80Val 
1 (Type/Class)What4.InterpretedFloatingPoint
2 (Data Constructor)What4.InterpretedFloatingPoint
XorWhat4.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
xorPredWhat4.Interface
xorToBitwiseDomainWhat4.Utils.BVDomain
yicesAdapterWhat4.Solver.Yices, What4.Solver
yicesDefaultFeaturesWhat4.Solver.Yices, What4.Solver
yicesEnableInteractiveWhat4.Solver.Yices
yicesEnableMCSatWhat4.Solver.Yices
YicesErrorWhat4.Solver.Yices
yicesEvalBoolWhat4.Solver.Yices
YicesExceptionWhat4.Solver.Yices
yicesGoalTimeoutWhat4.Solver.Yices
yicesOptionsWhat4.Solver.Yices, What4.Solver
YicesParseErrorWhat4.Solver.Yices
yicesPathWhat4.Solver.Yices, What4.Solver
yicesTypeWhat4.Solver.Yices
YicesUnsupportedWhat4.Solver.Yices
Z3 
1 (Type/Class)What4.Solver.Z3, What4.Solver
2 (Data Constructor)What4.Solver.Z3, What4.Solver
z3AdapterWhat4.Solver.Z3, What4.Solver
z3FeaturesWhat4.Solver.Z3, What4.Solver
z3OptionsWhat4.Solver.Z3, What4.Solver
z3PathWhat4.Solver.Z3, What4.Solver
z3TimeoutWhat4.Solver.Z3
ZBVWhat4.SWord
zeroWhat4.SemiRing
ZeroNatWhat4.BaseTypes, What4.Interface
zeroStatisticsWhat4.Interface
zext 
1 (Function)What4.Utils.BVDomain.Arith
2 (Function)What4.Utils.BVDomain.Bitwise
3 (Function)What4.Utils.BVDomain
_labeledPredWhat4.LabeledPred
_labeledPredMsgWhat4.LabeledPred
_partialPredWhat4.Partial
_partialValueWhat4.Partial
_stringAbsLengthWhat4.Utils.AbstractDomains