PropaFP-0.1.1.0: Auto-active verification of floating-point programs
Contents
Index
Index
Abs
PropaFP.Expression
Add
PropaFP.Expression
addBinding
PropaFP.Parsers.Lisp.DataTypes
addVarMapBoundsToF
PropaFP.Parsers.Smt
analyzeExpression
PropaFP.Parsers.Lisp.Parser
analyzeExpressionSequence
PropaFP.Parsers.Lisp.Parser
And
PropaFP.Expression
Application
PropaFP.Parsers.Lisp.DataTypes
BinOp
PropaFP.Expression
bisectInterval
PropaFP.VarMap
bisectN
PropaFP.VarMap
bisectTypedInterval
PropaFP.VarMap
bisectTypedVar
PropaFP.VarMap
bisectVar
PropaFP.VarMap
Boolean
PropaFP.Parsers.Lisp.DataTypes
boxToVarMap
PropaFP.VarMap
centre
PropaFP.VarMap
checkFWithEval
PropaFP.DeriveBounds
CNF
PropaFP.Parsers.Smt
cnfExpressionAndDomainsToDreal
PropaFP.Translators.DReal
cnfExpressionAndDomainsToMetiTarski
PropaFP.Translators.MetiTarski
cnfExpressionsToSMT
1 (Function)
PropaFP.Translators.MetiTarski
2 (Function)
PropaFP.Translators.DReal
cnfExpressionsToTptp
PropaFP.Translators.MetiTarski
collapseOr
PropaFP.Parsers.Smt
collapseOrs
PropaFP.Parsers.Smt
Comp
PropaFP.Expression
computeE
PropaFP.Expression
computeECNF
PropaFP.Expression
computeEDisjunction
PropaFP.Expression
computeQualifiedEs
PropaFP.Expression
Cond
PropaFP.Parsers.Lisp.DataTypes
conjunctionToSMT
PropaFP.Translators.DReal
Conn
PropaFP.Expression
contains
PropaFP.VarMap
Cos
PropaFP.Expression
Definition
PropaFP.Parsers.Lisp.DataTypes
deriveBoundsAndSimplify
PropaFP.DeriveBounds
deriveVCRanges
PropaFP.Parsers.Smt
determineFloatTypeE
PropaFP.Parsers.Smt
determineFloatTypeF
PropaFP.Parsers.Smt
disjunctionExpressionsToSMT
1 (Function)
PropaFP.Translators.MetiTarski
2 (Function)
PropaFP.Translators.DReal
disjunctionExpressionsToTptp
PropaFP.Translators.MetiTarski
Div
PropaFP.Expression
E
PropaFP.Expression
EBinOp
PropaFP.Expression
eContainsVars
PropaFP.Parsers.Smt
eliminateFloatsAndSimplifyVC
PropaFP.Parsers.Smt
eliminateFloatsF
PropaFP.EliminateFloats
eliminateKnownFunctionGuard
PropaFP.Parsers.Smt
eliminateKnownFunctionGuards
PropaFP.Parsers.Smt
EmptyEnvironment
PropaFP.Parsers.Lisp.DataTypes
ENonStrict
PropaFP.Expression
Environment
1 (Type/Class)
PropaFP.Parsers.Lisp.DataTypes
2 (Data Constructor)
PropaFP.Parsers.Lisp.DataTypes
Eq
PropaFP.Expression
ESafe
PropaFP.Expression
eSafeCNFToDNF
PropaFP.Expression
eSafeCNFToF
PropaFP.Expression
eSafeDisjToF
PropaFP.Expression
eSafeToF
PropaFP.Expression
EStrict
PropaFP.Expression
EUnOp
PropaFP.Expression
evalE
PropaFP.DeriveBounds
evalE_Rational
PropaFP.DeriveBounds
evalF_comparisons
PropaFP.DeriveBounds
Exception
PropaFP.Parsers.Lisp.DataTypes
Expression
PropaFP.Parsers.Lisp.DataTypes
expressionToBoxFun
PropaFP.Translators.BoxFun
expressionToFPTaylor
PropaFP.Translators.FPTaylor
expressionToSMT
PropaFP.Translators.DReal
expressionToTPTP
PropaFP.Translators.MetiTarski
expressionWithVarMapToFPTaylor
PropaFP.Translators.FPTaylor
extendEnvironment
PropaFP.Parsers.Lisp.DataTypes
extractSafeE
PropaFP.Expression
extractVariablesE
PropaFP.Expression
extractVariablesECNF
PropaFP.Expression
extractVariablesF
PropaFP.Expression
F
PropaFP.Expression
FComp
PropaFP.Expression
FConn
PropaFP.Expression
fContainsVars
PropaFP.Parsers.Smt
fDNFToEDNF
PropaFP.Expression
fDNFToFDNFWithoutEq
PropaFP.Expression
FFalse
PropaFP.Expression
filterOutCircularVarEqualities
PropaFP.Parsers.Smt
filterOutDuplicateVarEqualities
PropaFP.Parsers.Smt
findAbsoluteErrorUsingFPTaylor
PropaFP.EliminateFloats
findAssertions
PropaFP.Parsers.Smt
findDeclarations
PropaFP.Parsers.Smt
findFunctionInputsAndOutputs
PropaFP.Parsers.Smt
findGoalsInAssertions
PropaFP.Parsers.Smt
findIntegerVariables
PropaFP.Parsers.Smt
findVarEqualities
PropaFP.Parsers.Smt
findVariables
PropaFP.Parsers.Smt
findVariablesInExpressions
PropaFP.Parsers.Smt
findVariablesInFormula
PropaFP.Parsers.Smt
findVariableType
PropaFP.Parsers.Smt
flipStrictness
PropaFP.Expression
Float
PropaFP.Expression
Float32
PropaFP.Expression
Float64
PropaFP.Expression
fmapESafe
PropaFP.Expression
FNot
PropaFP.Expression
formulaAndVarMapToDReal
PropaFP.Translators.DReal
formulaAndVarMapToMetiTarski
PropaFP.Translators.MetiTarski
formulaToSMT
PropaFP.Translators.DReal
formulaToTPTP
PropaFP.Translators.MetiTarski
Frame
PropaFP.Parsers.Lisp.DataTypes
fToConjunction
PropaFP.Translators.DReal
fToECNF
PropaFP.Expression
fToEDNF
PropaFP.Expression
fToFDNF
PropaFP.Expression
FTrue
PropaFP.Expression
fullBisect
PropaFP.VarMap
Ge
PropaFP.Expression
getCorners
PropaFP.VarMap
getEdges
PropaFP.VarMap
getVarNamesWithTypes
PropaFP.VarMap
Gt
PropaFP.Expression
hasFloatE
PropaFP.Expression
hasFloatF
PropaFP.Expression
hasMinMaxAbsE
PropaFP.Expression
hasMinMaxAbsF
PropaFP.Expression
hasVarsE
PropaFP.Expression
hasVarsF
PropaFP.Expression
If
PropaFP.Parsers.Lisp.DataTypes
Impl
PropaFP.Expression
increaseDiameter
PropaFP.VarMap
increaseRadius
PropaFP.VarMap
inequalityEpsilon
PropaFP.Parsers.Smt
Integer
PropaFP.VarMap
intersectVarMap
PropaFP.VarMap
isScientificNumber
PropaFP.Parsers.Lisp.Parser
isTypedVarMapInverted
PropaFP.VarMap
isVarMapInverted
PropaFP.VarMap
knownFloatVars
PropaFP.Parsers.Smt
Lambda
PropaFP.Parsers.Lisp.DataTypes
latexShowComp
PropaFP.Expression
latexShowConn
PropaFP.Expression
latexShowE
PropaFP.Expression
latexShowF
PropaFP.Expression
Le
PropaFP.Expression
lengthE
PropaFP.Expression
lengthF
PropaFP.Expression
Lit
PropaFP.Expression
lookupValue
PropaFP.Parsers.Lisp.DataTypes
lowerbound
PropaFP.VarMap
Lt
PropaFP.Expression
Max
PropaFP.Expression
maxWidth
PropaFP.VarMap
Min
PropaFP.Expression
minMaxAbsEliminator
PropaFP.Eliminator
minMaxAbsEliminatorECNF
PropaFP.Eliminator
minMaxAbsEliminatorF
PropaFP.Eliminator
Mod
PropaFP.Expression
Mul
PropaFP.Expression
Name
1 (Type/Class)
PropaFP.Expression
2 (Data Constructor)
PropaFP.Expression
Negate
PropaFP.Expression
negateSafeE
PropaFP.Expression
normalizeBoolean
PropaFP.Expression
Null
PropaFP.Parsers.Lisp.DataTypes
Number
PropaFP.Parsers.Lisp.DataTypes
Or
PropaFP.Expression
Pair
PropaFP.Parsers.Lisp.DataTypes
pairToList
PropaFP.Parsers.Lisp.DataTypes
parse
PropaFP.Parsers.Lisp.Parser
parseDRealSmtToF
PropaFP.Parsers.DRealSmt
parseDRealVariables
PropaFP.Parsers.DRealSmt
parseDRealVC
PropaFP.Parsers.DRealSmt
parseDRealVCs
PropaFP.Parsers.DRealSmt
parseFCompOp
PropaFP.Parsers.Smt
parseFPTaylorRational
PropaFP.Translators.FPTaylor
parseIte
PropaFP.Parsers.Smt
parser
PropaFP.Parsers.Smt
parseRoundingMode
PropaFP.Parsers.Smt
parseSequence
PropaFP.Parsers.Lisp.Parser
parseSMT2
PropaFP.Parsers.Smt
parseVCToF
PropaFP.Parsers.Smt
parseVCToSolver
PropaFP.Parsers.Smt
ParsingMode
PropaFP.Parsers.Smt
Pi
PropaFP.Expression
Pow
PropaFP.Expression
PowI
PropaFP.Expression
prettyShowComp
PropaFP.Expression
prettyShowConn
PropaFP.Expression
prettyShowE
PropaFP.Expression
prettyShowECNF
PropaFP.Expression
prettyShowESafeCNF
PropaFP.Expression
prettyShowESafeDNF
PropaFP.Expression
prettyShowF
PropaFP.Expression
prettyShowFSafeDNF
PropaFP.Expression
prettyShowTypedVarMap
PropaFP.VarMap
prettyShowVarMap
PropaFP.VarMap
prettyShowVC
PropaFP.Expression
PrimitiveProcedure
PropaFP.Parsers.Lisp.DataTypes
processVC
PropaFP.Parsers.Smt
qualifiedEsToCNF2
PropaFP.Eliminator
qualifiedEsToDisjunction
PropaFP.Eliminator
qualifiedEsToF
PropaFP.Eliminator
qualifiedEToF
PropaFP.Eliminator
Real
PropaFP.VarMap
removeFloats
PropaFP.EliminateFloats
removeVariableFreeComparisons
PropaFP.Expression
replaceEInE
PropaFP.Expression
replaceEInF
PropaFP.Expression
RNA
PropaFP.Expression
RNE
PropaFP.Expression
RoundingMode
PropaFP.Expression
roundMPBall
PropaFP.DeriveBounds
RoundToInteger
PropaFP.Expression
RTN
PropaFP.Expression
RTP
PropaFP.Expression
RTZ
PropaFP.Expression
runDRealTranslatorCNF
PropaFP.Translators.DReal
runDRealTranslatorCNFWithVarMap
PropaFP.Translators.DReal
runMetiTarskiTranslatorCNFWithVarMap
PropaFP.Translators.MetiTarski
safeBoxToTypedVarMap
PropaFP.VarMap
safeIntersectVarMap
PropaFP.VarMap
safeVarMapToTypedVarMap
PropaFP.VarMap
scanHypotheses
PropaFP.DeriveBounds
scanHypothesis
PropaFP.DeriveBounds
showFrac
PropaFP.Translators.FPTaylor
simplifyE
PropaFP.Expression
simplifyEDoubleList
PropaFP.Expression
simplifyESafeDoubleList
PropaFP.Expression
simplifyF
PropaFP.Expression
simplifyFDNF
PropaFP.Expression
simplifyFDoubleList
PropaFP.Expression
Sin
PropaFP.Expression
Sqrt
PropaFP.Expression
Sub
PropaFP.Expression
substAllEqualities
PropaFP.Parsers.Smt
substVarEWithE
PropaFP.Expression
substVarEWithLit
PropaFP.Expression
substVarFWithE
PropaFP.Expression
substVarFWithLit
PropaFP.Expression
symbolicallySubstitutePiVars
PropaFP.Parsers.Smt
takeGoalFromAssertions
PropaFP.Parsers.Smt
taxicabWidth
PropaFP.VarMap
termDRealToE
PropaFP.Parsers.DRealSmt
termDRealToF
PropaFP.Parsers.DRealSmt
termsToF
PropaFP.Parsers.Smt
termToE
PropaFP.Parsers.Smt
termToF
PropaFP.Parsers.Smt
testOutput
PropaFP.Translators.FPTaylor
tokenize
PropaFP.Parsers.Lisp.Parser
toSearchBox
PropaFP.VarMap
transformImplications
PropaFP.Expression
typedMaxWidth
PropaFP.VarMap
TypedVar
PropaFP.VarMap
TypedVarInterval
PropaFP.VarMap
typedVarIntervalToVarInterval
PropaFP.VarMap
TypedVarMap
PropaFP.VarMap
typedVarMapToBox
PropaFP.VarMap
typedVarMapToVarMap
PropaFP.VarMap
UnOp
PropaFP.Expression
unsafeBoxToTypedVarMap
PropaFP.VarMap
unsafeIntersectVarMap
PropaFP.VarMap
unsafeVarMapToTypedVarMap
PropaFP.VarMap
updateLower
PropaFP.DeriveBounds
updateUpper
PropaFP.DeriveBounds
upperbound
PropaFP.VarMap
Var
PropaFP.Expression
VarBoundMap
PropaFP.DeriveBounds
Variable
PropaFP.Parsers.Lisp.DataTypes
variableBoundsToFPTaylor
PropaFP.Translators.FPTaylor
VarInterval
PropaFP.VarMap
VarMap
PropaFP.VarMap
varMapToBox
PropaFP.VarMap
VarName
PropaFP.DeriveBounds
VarType
PropaFP.VarMap
Why3
PropaFP.Parsers.Smt
widestInterval
PropaFP.VarMap
widestTypedInterval
PropaFP.VarMap
_f1
PropaFP.DeriveBounds
_f2
PropaFP.DeriveBounds
_f3
PropaFP.DeriveBounds
_f4
PropaFP.DeriveBounds
_f5
PropaFP.DeriveBounds