abs | What4.Protocol.SMTLib2.Syntax |
absAnd | What4.Utils.AbstractDomains |
absOr | What4.Utils.AbstractDomains |
Abstractable | What4.Utils.AbstractDomains |
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 |
addIsLeq | What4.BaseTypes, What4.Interface |
addIsLeqLeft1 | What4.BaseTypes, What4.Interface |
addMulDistribRight | What4.BaseTypes, What4.Interface |
addNat | What4.BaseTypes, What4.Interface |
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 |
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 | |
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.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 |
App | What4.Expr.Builder, What4.Expr |
app | What4.Protocol.SMTWriter |
append | |
1 (Function) | What4.Utils.Word16String |
2 (Function) | What4.Expr.StringSeq |
AppExpr | |
1 (Data Constructor) | What4.Expr.Builder, What4.Expr |
2 (Type/Class) | What4.Expr.Builder, What4.Expr |
appExprApp | What4.Expr.Builder, What4.Expr |
appExprId | What4.Expr.Builder, What4.Expr |
appExprLoc | What4.Expr.Builder, What4.Expr |
applySymFn | What4.Interface |
approximate | What4.Protocol.PolyRoot |
AppTheory | What4.Expr.AppTheory, What4.Expr |
appTheory | What4.Expr.AppTheory, What4.Expr |
appType | 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.Builder, What4.Expr |
arrayFromFn | What4.Interface |
arrayFromMap | What4.Interface |
arrayIte | What4.Interface |
arrayLookup | What4.Interface |
ArrayMap | 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.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.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.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.Builder |
ashr | |
1 (Function) | What4.Utils.BVDomain.Arith |
2 (Function) | What4.Utils.BVDomain.Bitwise |
3 (Function) | What4.Utils.BVDomain |
asInteger | What4.Interface |
asNat | What4.Interface |
asNegAtomList | What4.Protocol.SExp |
asNonceApp | What4.Expr.Builder |
asProdVar | What4.Expr.WeightedSum |
asRational | What4.Interface |
assert | What4.Protocol.SMTLib2.Syntax |
assertCommand | What4.Protocol.SMTWriter |
assertForall | What4.Solver.Yices |
assertNamed | What4.Protocol.SMTLib2.Syntax |
assertNamedCommand | What4.Protocol.SMTWriter |
asSingleNatRange | What4.Utils.AbstractDomains |
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 |
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 |