h&4-@      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                      Safe-Inferred.; Safe-Inferred-.;o        Safe-Inferred-.; Safe-Inferred-.7; "PropaFPAn assosciation list mapping variable names to rational interval domains%PropaFP5Get the width of the widest interval Fixme: maxWidth'PropaFP)Get the sum of the width of each interval(PropaFPIncrease the diameter of all variables in a varMap by the given rational)PropaFPIncrease the radius of all variables in a varMap by the given rational*PropaFP%Bisect all elements in a given VarMap+PropaFPBisect the domain of the given interval, resulting in a pair Vars-PropaFPBisect the given dimension of the given VarMap, resulting in a pair of VarMaps0PropaFP#Check whether or not v1 contain v2.1PropaFP5Convert VarMap to SearchBox with the provided minimum<PropaFP5Assumes varMaps have vars appearing in the same orderDPropaFPIntersect two varMaps This assumes that both VarMaps have the same variables in the same orderEPropaFP/Returns the widest interval in the given VarMap- !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHI-"#$! %&'()*+,-./0123456789:;<=>?@ABCDEFGHI Safe-Inferred-.; RPropaFPThe F type is used to specify comparisons between E types and logical connectives between F typesePropaFPThe E type represents the inequality: expression :: E >= 0 TODO: Add rounding operator with certain epsilon/floating-point typePropaFPEquivalent to E * -1 Example: ENonStrict e == e >= 0. negateSafeE (ENonStrict e) == e  0== -e 0 == (EStrict (EUnOp Negate e))PropaFPAdd bounds for any Float expressions addRoundingBounds :: E -> [[E]] addRoundingBounds (Float e significand) = [[exactExpression - machineEpsilon], [exactExpression + machineEpsilon]] where exactExpression = addRoundingBounds e machineEpsilon = 2^(-23) addRoundingBounds e = e%Various rules to simplify expressionsPropaFP4compute the value of E with Vars at specified pointsPropaFPGiven a list of qualified Es and points for all Vars, compute a list of valid values. A value is the computed result of the second element of the tuple and is valid if all the expressions in the list at the first element of the tuple compute to be above 0.PropaFPShow an expression in a human-readable format Rationals are converted into doublesPropaFPShow a conjunction of expressions in a human-readable format This is shown as an AND with each disjunction tabbed in with an OR If there is only one term in a disjunction, the expression is shown without an OR PropaFPExtract all variables in an expression Will not return duplicationesPropaFPExtract all variables in an expression Will not return duplicationesPropaFP9Normalize to and/or aggressively apply elimination rulesPQRWVUTSX[ZY\`_^]abdceonlkjgfhimputsrqv{zyxw|~}|~}v{zyxwputsrqeonlkjgfhimbdc\`_^]aX[ZYRWVUTSPQ Safe-Inferred-.;   Safe-Inferred-.;9PropaFP'All variables must appear in the VarMap Safe-Inferred-.;   Safe-Inferred-.;PropaFPGiven an expression, eliminate all Min, Max, and Abs occurences. This is done by:When we come across a Min e1 e2: 1) We have two cases 1a) if e2 >= e1, then choose e1 1b) if e1 >= e2, then choose e2 2) So, we eliminate min and add two elements to the qualified list 2a) Add e2 - e1 to the list of premises, call the eliminiator on e1 and e2 recursively, add any new premises from the recursive call to the list of premises, set the qualified value of e1 from the recursive call to be the qualified value in this case 2b) similar to 2a?Max e1 e2 is similar to Min e1 e2 Abs is treated as Max e (-e)If we come across any other operator, recursively call the eliminator on any expressions, add any resulting premises, and set the qualified value to be the operator called on the resulting Es PropaFPTranslate the qualified Es list to a single expression The qualified Es list is basically the following formula: e >= 0 == (p1 >= 0  p2 >= 0  p3 >=0 -> q1 >= 0) / repeat... where e is the expression passed to minMaxAbsEliminatorThis can be rewritten to (-p1 >= 0 / - p2 >= 0 / -p3 >= 0 / q1 >= 0) This is incorrect, strictness is not dealt with correctly qualifiedEsToCNF :: [([E],E)] -> E qualifiedEsToCNF [] = undefined qualifiedEsToCNF [([], q)] = q qualifiedEsToCNF [(ps, q)] = EBinOp Max (buildPs ps) q where buildPs :: [E] -> E buildPs [] = undefined buildPs [p] = (EUnOp Negate p) buildPs (p : ps) = EBinOp Max (EUnOp Negate p) (buildPs ps) qualifiedEsToCNF ((ps, q) : es) = EBinOp Min (qualifiedEsToCNF [(ps, q)]) (qualifiedEsToCNF es)Convert a list of qualified Es to a CNF represented as a list of lists  Safe-Inferred-.;OPropaFPMade for Float32/64 expressions >Deriving ranges for variables from hypotheses inside a formula(c) Michal Konecny 2013, 2021BSD3mikkonecny@gmail.com experimentalportable Safe-Inferred-.;7PropaFPReplace within a formula some comparisons with FTrue/FFalse, namely those comparisons that on the given box can be easily seen to be true/false.PropaFPcompute the value of E with Vars at specified points | (a generalised version of computeE)  Safe-Inferred-.;  Safe-Inferred-.;(PropaFPFind assertions in a parsed expression Assertions are Application types with the operator being a Variable equal to "assert" Assertions only have one operandsPropaFPFind function declarations in a parsed expression Function declarations are Application types with the operator being a Variable equal to "declare-fun" Function declarations contain 3 operands - Operand 1 is the name of the function - Operand 2 is an Application type which can be thought of as the parameters of the functions If the function has no paramters, this operand is LD.Null - Operand 3 is the type of the functionPropaFPFinds goals in assertion operands Goals are S-Expressions with a top level PropaFPTakes the last element from a list of assertions We assume that the last element is the goalPropaFPAttempts to parse FComp Ops, i.e. parse bool_eq to Just (FComp Eq)PropaFPReplace function guards which are known to be always true with true.PropaFPReplace function guard which is known to be always true with true.PropaFPTries to determine whether a Float operation is single or double precision by searching for the type of all variables appearing in the function. If the types match and are all either Float32/Float64, we can determine the type.PropaFPFind the type for the given variables Type is looked for in the supplied map If all found types match, return this typePropaFP.Process a parsed list of expressions to a VC. If the parsing mode is Why3, everything in the context implies the goal (empty context means we only have a goal). If the goal cannot be parsed, we return Nothing.If the parsing mode is CNF, parse all assertions into a CNF. If any assertion cannot be parsed, return Nothing. If any assertion contains Floats, return Nothing.PropaFPLooks for pi vars (vars named pi/pi{i} where {i} is some integer) and symbolic bounds. If the bounds are better than those given to the real pi in Why3, replace the variable with exact pi.PropaFPDerive ranges for a VC (Implication where a CNF implies a goal) Remove anything which refers to a variable for which we cannot derive ranges If the goal contains underivable variables, return NothingPropaFP2Filter out var equalities which rely on themselvesPropaFPFilter out var equalities which occur multiple times by choosing the var equality with the smallest length**  Safe-Inferred-.;-$PropaFP6Parser for SMT files produced by the dReal Translator.The DReal SMT file will have the first line declaring the SMT logic, which we ignore. The next few lines declare variables (if any) A variable is declared in the following format (declare-fun varName () varType) where varType can be Int or Real (assert (<= lowerBound varName)) (assert (<= varName upperBound))Both lowerBound and upperBound will be rationals, though can be safely converted to Integer for Int varsOnce the declare-fun lines end, we have an assert which contains the entire VC as an argument The rest of the file can be ignored (it will be (check-sat), (get-model), and (exit))PropaFPParses variables from a parsed file. First item must be a variable declaration Continues parsing variables until it reaches a non-variable assertion Returns a TypedVarMap and the rest of the parsed file. !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                     &PropaFP-0.1.0.0-GMViAzgRYdi8Ej9lszxkuDPropaFP.Parsers.Lisp.DataTypesPropaFP.Parsers.Lisp.ParserPropaFP.VarMapPropaFP.ExpressionPropaFP.Translators.MetiTarskiPropaFP.Translators.FPTaylorPropaFP.Translators.DRealPropaFP.EliminatorPropaFP.EliminateFloatsPropaFP.DeriveBoundsPropaFP.Translators.BoxFunPropaFP.Parsers.SmtPropaFP.Parsers.DRealSmt Paths_PropaFP ExpressionNullNumberBooleanVariablePair ExceptionLambdaPrimitiveProcedure Application DefinitionIfCond EnvironmentEmptyEnvironmentFrame addBinding lookupValueextendEnvironment pairToList$fEqExpression$fShowExpressionisScientificNumbertokenizeparse parseSequenceanalyzeExpressionanalyzeExpressionSequence TypedVarMapVarMapTypedVarIntervalTypedVar VarIntervalVarTypeRealIntegermaxWidth typedMaxWidth taxicabWidthincreaseDiameterincreaseRadius fullBisectbisectIntervalbisectTypedIntervalbisectN bisectVarbisectTypedVarcontains toSearchBoxcentre varMapToBoxtypedVarMapToBox boxToVarMapunsafeBoxToTypedVarMapsafeBoxToTypedVarMaptypedVarMapToVarMapunsafeVarMapToTypedVarMapsafeVarMapToTypedVarMapsafeIntersectVarMapunsafeIntersectVarMapisVarMapInvertedisTypedVarMapInvertedgetVarNamesWithTypes getCornersgetEdges upperbound lowerboundintersectVarMapwidestIntervalwidestTypedIntervaltypedVarIntervalToVarIntervalprettyShowVarMapprettyShowTypedVarMap$fShowTypedVarInterval$fEqTypedVarInterval$fOrdTypedVarInterval $fShowVarType $fEqVarType $fOrdVarTypeNameFFCompFConnFNotFTrueFFalseConnAndOrImplCompGtGeLtLeEqESafeEStrict ENonStrictEEBinOpEUnOpLitVarPowIFloat32Float64FloatPiRoundToInteger RoundingModeRNERTPRTNRTZRNAUnOpSqrtNegateAbsSinCosBinOpAddSubMulDivMinMaxPowModlengthFlengthEflipStrictness negateSafeE extractSafeE fmapESafefToECNFfToEDNFfToFDNFeSafeToF eSafeDisjToF eSafeCNFToF eSafeCNFToDNF simplifyE simplifyFsimplifyEDoubleList simplifyFDNFfDNFToFDNFWithoutEq fDNFToEDNFsimplifyFDoubleListsimplifyESafeDoubleListcomputeEcomputeQualifiedEscomputeEDisjunction computeECNFprettyShowESafeCNFprettyShowESafeDNFprettyShowFSafeDNF prettyShowVC latexShowE latexShowF latexShowComp latexShowConn prettyShowEprettyShowECNF prettyShowFprettyShowCompprettyShowConnextractVariablesEextractVariablesFextractVariablesECNFhasVarsEhasVarsF hasFloatE hasFloatFsubstVarEWithLitsubstVarFWithLitsubstVarEWithEsubstVarFWithEtransformImplicationsremoveVariableFreeComparisons hasMinMaxAbsE hasMinMaxAbsF replaceEInE replaceEInFnormalizeBoolean$fArbitraryBinOp$fArbitraryUnOp$fArbitraryRoundingMode$fArbitraryESafe$fArbitraryComp$fArbitraryConn $fArbitraryF $fArbitraryE$fArbitraryName $fShowName$fShowF$fEqF$fOrdF $fShowConn$fEqConn $fOrdConn $fShowComp$fEqComp $fOrdComp $fShowESafe $fEqESafe $fOrdESafe$fShowE$fEqE$fOrdE$fShowRoundingMode$fEqRoundingMode$fOrdRoundingMode $fShowUnOp$fEqUnOp $fOrdUnOp $fShowBinOp $fEqBinOp $fOrdBinOp formulaToTPTPexpressionToTPTPformulaAndVarMapToMetiTarskidisjunctionExpressionsToSMTcnfExpressionsToSMTdisjunctionExpressionsToTptpcnfExpressionsToTptp#cnfExpressionAndDomainsToMetiTarski$runMetiTarskiTranslatorCNFWithVarMapexpressionToFPTaylorvariableBoundsToFPTaylorshowFracexpressionWithVarMapToFPTaylorparseFPTaylorRational testOutputfToConjunctionconjunctionToSMT formulaToSMTexpressionToSMTformulaAndVarMapToDRealcnfExpressionAndDomainsToDrealrunDRealTranslatorCNFWithVarMaprunDRealTranslatorCNFminMaxAbsEliminatorFminMaxAbsEliminatorminMaxAbsEliminatorECNFqualifiedEsToCNF2qualifiedEsToDisjunctionqualifiedEsToF qualifiedEToF removeFloatseliminateFloatsFfindAbsoluteErrorUsingFPTaylor VarBoundMapVarName_f1_f2_f3_f4_f5deriveBoundsAndSimplifyscanHypothesesscanHypothesisevalF_comparisonsevalE_Rational updateUpper updateLowerevalE roundMPBallcheckFWithEvalexpressionToBoxFun ParsingModeWhy3CNFparser parseSMT2findAssertionsfindFunctionInputsAndOutputsfindDeclarations findVariablesfindIntegerVariablesfindGoalsInAssertionstakeGoalFromAssertions parseFCompOpparseItetermToFtermToE collapseOrs collapseOreliminateKnownFunctionGuardseliminateKnownFunctionGuardtermsToFdetermineFloatTypeEdetermineFloatTypeFfindVariableTypeknownFloatVarsfindVariablesInFormulafindVariablesInExpressionsparseRoundingMode processVCsymbolicallySubstitutePiVarsderiveVCRanges eContainsVars fContainsVarsinequalityEpsilonfindVarEqualitiesfilterOutCircularVarEqualitiesfilterOutDuplicateVarEqualitiessubstAllEqualitiesaddVarMapBoundsToFeliminateFloatsAndSimplifyVC parseVCToFparseVCToSolverparseDRealSmtToF parseDRealVCs parseDRealVCparseDRealVariables termDRealToF termDRealToEversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName,mixed-types-num-0.5.10-IzuurJsV0gNaQsdtLyjE1Numeric.MixedTypes.Boolnot