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

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

Index - A

A | What4.Serialize.Printer
abcOptions | What4.Solver.ExternalABC, What4.Solver
abcPath | What4.Solver.ExternalABC, What4.Solver
ABool | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
abs | What4.Protocol.SMTLib2.Syntax
absAnd | What4.Utils.AbstractDomains
absOr | What4.Utils.AbstractDomains
Abstractable | What4.Utils.AbstractDomains
abstractEval | What4.Expr.App
AbstractValue | What4.Utils.AbstractDomains
AbstractValueWrapper |
1 (Type/Class) | What4.Utils.AbstractDomains
2 (Data Constructor) | What4.Utils.AbstractDomains
ABV | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AckAction | What4.Protocol.SMTWriter
AckError | What4.Protocol.SMTLib2.Response
AckFail | What4.Protocol.SMTLib2.Response
AckInfeasible | What4.Protocol.SMTLib2.Response
AcknowledgementAction | What4.Protocol.SMTWriter
AckSat | What4.Protocol.SMTLib2.Response
AckSkipped | What4.Protocol.SMTLib2.Response
AckSuccess | What4.Protocol.SMTLib2.Response
AckSuccessSExp | What4.Protocol.SMTLib2.Response
AckUnknown | What4.Protocol.SMTLib2.Response
AckUnsat | What4.Protocol.SMTLib2.Response
AckUnsupported | What4.Protocol.SMTLib2.Response
add |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.SemiRing
3 (Function) | What4.Utils.BVDomain.Arith
4 (Function) | What4.Utils.BVDomain
5 (Function) | What4.Expr.WeightedSum
6 (Function) | What4.Expr.UnaryBV
addBoundInput | What4.Protocol.VerilogWriter.AST
addCommand | What4.Protocol.SMTWriter, What4.Solver.Yices
addCommandNoAck | What4.Protocol.SMTWriter
addCommands | What4.Protocol.SMTWriter
addCondition | What4.Partial
addConstant | What4.Expr.WeightedSum
addConstraint | What4.Protocol.SMTWriter
addDeclareVar | What4.Protocol.SMTWriter
addFreshInput | What4.Protocol.VerilogWriter.AST
addFreshWire | What4.Protocol.VerilogWriter.AST
addIsLeq | What4.BaseTypes, What4.Interface
addIsLeqLeft1 | What4.BaseTypes, What4.Interface
addMulDistribRight | What4.BaseTypes, What4.Interface
addNat | What4.BaseTypes, What4.Interface
addOutput | What4.Protocol.VerilogWriter.AST
addPrefixIsLeq | What4.BaseTypes, What4.Interface
addRange | What4.Utils.AbstractDomains
addSignedOF | What4.Interface
addSynthFun | What4.Protocol.SMTWriter
addUnsignedOF | What4.Interface
addVar |
1 (Function) | What4.Expr.BoolMap
2 (Function) | What4.Expr.WeightedSum
addVars | What4.Expr.WeightedSum
addWire | What4.Protocol.VerilogWriter.AST
AFloat | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AId | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
AInt | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
allLogic | What4.Protocol.SMTLib2.Syntax
allSupported | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
allTrueEntries | What4.Interface
all_supported | What4.Protocol.SMTLib2
alter | What4.Utils.AnnotatedMap
alterF | What4.Utils.AnnotatedMap
AlwaysUnfold | What4.Interface
ANat | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
And | What4.Protocol.VerilogWriter.AST
and |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
andAll | What4.Protocol.SMTWriter
andAllOf | What4.Interface
andPred | What4.Interface
and_scalar | What4.Utils.BVDomain.XOR
AnnotatedMap | What4.Utils.AnnotatedMap
annotateTerm | What4.Interface
Annotation | What4.Expr.App, What4.Expr.Builder, What4.Expr
annotation | What4.Utils.AnnotatedMap
AnOnlineSolver |
1 (Type/Class) | What4.Protocol.Online
2 (Data Constructor) | What4.Protocol.Online
any |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
APE | What4.Expr.App
apeDoc | What4.Expr.App
apeExprs | What4.Expr.App
apeIndex | What4.Expr.App
apeLength | What4.Expr.App
apeLoc | What4.Expr.App
apeName | What4.Expr.App
App | What4.Expr.App, What4.Expr.Builder, What4.Expr
app | What4.Protocol.SMTWriter
append |
1 (Function) | What4.Utils.Word16String
2 (Function) | What4.Expr.StringSeq
appEqF | What4.Expr.App
AppExpr |
1 (Data Constructor) | What4.Expr.App, What4.Expr.Builder, What4.Expr
2 (Type/Class) | What4.Expr.App, What4.Expr.Builder, What4.Expr
appExpr | What4.Expr.Allocator
appExprAbsValue | What4.Expr.App
appExprApp | What4.Expr.App, What4.Expr.Builder, What4.Expr
AppExprCtor | What4.Expr.App
appExprId | What4.Expr.App, What4.Expr.Builder, What4.Expr
appExprLoc | What4.Expr.App, What4.Expr.Builder, What4.Expr
applySymFn | What4.Interface
AppPPExpr |
1 (Data Constructor) | What4.Expr.App
2 (Type/Class) | What4.Expr.App
approximate | What4.Protocol.PolyRoot
AppTheory | What4.Expr.AppTheory, What4.Expr
appTheory | What4.Expr.AppTheory, What4.Expr
appType | What4.Expr.App, What4.Expr.Builder
app_list | What4.Protocol.SMTWriter
Arccos | What4.SpecialFunctions
Arccosh | What4.SpecialFunctions
Arcsin | What4.SpecialFunctions
Arcsinh | What4.SpecialFunctions
Arctan | What4.SpecialFunctions
Arctan2 | What4.SpecialFunctions
Arctanh | What4.SpecialFunctions
AReal | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
arithDomainData | What4.Utils.BVDomain.Arith, What4.Utils.BVDomain
arithToXorDomain | What4.Utils.BVDomain
Array | What4.Protocol.SMTLib2.Parse
ArrayConcrete | What4.Expr.GroundEval, What4.Expr
arrayConst |
1 (Function) | What4.Protocol.SMTLib2.Syntax
2 (Function) | What4.Protocol.SMTLib2
arrayConstant | What4.Protocol.SMTWriter
ArrayConstantFn | What4.Protocol.SMTWriter
arrayCopy | What4.Interface
arrayEq | What4.Interface
ArrayFromFn | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayFromFn | What4.Interface
arrayFromMap | What4.Interface
arrayIte | What4.Interface
arrayLookup | What4.Interface
ArrayMap | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayMap | What4.Interface
ArrayMapping | What4.Expr.GroundEval, What4.Expr
arrayRangeEq | What4.Interface
ArrayResultWrapper |
1 (Type/Class) | What4.Interface, What4.Expr.Builder
2 (Data Constructor) | What4.Interface, What4.Expr.Builder
arraySelect |
1 (Function) | What4.Protocol.SMTWriter
2 (Function) | What4.Protocol.SMTLib2
arraySet | What4.Interface
arraySort | What4.Protocol.SMTLib2.Syntax, What4.Protocol.SMTLib2
arrayStore | What4.Protocol.SMTLib2
ArrayTheory | What4.Expr.AppTheory, What4.Expr
ArrayTrueOnEntries | What4.Expr.App, What4.Expr.Builder, What4.Expr
arrayTrueOnEntries | What4.Interface
arrayTypeIndices | What4.BaseTypes, What4.Interface
arrayTypeResult | What4.BaseTypes, What4.Interface
arrayUpdate |
1 (Function) | What4.Interface
2 (Function) | What4.Protocol.SMTWriter
arrayUpdateAbs | What4.Expr.ArrayUpdateMap
arrayUpdateAtIdxLits | What4.Interface
ArrayUpdateMap | What4.Expr.ArrayUpdateMap
asAffineVar |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Interface
asApp | What4.Expr.App, What4.Expr.Builder
asArithDomain | What4.Utils.BVDomain
asAtomList | What4.Protocol.SExp
asBitwiseDomain | What4.Utils.BVDomain
asBV | What4.Interface
asComplex | What4.Interface
asConcrete | What4.Interface
asConjunction | What4.Expr.App, What4.Expr.Builder
AsConst | What4.Protocol.SMTLib2.Parse
asConstant |
1 (Function) | What4.Expr.WeightedSum
2 (Function) | What4.Expr.UnaryBV
asConstantArray | What4.Interface
asConstantPred | What4.Interface
asDisjunction | What4.Expr.App, What4.Expr.Builder
asFloat | What4.Interface
ashr |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain
asInteger | What4.Interface
asMatlabSolverFn | What4.Expr.App
asNat | What4.Interface
asNegAtom | What4.Expr.App
asNegAtomList | What4.Protocol.SExp
asNonceApp | What4.Expr.App, What4.Expr.Builder
asPosAtom | What4.Expr.App
asProdVar | What4.Expr.WeightedSum
asRational | What4.Interface
asSemiRingLit | What4.Expr.App
asSemiRingProd | What4.Expr.App
asSemiRingSum | What4.Expr.App
assert | What4.Protocol.SMTLib2.Syntax
assertCommand | What4.Protocol.SMTWriter
assertForall | What4.Solver.Yices
assertNamed | What4.Protocol.SMTLib2.Syntax
assertNamedCommand | What4.Protocol.SMTWriter
Assign | What4.Protocol.VerilogWriter.AST
asSingleRange | What4.Utils.AbstractDomains
asSingleton |
1 (Function) | What4.Utils.BVDomain.Arith
2 (Function) | What4.Utils.BVDomain.Bitwise
3 (Function) | What4.Utils.BVDomain.XOR
4 (Function) | What4.Utils.BVDomain
asSMT2Type | What4.Protocol.SMTLib2
asString | What4.Interface
asStruct | What4.Interface
assume | What4.Protocol.SMTWriter, What4.Protocol.SMTLib2, What4.Solver.Yices
assumedProp | Test.Verification
assumeFormula | What4.Protocol.SMTWriter
assumeFormulaWithFreshName | What4.Protocol.SMTWriter
assumeFormulaWithName | What4.Protocol.SMTWriter
Assuming | Test.Verification
assuming | Test.Verification
Assumption | Test.Verification
AssumptionProp | Test.Verification
AStr | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
asVar | What4.Expr.WeightedSum
asWeightedSum | What4.Expr.App
asWeightedVar | What4.Expr.WeightedSum
asXorDomain | What4.Utils.BVDomain
asyncLinked | What4.Utils.Serialize
Atom | What4.Serialize.SETokens, What4.Serialize.Printer, What4.Serialize.Parser
avCheckEq | What4.Utils.AbstractDomains
avContains | What4.Utils.AbstractDomains
avJoin | What4.Utils.AbstractDomains
avOverlap | What4.Utils.AbstractDomains
avSingle | What4.Utils.AbstractDomains
avTop | What4.Utils.AbstractDomains