AERN-RnToRm-0.5: src/Data/Number/ER/RnToRm/UnitDom/Base/Tests/Properties/Common.hs
{-|
Module : Data.Number.ER.RnToRm.UnitDom.Base.Tests.Properties.Common
Description : (testing) generating polynomials for tests
Copyright : (c) 2007-2008 Michal Konecny
License : BSD3
Maintainer : mik@konecny.aow.cz
Stability : experimental
Portability : portable
Auxiliary functions for use in test for polynomial enclosure arithmetic.
-}
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 {-^ report file name -} ->
testId {-^ item to identify the random input given to the test -} ->
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 {-^ report file name -} ->
testId {-^ item to identify the random input given to the test -} ->
(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 -- enclosure already in the range
False -> -- a shift needed to get above the lower bound
UFB.addEncl md ms (b2encl $ lowerB - preLowerBoundB + sepB) preEncl
(Nothing, Just upperB) ->
case preUpperBoundB < upperB of
True -> preEncl -- enclosure already in the range
False -> -- a shift needed to get below the upper bound
UFB.addEncl md ms (b2encl $ upperB - preUpperBoundB - sepB) preEncl
(Just lowerB, Just upperB) ->
case lowerB < preLowerBoundB && preUpperBoundB < upperB of
True -> preEncl -- enclosure already in the range
_ ->
case preWidthB + sepB <= widthB of
True -> -- no scaling needed, only shifting by a constant to the centre of the range
UFB.addEncl md ms
(b2encl $ lowerB - preLowerBoundB + (preWidthB - widthB)/2)
preEncl
_ -> -- full affine transformation needed
UFB.addEncl md ms
(b2encl $ lowerB + sepB) $
UFB.multiplyEncl md ms -- scale preEncl so that it fits inside the range
(b2encl $ widthB / saferPreWidthB) $
UFB.addEncl md ms -- shift preEncl so that it is non-negative and as close to 0 as safely possible
(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 {-^ report file name -} ->
testId {-^ item to identify the random input given to the test -} ->
(ra -> ra -> ra)
{-^ this real approx operation has to return an *inner* approximation of the exact result set,
ie each number that the approximation supports is in the maximal extension -} ->
(fb, fb) {-^ enclosure of argument 1 -} ->
(fb, fb) {-^ enclosure of argument 2 -} ->
(fb, fb) {-^ alleged enclosure of result -} ->
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
-- resAtPoint = p1OpInnerP2AtPoint -- for dummy testing that never <<loop>>s
p1AtPoint = UFB.evalEnclInner point p1Encl
p2AtPoint = UFB.evalEnclInner point p2Encl
enclAtKeyPointsPointwiseUnaryInnerInOuter ::
(UFB.ERUnitFnBaseEncl boxb boxra varid b ra fb, Show boxra, Show testId) =>
String {-^ report file name -} ->
testId {-^ item to identify the random input given to the test -} ->
(ra -> ra)
{-^ this real approx operation has to return an inner approximation of the exact result set,
ie each number that the approximation supports is in the maximal extension -} ->
(fb, fb) {-^ enclosure of argument -} ->
(fb, fb) {-^ alleged enclosure of result -} ->
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 =
-- normaliseERInterval $
UFB.evalEnclInner point fbEncl
enclAtKeyPointsConsistent ::
(UFB.ERUnitFnBaseEncl boxb boxra varid b ra fb, Show boxra, Show testId) =>
String {-^ report file name -} ->
testId {-^ item to identify the random input given to the test -} ->
(boxra -> ra)
{-^ this operation has to return an inner approximation of the exact result set,
ie each number that the approximation supports is a solution in the maximal extension -} ->
[varid] {-^ variables to test over -} ->
(fb, fb) {-^ alleged enclosure of result -} ->
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