| * | 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 |
| abcOptions | What4.Solver.ExternalABC, What4.Solver |
| abcPath | What4.Solver.ExternalABC, What4.Solver |
| abs | What4.Protocol.SMTLib2.Syntax |
| absAnd | What4.Utils.AbstractDomains |
| absOr | What4.Utils.AbstractDomains |
| Abstractable | What4.Utils.AbstractDomains |
| abstractEval | What4.Expr.App |
| AbstractValue | What4.Utils.AbstractDomains |
| AbstractValueWrapper | |
| 1 (Type/Class) | What4.Utils.AbstractDomains |
| 2 (Data Constructor) | What4.Utils.AbstractDomains |
| AckAction | What4.Protocol.SMTWriter |
| AcknowledgementAction | What4.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 |
| addCommand | What4.Protocol.SMTWriter, What4.Solver.Yices |
| addCommandNoAck | What4.Protocol.SMTWriter |
| addCommands | What4.Protocol.SMTWriter |
| addCondition | What4.Partial |
| addConstant | What4.Expr.WeightedSum |
| addFreshInput | What4.Protocol.VerilogWriter.AST |
| addFreshWire | What4.Protocol.VerilogWriter.AST |
| addIsLeq | What4.BaseTypes, What4.Interface |
| addIsLeqLeft1 | What4.BaseTypes, What4.Interface |
| addMulDistribRight | What4.BaseTypes, What4.Interface |
| addNat | What4.BaseTypes, What4.Interface |
| addOutput | What4.Protocol.VerilogWriter.AST |
| addPrefixIsLeq | What4.BaseTypes, What4.Interface |
| addRange | What4.Utils.AbstractDomains |
| addSignedOF | What4.Interface |
| addUnsignedOF | What4.Interface |
| addVar | |
| 1 (Function) | What4.Expr.BoolMap |
| 2 (Function) | What4.Expr.WeightedSum |
| addVars | What4.Expr.WeightedSum |
| addWire | What4.Protocol.VerilogWriter.AST |
| allSupported | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| allTrueEntries | What4.Interface |
| all_supported | What4.Protocol.SMTLib2 |
| alter | What4.Utils.AnnotatedMap |
| alterF | What4.Utils.AnnotatedMap |
| AlwaysUnfold | What4.Interface |
| And | What4.Protocol.VerilogWriter.AST |
| and | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| andAll | What4.Protocol.SMTWriter |
| andAllOf | What4.Interface |
| andPred | What4.Interface |
| and_scalar | What4.Utils.BVDomain.XOR |
| AnnotatedMap | What4.Utils.AnnotatedMap |
| annotateTerm | What4.Interface |
| Annotation | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| annotation | What4.Utils.AnnotatedMap |
| AnOnlineSolver | |
| 1 (Type/Class) | What4.Protocol.Online |
| 2 (Data Constructor) | What4.Protocol.Online |
| any | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| APE | What4.Expr.App |
| apeDoc | What4.Expr.App |
| apeExprs | What4.Expr.App |
| apeIndex | What4.Expr.App |
| apeLength | What4.Expr.App |
| apeLoc | What4.Expr.App |
| apeName | What4.Expr.App |
| App | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| app | What4.Protocol.SMTWriter |
| append | |
| 1 (Function) | What4.Utils.Word16String |
| 2 (Function) | What4.Expr.StringSeq |
| appEqF | What4.Expr.App |
| AppExpr | |
| 1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| 2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| appExprAbsValue | What4.Expr.App |
| appExprApp | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| AppExprCtor | What4.Expr.App |
| appExprId | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| appExprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| applySymFn | What4.Interface |
| AppPPExpr | |
| 1 (Data Constructor) | What4.Expr.App |
| 2 (Type/Class) | What4.Expr.App |
| approximate | What4.Protocol.PolyRoot |
| AppTheory | What4.Expr.AppTheory, What4.Expr |
| appTheory | What4.Expr.AppTheory, What4.Expr |
| appType | What4.Expr.App, What4.Expr.Builder |
| app_list | What4.Protocol.SMTWriter |
| arithDomainData | What4.Utils.BVDomain.Arith, What4.Utils.BVDomain |
| arithToXorDomain | What4.Utils.BVDomain |
| Array | What4.Protocol.SMTLib2.Parse |
| ArrayConcrete | What4.Expr.GroundEval, What4.Expr |
| arrayConst | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| arrayConstant | What4.Protocol.SMTWriter |
| ArrayConstantFn | What4.Protocol.SMTWriter |
| arrayEq | What4.Interface |
| ArrayFromFn | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| arrayFromFn | What4.Interface |
| arrayFromMap | What4.Interface |
| arrayIte | What4.Interface |
| arrayLookup | What4.Interface |
| ArrayMap | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| arrayMap | What4.Interface |
| ArrayMapping | What4.Expr.GroundEval, What4.Expr |
| 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 |
| arraySort | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| arrayStore | What4.Protocol.SMTLib2 |
| ArrayTheory | What4.Expr.AppTheory, What4.Expr |
| ArrayTrueOnEntries | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| arrayTrueOnEntries | What4.Interface |
| arrayTypeIndices | What4.BaseTypes, What4.Interface |
| arrayTypeResult | What4.BaseTypes, What4.Interface |
| arrayUpdate | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| arrayUpdateAbs | What4.Expr.ArrayUpdateMap |
| arrayUpdateAtIdxLits | What4.Interface |
| ArrayUpdateMap | What4.Expr.ArrayUpdateMap |
| asAffineVar | |
| 1 (Function) | What4.Expr.WeightedSum |
| 2 (Function) | What4.Interface |
| asApp | What4.Expr.App, What4.Expr.Builder |
| asArithDomain | What4.Utils.BVDomain |
| asAtomList | What4.Protocol.SExp |
| asBitwiseDomain | What4.Utils.BVDomain |
| asBV | What4.Interface |
| asComplex | What4.Interface |
| asConcrete | What4.Interface |
| asConjunction | What4.Expr.App, What4.Expr.Builder |
| AsConst | What4.Protocol.SMTLib2.Parse |
| asConstant | |
| 1 (Function) | What4.Expr.WeightedSum |
| 2 (Function) | What4.Expr.UnaryBV |
| asConstantArray | What4.Interface |
| asConstantPred | What4.Interface |
| asDisjunction | What4.Expr.App, What4.Expr.Builder |
| asFloat | What4.Interface |
| ashr | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| asInteger | What4.Interface |
| asMatlabSolverFn | What4.Expr.App |
| asNat | What4.Interface |
| asNegAtom | What4.Expr.App |
| asNegAtomList | What4.Protocol.SExp |
| asNonceApp | What4.Expr.App, What4.Expr.Builder |
| asPosAtom | What4.Expr.App |
| asProdVar | What4.Expr.WeightedSum |
| asRational | What4.Interface |
| asSemiRingLit | What4.Expr.App |
| asSemiRingProd | What4.Expr.App |
| asSemiRingSum | What4.Expr.App |
| assert | What4.Protocol.SMTLib2.Syntax |
| assertCommand | What4.Protocol.SMTWriter |
| assertForall | What4.Solver.Yices |
| assertNamed | What4.Protocol.SMTLib2.Syntax |
| assertNamedCommand | What4.Protocol.SMTWriter |
| Assign | What4.Protocol.VerilogWriter.AST |
| asSingleRange | What4.Utils.AbstractDomains |
| asSingleton | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| asSMT2Type | What4.Protocol.SMTLib2 |
| asString | What4.Interface |
| asStruct | What4.Interface |
| assume | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2, What4.Solver.Yices |
| assumedProp | Test.Verification |
| assumeFormula | What4.Protocol.SMTWriter |
| assumeFormulaWithFreshName | What4.Protocol.SMTWriter |
| assumeFormulaWithName | What4.Protocol.SMTWriter |
| Assuming | Test.Verification |
| assuming | Test.Verification |
| Assumption | Test.Verification |
| AssumptionProp | Test.Verification |
| asVar | What4.Expr.WeightedSum |
| asWeightedSum | What4.Expr.App |
| asWeightedVar | What4.Expr.WeightedSum |
| asXorDomain | What4.Utils.BVDomain |
| avCheckEq | What4.Utils.AbstractDomains |
| avContains | What4.Utils.AbstractDomains |
| avJoin | What4.Utils.AbstractDomains |
| avOverlap | What4.Utils.AbstractDomains |
| avSingle | What4.Utils.AbstractDomains |
| avTop | What4.Utils.AbstractDomains |
| backendPred | What4.Interface |
| BaseArrayRepr | What4.BaseTypes, What4.Interface |
| BaseArrayType | What4.BaseTypes, What4.Interface |
| BaseBoolRepr | What4.BaseTypes, What4.Interface |
| BaseBoolType | What4.BaseTypes, What4.Interface |
| BaseBVRepr | What4.BaseTypes, What4.Interface |
| BaseBVType | What4.BaseTypes, What4.Interface |
| BaseComplexRepr | What4.BaseTypes, What4.Interface |
| BaseComplexType | What4.BaseTypes, What4.Interface |
| baseDefaultValue | What4.Interface |
| BaseEq | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| BaseFloatRepr | What4.BaseTypes, What4.Interface |
| BaseFloatType | What4.BaseTypes, What4.Interface |
| BaseIntegerRepr | What4.BaseTypes, What4.Interface |
| BaseIntegerType | What4.BaseTypes, What4.Interface |
| baseIsConcrete | What4.Interface |
| BaseIte | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| BaseRealRepr | What4.BaseTypes, What4.Interface |
| BaseRealType | What4.BaseTypes, What4.Interface |
| BaseStringRepr | What4.BaseTypes, What4.Interface |
| BaseStringType | What4.BaseTypes, What4.Interface |
| BaseStructRepr | What4.BaseTypes, What4.Interface |
| BaseStructType | What4.BaseTypes, What4.Interface |
| BaseType | What4.BaseTypes, What4.Interface |
| baseTypeIte | What4.Interface |
| BaseTypeRepr | What4.BaseTypes, What4.Interface |
| bfStatus | What4.Utils.FloatHelpers |
| BigEndian | What4.Utils.Endian |
| BinaryPos | What4.ProgramLoc |
| bindVarAsFree | What4.Protocol.SMTWriter |
| Binop | |
| 1 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| 2 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| binop | What4.Protocol.VerilogWriter.AST |
| binopDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| binopType | What4.Protocol.VerilogWriter.AST |
| bin_app | What4.Protocol.SMTLib2.Syntax |
| Bit | What4.Protocol.VerilogWriter.AST |
| bit | What4.Protocol.VerilogWriter.AST |
| bit0 | What4.Protocol.SMTLib2.Syntax |
| bit1 | What4.Protocol.SMTLib2.Syntax |
| bitbounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise, What4.Utils.BVDomain |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| bitle | What4.Utils.BVDomain.Bitwise |
| BitSelect | What4.Protocol.VerilogWriter.AST |
| bitSelect | What4.Protocol.VerilogWriter.AST |
| BitVec | What4.Protocol.SMTLib2.Parse |
| BitvectorTheory | What4.Expr.AppTheory, What4.Expr |
| bitwiseRoundAbove | What4.Utils.BVDomain |
| bitwiseRoundBetween | What4.Utils.BVDomain |
| bitwiseToXorDomain | What4.Utils.BVDomain |
| Bool | What4.Protocol.SMTLib2.Parse |
| Boolector | |
| 1 (Type/Class) | What4.Solver.Boolector, What4.Solver |
| 2 (Data Constructor) | What4.Solver.Boolector, What4.Solver |
| boolectorAdapter | What4.Solver.Boolector, What4.Solver |
| boolectorFeatures | What4.Solver.Boolector, What4.Solver |
| boolectorOptions | What4.Solver.Boolector, What4.Solver |
| boolectorPath | What4.Solver.Boolector, What4.Solver |
| BoolExpr | |
| 1 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| 2 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| boolExpr | What4.Protocol.SMTWriter |
| BoolLit | What4.Protocol.VerilogWriter.AST |
| BoolMap | What4.Expr.BoolMap |
| BoolMapDualUnit | What4.Expr.BoolMap |
| BoolMapTerms | What4.Expr.BoolMap |
| BoolMapUnit | What4.Expr.BoolMap |
| BoolMapView | What4.Expr.BoolMap |
| boolOptSty | What4.Config |
| BoolOrFn | What4.Expr.MATLAB |
| BoolProperty | Test.Verification |
| boolSort | What4.Protocol.SMTLib2.Syntax |
| BoolTheory | What4.Expr.AppTheory, What4.Expr |
| BoolTypeMap | What4.Protocol.SMTWriter |
| Bound | What4.Config |
| boundInnerTerm | What4.Expr.VarIdentification |
| BoundQuant | What4.Expr.VarIdentification |
| boundQuant | What4.Expr.VarIdentification |
| boundTopTerm | What4.Expr.VarIdentification |
| BoundVar | What4.Interface |
| boundVar | What4.Expr.VarIdentification |
| BoundVarExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| BoundVarMap | What4.Expr.App |
| boundVars | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| boundVars' | What4.Expr.App |
| builder_list | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTWriter |
| BVAdd | What4.Protocol.VerilogWriter.AST |
| bvAdd | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvadd | What4.Protocol.SMTLib2.Syntax |
| BVAnd | What4.Protocol.VerilogWriter.AST |
| bvAnd | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvand | What4.Protocol.SMTLib2.Syntax |
| bvAndBits | What4.Interface |
| BVar | What4.Expr.App |
| bvarAbstractValue | What4.Expr.App, What4.Expr.Builder |
| bvarId | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| BVArith | What4.SemiRing |
| BVArithRepr | What4.SemiRing, What4.Expr |
| bvarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvarLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvarName | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvarType | What4.Expr.App, What4.Expr.Builder |
| BVAshr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvAshr | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvashr | What4.Protocol.SMTLib2.Syntax |
| bvAsSignedInteger | What4.SWord |
| bvAsUnsignedInteger | What4.SWord |
| bvAtBE | What4.SWord |
| bvAtLE | What4.SWord |
| bvbinary | What4.Protocol.SMTLib2.Syntax |
| BVBitInterval | What4.Utils.BVDomain.Bitwise |
| bvBitreverse | What4.Interface |
| BVBits | What4.SemiRing |
| BVBitsRepr | What4.SemiRing, What4.Expr |
| BVConcat | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvConcat | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| BVConst | |
| 1 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| 2 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| BVCountLeadingZeros | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvCountLeadingZeros | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVCountTrailingZeros | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvCountTrailingZeros | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVDAny | What4.Utils.BVDomain.Arith |
| BVDArith | What4.Utils.BVDomain |
| BVDBitwise | What4.Utils.BVDomain |
| bvdecimal | What4.Protocol.SMTLib2.Syntax |
| BVDInterval | What4.Utils.BVDomain.Arith |
| BVDiv | What4.Protocol.VerilogWriter.AST |
| bvdMask | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| BVDomain | What4.Utils.BVDomain |
| bvdomainRangeLimitOption | What4.Expr.Builder |
| BVDXor | What4.Utils.BVDomain.XOR |
| bvEq | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvExtract | What4.Protocol.SMTWriter |
| BVFill | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvFill | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVFlavor | What4.SemiRing, What4.Expr |
| BVFlavorRepr | What4.SemiRing, What4.Expr |
| bvForall | What4.SWord |
| bvhexadecimal | What4.Protocol.SMTLib2.Syntax |
| BVI | What4.Expr.VarIdentification |
| BVIndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder |
| bvIsNeg | What4.Interface |
| bvIsNonzero | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVIsNonZeroFn | What4.Expr.MATLAB |
| bvIte | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| bvJoin | What4.SWord |
| bvJoinVector | What4.Interface |
| bvLg2 | What4.SWord |
| BVLit | What4.Protocol.VerilogWriter.AST |
| bvLit | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVLshr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvLshr | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvlshr | What4.Protocol.SMTLib2.Syntax |
| BVMul | What4.Protocol.VerilogWriter.AST |
| bvMul | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvmul | What4.Protocol.SMTLib2.Syntax |
| bvNe | What4.Interface |
| bvNeg | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvneg | What4.Protocol.SMTLib2.Syntax |
| BVNot | What4.Protocol.VerilogWriter.AST |
| bvNot | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvnot | What4.Protocol.SMTLib2.Syntax |
| bvNotBits | What4.Interface |
| BVOr | What4.Protocol.VerilogWriter.AST |
| bvOr | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvor | What4.Protocol.SMTLib2.Syntax |
| bvOrAbs | What4.Expr.App, What4.Expr.Builder |
| BVOrBits | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvOrBits | What4.Interface |
| bvOrContains | What4.Expr.App |
| bvOrInsert | What4.Expr.App, What4.Expr.Builder |
| BVOrNote | |
| 1 (Type/Class) | What4.Expr.App |
| 2 (Data Constructor) | What4.Expr.App |
| BVOrSet | |
| 1 (Type/Class) | What4.Expr.App, What4.Expr.Builder |
| 2 (Data Constructor) | What4.Expr.App |
| bvOrSingleton | What4.Expr.App, What4.Expr.Builder |
| bvOrToList | What4.Expr.App, What4.Expr.Builder |
| bvOrUnion | What4.Expr.App, What4.Expr.Builder |
| bvPackBE | What4.SWord |
| bvPackLE | What4.SWord |
| BVPopcount | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvPopcount | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVPow | What4.Protocol.VerilogWriter.AST |
| BVRem | What4.Protocol.VerilogWriter.AST |
| BVRol | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvRol | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVRor | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvRor | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVRotateL | What4.Protocol.VerilogWriter.AST |
| BVRotateR | What4.Protocol.VerilogWriter.AST |
| BVSdiv | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvSDiv | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvSdiv | What4.Interface |
| bvsdiv | What4.Protocol.SMTLib2.Syntax |
| BVSelect | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvSelect | What4.Interface |
| bvSet | What4.Interface |
| bvSetBE | What4.SWord |
| bvSetLE | What4.SWord |
| BVSext | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvSext | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| bvSge | What4.Interface |
| bvsge | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvSgt | What4.Interface |
| bvsgt | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| BVShiftL | What4.Protocol.VerilogWriter.AST |
| BVShiftR | What4.Protocol.VerilogWriter.AST |
| BVShiftRA | What4.Protocol.VerilogWriter.AST |
| BVShl | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvShl | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvshl | What4.Protocol.SMTLib2.Syntax |
| bvsignExtend | What4.Protocol.SMTLib2.Syntax |
| bvSLe | What4.Protocol.SMTWriter |
| bvSle | What4.Interface |
| bvsle | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvSliceBE | What4.SWord |
| bvSliceLE | What4.SWord |
| BVSlt | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvSLt | What4.Protocol.SMTWriter |
| bvSlt | What4.Interface |
| bvslt | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvSort | What4.Protocol.SMTLib2.Syntax |
| bvSplitVector | What4.Interface |
| BVSrem | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvSRem | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvSrem | What4.Interface |
| bvsrem | What4.Protocol.SMTLib2.Syntax |
| BVSub | What4.Protocol.VerilogWriter.AST |
| bvSub | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| 3 (Function) | What4.Protocol.SMTWriter |
| bvsub | What4.Protocol.SMTLib2.Syntax |
| bvSum | What4.Expr.Builder |
| bvSumExpr | What4.Protocol.SMTWriter |
| bvSwap | What4.Interface |
| BVTerm | What4.Protocol.SMTLib2.Parse |
| bvTerm | What4.Protocol.SMTWriter |
| BVTestBit | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvTestBit | What4.Protocol.SMTWriter |
| BVToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvToFloat | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| BVToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvToInteger | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| BVToIntegerFn | What4.Expr.MATLAB |
| bvToNat | What4.Interface |
| bvTrunc | What4.Interface |
| BVTypeMap | What4.Protocol.SMTWriter |
| BVUdiv | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvUDiv | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvUdiv | What4.Interface |
| bvudiv | What4.Protocol.SMTLib2.Syntax |
| bvUge | What4.Interface |
| bvuge | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvUgt | What4.Interface |
| bvugt | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvULe | What4.Protocol.SMTWriter |
| bvUle | What4.Interface |
| bvule | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| BVUlt | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvULt | What4.Protocol.SMTWriter |
| bvUlt | What4.Interface |
| bvult | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SWord |
| bvUnary | What4.Expr.Builder |
| BVUnaryTerm | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvUnpackBE | What4.SWord |
| bvUnpackLE | What4.SWord |
| BVUrem | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvURem | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvUrem | What4.Interface |
| bvurem | What4.Protocol.SMTLib2.Syntax |
| bvWidth | |
| 1 (Function) | What4.Interface, What4.Expr.Builder |
| 2 (Function) | What4.SWord |
| BVXor | What4.Protocol.VerilogWriter.AST |
| bvXor | |
| 1 (Function) | What4.SWord |
| 2 (Function) | What4.Protocol.SMTWriter |
| bvxor | What4.Protocol.SMTLib2.Syntax |
| bvXorBits | What4.Interface |
| bvzeroExtend | What4.Protocol.SMTLib2.Syntax |
| BVZext | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| bvZext | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| cache | What4.Expr.App |
| cacheStartSizeOption | What4.Expr.Builder |
| cacheTerms | What4.Expr.Builder |
| carrylessMultiply | What4.Interface |
| CeilReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| Char16 | What4.BaseTypes, What4.Interface |
| Char16Literal | What4.Utils.StringLiteral, What4.Interface |
| Char16Repr | What4.BaseTypes, What4.Interface |
| Char8 | What4.BaseTypes, What4.Interface |
| Char8Literal | What4.Utils.StringLiteral, What4.Interface |
| Char8Repr | What4.BaseTypes, What4.Interface |
| Char8TypeMap | What4.Protocol.SMTWriter |
| check | What4.Protocol.Online |
| checkAndGetModel | What4.Protocol.Online |
| checkCommands | What4.Protocol.SMTWriter |
| checkOptSetResult | What4.Config |
| checkSat | What4.Protocol.SMTLib2.Syntax |
| checkSatAssuming | What4.Protocol.SMTLib2.Syntax |
| CheckSatError | What4.Protocol.SMTLib2.Parse |
| checkSatisfiable | What4.Protocol.Online |
| checkSatisfiableWithModel | What4.Protocol.Online |
| CheckSatResponse | What4.Protocol.SMTLib2.Parse |
| CheckSatUnsupported | What4.Protocol.SMTLib2.Parse |
| checkSatWithAssumptions | What4.Protocol.SMTLib2.Syntax |
| checkSolverVersion | What4.Protocol.SMTLib2 |
| checkSolverVersion' | What4.Protocol.SMTLib2 |
| checkWithAssumptions | What4.Protocol.Online |
| checkWithAssumptionsAndModel | What4.Protocol.Online |
| checkWithAssumptionsCommands | What4.Protocol.SMTWriter |
| chooseBool | Test.Verification |
| chooseInt | Test.Verification |
| chooseInteger | Test.Verification |
| clampedIntAbs | What4.Expr.MATLAB |
| ClampedIntAbsFn | What4.Expr.MATLAB |
| clampedIntAdd | What4.Expr.MATLAB |
| ClampedIntAddFn | What4.Expr.MATLAB |
| clampedIntMul | What4.Expr.MATLAB |
| ClampedIntMulFn | What4.Expr.MATLAB |
| clampedIntNeg | What4.Expr.MATLAB |
| ClampedIntNegFn | What4.Expr.MATLAB |
| clampedIntSub | What4.Expr.MATLAB |
| ClampedIntSubFn | What4.Expr.MATLAB |
| clampedIntToBV | What4.Interface |
| clampedIntToSBV | What4.Interface |
| clampedUIntAdd | What4.Expr.MATLAB |
| ClampedUIntAddFn | What4.Expr.MATLAB |
| clampedUIntMul | What4.Expr.MATLAB |
| ClampedUIntMulFn | What4.Expr.MATLAB |
| clampedUIntSub | What4.Expr.MATLAB |
| ClampedUIntSubFn | What4.Expr.MATLAB |
| cleanupProcess | What4.Utils.Process |
| clearIdxCache | What4.Expr.Builder |
| clz | |
| 1 (Function) | What4.Utils.Arithmetic |
| 2 (Function) | What4.Utils.BVDomain |
| Cmd | What4.Protocol.SMTLib2.Syntax |
| Coefficient | What4.SemiRing, What4.Expr |
| CollectedVarInfo | What4.Expr.VarIdentification |
| CollectorResults | |
| 1 (Type/Class) | What4.Protocol.SMTWriter |
| 2 (Data Constructor) | What4.Protocol.SMTWriter |
| collectVarInfo | What4.Expr.VarIdentification |
| combine | What4.Expr.BoolMap |
| Command | |
| 1 (Type/Class) | What4.Protocol.SMTLib2.Syntax |
| 2 (Type/Class) | What4.Protocol.SMTWriter |
| commentCommand | What4.Protocol.SMTWriter |
| compareExpr | What4.Expr.App |
| compareNat | What4.BaseTypes, What4.Interface |
| Complex | What4.Utils.Complex |
| complexAdd | What4.Utils.Complex |
| complexAsRational | What4.Utils.Complex |
| complexDiv | What4.Utils.Complex |
| complexMul | What4.Utils.Complex |
| complexNegate | What4.Utils.Complex |
| complexRecip | What4.Utils.Complex |
| complexSub | What4.Utils.Complex |
| ComplexToArrayTypeMap | What4.Protocol.SMTWriter |
| ComplexToStructTypeMap | What4.Protocol.SMTWriter |
| ComputableArithTheory | What4.Expr.AppTheory, What4.Expr |
| computeDefaultSolverBounds | What4.Utils.Versions |
| Concat | What4.Protocol.VerilogWriter.AST |
| concat | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain |
| concat2 | What4.Protocol.VerilogWriter.AST |
| ConcreteArray | What4.Concrete |
| ConcreteBool | What4.Concrete |
| ConcreteBV | What4.Concrete |
| ConcreteComplex | What4.Concrete |
| ConcreteInteger | What4.Concrete |
| concreteRange | What4.Utils.AbstractDomains |
| ConcreteReal | What4.Concrete |
| ConcreteString | What4.Concrete |
| ConcreteStruct | What4.Concrete |
| concreteToSym | What4.Interface |
| concreteType | What4.Concrete |
| ConcreteVal | What4.Concrete |
| ConcreteValue | What4.Utils.AbstractDomains |
| ConcreteValueWrapper | |
| 1 (Type/Class) | What4.Utils.AbstractDomains |
| 2 (Data Constructor) | What4.Utils.AbstractDomains |
| Config | What4.Config |
| ConfigDesc | What4.Config |
| configHelp | What4.Config |
| ConfigOption | What4.Config |
| configOption | What4.Config |
| configOptionName | What4.Config |
| configOptionNameParts | What4.Config |
| configOptionText | What4.Config |
| configOptionType | What4.Config |
| ConfigValue | |
| 1 (Type/Class) | What4.Config |
| 2 (Data Constructor) | What4.Config |
| ConjPred | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| Connection | What4.Solver.Yices |
| connHandle | What4.Protocol.SMTWriter |
| connInputHandle | What4.Protocol.SMTWriter |
| connState | What4.Protocol.SMTWriter |
| constant | |
| 1 (Function) | What4.Expr.WeightedSum |
| 2 (Function) | What4.Expr.UnaryBV |
| ConstantArray | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| constantArray | What4.Interface |
| contains | What4.Expr.BoolMap |
| ContinueOnError | What4.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_scalar | What4.Utils.BVDomain.XOR |
| correct_any | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_arithToBitwise | What4.Utils.BVDomain |
| correct_arithToXorDomain | What4.Utils.BVDomain |
| correct_ashr | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_asXorDomain | What4.Utils.BVDomain |
| correct_bitbounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.XOR |
| correct_bitwiseToArith | What4.Utils.BVDomain |
| correct_bitwiseToXorDomain | What4.Utils.BVDomain |
| correct_bra1 | What4.Utils.BVDomain |
| correct_bra2 | What4.Utils.BVDomain |
| correct_brb1 | What4.Utils.BVDomain |
| correct_brb2 | What4.Utils.BVDomain |
| correct_clz | What4.Utils.BVDomain |
| correct_concat | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_ctz | What4.Utils.BVDomain |
| correct_eq | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_fromXorDomain | What4.Utils.BVDomain |
| correct_intersection | What4.Utils.BVDomain.Bitwise |
| correct_lshr | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_mul | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_neg | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_not | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_or | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| correct_overlap | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_popcnt | What4.Utils.BVDomain |
| correct_rol | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| correct_ror | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| correct_sbounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_scale | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_scale_eq | What4.Utils.BVDomain.Arith |
| correct_sdiv | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_sdivRange | What4.Utils.BVDomain.Arith |
| correct_select | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_shl | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_shrink | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| correct_sign_ext | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_singleton | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| correct_slt | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_srem | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_testBit | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| correct_trunc | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| correct_ubounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_udiv | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_ult | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_union | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| correct_unknowns | What4.Utils.BVDomain.Arith |
| correct_urem | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| correct_xor | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain.XOR |
| 3 (Function) | What4.Utils.BVDomain |
| correct_xorToBitwiseDomain | What4.Utils.BVDomain |
| correct_zero_ext | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| countOccurrences | What4.Expr.App |
| countOccurrences' | What4.Expr.App |
| count_subterms | What4.Expr.Simplify |
| Cplx | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| cplxAdd | What4.Interface |
| CplxAddFn | What4.Expr.MATLAB |
| cplxCeil | What4.Interface |
| CplxCeilFn | What4.Expr.MATLAB |
| cplxConj | What4.Interface |
| cplxCos | What4.Interface |
| CplxCosFn | What4.Expr.MATLAB |
| cplxDiv | What4.Interface |
| cplxEq | What4.Interface |
| cplxExp | What4.Interface |
| CplxExpFn | What4.Expr.MATLAB |
| CplxExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| cplxExprAsInteger | What4.Interface |
| cplxExprAsRational | What4.Interface |
| cplxFloor | What4.Interface |
| CplxFloorFn | What4.Expr.MATLAB |
| cplxFromReal | What4.Interface |
| cplxGetParts | What4.Interface |
| cplxHypot | What4.Interface |
| CplxIsNonZeroFn | What4.Expr.MATLAB |
| CplxIsRealFn | What4.Expr.MATLAB |
| cplxIte | What4.Interface |
| cplxLog | What4.Interface |
| cplxLogBase | What4.Interface |
| CplxLogBaseFn | What4.Expr.MATLAB |
| CplxLogFn | What4.Expr.MATLAB |
| cplxMag | What4.Interface |
| CplxMagFn | What4.Expr.MATLAB |
| cplxMul | What4.Interface |
| CplxMulFn | What4.Expr.MATLAB |
| cplxNe | What4.Interface |
| cplxNeg | What4.Interface |
| CplxNegFn | What4.Expr.MATLAB |
| cplxRound | What4.Interface |
| CplxRoundFn | What4.Expr.MATLAB |
| cplxSin | What4.Interface |
| CplxSinFn | What4.Expr.MATLAB |
| cplxSqrt | What4.Interface |
| CplxSqrtFn | What4.Expr.MATLAB |
| cplxSub | What4.Interface |
| CplxSubFn | What4.Expr.MATLAB |
| cplxTan | What4.Interface |
| CplxTanFn | What4.Expr.MATLAB |
| crBindings | What4.Protocol.SMTWriter |
| crFreeConstants | What4.Protocol.SMTWriter |
| crResult | What4.Protocol.SMTWriter |
| crSideConds | What4.Protocol.SMTWriter |
| ctz | |
| 1 (Function) | What4.Utils.Arithmetic |
| 2 (Function) | What4.Utils.BVDomain |
| curProgramLoc | What4.Expr.Builder |
| CVC4 | |
| 1 (Type/Class) | What4.Solver.CVC4, What4.Solver |
| 2 (Data Constructor) | What4.Solver.CVC4, What4.Solver |
| cvc4Adapter | What4.Solver.CVC4, What4.Solver |
| cvc4Features | What4.Solver.CVC4, What4.Solver |
| cvc4Options | What4.Solver.CVC4, What4.Solver |
| cvc4Path | What4.Solver.CVC4, What4.Solver |
| cvc4Timeout | What4.Solver.CVC4 |
| dblPosIsPos | What4.BaseTypes, What4.Interface |
| DBV | What4.SWord |
| decDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| decideLeq | What4.BaseTypes, What4.Interface |
| decimal | What4.Protocol.SMTLib2.Syntax |
| declareCommand | What4.Protocol.SMTWriter |
| declareConst | What4.Protocol.SMTLib2.Syntax |
| declareFun | What4.Protocol.SMTLib2.Syntax |
| declareSort | What4.Protocol.SMTLib2.Syntax |
| DeclareSortResponse | What4.Protocol.SMTLib2.Parse |
| declareStructDatatype | What4.Protocol.SMTWriter |
| decNat | What4.BaseTypes, What4.Interface |
| defaultFeatures | What4.Protocol.SMTLib2 |
| defaultLogData | What4.Solver.Adapter, What4.Solver |
| defaultPPExprOpts | What4.Expr.App |
| defaultSolverAdapter | What4.Solver.Adapter, What4.Solver |
| defaultSolverArgs | What4.Protocol.SMTLib2 |
| defaultSolverBounds | What4.Protocol.SMTLib2 |
| defaultSolverPath | What4.Protocol.SMTLib2 |
| defaultValueForType | What4.Expr.GroundEval |
| defaultWriteSMTLIB2Features | What4.Solver.Adapter |
| defineCommand | What4.Protocol.SMTWriter |
| definedFn | What4.Interface |
| DefinedFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| DefineFun | |
| 1 (Type/Class) | What4.Protocol.SMTLib2.Parse |
| 2 (Data Constructor) | What4.Protocol.SMTLib2.Parse |
| defineFun | What4.Protocol.SMTLib2.Syntax |
| DefineFunResponse | What4.Protocol.SMTLib2.Parse |
| defineSort | What4.Protocol.SMTLib2.Syntax |
| DefineStyle | What4.Protocol.SMTWriter |
| delete | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Expr.ArrayUpdateMap |
| deleteFindMax | What4.Utils.LeqMap |
| deleteFindMin | What4.Utils.LeqMap |
| deleteIdxValue | What4.Expr.Builder |
| demuxProcessHandles | What4.Utils.HandleReader |
| difference | What4.Utils.AnnotatedMap |
| distinct | What4.Protocol.SMTLib2.Syntax |
| div | What4.Protocol.SMTLib2.Syntax |
| divNat | What4.BaseTypes, What4.Interface |
| Domain | |
| 1 (Type/Class) | What4.Utils.BVDomain.Arith |
| 2 (Type/Class) | What4.Utils.BVDomain.Bitwise |
| 3 (Type/Class) | What4.Utils.BVDomain.XOR |
| domain | What4.Expr.UnaryBV |
| domainsOverlap | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| DoubleDoubleFloat | What4.InterpretedFloatingPoint |
| DoubleDoubleFloatRepr | What4.InterpretedFloatingPoint |
| DoubleFloat | What4.InterpretedFloatingPoint |
| DoubleFloatRepr | What4.InterpretedFloatingPoint |
| DReal | |
| 1 (Type/Class) | What4.Solver.DReal, What4.Solver |
| 2 (Data Constructor) | What4.Solver.DReal, What4.Solver |
| drealAdapter | What4.Solver.DReal, What4.Solver |
| DRealBindings | What4.Solver.DReal, What4.Solver |
| drealOptions | What4.Solver.DReal |
| drealPath | What4.Solver.DReal, What4.Solver |
| drop | What4.Utils.Word16String |
| Dummy | What4.Expr.App |
| efSolveCommand | What4.Solver.Yices |
| empty | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.LeqMap |
| 3 (Function) | What4.Utils.Word16String |
| 4 (Function) | What4.Expr.ArrayUpdateMap |
| emptySolverBounds | What4.Utils.Versions |
| emptySymbol | What4.Symbol, What4.Interface |
| emptySymbolVarBimap | What4.Expr.Builder |
| emptyWordMap | What4.WordMap |
| Endian | What4.Utils.Endian |
| entryStackHeight | What4.Protocol.SMTWriter |
| enumOptSty | What4.Config |
| Eq | What4.Protocol.VerilogWriter.AST |
| eq | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SemiRing |
| 3 (Function) | What4.Utils.BVDomain.Arith |
| 4 (Function) | What4.Utils.BVDomain.Bitwise |
| 5 (Function) | What4.Utils.BVDomain |
| 6 (Function) | What4.Expr.UnaryBV |
| eqBy | What4.Utils.AnnotatedMap |
| eqPred | What4.Interface |
| EqualityDefinition | What4.Protocol.SMTWriter |
| Err | What4.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 |
| evalBoundVars | What4.Expr.Builder |
| evalGroundApp | What4.Expr.GroundEval |
| evalGroundExpr | What4.Expr.GroundEval |
| evalGroundNonceApp | What4.Expr.GroundEval |
| evalM | What4.Expr.WeightedSum |
| evalMatlabSolverFn | What4.Expr.MATLAB |
| evaluate | What4.Expr.UnaryBV |
| Exclusive | What4.Config |
| executablePathOptSty | What4.Config |
| execVerilogM | What4.Protocol.VerilogWriter.AST |
| ExistBound | What4.Expr.VarIdentification |
| existQuantifiers | What4.Expr.VarIdentification |
| Exists | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| exists | What4.Protocol.SMTLib2.Syntax |
| existsExpr | What4.Protocol.SMTWriter |
| ExistsForall | What4.Expr.VarIdentification |
| ExistsOnly | What4.Expr.VarIdentification |
| existsPred | What4.Interface |
| exit | What4.Protocol.SMTLib2.Syntax |
| Exp | What4.Protocol.VerilogWriter.AST |
| expandEnvironmentPath | What4.Utils.Environment |
| expDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| exponentBits | What4.SFloat |
| Expr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| exprAbsValue | What4.Expr.App |
| ExprBoundVar | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| ExprBuilder | What4.Expr.Builder, What4.Expr |
| exprCounter | What4.Expr.Builder |
| exprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| exprMaybeId | What4.Expr.Builder |
| ExprPPIndex | What4.Expr.App |
| exprPrettyArg | What4.Expr.App |
| exprPrettyIndices | What4.Expr.App |
| ExprRangeBindings | What4.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 |
| exprToModule | What4.Protocol.VerilogWriter |
| exprToVerilogExpr | What4.Protocol.VerilogWriter.Backend |
| exprType | What4.Interface, What4.Expr.Builder |
| exprVerilog | What4.Protocol.VerilogWriter |
| expType | What4.Protocol.VerilogWriter.AST |
| extendConfig | What4.Config |
| ExternalABC | |
| 1 (Type/Class) | What4.Solver.ExternalABC, What4.Solver |
| 2 (Data Constructor) | What4.Solver.ExternalABC, What4.Solver |
| externalABCAdapter | What4.Solver.ExternalABC, What4.Solver |
| extract | What4.Protocol.SMTLib2.Syntax |
| extractCommon | What4.Expr.WeightedSum |
| false | What4.Protocol.SMTLib2.Syntax |
| falsePred | What4.Interface |
| fillright | What4.Utils.BVDomain.Arith |
| filter | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Expr.ArrayUpdateMap |
| filterAsync | What4.Utils.Process |
| filterGt | What4.Utils.LeqMap |
| filterLt | What4.Utils.LeqMap |
| findExecutable | What4.Utils.Environment |
| findExprToRemove | What4.Expr.App |
| findMax | What4.Utils.LeqMap |
| findMin | What4.Utils.LeqMap |
| findSolverPath | What4.Utils.Process |
| findSubstring | What4.Utils.Word16String |
| FixedPPExpr | What4.Expr.App |
| Flags | What4.Expr.Builder, What4.Expr |
| FloatAbs | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatAbs | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatAdd | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatAdd | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatCast | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatCast | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatDiv | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatEq | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatExpr | |
| 1 (Type/Class) | What4.Expr.App, What4.Expr.Builder |
| 2 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| FloatFMA | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatFMA | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatFpApart | What4.Interface |
| FloatFpEq | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatFpEq | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatFpUnordered | What4.Interface |
| FloatFromBinary | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatFromBinary | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatFromInteger | What4.Utils.FloatHelpers |
| floatFromRational | What4.Utils.FloatHelpers |
| floatGe | What4.Interface |
| floatGt | What4.Interface |
| FloatIEEE | What4.Expr.Builder, What4.Expr |
| FloatIEEERepr | What4.Expr.Builder, What4.Expr |
| FloatInfo | What4.InterpretedFloatingPoint |
| FloatInfoRepr | What4.InterpretedFloatingPoint |
| FloatInfoToBitWidth | What4.InterpretedFloatingPoint |
| floatInfoToBVTypeRepr | What4.InterpretedFloatingPoint |
| FloatInfoToPrecision | What4.InterpretedFloatingPoint |
| floatInfoToPrecisionRepr | What4.InterpretedFloatingPoint |
| FloatingPoint | What4.Protocol.SMTLib2.Parse |
| FloatingPointPrecision | What4.BaseTypes, What4.Interface |
| FloatingPointPrecisionRepr | What4.BaseTypes, What4.Interface |
| FloatingPointTheory | What4.Expr.AppTheory, What4.Expr |
| FloatIsInf | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsInf | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsNaN | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsNaN | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsNeg | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsNeg | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsNorm | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsNorm | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsPos | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsPos | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsSubnorm | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsSubnorm | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatIsZero | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatIsZero | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatIte | What4.Interface |
| FloatLe | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatLe | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatLit | What4.Interface |
| floatLitRational | What4.Interface |
| FloatLt | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatLt | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatMax | What4.Interface |
| floatMin | What4.Interface |
| FloatMode | What4.Expr.Builder, What4.Expr |
| FloatModeRepr | What4.Expr.Builder, What4.Expr |
| FloatMul | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatMul | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatNaN | What4.Interface |
| floatNe | What4.Interface |
| FloatNeg | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatNeg | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatNInf | What4.Interface |
| floatNZero | What4.Interface |
| floatPInf | What4.Interface |
| FloatPrecision | What4.BaseTypes, What4.Interface |
| floatPrecision | What4.Interface |
| FloatPrecisionBits | What4.BaseTypes, What4.Interface |
| FloatPrecisionRepr | What4.BaseTypes, What4.Interface |
| floatPrecisionToBVType | What4.BaseTypes, What4.Interface |
| FloatPrecisionToInfo | What4.InterpretedFloatingPoint |
| floatPrecisionToInfoRepr | What4.InterpretedFloatingPoint |
| floatPZero | What4.Interface |
| FloatReal | What4.Expr.Builder, What4.Expr |
| FloatRealRepr | What4.Expr.Builder, What4.Expr |
| FloatRem | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatRem | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatRound | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatRound | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatRoundToInt | What4.Utils.FloatHelpers |
| FloatSqrt | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatSqrt | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatSub | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatSub | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatTerm | What4.Protocol.SMTWriter |
| FloatToBinary | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatToBinary | What4.Interface |
| FloatToBV | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatToBV | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| floatToInteger | What4.Utils.FloatHelpers |
| floatToRational | What4.Utils.FloatHelpers |
| FloatToReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatToReal | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatToSBV | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| floatToSBV | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| FloatTypeMap | What4.Protocol.SMTWriter |
| FloatUninterpreted | What4.Expr.Builder, What4.Expr |
| FloatUninterpretedRepr | What4.Expr.Builder, What4.Expr |
| FloorReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| FnApp | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| fnArgTypes | What4.Interface |
| FnArrayTypeMap | What4.Protocol.SMTWriter |
| fnReturnType | What4.Interface |
| FnSymbolBinding | What4.Expr.Builder |
| FnTheory | What4.Expr.AppTheory, What4.Expr |
| foldl' | What4.Utils.Word16String |
| foldlWithKey' | What4.Utils.LeqMap |
| Forall | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| forall | What4.Protocol.SMTLib2.Syntax |
| ForallBound | What4.Expr.VarIdentification |
| forallExpr | What4.Protocol.SMTWriter |
| forallPred | What4.Interface |
| forallQuantifiers | What4.Expr.VarIdentification |
| forgetModelAndCore | What4.SatResult, What4.Solver |
| fp80ToBits | What4.InterpretedFloatingPoint |
| fp80ToRational | What4.InterpretedFloatingPoint |
| fpAbs | What4.SFloat |
| fpActual | What4.SFloat |
| fpAdd | What4.SFloat |
| fpAsLit | What4.SFloat |
| fpDiv | What4.SFloat |
| fpEq | What4.SFloat |
| fpEqIEEE | What4.SFloat |
| fpExpected | What4.SFloat |
| fpFMA | What4.SFloat |
| fpFresh | What4.SFloat |
| fpFromBinary | What4.SFloat |
| fpFromInteger | What4.SFloat |
| fpFromLit | What4.SFloat |
| fpFromRational | What4.SFloat |
| fpFromRationalLit | What4.SFloat |
| fpFromReal | What4.SFloat |
| fpGtIEEE | What4.SFloat |
| fpIsInf | What4.SFloat |
| fpIsNaN | What4.SFloat |
| fpIsNeg | What4.SFloat |
| fpIsNorm | What4.SFloat |
| fpIsSubnorm | What4.SFloat |
| fpIsZero | What4.SFloat |
| fpIte | What4.SFloat |
| fpLtIEEE | What4.SFloat |
| fpMax | What4.SFloat |
| fpMin | What4.SFloat |
| fpMul | What4.SFloat |
| fpNaN | What4.SFloat |
| fpNeg | What4.SFloat |
| fpNegInf | What4.SFloat |
| fpOpts | What4.Utils.FloatHelpers |
| fppOpts | What4.Utils.FloatHelpers |
| fpPosInf | What4.SFloat |
| fpRepr | What4.SFloat |
| fpReprOf | What4.SFloat |
| fpRound | What4.SFloat |
| fpSize | What4.SFloat |
| fpSqrt | What4.SFloat |
| fpSub | What4.SFloat |
| fpToBinary | What4.SFloat |
| fpToRational | What4.SFloat |
| fpToReal | What4.SFloat |
| FPTypeError | |
| 1 (Type/Class) | What4.SFloat |
| 2 (Data Constructor) | What4.SFloat |
| fpWho | What4.SFloat |
| freshBoundedBV | What4.Interface |
| freshBoundedInt | What4.Interface |
| freshBoundedNat | What4.Interface |
| freshBoundedReal | What4.Interface |
| freshBoundedSBV | What4.Interface |
| freshBoundVar | What4.Interface |
| freshBoundVarName | What4.Protocol.SMTWriter |
| freshBV | What4.SWord |
| freshConstant | What4.Interface |
| freshFloatBoundVar | What4.InterpretedFloatingPoint |
| freshFloatConstant | What4.InterpretedFloatingPoint |
| freshFloatLatch | What4.InterpretedFloatingPoint |
| freshIdentifier | What4.Protocol.VerilogWriter.AST |
| freshLatch | What4.Interface |
| freshNat | What4.Interface |
| freshTotalUninterpFn | What4.Interface |
| fromAscEltList | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| fromAscList | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Expr.ArrayUpdateMap |
| fromChar16Lit | What4.Utils.StringLiteral |
| fromChar8Lit | What4.Utils.StringLiteral |
| fromConcreteBool | What4.Concrete |
| fromConcreteBV | What4.Concrete |
| fromConcreteComplex | What4.Concrete |
| fromConcreteInteger | What4.Concrete |
| fromConcreteReal | What4.Concrete |
| fromConcreteString | What4.Concrete |
| fromDistinctAscList | What4.Utils.LeqMap |
| fromDistinctDescList | What4.Utils.LeqMap |
| fromLEByteString | What4.Utils.Word16String |
| fromTerms | What4.Expr.WeightedSum |
| fromText | What4.Protocol.SMTWriter |
| fromUnicodeLit | What4.Utils.StringLiteral |
| fromVars | What4.Expr.BoolMap |
| fromXorDomain | What4.Utils.BVDomain |
| fromYicesText | What4.Protocol.PolyRoot |
| funArgs | What4.Protocol.SMTLib2.Parse |
| FunctionDefinition | What4.Protocol.SMTWriter |
| FunctionName | What4.FunctionName |
| functionName | What4.FunctionName |
| functionNameFromText | What4.FunctionName |
| funDef | What4.Protocol.SMTLib2.Parse |
| funResultSort | What4.Protocol.SMTLib2.Parse |
| funSymbol | What4.Protocol.SMTLib2.Parse |
| ge | What4.Protocol.SMTLib2.Syntax |
| Gen | Test.Verification |
| genChooseBool | Test.Verification |
| genChooseInt | Test.Verification |
| genChooseInteger | Test.Verification |
| genDomain | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| genElement | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| GenEnv | |
| 1 (Type/Class) | Test.Verification |
| 2 (Data Constructor) | Test.Verification |
| genGetSize | Test.Verification |
| genPair | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| getAbsValue | What4.Utils.AbstractDomains |
| getAnnotation | What4.Interface |
| getAvgBindings | What4.Solver.DReal |
| getBoundBindings | What4.Solver.DReal |
| getConfiguration | What4.Interface |
| getConfigValues | What4.Config |
| getCurrentProgramLoc | What4.Interface |
| getErrorBehavior | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| getGoalTimeoutInMilliSeconds | What4.Protocol.Online |
| getGoalTimeoutInSeconds | What4.Protocol.Online |
| getImagPart | What4.Interface |
| getInfo | What4.Protocol.SMTLib2.Syntax |
| getMaybeOpt | What4.Config |
| getModel | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.Online |
| GetModelResponse | What4.Protocol.SMTLib2.Parse |
| getName | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| getOpt | What4.Config |
| getOption | What4.Config |
| getOptionSetting | What4.Config |
| getOptionSettingFromText | What4.Config |
| getRealPart | What4.Interface |
| getSatResult | What4.Protocol.Online |
| getSize | Test.Verification |
| getSolverLogListener | What4.Interface |
| getStatistics | What4.Interface |
| getSymbolVarBimap | What4.Expr.Builder |
| getUnsatAssumptions | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.Online |
| getUnsatAssumptionsCommand | What4.Protocol.SMTWriter |
| getUnsatCore | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.Online |
| getUnsatCoreCommand | What4.Protocol.SMTWriter |
| getValue | What4.Protocol.SMTLib2.Syntax |
| getVersion | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| GroundArray | What4.Expr.GroundEval, What4.Expr |
| groundEq | What4.Expr.GroundEval |
| groundEval | What4.Expr.GroundEval, What4.Expr |
| GroundEvalFn | |
| 1 (Type/Class) | What4.Expr.GroundEval, What4.Expr |
| 2 (Data Constructor) | What4.Expr.GroundEval, What4.Expr |
| GroundValue | What4.Expr.GroundEval, What4.Expr |
| GroundValueWrapper | What4.Expr.GroundEval, What4.Expr |
| gt | What4.Protocol.SMTLib2.Syntax |
| GVW | What4.Expr.GroundEval, What4.Expr |
| HalfFloat | What4.InterpretedFloatingPoint |
| HalfFloatRepr | What4.InterpretedFloatingPoint |
| halfNat | What4.BaseTypes, What4.Interface |
| HandleReader | |
| 1 (Type/Class) | What4.Utils.HandleReader, What4.Solver.Yices |
| 2 (Data Constructor) | What4.Utils.HandleReader |
| HasAbsValue | What4.Utils.AbstractDomains, What4.Interface |
| HasCallStack | What4.Panic |
| hashApp | What4.Expr.App |
| hashIndexLit | What4.IndexLit |
| hasProblemFeature | What4.ProblemFeatures |
| HasProgramLoc | What4.ProgramLoc |
| hexDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| hrChan | What4.Utils.HandleReader |
| hrHandle | What4.Utils.HandleReader |
| hrThreadId | What4.Utils.HandleReader |
| iBVToFloat | What4.InterpretedFloatingPoint |
| Ident | What4.Protocol.VerilogWriter.AST |
| identDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| Identifier | What4.Protocol.VerilogWriter.AST |
| IdxCache | What4.Expr.Builder |
| idxCacheEval | What4.Expr.Builder |
| idxCacheEval' | What4.Expr.Builder |
| IExp | |
| 1 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| 2 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| iexpDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| iexpType | What4.Protocol.VerilogWriter.AST |
| IfEqTerm | What4.Protocol.SMTLib2.Parse |
| iFloatAbs | What4.InterpretedFloatingPoint |
| iFloatAdd | What4.InterpretedFloatingPoint |
| iFloatBaseTypeRepr | What4.InterpretedFloatingPoint |
| iFloatCast | What4.InterpretedFloatingPoint |
| iFloatDiv | What4.InterpretedFloatingPoint |
| iFloatEq | What4.InterpretedFloatingPoint |
| iFloatFMA | What4.InterpretedFloatingPoint |
| iFloatFpApart | What4.InterpretedFloatingPoint |
| iFloatFpEq | What4.InterpretedFloatingPoint |
| iFloatFromBinary | What4.InterpretedFloatingPoint |
| iFloatGe | What4.InterpretedFloatingPoint |
| iFloatGt | What4.InterpretedFloatingPoint |
| iFloatIsInf | What4.InterpretedFloatingPoint |
| iFloatIsNaN | What4.InterpretedFloatingPoint |
| iFloatIsNeg | What4.InterpretedFloatingPoint |
| iFloatIsNorm | What4.InterpretedFloatingPoint |
| iFloatIsPos | What4.InterpretedFloatingPoint |
| iFloatIsSubnorm | What4.InterpretedFloatingPoint |
| iFloatIsZero | What4.InterpretedFloatingPoint |
| iFloatIte | What4.InterpretedFloatingPoint |
| iFloatLe | What4.InterpretedFloatingPoint |
| iFloatLitDouble | What4.InterpretedFloatingPoint |
| iFloatLitLongDouble | What4.InterpretedFloatingPoint |
| iFloatLitRational | What4.InterpretedFloatingPoint |
| iFloatLitSingle | What4.InterpretedFloatingPoint |
| iFloatLt | What4.InterpretedFloatingPoint |
| iFloatMax | What4.InterpretedFloatingPoint |
| iFloatMin | What4.InterpretedFloatingPoint |
| iFloatMul | What4.InterpretedFloatingPoint |
| iFloatNaN | What4.InterpretedFloatingPoint |
| iFloatNe | What4.InterpretedFloatingPoint |
| iFloatNeg | What4.InterpretedFloatingPoint |
| iFloatNInf | What4.InterpretedFloatingPoint |
| iFloatNZero | What4.InterpretedFloatingPoint |
| iFloatPInf | What4.InterpretedFloatingPoint |
| iFloatPZero | What4.InterpretedFloatingPoint |
| iFloatRem | What4.InterpretedFloatingPoint |
| iFloatRound | What4.InterpretedFloatingPoint |
| iFloatSqrt | What4.InterpretedFloatingPoint |
| iFloatSub | What4.InterpretedFloatingPoint |
| iFloatToBinary | What4.InterpretedFloatingPoint |
| iFloatToBV | What4.InterpretedFloatingPoint |
| iFloatToReal | What4.InterpretedFloatingPoint |
| iFloatToSBV | What4.InterpretedFloatingPoint |
| ImagPart | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| imagPart | What4.Utils.Complex |
| ImagPartOfCplxFn | What4.Expr.MATLAB |
| ImmediateExit | What4.Protocol.Online |
| implies | What4.Protocol.SMTLib2.Syntax |
| impliesExpr | What4.Protocol.SMTWriter |
| impliesPred | What4.Interface |
| Inclusive | |
| 1 (Data Constructor) | What4.Utils.AbstractDomains |
| 2 (Data Constructor) | What4.Config |
| incNat | What4.BaseTypes, What4.Interface |
| incOccurrence | What4.Expr.App |
| IncrHash | What4.Utils.IncrHash |
| index | What4.Utils.Word16String |
| IndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder |
| indexLit | What4.Interface |
| IndicesInRange | What4.Expr.MATLAB |
| InfoKeyword | What4.Protocol.SMTLib2.Syntax |
| initialConfig | What4.Config |
| initializationLoc | What4.ProgramLoc |
| initModuleState | What4.Protocol.VerilogWriter.AST |
| inlineDefineFun | What4.Interface |
| inNewFrame | What4.Protocol.Online, What4.Solver.Yices |
| inNewFrameWithVars | What4.Protocol.Online |
| Input | What4.Protocol.VerilogWriter.AST |
| inputDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| insert | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.LeqMap |
| 3 (Function) | What4.Expr.ArrayUpdateMap |
| insertIdxValue | What4.Expr.Builder |
| insertWordMap | What4.WordMap |
| instantiate | What4.Expr.UnaryBV |
| Int | What4.Protocol.SMTLib2.Parse |
| IntAbs | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| intAbs | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| intAbsRange | What4.Utils.AbstractDomains |
| intAdd | What4.Interface |
| IntDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| intDiv | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| IntDivisible | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| intDivisible | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| intDivRange | What4.Utils.AbstractDomains |
| integerBounds | What4.Interface |
| IntegerExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| integerOptSty | What4.Config |
| integerTerm | What4.Protocol.SMTWriter |
| IntegerToBV | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| integerToBV | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| integerToNat | What4.Interface |
| IntegerToReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| integerToReal | What4.Interface |
| IntegerToRealFn | What4.Expr.MATLAB |
| IntegerTypeMap | What4.Protocol.SMTWriter |
| integerWithMaxOptSty | What4.Config |
| integerWithMinOptSty | What4.Config |
| integerWithRangeOptSty | What4.Config |
| intEq | What4.Interface |
| InternalPos | What4.ProgramLoc |
| intersection | What4.Utils.BVDomain.Bitwise |
| interval | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| IntIndexLit | What4.IndexLit, What4.Interface, What4.Expr.Builder |
| intIte | What4.Interface |
| intLe | What4.Interface |
| IntLeFn | What4.Expr.MATLAB |
| intLit | What4.Interface |
| intLt | What4.Interface |
| intMax | What4.Interface |
| intMin | What4.Interface |
| IntMod | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| intMod | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| intModRange | What4.Utils.AbstractDomains |
| intMul | What4.Interface |
| intNeg | What4.Interface |
| IntSeqFn | What4.Expr.MATLAB |
| intSetWidth | What4.Interface |
| IntSetWidthFn | What4.Expr.MATLAB |
| intSort | What4.Protocol.SMTLib2.Syntax |
| intSub | What4.Interface |
| intSum | What4.Expr.Builder |
| IntTerm | What4.Protocol.SMTLib2.Parse |
| intToUInt | What4.Interface |
| IntToUIntFn | What4.Expr.MATLAB |
| intValue | What4.BaseTypes, What4.Interface |
| InvalidRange | |
| 1 (Type/Class) | What4.Interface |
| 2 (Data Constructor) | What4.Interface |
| iRealToFloat | What4.InterpretedFloatingPoint |
| iSBVToFloat | What4.InterpretedFloatingPoint |
| isEq | What4.Interface |
| IsEqFn | What4.Expr.MATLAB |
| IsExpr | What4.Interface |
| IsExprBuilder | What4.Interface |
| isInconsistent | What4.Expr.BoolMap |
| isInfixOf | What4.Utils.Word16String |
| isInt | What4.Protocol.SMTLib2.Syntax |
| isInteger | What4.Interface |
| IsIntegerFn | What4.Expr.MATLAB |
| IsInterpretedFloatExprBuilder | What4.InterpretedFloatingPoint |
| IsInterpretedFloatSymExprBuilder | What4.InterpretedFloatingPoint |
| isNonLinearApp | What4.Expr.App |
| isNonZero | What4.Interface |
| isNull | What4.Expr.BoolMap |
| isPosNat | What4.BaseTypes, What4.Interface |
| isPow2 | What4.Utils.Arithmetic |
| isPrefixOf | What4.Utils.Word16String |
| isReal | What4.Interface |
| isSat | What4.SatResult, What4.Solver |
| isSuffixOf | What4.Utils.Word16String |
| IsSymExprBuilder | What4.Interface |
| IsSymFn | What4.Interface |
| isUnknown | What4.SatResult, What4.Solver |
| isUnsat | What4.SatResult, What4.Solver |
| isZero | What4.Expr.WeightedSum |
| IsZeroNat | What4.BaseTypes, What4.Interface |
| isZeroNat | What4.BaseTypes, What4.Interface |
| isZeroOrGT1 | What4.BaseTypes, What4.Interface |
| ite | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTWriter |
| iteList | What4.Interface |
| Item | What4.Protocol.VerilogWriter.AST |
| iteM | What4.Interface |
| itePred | What4.Interface |
| itePredM | What4.Interface |
| iteSize | What4.Expr.App, What4.Expr.Builder |
| joinMaybePE | What4.Partial |
| joinRange | What4.Utils.AbstractDomains |
| justPartExpr | What4.Partial |
| keys | What4.Utils.LeqMap |
| keysSet | What4.Expr.ArrayUpdateMap |
| killSolver | What4.Protocol.Online |
| KnownCtx | What4.BaseTypes, What4.Interface |
| knownNat | What4.BaseTypes, What4.Interface |
| KnownRepr | What4.BaseTypes, What4.Interface |
| knownRepr | What4.BaseTypes, What4.Interface |
| LabeledPred | |
| 1 (Type/Class) | What4.LabeledPred |
| 2 (Data Constructor) | What4.LabeledPred |
| labeledPred | What4.LabeledPred |
| labeledPredMsg | What4.LabeledPred |
| lambdaTerm | What4.Protocol.SMTWriter |
| latches | What4.Expr.VarIdentification |
| LatchVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| Le | What4.Protocol.VerilogWriter.AST |
| le | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SemiRing |
| lemmaFloatPrecisionIsPos | What4.BaseTypes, What4.Interface |
| lemmaMul | What4.BaseTypes, What4.Interface |
| length | What4.Utils.Word16String |
| leqAdd | What4.BaseTypes, What4.Interface |
| leqAdd2 | What4.BaseTypes, What4.Interface |
| leqAddPos | What4.BaseTypes, What4.Interface |
| LeqMap | What4.Utils.LeqMap |
| leqMulCongr | What4.BaseTypes, What4.Interface |
| leqMulMono | What4.BaseTypes, What4.Interface |
| leqMulPos | What4.BaseTypes, What4.Interface |
| LeqProof | |
| 1 (Data Constructor) | What4.BaseTypes, What4.Interface |
| 2 (Type/Class) | What4.BaseTypes, What4.Interface |
| leqProof | What4.BaseTypes, What4.Interface |
| leqRefl | What4.BaseTypes, What4.Interface |
| leqSub | What4.BaseTypes, What4.Interface |
| leqSub2 | What4.BaseTypes, What4.Interface |
| leqTrans | What4.BaseTypes, What4.Interface |
| lessThanAsymmetric | What4.BaseTypes, What4.Interface |
| lessThanIrreflexive | What4.BaseTypes, What4.Interface |
| letBinder | What4.Protocol.SMTLib2.Syntax |
| letExpr | What4.Protocol.SMTWriter |
| lg | What4.Utils.Arithmetic |
| lgCeil | What4.Utils.Arithmetic |
| LHS | |
| 1 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| 2 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| LHSBit | What4.Protocol.VerilogWriter.AST |
| lhsDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| liftST | What4.Utils.MonadST |
| LinearArithTheory | What4.Expr.AppTheory, What4.Expr |
| lineBufferedOutputStream | What4.Utils.HandleReader |
| listOptSty | What4.Config |
| litBool | What4.Protocol.VerilogWriter.AST |
| litBV | What4.Protocol.VerilogWriter.AST |
| LittleEndian | What4.Utils.Endian |
| logCallback | What4.Solver.Adapter, What4.Solver |
| logCallbackVerbose | What4.Solver.Adapter, What4.Solver |
| LogData | |
| 1 (Type/Class) | What4.Solver.Adapter, What4.Solver |
| 2 (Data Constructor) | What4.Solver.Adapter, What4.Solver |
| logErrorStream | What4.Utils.Streams |
| logHandle | What4.Solver.Adapter, What4.Solver |
| Logic | |
| 1 (Type/Class) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| 2 (Data Constructor) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| logReason | What4.Solver.Adapter, What4.Solver |
| logSolverEvent | What4.Interface |
| logVerbosity | What4.Solver.Adapter, What4.Solver |
| lookup | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Expr.ArrayUpdateMap |
| lookupArray | What4.Expr.GroundEval, What4.Expr |
| lookupBindingOfSymbol | What4.Expr.Builder |
| lookupGE | What4.Utils.LeqMap |
| lookupGT | What4.Utils.LeqMap |
| lookupIdx | What4.Expr.Builder |
| lookupIdxValue | What4.Expr.Builder |
| lookupLE | What4.Utils.LeqMap |
| lookupLT | What4.Utils.LeqMap |
| lookupSymbolOfBinding | What4.Expr.Builder |
| lookupWordMap | What4.WordMap |
| lower | What4.Utils.Versions |
| lshr | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| Lt | What4.Protocol.VerilogWriter.AST |
| lt | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SemiRing |
| magnitude | What4.Utils.Complex |
| magnitudeSq | What4.Utils.Complex |
| mapKeysMonotonic | What4.Utils.LeqMap |
| mapMaybe | What4.Utils.AnnotatedMap |
| MapOverArrays | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| mapRange | What4.Utils.AbstractDomains |
| matlabSolverArgTypes | What4.Expr.MATLAB |
| MatlabSolverFn | What4.Expr.MATLAB |
| MatlabSolverFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| matlabSolverReturnType | What4.Expr.MATLAB |
| MatlabSymbolicArrayBuilder | What4.Expr.MATLAB |
| maxNat | What4.BaseTypes, What4.Interface |
| maxSigned | What4.BaseTypes, What4.Interface |
| maxSignedBV | What4.Interface |
| maxUnsigned | What4.BaseTypes, What4.Interface |
| maxUnsignedBV | What4.Interface |
| maxValueBound | What4.Utils.AbstractDomains |
| maybePartExpr | What4.Partial |
| member | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| mergeA | What4.Utils.AnnotatedMap |
| mergeM | What4.Expr.ArrayUpdateMap |
| mergePartial | What4.Partial |
| mergePartials | What4.Partial |
| mergeWithKey | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.LeqMap |
| mergeWithKeyM | What4.Utils.AnnotatedMap |
| minSigned | What4.BaseTypes, What4.Interface |
| minSignedBV | What4.Interface |
| minUnsigned | What4.BaseTypes, What4.Interface |
| minUnsignedBV | What4.Interface |
| minusPlusCancel | What4.BaseTypes, What4.Interface |
| minValueBound | What4.Utils.AbstractDomains |
| minViewWithKey | What4.Utils.LeqMap |
| mkAtomicFormula | What4.Protocol.SMTWriter |
| mkBaseExpr | What4.Protocol.SMTWriter |
| mkComplex | What4.Interface |
| mkComplexLit | What4.Interface |
| mkExpr | What4.Expr.App |
| mkFormula | What4.Protocol.SMTWriter |
| mkFreeVar | What4.Protocol.SMTWriter |
| mkIncrHash | What4.Utils.IncrHash |
| mkLet | What4.Protocol.VerilogWriter.AST |
| mkMatlabSolverFn | What4.Expr.MATLAB |
| mkModule | What4.Protocol.VerilogWriter.AST |
| mkNatRepr | What4.BaseTypes, What4.Interface |
| mkOpt | What4.Config |
| mkPE | What4.Partial |
| mkProgramLoc | What4.ProgramLoc |
| mkRational | What4.Interface |
| mkReal | What4.Interface |
| mkSMTTerm | What4.Protocol.SMTWriter |
| mkStruct | What4.Interface |
| mod | What4.Protocol.SMTLib2.Syntax |
| ModelResponse | What4.Protocol.SMTLib2.Parse |
| Module | |
| 1 (Type/Class) | What4.Protocol.VerilogWriter.AST, What4.Protocol.VerilogWriter |
| 2 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| moduleDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| ModuleState | |
| 1 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| 2 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| MonadST | What4.Utils.MonadST |
| mul | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.SemiRing |
| 3 (Function) | What4.Utils.BVDomain.Arith |
| 4 (Function) | What4.Utils.BVDomain |
| mul2Plus | What4.BaseTypes, What4.Interface |
| mulCancelR | What4.BaseTypes, What4.Interface |
| mulComm | What4.BaseTypes, What4.Interface |
| mulRange | What4.Utils.AbstractDomains |
| mulSignedOF | What4.Interface |
| MultiRange | What4.Utils.AbstractDomains, What4.Interface |
| mulUnsignedOF | What4.Interface |
| Mux | What4.Protocol.VerilogWriter.AST |
| mux | |
| 1 (Function) | What4.Expr.UnaryBV |
| 2 (Function) | What4.Protocol.VerilogWriter.AST |
| muxRange | What4.Interface |
| muxWordMap | What4.WordMap |
| Name | What4.Protocol.SMTLib2.Syntax |
| namedTerm | What4.Protocol.SMTLib2.Syntax |
| nameResult | What4.Protocol.SMTLib2 |
| natAdd | What4.Interface |
| NatCaseEQ | What4.BaseTypes, What4.Interface |
| NatCaseGT | What4.BaseTypes, What4.Interface |
| NatCaseLT | What4.BaseTypes, What4.Interface |
| NatCases | What4.BaseTypes, What4.Interface |
| NatComparison | What4.BaseTypes, What4.Interface |
| natDiv | What4.Interface |
| NatEQ | What4.BaseTypes, What4.Interface |
| natEq | What4.Interface |
| natForEach | What4.BaseTypes, What4.Interface |
| natFromZero | What4.BaseTypes, What4.Interface |
| NatGT | What4.BaseTypes, What4.Interface |
| natIte | What4.Interface |
| natLe | What4.Interface |
| natLit | What4.Interface |
| NatLT | What4.BaseTypes, What4.Interface |
| natLt | What4.Interface |
| natMod | What4.Interface |
| natMul | What4.Interface |
| natMultiply | What4.BaseTypes, What4.Interface |
| natRec | What4.BaseTypes, What4.Interface |
| natRecBounded | What4.BaseTypes, What4.Interface |
| natRecStrong | What4.BaseTypes, What4.Interface |
| NatRepr | What4.BaseTypes, What4.Interface |
| natSub | What4.Interface |
| natToInteger | What4.Interface |
| natToReal | What4.Interface |
| natValue | What4.BaseTypes, What4.Interface |
| Ne | What4.Protocol.VerilogWriter.AST |
| neg | What4.Expr.UnaryBV |
| negate | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain |
| negatePolarity | What4.Expr.BoolMap, What4.Expr.Builder |
| negateRange | What4.Utils.AbstractDomains |
| Negative | What4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification |
| NeverUnfold | What4.Interface |
| newConnection | What4.Solver.Yices |
| newDefaultWriter | What4.Protocol.SMTLib2 |
| newExprBuilder | What4.Expr.Builder, What4.Expr |
| newIdxCache | What4.Expr.Builder |
| newWriter | What4.Protocol.SMTLib2 |
| newWriterConn | What4.Protocol.SMTWriter |
| nextMultiple | What4.Utils.Arithmetic |
| nextPow2Multiple | What4.Utils.Arithmetic |
| NoErr | What4.Partial |
| noFeatures | What4.ProblemFeatures |
| NonceApp | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| NonceAppExpr | |
| 1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| 2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| NonceAppExprCtor | What4.Expr.App |
| nonceAppType | What4.Expr.App, What4.Expr.Builder |
| nonceExprAbsValue | What4.Expr.App |
| nonceExprApp | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| nonceExprId | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| nonceExprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| nonempty | What4.Utils.BVDomain.Bitwise |
| NonlinearArithTheory | What4.Expr.AppTheory, What4.Expr |
| NonZeroNat | What4.BaseTypes, What4.Interface |
| Not | What4.Protocol.VerilogWriter.AST |
| not | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain |
| notExpr | What4.Protocol.SMTWriter |
| NotPred | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| notPred | What4.Interface |
| null | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.LeqMap |
| 3 (Function) | What4.Utils.Word16String |
| 4 (Function) | What4.Expr.ArrayUpdateMap |
| nullAcknowledgementAction | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2 |
| nullProd | What4.Expr.WeightedSum |
| numeral | What4.Protocol.SMTLib2.Syntax |
| Occurrence | What4.SemiRing |
| OccurrenceTable | What4.Expr.App |
| occ_add | What4.SemiRing |
| occ_compare | What4.SemiRing |
| occ_count | What4.SemiRing |
| occ_eq | What4.SemiRing |
| occ_hashWithSalt | What4.SemiRing |
| occ_one | What4.SemiRing |
| one | What4.SemiRing |
| OnlineSolver | What4.Protocol.Online |
| OnlyIntRepr | |
| 1 (Type/Class) | What4.Utils.OnlyIntRepr |
| 2 (Data Constructor) | What4.Utils.OnlyIntRepr |
| Opt | What4.Config |
| opt | What4.Config |
| optErr | What4.Config |
| optionSetError | What4.Config |
| OptionSetResult | |
| 1 (Type/Class) | What4.Config |
| 2 (Data Constructor) | What4.Config |
| OptionSetting | |
| 1 (Type/Class) | What4.Config |
| 2 (Data Constructor) | What4.Config |
| optionSettingName | What4.Config |
| optionSetWarnings | What4.Config |
| OptionStyle | |
| 1 (Type/Class) | What4.Config |
| 2 (Data Constructor) | What4.Config |
| optOK | What4.Config |
| optU | What4.Config |
| optUV | What4.Config |
| optV | What4.Config |
| optWarn | What4.Config |
| opt_default_value | What4.Config |
| opt_help | What4.Config |
| opt_onset | What4.Config |
| opt_type | What4.Config |
| Or | What4.Protocol.VerilogWriter.AST |
| or | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| orAll | What4.Protocol.SMTWriter |
| orderedSemiRing | What4.SemiRing |
| OrderedSemiRingIntegerRepr | What4.SemiRing, What4.Expr |
| OrderedSemiRingRealRepr | What4.SemiRing, What4.Expr |
| OrderedSemiRingRepr | What4.SemiRing, What4.Expr |
| orOneOf | What4.Interface |
| orPred | What4.Interface |
| OtherPos | What4.ProgramLoc |
| Output | What4.Protocol.VerilogWriter.AST |
| pairwise_app | What4.Protocol.SMTLib2.Syntax |
| Panic | What4.Panic |
| panic | What4.Panic |
| parenIf | What4.Expr.App |
| parseNextWord | What4.Protocol.SExp |
| parseSExp | What4.Protocol.SExp |
| parseSolverBounds | What4.Utils.Versions |
| parseYicesRoot | What4.Protocol.PolyRoot |
| PartExpr | What4.Partial |
| Partial | |
| 1 (Type/Class) | What4.Partial |
| 2 (Data Constructor) | What4.Partial |
| partialPred | What4.Partial |
| PartialT | |
| 1 (Type/Class) | What4.Partial |
| 2 (Data Constructor) | What4.Partial |
| partialValue | What4.Partial |
| PartialWithErr | What4.Partial |
| partitionByPreds | What4.LabeledPred |
| partitionByPredsM | What4.LabeledPred |
| partitionLabeledPreds | What4.LabeledPred |
| PE | What4.Partial |
| Pi | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| plFunction | What4.ProgramLoc |
| plSourceLoc | What4.ProgramLoc |
| plusAssoc | What4.BaseTypes, What4.Interface |
| plusComm | What4.BaseTypes, What4.Interface |
| plusMinusCancel | What4.BaseTypes, What4.Interface |
| pmember | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| Polarity | What4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification |
| pop | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.Online, What4.Solver.Yices |
| popcnt | What4.Utils.BVDomain |
| popCommand | What4.Protocol.SMTWriter |
| popEntryStack | What4.Protocol.SMTWriter |
| popEntryStackToTop | What4.Protocol.SMTWriter |
| popManyCommands | What4.Protocol.SMTWriter |
| pos | What4.ProgramLoc |
| Posd | |
| 1 (Type/Class) | What4.ProgramLoc |
| 2 (Data Constructor) | What4.ProgramLoc |
| Position | What4.ProgramLoc |
| Positive | What4.Expr.BoolMap, What4.Expr.Builder, What4.Expr.VarIdentification |
| pos_val | What4.ProgramLoc |
| ppApp' | What4.Expr.App |
| ppBoundVar | What4.Expr.App, What4.Expr.Builder |
| ppConcrete | What4.Concrete |
| PPExpr | What4.Expr.App |
| ppExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| ppExpr' | What4.Expr.App |
| ppExprDoc | What4.Expr.App |
| ppExprLength | What4.Expr.App |
| PPExprOpts | |
| 1 (Type/Class) | What4.Expr.App |
| 2 (Data Constructor) | What4.Expr.App |
| ppExprTop | What4.Expr.App, What4.Expr.Builder |
| ppExpr_maxWidth | What4.Expr.App |
| ppExpr_useDecimal | What4.Expr.App |
| PPIndex | What4.Expr.App |
| ppMatlabSolverFn | What4.Expr.MATLAB |
| ppNoFileName | What4.ProgramLoc |
| ppNonceApp | What4.Expr.App |
| ppSolverSymbolError | What4.Symbol |
| ppSolverVersionCheckError | What4.Protocol.SMTLib2 |
| ppSolverVersionError | What4.Protocol.SMTLib2 |
| ppVar | What4.Expr.App |
| ppVarTypeCode | What4.Expr.App |
| Prec128 | What4.BaseTypes, What4.Interface |
| Prec16 | What4.BaseTypes, What4.Interface |
| Prec32 | What4.BaseTypes, What4.Interface |
| Prec64 | What4.BaseTypes, What4.Interface |
| Prec80 | What4.BaseTypes, What4.Interface |
| precise_overlap | What4.Utils.BVDomain |
| precisionBits | What4.SFloat |
| preCondition | Test.Verification |
| Pred | What4.Interface |
| predicateVarInfo | What4.Expr.VarIdentification |
| predNat | What4.BaseTypes, What4.Interface |
| predToBV | What4.Interface |
| PredToBVFn | What4.Expr.MATLAB |
| PredToIntegerFn | What4.Expr.MATLAB |
| predToReal | What4.Interface |
| PrettyApp | What4.Expr.App |
| prettyApp | What4.Expr.App |
| PrettyArg | |
| 1 (Type/Class) | What4.Expr.App |
| 2 (Data Constructor) | What4.Expr.App |
| PrettyFunc | What4.Expr.App |
| PrettyText | What4.Expr.App |
| PrimArrayTypeMap | What4.Protocol.SMTWriter |
| printSymExpr | What4.Interface |
| printSymNat | What4.Interface |
| ProblemFeatures | What4.ProblemFeatures |
| problemFeatures | What4.Expr.VarIdentification |
| prodAbsValue | What4.Expr.WeightedSum |
| prodContains | What4.Expr.WeightedSum |
| prodEval | What4.Expr.WeightedSum |
| prodEvalM | What4.Expr.WeightedSum |
| prodMul | What4.Expr.WeightedSum |
| prodRepr | What4.Expr.WeightedSum |
| prodVar | What4.Expr.WeightedSum |
| ProgramLoc | What4.ProgramLoc |
| programLoc | What4.ProgramLoc |
| proper | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| Property | Test.Verification |
| property | Test.Verification |
| push | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.Online, What4.Solver.Yices |
| pushCommand | What4.Protocol.SMTWriter |
| pushEntryStack | What4.Protocol.SMTWriter |
| qf_bv | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| QuadFloat | What4.InterpretedFloatingPoint |
| QuadFloatRepr | What4.InterpretedFloatingPoint |
| quantAbsEval | What4.Expr.App |
| QuantifierInfo | What4.Expr.VarIdentification |
| QuantifierInfoMap | What4.Expr.VarIdentification |
| QuantifierTheory | What4.Expr.AppTheory, What4.Expr |
| QuantifierVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| quantTheory | What4.Expr.AppTheory, What4.Expr |
| queryErrorBehavior | What4.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 |
| rangeCheckEq | What4.Utils.AbstractDomains |
| rangeCheckLe | What4.Utils.AbstractDomains |
| rangeHiBound | What4.Utils.AbstractDomains |
| rangeLowBound | What4.Utils.AbstractDomains |
| rangeMax | What4.Utils.AbstractDomains |
| rangeMin | What4.Utils.AbstractDomains |
| rangeScalarMul | What4.Utils.AbstractDomains |
| rationalAsInteger | What4.Interface |
| rationalBounds | What4.Interface |
| rationalTerm | What4.Protocol.SMTWriter |
| RatPPIndex | What4.Expr.App |
| RatTerm | What4.Protocol.SMTLib2.Parse |
| RAV | What4.Utils.AbstractDomains |
| ravAdd | What4.Utils.AbstractDomains |
| ravCheckEq | What4.Utils.AbstractDomains |
| ravCheckLe | What4.Utils.AbstractDomains |
| ravConcreteRange | What4.Utils.AbstractDomains |
| ravIsInteger | What4.Utils.AbstractDomains |
| ravJoin | What4.Utils.AbstractDomains |
| ravMul | What4.Utils.AbstractDomains |
| ravRange | What4.Utils.AbstractDomains |
| ravScalarMul | What4.Utils.AbstractDomains |
| ravSingle | What4.Utils.AbstractDomains |
| ravUnbounded | What4.Utils.AbstractDomains |
| readAllLines | What4.Utils.HandleReader |
| readCheckSatResponse | What4.Protocol.SMTLib2.Parse |
| readDecimal | What4.Protocol.ReadDecimal |
| readGetModelResponse | What4.Protocol.SMTLib2.Parse |
| readNextLine | What4.Utils.HandleReader |
| Real | What4.Protocol.SMTLib2.Parse |
| realAbs | What4.Interface |
| RealAbstractValue | What4.Utils.AbstractDomains |
| realAdd | What4.Interface |
| RealATan2 | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realATan2 | What4.Protocol.SMTWriter |
| realAtan2 | What4.Interface |
| realCeil | What4.Interface |
| RealCos | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realCos | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| RealCosFn | What4.Expr.MATLAB |
| RealCosh | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realCosh | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| RealDiv | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realDiv | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| realEq | What4.Interface |
| RealExp | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realExp | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| RealExpr | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realExprAsInteger | What4.Interface |
| realFloor | What4.Interface |
| realGe | What4.Interface |
| realGt | What4.Interface |
| realHypot | What4.Interface |
| RealIsInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realIsInteger | What4.Protocol.SMTWriter |
| realIsNonNeg | What4.Interface |
| RealIsNonZeroFn | What4.Expr.MATLAB |
| realIte | What4.Interface |
| realLe | What4.Interface |
| realLit | What4.Interface |
| RealLog | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realLog | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| realLt | What4.Interface |
| realMax | What4.Interface |
| realMin | What4.Interface |
| realMod | What4.Interface |
| realMul | What4.Interface |
| realNe | What4.Interface |
| realNeg | What4.Interface |
| realOptSty | What4.Config |
| RealPart | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realPart | What4.Utils.Complex |
| RealPartOfCplxFn | What4.Expr.MATLAB |
| realPi | What4.Interface |
| realRound | What4.Interface |
| realRoundEven | What4.Interface |
| RealSeqFn | What4.Expr.MATLAB |
| RealSin | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realSin | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| RealSinFn | What4.Expr.MATLAB |
| RealSinh | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realSinh | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| realSort | What4.Protocol.SMTLib2.Syntax |
| realSq | What4.Interface |
| RealSqrt | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realSqrt | What4.Interface |
| realSub | What4.Interface |
| realSum | What4.Expr.Builder |
| realTan | What4.Interface |
| realTanh | What4.Interface |
| realToBV | What4.Interface |
| RealToComplexFn | What4.Expr.MATLAB |
| RealToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realToFloat | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| RealToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| realToInteger | What4.Interface |
| RealToIntegerFn | What4.Expr.MATLAB |
| realToNat | What4.Interface |
| realToSBV | What4.Interface |
| RealToSBVFn | What4.Expr.MATLAB |
| RealToUBVFn | What4.Expr.MATLAB |
| realTrunc | What4.Interface |
| RealTypeMap | What4.Protocol.SMTWriter |
| realWithMaxOptSty | What4.Config |
| realWithMinOptSty | What4.Config |
| realWithRangeOptSty | What4.Config |
| RealWorld | What4.Utils.MonadST |
| realZero | What4.Interface |
| recommended | What4.Utils.Versions |
| recordExprVars | What4.Expr.VarIdentification |
| reduceApp | What4.Expr.App |
| reduceIntSumMod | What4.Expr.WeightedSum |
| Refl | What4.BaseTypes, What4.Interface |
| removeVar | What4.Expr.BoolMap |
| renderTerm | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| reset | What4.Protocol.Online |
| resetAssertions | What4.Protocol.SMTLib2.Syntax |
| resetCommand | What4.Protocol.SMTWriter |
| resetDeclaredStructs | What4.Protocol.SMTWriter |
| resetEntryStack | What4.Protocol.SMTWriter |
| resolveSolverPath | What4.Utils.Process |
| returnMaybe | What4.Partial |
| returnPartial | What4.Partial |
| returnUnassigned | What4.Partial |
| reversePolarities | What4.Expr.BoolMap |
| RNA | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| RNE | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| rol | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| Root | What4.Protocol.PolyRoot |
| ror | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| rotateDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| rotateLeft | What4.Utils.Arithmetic |
| rotateRight | What4.Utils.Arithmetic |
| roundAway | What4.Utils.Arithmetic |
| RoundEvenReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| RoundingMode | |
| 1 (Data Constructor) | What4.Protocol.SMTLib2.Parse |
| 2 (Type/Class) | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| RoundReal | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| RTN | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| RTP | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| RTZ | What4.Utils.FloatHelpers, What4.Interface, What4.Protocol.SMTWriter |
| runAckAction | What4.Protocol.SMTWriter |
| runBoolectorInOverride | What4.Solver.Boolector, What4.Solver |
| runCheckSat | What4.Protocol.SMTLib2 |
| runCVC4InOverride | What4.Solver.CVC4, What4.Solver |
| runDRealInOverride | What4.Solver.DReal, What4.Solver |
| runExternalABCInOverride | What4.Solver.ExternalABC, What4.Solver |
| runInSandbox | What4.Protocol.SMTWriter |
| runPartialT | What4.Partial |
| runSolverInOverride | What4.Protocol.SMTLib2 |
| runSTPInOverride | What4.Solver.STP, What4.Solver |
| runVerilogM | What4.Protocol.VerilogWriter.AST |
| runYicesInOverride | What4.Solver.Yices, What4.Solver |
| runZ3InOverride | What4.Solver.Z3, What4.Solver |
| safeSymbol | What4.Symbol, What4.Interface |
| sameTerm | What4.Expr.App |
| SApp | What4.Protocol.SExp |
| Sat | What4.SatResult, What4.Solver |
| SAtom | What4.Protocol.SExp |
| satQueryError | What4.Interface |
| satQueryReason | What4.Interface |
| satQueryResult | What4.Interface |
| satQuerySolverName | What4.Interface |
| SatResponse | What4.Protocol.SMTLib2.Parse |
| SatResult | What4.SatResult, What4.Solver |
| sbBVDomainRangeLimit | What4.Expr.Builder |
| sbCacheStartSize | What4.Expr.Builder |
| sbMakeExpr | What4.Expr.Builder |
| sbNonceExpr | What4.Expr.Builder |
| sbounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| sbUnaryThreshold | What4.Expr.Builder |
| sbUserState | What4.Expr.Builder |
| SBVToFloat | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| sbvToFloat | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| SBVToInteger | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| sbvToInteger | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| SBVToIntegerFn | What4.Expr.MATLAB |
| sbvToReal | What4.Interface |
| scalarMul | What4.Expr.Builder |
| scale | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| 3 (Function) | What4.Expr.WeightedSum |
| scaledVar | What4.Expr.WeightedSum |
| scalMult | What4.Protocol.VerilogWriter.AST |
| sciLit | What4.Interface |
| Scope | What4.Expr.VarIdentification |
| sdiv | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| select | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain |
| SelectArray | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SemiRing | What4.SemiRing, What4.Expr |
| SemiRingBase | What4.SemiRing |
| semiRingBase | What4.SemiRing |
| SemiRingBV | What4.SemiRing |
| SemiRingBVRepr | What4.SemiRing, What4.Expr |
| SemiRingInteger | What4.SemiRing |
| SemiRingIntegerRepr | What4.SemiRing, What4.Expr |
| SemiRingLe | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SemiRingLiteral | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SemiRingProd | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SemiRingProduct | What4.Expr.WeightedSum |
| SemiRingReal | What4.SemiRing |
| SemiRingRealRepr | What4.SemiRing, What4.Expr |
| SemiRingRepr | What4.SemiRing, What4.Expr |
| SemiRingSum | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SemiRingView | What4.Expr.App |
| sendCheck | What4.Solver.Yices |
| sendCheckExistsForall | What4.Solver.Yices |
| Session | |
| 1 (Type/Class) | What4.Protocol.SMTLib2 |
| 2 (Data Constructor) | What4.Protocol.SMTLib2 |
| sessionResponse | What4.Protocol.SMTLib2 |
| sessionWriter | What4.Protocol.SMTLib2 |
| setCurrentProgramLoc | What4.Interface |
| setDefaultLogicAndOptions | What4.Protocol.SMTLib2 |
| setLogic | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| setOpt | What4.Config |
| setOptCommand | What4.Protocol.SMTWriter |
| setOption | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Config |
| 3 (Function) | What4.Protocol.SMTLib2 |
| setParam | What4.Solver.Yices |
| setProduceModels | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Protocol.SMTLib2 |
| setSolverLogListener | What4.Interface |
| setYicesParams | What4.Solver.Yices |
| set_opt_default | What4.Config |
| set_opt_onset | What4.Config |
| SExp | What4.Protocol.SExp |
| sext | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| 4 (Function) | What4.Expr.UnaryBV |
| SFloat | |
| 1 (Type/Class) | What4.SFloat |
| 2 (Data Constructor) | What4.SFloat |
| SFloatBinArith | What4.SFloat |
| SFloatRel | What4.SFloat |
| shl | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| shouldUnfold | What4.Interface |
| showPrettyArg | What4.Expr.App |
| shutdownSolver | What4.Protocol.SMTLib2 |
| shutdownSolverProcess | What4.Protocol.Online |
| signed | What4.Protocol.VerilogWriter.AST |
| signedBVBounds | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| signedClamp | What4.BaseTypes, What4.Interface |
| signedWideMultiplyBV | What4.Interface |
| SimpleWordMap | What4.WordMap |
| simplify | What4.Expr.Simplify |
| SingleFloat | What4.InterpretedFloatingPoint |
| SingleFloatRepr | What4.InterpretedFloatingPoint |
| SingleRange | What4.Utils.AbstractDomains, What4.Interface |
| singleRange | What4.Utils.AbstractDomains |
| singleton | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain.XOR |
| 5 (Function) | What4.Utils.BVDomain |
| 6 (Function) | What4.Utils.LeqMap |
| 7 (Function) | What4.Utils.Word16String |
| 8 (Function) | What4.Expr.ArrayUpdateMap |
| 9 (Function) | What4.Expr.StringSeq |
| size | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain |
| 5 (Function) | What4.Utils.LeqMap |
| 6 (Function) | What4.Expr.UnaryBV |
| skipSpaceOrNewline | What4.Protocol.SExp |
| slt | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| 3 (Function) | What4.Expr.UnaryBV |
| smokeTest | What4.Solver.Adapter, What4.Solver |
| smtAckResult | What4.Protocol.SMTLib2 |
| smtEvalBool | What4.Protocol.SMTWriter |
| smtEvalBV | What4.Protocol.SMTWriter |
| smtEvalBvArray | What4.Protocol.SMTWriter |
| SMTEvalBVArrayFn | What4.Protocol.SMTWriter |
| SMTEvalBVArrayWrapper | |
| 1 (Type/Class) | What4.Protocol.SMTWriter |
| 2 (Data Constructor) | What4.Protocol.SMTWriter |
| smtEvalFloat | What4.Protocol.SMTWriter |
| SMTEvalFunctions | |
| 1 (Type/Class) | What4.Protocol.SMTWriter |
| 2 (Data Constructor) | What4.Protocol.SMTWriter |
| smtEvalFuns | What4.Protocol.SMTWriter |
| smtEvalReal | What4.Protocol.SMTWriter |
| smtEvalString | What4.Protocol.SMTWriter |
| smtExprGroundEvalFn | What4.Protocol.SMTWriter |
| smtFnApp | What4.Protocol.SMTWriter |
| smtFnUpdate | What4.Protocol.SMTWriter |
| SMTInfoFlag | What4.Protocol.SMTLib2.Syntax |
| smtlib2arrayConstant | What4.Protocol.SMTLib2 |
| smtlib2arraySelect | What4.Protocol.SMTLib2 |
| smtlib2arrayType | What4.Protocol.SMTLib2 |
| smtlib2arrayUpdate | What4.Protocol.SMTLib2 |
| smtlib2declareStructCmd | What4.Protocol.SMTLib2 |
| SMTLib2Error | What4.Protocol.SMTLib2 |
| SMTLib2Exception | What4.Protocol.SMTLib2 |
| smtlib2exitCommand | What4.Protocol.SMTLib2 |
| SMTLib2GenericSolver | What4.Protocol.SMTLib2 |
| SMTLib2ParseError | What4.Protocol.SMTLib2 |
| smtlib2StringAppend | What4.Protocol.SMTLib2 |
| smtlib2StringContains | What4.Protocol.SMTLib2 |
| smtlib2StringIndexOf | What4.Protocol.SMTLib2 |
| smtlib2StringIsPrefixOf | What4.Protocol.SMTLib2 |
| smtlib2StringIsSuffixOf | What4.Protocol.SMTLib2 |
| smtlib2StringLength | What4.Protocol.SMTLib2 |
| smtlib2StringSort | What4.Protocol.SMTLib2 |
| smtlib2StringSubstring | What4.Protocol.SMTLib2 |
| smtlib2StringTerm | What4.Protocol.SMTLib2 |
| smtlib2StructCtor | What4.Protocol.SMTLib2 |
| smtlib2StructProj | What4.Protocol.SMTLib2 |
| smtlib2StructSort | What4.Protocol.SMTLib2 |
| SMTLib2Tweaks | What4.Protocol.SMTLib2 |
| smtlib2tweaks | What4.Protocol.SMTLib2 |
| SMTLib2Unsupported | What4.Protocol.SMTLib2 |
| smtLibEvalFuns | What4.Protocol.SMTLib2 |
| SMTReadWriter | What4.Protocol.SMTWriter |
| smtSatResult | What4.Protocol.SMTWriter |
| smtUnsatAssumptionsResult | What4.Protocol.SMTWriter |
| smtUnsatCoreResult | What4.Protocol.SMTWriter |
| SMTWriter | What4.Protocol.SMTWriter |
| smtWriterName | What4.Protocol.SMTWriter |
| SolverAdapter | |
| 1 (Type/Class) | What4.Solver.Adapter, What4.Solver |
| 2 (Data Constructor) | What4.Solver.Adapter, What4.Solver |
| solverAdapterOptions | What4.Solver.Adapter, What4.Solver |
| SolverBounds | |
| 1 (Type/Class) | What4.Utils.Versions |
| 2 (Data Constructor) | What4.Utils.Versions |
| solverCleanupCallback | What4.Protocol.Online |
| solverConn | What4.Protocol.Online |
| solverEarlyUnsat | What4.Protocol.Online |
| SolverEndSATQuery | What4.Interface |
| solverErrorBehavior | What4.Protocol.Online |
| solverEvalFuns | What4.Protocol.Online |
| SolverEvent | What4.Interface |
| SolverGoalTimeout | |
| 1 (Type/Class) | What4.Protocol.Online |
| 2 (Data Constructor) | What4.Protocol.Online |
| solverGoalTimeout | What4.Protocol.Online |
| solverHandle | What4.Protocol.Online |
| solverLogFn | What4.Protocol.Online |
| solverName | What4.Protocol.Online |
| SolverProcess | |
| 1 (Type/Class) | What4.Protocol.Online |
| 2 (Data Constructor) | What4.Protocol.Online |
| solverResponse | What4.Protocol.Online |
| SolverStartSATQuery | What4.Interface |
| solverStderr | What4.Protocol.Online |
| solverStdin | What4.Protocol.Online |
| solverSupportsResetAssertions | What4.Protocol.Online |
| SolverSymbol | What4.Symbol, What4.Interface |
| solverSymbolAsText | What4.Symbol |
| SolverSymbolError | What4.Symbol |
| solver_adapter_check_sat | What4.Solver.Adapter, What4.Solver |
| solver_adapter_config_options | What4.Solver.Adapter, What4.Solver |
| solver_adapter_name | What4.Solver.Adapter, What4.Solver |
| solver_adapter_write_smt2 | What4.Solver.Adapter, What4.Solver |
| Some | What4.BaseTypes, What4.Interface |
| someNat | What4.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 |
| SourcePos | What4.ProgramLoc |
| sourcePos | What4.ProgramLoc |
| splitEntry | What4.Utils.LeqMap |
| splitLeq | What4.Utils.LeqMap |
| SplitPPExprList | What4.Expr.App |
| srem | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| sr_compare | What4.SemiRing |
| SR_Constant | What4.Expr.App |
| SR_General | What4.Expr.App |
| sr_hashWithSalt | What4.SemiRing |
| SR_Prod | What4.Expr.App |
| SR_Sum | What4.Expr.App |
| SString | What4.Protocol.SExp |
| ST | What4.Utils.MonadST |
| startCaching | What4.Expr.Builder |
| startFunctionName | What4.FunctionName |
| startHandleReader | What4.Utils.HandleReader, What4.Solver.Yices |
| startOfFile | What4.ProgramLoc |
| startProcess | What4.Utils.Process |
| startSolver | What4.Protocol.SMTLib2 |
| startSolverProcess | What4.Protocol.Online |
| statAllocs | What4.Interface |
| Statistics | |
| 1 (Type/Class) | What4.Interface |
| 2 (Data Constructor) | What4.Interface |
| statNonLinearOps | What4.Interface |
| stopCaching | What4.Expr.Builder |
| stopHandleReader | What4.Utils.HandleReader |
| store | What4.Protocol.SMTLib2.Syntax |
| StoreTerm | What4.Protocol.SMTLib2.Parse |
| STP | |
| 1 (Type/Class) | What4.Solver.STP, What4.Solver |
| 2 (Data Constructor) | What4.Solver.STP, What4.Solver |
| stpAdapter | What4.Solver.STP, What4.Solver |
| stpFeatures | What4.Solver.STP, What4.Solver |
| stpOptions | What4.Solver.STP, What4.Solver |
| stpPath | What4.Solver.STP, What4.Solver |
| streamLines | What4.Utils.HandleReader |
| StringAbs | What4.Utils.AbstractDomains |
| stringAbsConcat | What4.Utils.AbstractDomains |
| stringAbsContains | What4.Utils.AbstractDomains |
| stringAbsEmpty | What4.Utils.AbstractDomains |
| stringAbsIndexOf | What4.Utils.AbstractDomains |
| stringAbsIsPrefixOf | What4.Utils.AbstractDomains |
| stringAbsIsSuffixOf | What4.Utils.AbstractDomains |
| stringAbsJoin | What4.Utils.AbstractDomains |
| stringAbsLength | What4.Utils.AbstractDomains |
| stringAbsOverlap | What4.Utils.AbstractDomains |
| stringAbsSingle | What4.Utils.AbstractDomains |
| stringAbsSubstring | What4.Utils.AbstractDomains |
| stringAbsTop | What4.Utils.AbstractDomains |
| StringAbstractValue | What4.Utils.AbstractDomains |
| StringAppend | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringAppend | What4.Protocol.SMTWriter |
| stringConcat | What4.Interface |
| StringContains | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringContains | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| stringEmpty | What4.Interface |
| stringEq | What4.Interface |
| StringExpr | |
| 1 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| 2 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| StringIndexOf | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringIndexOf | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| StringInfo | What4.BaseTypes, What4.Interface |
| stringInfo | What4.Interface |
| StringInfoRepr | What4.BaseTypes, What4.Interface |
| StringIsPrefixOf | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringIsPrefixOf | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| StringIsSuffixOf | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringIsSuffixOf | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| stringIte | What4.Interface |
| StringLength | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringLength | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| stringLit | What4.Interface |
| stringLitBounds | What4.Utils.StringLiteral |
| stringLitContains | What4.Utils.StringLiteral |
| stringLitEmpty | What4.Utils.StringLiteral |
| StringLiteral | What4.Utils.StringLiteral, What4.Interface |
| stringLiteralInfo | What4.Utils.StringLiteral, What4.Interface |
| stringLitIndexOf | What4.Utils.StringLiteral |
| stringLitIsPrefixOf | What4.Utils.StringLiteral |
| stringLitIsSuffixOf | What4.Utils.StringLiteral |
| stringLitLength | What4.Utils.StringLiteral |
| stringLitNull | What4.Utils.StringLiteral |
| stringLitSubstring | What4.Utils.StringLiteral |
| stringOptSty | What4.Config |
| stringPPExpr | What4.Expr.App |
| stringPrettyArg | What4.Expr.App |
| StringSeq | What4.Expr.StringSeq |
| stringSeqAbs | What4.Expr.StringSeq |
| StringSeqEntry | What4.Expr.StringSeq |
| StringSeqLiteral | What4.Expr.StringSeq |
| StringSeqTerm | What4.Expr.StringSeq |
| StringSubstring | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| stringSubstring | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.Protocol.SMTWriter |
| stringTerm | What4.Protocol.SMTWriter |
| StringTheory | What4.Expr.AppTheory, What4.Expr |
| stringToSExp | What4.Protocol.SExp |
| StructCtor | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| structCtor | What4.Protocol.SMTWriter |
| structEq | What4.Interface |
| StructField | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| structField | What4.Interface |
| structIte | What4.Interface |
| structProj | What4.Protocol.SMTWriter |
| StructTheory | What4.Expr.AppTheory, What4.Expr |
| StructTypeMap | What4.Protocol.SMTWriter |
| sub | What4.Protocol.SMTLib2.Syntax |
| subNat | What4.BaseTypes, What4.Interface |
| subSignedOF | What4.Interface |
| subUnsignedOF | What4.Interface |
| sumAbsValue | What4.Expr.WeightedSum |
| sumExpr | What4.Protocol.SMTWriter |
| sumOffset | What4.Expr.WeightedSum |
| sumRepr | What4.Expr.WeightedSum |
| supportedFeatures | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2 |
| supportFunctionArguments | What4.Protocol.SMTWriter |
| supportFunctionDefs | What4.Protocol.SMTWriter |
| supportQuantifiers | What4.Protocol.SMTWriter |
| supportsResetAssertions | What4.Protocol.SMTLib2 |
| SupportTermOps | What4.Protocol.SMTWriter |
| SWord | What4.SWord |
| SymAnnotation | What4.Interface |
| SymArray | What4.Interface |
| Symbol | |
| 1 (Type/Class) | What4.Protocol.SMTLib2.Parse |
| 2 (Type/Class) | What4.Protocol.SMTLib2.Syntax |
| SymbolBinding | What4.Expr.Builder |
| SymbolTerm | What4.Protocol.SMTLib2.Parse |
| SymbolVarBimap | What4.Expr.Builder |
| SymBV | What4.Interface |
| SymCplx | What4.Interface |
| SymEncoder | |
| 1 (Type/Class) | What4.Interface |
| 2 (Data Constructor) | What4.Interface |
| symEncoderType | What4.Interface |
| SymExpr | What4.Interface, What4.Expr.Builder |
| SymFloat | What4.Interface |
| SymFn | What4.Interface |
| symFnArgTypes | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFnId | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| SymFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFnLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFnName | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFnReturnType | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| symFromExpr | What4.Interface |
| SymInteger | What4.Interface |
| SymInterpretedFloat | What4.InterpretedFloatingPoint |
| SymInterpretedFloatType | What4.InterpretedFloatingPoint |
| SymNat | What4.Interface |
| SymReal | What4.Interface |
| SymString | What4.Interface |
| SymStruct | What4.Interface |
| symToExpr | What4.Interface |
| sym_evaluate | What4.Expr.UnaryBV |
| systemSymbol | What4.Symbol |
| T | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| take | What4.Utils.Word16String |
| teeInputStream | What4.Utils.HandleReader |
| teeOutputStream | What4.Utils.HandleReader |
| Term | |
| 1 (Type/Class) | What4.Protocol.SMTLib2.Parse |
| 2 (Type/Class) | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| 3 (Type/Class) | What4.Protocol.SMTWriter |
| termIntegerToReal | What4.Protocol.SMTWriter |
| termRealToInteger | What4.Protocol.SMTWriter |
| term_app | What4.Protocol.SMTLib2.Syntax |
| testBit | |
| 1 (Function) | What4.Utils.BVDomain.Bitwise |
| 2 (Function) | What4.Utils.BVDomain |
| testBitBV | What4.Interface |
| TestEquality | What4.BaseTypes, What4.Interface |
| testEquality | What4.BaseTypes, What4.Interface |
| testExprSymFnEq | What4.Expr.App |
| testLeq | What4.BaseTypes, What4.Interface |
| testNatCases | What4.BaseTypes, What4.Interface |
| testSolverFnEq | What4.Expr.MATLAB |
| testStrictLeq | What4.BaseTypes, What4.Interface |
| textPPExpr | What4.Expr.App |
| Tm | What4.Expr.WeightedSum |
| toBaseTypeRepr | What4.Utils.OnlyIntRepr |
| toDescList | What4.Utils.LeqMap |
| toIncrHash | What4.Utils.IncrHash |
| toIncrHashWithSalt | What4.Utils.IncrHash |
| toInt | What4.Protocol.SMTLib2.Syntax |
| toLEByteString | What4.Utils.Word16String |
| toList | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.LeqMap |
| 3 (Function) | What4.Expr.ArrayUpdateMap |
| 4 (Function) | What4.Expr.StringSeq |
| toMap | What4.Expr.ArrayUpdateMap |
| toNativeProperty | Test.Verification |
| toReal | What4.Protocol.SMTLib2.Syntax |
| toRoundMode | What4.Utils.FloatHelpers |
| toSigned | What4.BaseTypes, What4.Interface |
| toUnsigned | What4.BaseTypes, What4.Interface |
| transformSum | What4.Expr.WeightedSum |
| traverseApp | What4.Expr.App, What4.Expr.Builder |
| traverseArrayResultWrapper | What4.Expr.App |
| traverseArrayResultWrapperAssignment | What4.Expr.App |
| traverseArrayUpdateMap | What4.Expr.ArrayUpdateMap |
| traverseBVOrSet | What4.Expr.App, What4.Expr.Builder |
| traverseCoeffs | What4.Expr.WeightedSum |
| traverseMatlabSolverFn | What4.Expr.MATLAB |
| traverseMaybeWithKey | What4.Utils.AnnotatedMap |
| traversePreds | What4.Expr.UnaryBV |
| traverseProdVars | What4.Expr.WeightedSum |
| traverseSatResult | What4.SatResult, What4.Solver |
| traverseStringSeq | What4.Expr.StringSeq |
| traverseVars | |
| 1 (Function) | What4.Expr.BoolMap |
| 2 (Function) | What4.Expr.WeightedSum |
| true | What4.Protocol.SMTLib2.Syntax |
| truePred | What4.Interface |
| trunc | What4.Expr.UnaryBV |
| tryComplexSqrt | What4.Utils.Complex |
| tryEvalGroundExpr | What4.Expr.GroundEval |
| tryIntSqrt | What4.Utils.Arithmetic |
| tryMagnitude | What4.Utils.Complex |
| tryRationalSqrt | What4.Utils.Arithmetic |
| trySetOpt | What4.Config |
| typeDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| TypeMap | What4.Protocol.SMTWriter |
| typeMap | What4.Protocol.SMTWriter |
| typeTheory | What4.Expr.AppTheory |
| ubounds | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| udiv | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| uext | What4.Expr.UnaryBV |
| uintSetWidth | What4.Interface |
| UIntSetWidthFn | What4.Expr.MATLAB |
| uintToInt | What4.Interface |
| UIntToIntFn | What4.Expr.MATLAB |
| uintToReal | What4.Interface |
| ult | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| 3 (Function) | What4.Expr.UnaryBV |
| UnaryBV | What4.Expr.UnaryBV, What4.Expr |
| unaryThresholdOption | What4.Expr.Builder |
| Unassigned | What4.Partial |
| Unbounded | |
| 1 (Data Constructor) | What4.Utils.AbstractDomains |
| 2 (Data Constructor) | What4.Config |
| unboundedRange | What4.Utils.AbstractDomains |
| unconstrainedAbsValue | What4.Expr.App |
| unEvalBVArrayWrapper | What4.Protocol.SMTWriter |
| UnfoldConcrete | What4.Interface |
| UnfoldPolicy | What4.Interface |
| unGVW | What4.Expr.GroundEval, What4.Expr |
| Unicode | What4.BaseTypes, What4.Interface |
| UnicodeLiteral | What4.Utils.StringLiteral, What4.Interface |
| UnicodeRepr | What4.BaseTypes, What4.Interface |
| uninterpConstants | What4.Expr.VarIdentification |
| UninterpFnInfo | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| UninterpVarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| union | |
| 1 (Function) | What4.Utils.AnnotatedMap |
| 2 (Function) | What4.Utils.BVDomain.Arith |
| 3 (Function) | What4.Utils.BVDomain.Bitwise |
| 4 (Function) | What4.Utils.BVDomain |
| 5 (Function) | What4.Utils.LeqMap |
| unionWith | What4.Utils.AnnotatedMap |
| unionWithKeyMaybe | What4.Utils.AnnotatedMap |
| Unknown | What4.SatResult, What4.Solver |
| UnknownResponse | What4.Protocol.SMTLib2.Parse |
| unknowns | What4.Utils.BVDomain.Arith |
| Unop | |
| 1 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| 2 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| unop | What4.Protocol.VerilogWriter.AST |
| unopDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| unPartial | What4.Partial |
| Unsat | What4.SatResult, What4.Solver |
| UnsatResponse | What4.Protocol.SMTLib2.Parse |
| unsignedBVBounds | |
| 1 (Function) | What4.Interface |
| 2 (Function) | What4.SWord |
| unsignedClamp | What4.BaseTypes, What4.Interface |
| unsignedEntries | What4.Expr.UnaryBV |
| unsignedRanges | What4.Expr.UnaryBV |
| unsignedWideMultiplyBV | What4.Interface |
| unSort | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2 |
| UnsupportedFloat | |
| 1 (Type/Class) | What4.SFloat |
| 2 (Data Constructor) | What4.SFloat |
| unWrap | What4.Expr.BoolMap |
| unwrapArrayResult | What4.Interface, What4.Expr.Builder |
| unwrapAV | What4.Utils.AbstractDomains |
| unwrapCV | What4.Utils.AbstractDomains |
| un_app | What4.Protocol.SMTLib2.Syntax |
| UpdateArray | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| upper | What4.Utils.Versions |
| urem | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain |
| useBitvectors | What4.ProblemFeatures |
| useComputableReals | What4.ProblemFeatures |
| useExistForall | What4.ProblemFeatures |
| useFloatingPoint | What4.ProblemFeatures |
| useIntegerArithmetic | What4.ProblemFeatures |
| useLinearArithmetic | What4.ProblemFeatures |
| useNonlinearArithmetic | What4.ProblemFeatures |
| useQuantifiers | What4.ProblemFeatures |
| userSymbol | What4.Symbol, What4.Interface |
| useStrings | What4.ProblemFeatures |
| useStructs | What4.ProblemFeatures |
| useSymbolicArrays | What4.ProblemFeatures |
| useUnsatAssumptions | What4.ProblemFeatures |
| useUnsatCores | What4.ProblemFeatures |
| ValueBound | What4.Utils.AbstractDomains |
| ValueRange | What4.Utils.AbstractDomains, What4.Interface |
| valueRange | What4.Utils.AbstractDomains |
| var | |
| 1 (Function) | What4.Expr.BoolMap |
| 2 (Function) | What4.Expr.WeightedSum |
| varErrors | What4.Expr.VarIdentification |
| varExpr | What4.Interface |
| VarKind | What4.Expr.App, What4.Expr.Builder, What4.Expr |
| VarRecorder | What4.Expr.VarIdentification |
| varSort | What4.Protocol.SMTLib2.Syntax |
| VarSymbolBinding | What4.Expr.Builder |
| ver | What4.Utils.Versions |
| verbosity | What4.Config |
| verbosityLogger | What4.Config |
| Verifiable | Test.Verification |
| verifying | Test.Verification |
| VerilogM | |
| 1 (Type/Class) | What4.Protocol.VerilogWriter.AST |
| 2 (Data Constructor) | What4.Protocol.VerilogWriter.AST |
| Version | What4.Protocol.SMTLib2.Syntax |
| versionResult | What4.Protocol.SMTLib2 |
| viewBoolMap | What4.Expr.BoolMap |
| viewSemiRing | What4.Expr.App |
| vsBoolCache | What4.Protocol.VerilogWriter.AST |
| vsBVCache | What4.Protocol.VerilogWriter.AST |
| vsExpCache | What4.Protocol.VerilogWriter.AST |
| vsFreshIdent | What4.Protocol.VerilogWriter.AST |
| vsInputs | What4.Protocol.VerilogWriter.AST |
| vsOutputs | What4.Protocol.VerilogWriter.AST |
| vsSym | What4.Protocol.VerilogWriter.AST |
| vsWires | What4.Protocol.VerilogWriter.AST |
| WeightedSum | What4.Expr.WeightedSum, What4.Expr |
| What4 | What4.Panic |
| width | What4.Expr.UnaryBV |
| widthVal | What4.BaseTypes, What4.Interface |
| Wire | What4.Protocol.VerilogWriter.AST |
| wireDoc | What4.Protocol.VerilogWriter.ABCVerilog |
| withAbstractable | What4.Utils.AbstractDomains |
| withAddLeq | What4.BaseTypes, What4.Interface |
| withAddMulDistribRight | What4.BaseTypes, What4.Interface |
| withAddPrefixLeq | What4.BaseTypes, What4.Interface |
| withBoolector | What4.Solver.Boolector, What4.Solver |
| withCVC4 | What4.Solver.CVC4, What4.Solver |
| withDivModNat | What4.BaseTypes, What4.Interface |
| withHandleReader | What4.Utils.HandleReader |
| withKnownNat | What4.BaseTypes, What4.Interface |
| withLeqProof | What4.BaseTypes, What4.Interface |
| withProcessHandles | What4.Utils.Process |
| withSolver | What4.Protocol.SMTLib2 |
| withSTP | What4.Solver.STP, What4.Solver |
| withSubMulDistribRight | What4.BaseTypes, What4.Interface |
| withZ3 | What4.Solver.Z3, What4.Solver |
| Word16String | What4.Utils.Word16String |
| WordMap | What4.WordMap |
| Wrap | |
| 1 (Type/Class) | What4.Expr.BoolMap |
| 2 (Data Constructor) | What4.Expr.BoolMap |
| writeABCSMT2File | What4.Solver.ExternalABC, What4.Solver |
| writeCheckSat | What4.Protocol.SMTLib2 |
| writeCommand | What4.Protocol.SMTWriter |
| writeCVC4SMT2File | What4.Solver.CVC4, What4.Solver |
| writeDefaultSMT2 | What4.Protocol.SMTLib2 |
| writeDRealSMT2File | What4.Solver.DReal, What4.Solver |
| writeExit | What4.Protocol.SMTLib2 |
| writeGetValue | What4.Protocol.SMTLib2 |
| writeMultiAsmpCVC4SMT2File | What4.Solver.CVC4 |
| Writer | What4.Protocol.SMTLib2 |
| WriterConn | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2 |
| writeYicesFile | What4.Solver.Yices, What4.Solver |
| writeZ3SMT2File | What4.Solver.Z3 |
| X86_80Float | What4.InterpretedFloatingPoint |
| X86_80FloatRepr | What4.InterpretedFloatingPoint |
| X86_80Val | |
| 1 (Type/Class) | What4.InterpretedFloatingPoint |
| 2 (Data Constructor) | What4.InterpretedFloatingPoint |
| Xor | What4.Protocol.VerilogWriter.AST |
| xor | |
| 1 (Function) | What4.Protocol.SMTLib2.Syntax |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain.XOR |
| 4 (Function) | What4.Utils.BVDomain |
| xorPred | What4.Interface |
| xorToBitwiseDomain | What4.Utils.BVDomain |
| yicesAdapter | What4.Solver.Yices, What4.Solver |
| yicesDefaultFeatures | What4.Solver.Yices, What4.Solver |
| yicesEnableInteractive | What4.Solver.Yices |
| yicesEnableMCSat | What4.Solver.Yices |
| YicesError | What4.Solver.Yices |
| yicesEvalBool | What4.Solver.Yices |
| YicesException | What4.Solver.Yices |
| yicesGoalTimeout | What4.Solver.Yices |
| yicesOptions | What4.Solver.Yices, What4.Solver |
| YicesParseError | What4.Solver.Yices |
| yicesPath | What4.Solver.Yices, What4.Solver |
| yicesType | What4.Solver.Yices |
| YicesUnsupported | What4.Solver.Yices |
| Z3 | |
| 1 (Type/Class) | What4.Solver.Z3, What4.Solver |
| 2 (Data Constructor) | What4.Solver.Z3, What4.Solver |
| z3Adapter | What4.Solver.Z3, What4.Solver |
| z3Features | What4.Solver.Z3, What4.Solver |
| z3Options | What4.Solver.Z3, What4.Solver |
| z3Path | What4.Solver.Z3, What4.Solver |
| z3Timeout | What4.Solver.Z3 |
| ZBV | What4.SWord |
| zero | What4.SemiRing |
| ZeroNat | What4.BaseTypes, What4.Interface |
| zeroStatistics | What4.Interface |
| zext | |
| 1 (Function) | What4.Utils.BVDomain.Arith |
| 2 (Function) | What4.Utils.BVDomain.Bitwise |
| 3 (Function) | What4.Utils.BVDomain |
| _labeledPred | What4.LabeledPred |
| _labeledPredMsg | What4.LabeledPred |
| _partialPred | What4.Partial |
| _partialValue | What4.Partial |
| _stringAbsLength | What4.Utils.AbstractDomains |