LPPaver.Decide.Util

Module defining useful utility functions for the LPPaver.Decide modules

Documentation

trace :: p -> p -> p

Dummy trace function

applyExpression :: E -> VarMap -> Precision -> CN MPBall

Calculate the range of some E expression over the given VarMap with the given Precision using apply.

gradientExpression :: E -> VarMap -> Precision -> Vector (CN MPBall)

Calculate the gradient of some E expression over the given VarMap with the given Precision using gradient.

applyExpressionList :: [E] -> VarMap -> Precision -> [CN MPBall]

Run applyExpression on each E in a given list

gradientExpressionList :: [E] -> VarMap -> Precision -> [Vector (CN MPBall)]

Run gradientExpression on each E in a given list

applyExpressionDoubleList :: [[E]] -> VarMap -> Precision -> [[CN MPBall]]

Run applyExpressionList on each '[E.E]' in a given list

gradientExpressionDoubleList :: [[E]] -> VarMap -> Precision -> [[Vector (CN MPBall)]]

Run gradientExpressionList on each '[E.E]' in a given list

applyESafeDoubleList :: [[ESafe]] -> VarMap -> Precision -> [[CN MPBall]]

Run applyExpressionDoubleList on an [[ESafe]]

gradientESafeDoubleList :: [[ESafe]] -> VarMap -> Precision -> [[Vector (CN MPBall)]]

Run gradientExpressionDoubleList on an [[ESafe]]

checkFWithApply :: F -> VarMap -> Precision -> CN Kleenean

Evaluate an F over some VarMap with a given Precision using applyExpression

filterOutFalseExpressions :: [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]

Filter out expressions in a list which are certainly false. If an expression cannot be evaluated, do not filter it out.

filterOutTrueExpressions :: [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]

Filter out expressions in a list which are certainly true. If an expression cannot be evaluated, do not filter it out.

decideRangesGEZero :: [((E, BoxFun), CN MPBall)] -> Bool

Returns true if any of the ranges of the given Expression have been evaluated to be greater than or equal to zero.

mean :: [CN Dyadic] -> CN Rational

The mean of a list of 'CN Dyadic' numbers.

safeMaximum :: (HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a), CanTestErrorsPresent a) => a -> [a] -> a

Safely find the maximum of a list of ordered elements, avoiding exceptions by ignoring anything with errors

safeMaximumCentre :: [BoxFun] -> Box -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)

Safely find the maximum centre of a list of BoxFuns over a given Box, avoiding exceptions by ignoring anything with errors

safeMaximumMinimum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)

Safely find the maximum minimum of a list of BoxFuns over a given Box, avoiding exceptions by ignoring anything with errors

safeMaximumMaximum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)

Safely find the maximum maximum of a list of BoxFuns over a given Box, avoiding exceptions by ignoring anything with errors

bisectWidestInterval :: VarMap -> (VarMap, VarMap)

Bisect the widest interval in a VarMap

bisectWidestTypedInterval :: TypedVarMap -> (TypedVarMap, TypedVarMap)

Bisect the widest interval in a TypedVarMap

ensureVarMapWithinVarMap :: VarMap -> VarMap -> VarMap

Ensures that the first varMap is within the second varMap If it is, returns the first varMap. If it isn't modifies the varMap so that the returned varMap is within the second varMap Both varmaps must have the same number of vars in the same order (order of vars not checked)

safelyComputeCornerValuesAndDerivatives :: [((ESafe, BoxFun), CN MPBall)] -> Box -> Maybe [(CN MPBall, CN MPBall, Vector (CN MPBall))]

Version of computeCornerValuesAndDerivatives that returns Nothing if a calculation contains an error

computeCornerValuesAndDerivatives :: [((ESafe, BoxFun), CN MPBall)] -> Box -> [(CN MPBall, CN MPBall, Vector (CN MPBall))]

Return the value of the given ESafe expression/BoxFun at the extreme left corner and the extreme right corner as well as partial derivatives over the given Box. Extreme corners are defined as the minimummaximum of every interval in a Box for the leftright extreme corners respectively.

decideConjunctionRangesFalse :: [((ESafe, BoxFun), CN MPBall)] -> Bool

Decide if the ranges of a conjunction of ESafe expressions is false in a standard manner A range with an error is treated as false.

decideConjunctionRangesTrue :: [((ESafe, BoxFun), CN MPBall)] -> Bool

Decide if the ranges of a conjunction of ESafe expressions is true in a standard manner A range with an error is treated as false.

decideDisjunctionRangesTrue :: [((ESafe, BoxFun), CN MPBall)] -> Bool

Decide if the ranges of a disjunction of ESafe expressions is true in a standard manner A range with an error is treated as false.

decideDisjunctionRangesFalse :: [((ESafe, BoxFun), CN MPBall)] -> Bool

Decide if the ranges of a disjunction of ESafe expressions is false in a standard manner A range with an error is treated as false.

decideDisjunctionFalse :: [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool

Evaluate the range of each ESafe expression in a disjunction and check if the disjunction is false in a standard manner.

decideCNFFalse :: [[(ESafe, BoxFun)]] -> TypedVarMap -> Precision -> Bool

Evaluate the range of each ESafe expression in a CNF and check if the CNF is false in a standard manner.

decideConjunctionTrue :: [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool

Evaluate the range of each ESafe expression in a conjunction and check if the conjunction is true in a standard manner.

checkDisjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)

Check the results of a disjunction in a standard manner

checkConjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)

Check the results of a conjunction in a standard manner

substituteConjunctionEqualities :: [ESafe] -> [ESafe]

Substitute all variable-defining equalities in a given conjunction. Simplify the conjunction after substituting all variable-defining equalities.