module Data.Number.ER.RnToRm.UnitDom.Base.Tests.Properties.Common
where
import Data.Number.ER.RnToRm.UnitDom.Base.Tests.Generate
import qualified Data.Number.ER.RnToRm.UnitDom.Base as UFB
import Data.Number.ER.RnToRm.UnitDom.Base ((+^),(-^),(*^))
import Data.Number.ER.Real.Approx.Tests.Reporting
import qualified Data.Number.ER.Real.Base as B
import qualified Data.Number.ER.BasicTypes.DomainBox as DBox
import Data.Number.ER.BasicTypes.DomainBox (VariableID(..), DomainBox, DomainBoxMappable, DomainIntBox)
import Data.Number.ER.Misc
import qualified Data.Number.ER.Real.Approx as RA
fbAtKeyPointsCanBeLeq ::
(UFB.ERUnitFnBase boxb boxra varid b ra fb, Show boxra, Show testId) =>
String ->
testId ->
fb ->
fb ->
Bool
fbAtKeyPointsCanBeLeq reportFileName testId fb1 fb2 =
and $ map testPoint points
where
points = getKeyPoints (fb1 +^ fb2)
testPoint point
| lower1 <= upper2 =
unsafeERTestReport reportFileName
(testId, point, val1, val2) $
True
| otherwise =
unsafePrint
(
"Failure at point = " ++ (show point)
) $
False
where
val1 = UFB.evalApprox point fb1
val2 = UFB.evalApprox point fb2
(lower1, upper1) = UFB.raEndpoints fb1 val1
(lower2, upper2) = UFB.raEndpoints fb1 val2
getKeyPoints fb =
getKeyPointsForVars $ UFB.getVariables fb
getKeyPointsForVars vars =
points
where
points = map DBox.fromList $ allCombinations $ varDomPoints
varDomPoints = map (\v -> (v,[1,0,1])) vars
fbAtKeyPointsPointwiseBinaryDownUpConsistent ::
(UFB.ERUnitFnBase boxb boxra varid b ra fb, Show boxra, Show testId) =>
String ->
testId ->
(ra -> ra -> ra) ->
fb -> fb ->
(fb, fb) ->
Bool
fbAtKeyPointsPointwiseBinaryDownUpConsistent reportFileName testId raOp fb1 fb2 (resLow, resHigh) =
and $ map testPoint points
where
points = getKeyPoints (fb1 +^ fb2)
testPoint point
| ok =
unsafeERTestReport reportFileName
(testId, point, raOpAtPoint, resAtPoint) $
True
| otherwise =
unsafePrint
(
"fbAtKeyPointsPointwiseBinaryDownUpConsistent failed:"
++ "\n point = " ++ show point
++ "\n raOpAtPoint = " ++ show raOpAtPoint
++ "\n resAtPoint = " ++ show resAtPoint
)
False
where
ok = not $ RA.isDisjoint resAtPoint raOpAtPoint
resAtPoint = valLow RA.\/ valHigh
resAtPointLow = fst $ UFB.raEndpoints fb1 $ valLow
resAtPointHigh = snd $ UFB.raEndpoints fb1 $ valHigh
valLow = UFB.evalApprox point resLow
valHigh = UFB.evalApprox point resHigh
raOpAtPoint= raOp fb1AtPoint fb2AtPoint
fb1AtPoint = UFB.evalApprox point fb1
fb2AtPoint = UFB.evalApprox point fb2
enclRestrictRange ix md ms (Nothing, Nothing) preEncl = (True, preEncl)
enclRestrictRange ix md ms (maybeLower, maybeUpper) preEncl =
(succeeded, fbEncl)
where
succeeded = lowerSucceeded && upperSucceeded
lowerSucceeded =
case maybeLower of
Nothing -> True
Just lower -> lower < pLowerBound
upperSucceeded =
case maybeUpper of
Nothing -> True
Just upper -> pUpperBound < upper
(pLowerBound, pUpperBound) = UFB.boundsEncl ix fbEncl
fbEncl =
case (maybeLower, maybeUpper) of
(Just lowerB, Nothing) ->
case lowerB < preLowerBoundB of
True -> preEncl
False ->
UFB.addEncl md ms (b2encl $ lowerB preLowerBoundB + sepB) preEncl
(Nothing, Just upperB) ->
case preUpperBoundB < upperB of
True -> preEncl
False ->
UFB.addEncl md ms (b2encl $ upperB preUpperBoundB sepB) preEncl
(Just lowerB, Just upperB) ->
case lowerB < preLowerBoundB && preUpperBoundB < upperB of
True -> preEncl
_ ->
case preWidthB + sepB <= widthB of
True ->
UFB.addEncl md ms
(b2encl $ lowerB preLowerBoundB + (preWidthB widthB)/2)
preEncl
_ ->
UFB.addEncl md ms
(b2encl $ lowerB + sepB) $
UFB.multiplyEncl md ms
(b2encl $ widthB / saferPreWidthB) $
UFB.addEncl md ms
(b2encl $ sepB preLowerBoundB)
preEncl
where
widthB = upperB lowerB
saferPreWidthB = preWidthB + 2 * sepB
sepB = preWidthB / 1000000
preWidthB = preUpperBoundB preLowerBoundB
(preLowerBoundB, preUpperBoundB) = UFB.boundsEncl ix preEncl
b2encl b = UFB.constEncl (b,b)
enclAtKeyPointsPointwiseBinaryInnerInOuter ::
(UFB.ERUnitFnBaseEncl boxb boxra varid b ra fb, Show boxra, Show testId) =>
String ->
testId ->
(ra -> ra -> ra)
->
(fb, fb) ->
(fb, fb) ->
(fb, fb) ->
Bool
enclAtKeyPointsPointwiseBinaryInnerInOuter
reportFileName testId
raOpInner
p1Encl@(p1LowNeg, p1High) p2Encl@(p2LowNeg, p2High) resEncl =
and $ map testPoint points
where
points = getKeyPoints (p1High +^ p2High +^ p1LowNeg +^ p2LowNeg)
testPoint point
| result =
unsafeERTestReport reportFileName
(testId, point, p1OpInnerP2AtPoint, resAtPoint) $
result
| otherwise =
unsafePrint
(
"enclAtKeyPointsPointwiseBinaryInnerInOuter failed"
++ "\n point = " ++ show point
++ "\n p1AtPoint = " ++ show p1AtPoint
++ "\n p2AtPoint = " ++ show p2AtPoint
++ "\n p1OpInnerP2AtPoint = " ++ show p1OpInnerP2AtPoint
++ "\n resAtPoint = " ++ show resAtPoint
) $
result
where
result = p1OpInnerP2AtPoint `RA.refines` resAtPoint
p1OpInnerP2AtPoint = p1AtPoint `raOpInner` p2AtPoint
resAtPoint = UFB.evalEncl point resEncl
p1AtPoint = UFB.evalEnclInner point p1Encl
p2AtPoint = UFB.evalEnclInner point p2Encl
enclAtKeyPointsPointwiseUnaryInnerInOuter ::
(UFB.ERUnitFnBaseEncl boxb boxra varid b ra fb, Show boxra, Show testId) =>
String ->
testId ->
(ra -> ra)
->
(fb, fb) ->
(fb, fb) ->
Bool
enclAtKeyPointsPointwiseUnaryInnerInOuter
reportFileName testId
raOpInner
fbEncl@(pLowNeg, pHigh) resEncl =
and $ map testPoint points
where
points = getKeyPoints (pHigh +^ pLowNeg)
testPoint point
| result =
unsafeERTestReport reportFileName
(testId, point, opInnerPAtPoint, resAtPoint) $
result
| otherwise =
unsafePrint
(
"enclAtKeyPointsPointwiseUnaryInnerInOuter failed"
++ "\n point = " ++ show point
++ "\n pAtPoint = " ++ show pAtPoint
++ "\n opInnerPAtPoint = " ++ show opInnerPAtPoint
++ "\n resAtPoint = " ++ show resAtPoint
) $
result
where
result = opInnerPAtPoint `RA.refines` resAtPoint
opInnerPAtPoint = raOpInner pAtPoint
resAtPoint = UFB.evalEncl point resEncl
pAtPoint =
UFB.evalEnclInner point fbEncl
enclAtKeyPointsConsistent ::
(UFB.ERUnitFnBaseEncl boxb boxra varid b ra fb, Show boxra, Show testId) =>
String ->
testId ->
(boxra -> ra)
->
[varid] ->
(fb, fb) ->
Bool
enclAtKeyPointsConsistent
reportFileName testId
opInner allVars resEncl@(resLowNeg, resHigh) =
and $ map testPoint points
where
points = getKeyPointsForVars allVars
testPoint point
| result =
unsafeERTestReport reportFileName
(testId, point, opInnerAtPoint, resAtPoint) $
result
| otherwise =
unsafePrint
(
"enclAtKeyPointsConsistent failed"
++ "\n point = " ++ show point
++ "\n opInnerAtPoint = " ++ show opInnerAtPoint
++ "\n resAtPoint = " ++ show resAtPoint
) $
result
where
result = opInnerAtPoint `RA.refines` resAtPoint
opInnerAtPoint = opInner point
resAtPoint = UFB.evalEncl point resEncl