safeSymbol | What4.Symbol, What4.Interface |
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 |
sbStateManager | What4.Expr.Builder |
sbUnaryThreshold | What4.Expr.Builder |
SBVToFloat | What4.Expr.Builder, What4.Expr |
sbvToFloat | |
1 (Function) | What4.Interface |
2 (Function) | What4.Protocol.SMTWriter |
SBVToInteger | 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 |
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.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.Builder, What4.Expr |
SemiRingLiteral | What4.Expr.Builder, What4.Expr |
SemiRingNat | What4.SemiRing |
SemiRingNatRepr | What4.SemiRing, What4.Expr |
SemiRingProd | 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.Builder, What4.Expr |
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 |
shl | |
1 (Function) | What4.Utils.BVDomain.Arith |
2 (Function) | What4.Utils.BVDomain.Bitwise |
3 (Function) | What4.Utils.BVDomain |
shouldUnfold | What4.Interface |
shutdownSolver | What4.Protocol.SMTLib2 |
shutdownSolverProcess | What4.Protocol.Online |
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 |
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 |
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 |
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 |
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 |
srem | |
1 (Function) | What4.Utils.BVDomain.Arith |
2 (Function) | What4.Utils.BVDomain |
sr_compare | What4.SemiRing |
sr_hashWithSalt | What4.SemiRing |
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.Builder, What4.Expr |
stringAppend | What4.Protocol.SMTWriter |
stringConcat | What4.Interface |
StringContains | 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.Builder, What4.Expr |
2 (Data Constructor) | What4.Expr.Builder, What4.Expr |
StringIndexOf | 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.Builder, What4.Expr |
stringIsPrefixOf | |
1 (Function) | What4.Interface |
2 (Function) | What4.Protocol.SMTWriter |
StringIsSuffixOf | What4.Expr.Builder, What4.Expr |
stringIsSuffixOf | |
1 (Function) | What4.Interface |
2 (Function) | What4.Protocol.SMTWriter |
stringIte | What4.Interface |
StringLength | 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 |
StringSeq | What4.Expr.StringSeq |
stringSeqAbs | What4.Expr.StringSeq |
StringSeqEntry | What4.Expr.StringSeq |
StringSeqLiteral | What4.Expr.StringSeq |
StringSeqTerm | What4.Expr.StringSeq |
StringSubstring | 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.Builder, What4.Expr |
structCtor | What4.Protocol.SMTWriter |
structEq | What4.Interface |
StructField | 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.Builder, What4.Expr |
symFnId | What4.Expr.Builder, What4.Expr |
SymFnInfo | What4.Expr.Builder, What4.Expr |
symFnInfo | What4.Expr.Builder, What4.Expr |
symFnLoc | What4.Expr.Builder, What4.Expr |
symFnName | What4.Expr.Builder, What4.Expr |
symFnReturnType | 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 |