{-|
Module      : LPPaver.Decide.Util
Description : Utility functions for LPPaver.Decide modules
Copyright   : (c) Junaid Rasheed, 2021-2022
License     : MPL
Maintainer  : jrasheed178@gmail.com
Stability   : experimental
Module defining useful utility functions for the LPPaver.Decide modules
-}
module LPPaver.Decide.Util where

import MixedTypesNumPrelude
import qualified Prelude as P
import Data.List (nub, sortBy, partition)
import Data.Bifunctor
import PropaFP.Parsers.Smt (findVariablesInExpressions)
import AERN2.MP.Dyadic
import Control.CollectErrors
import AERN2.MP.Ball
import qualified Numeric.CollectErrors as CN
import AERN2.BoxFun.Type
import AERN2.BoxFun.Box
import qualified PropaFP.Expression as E
import PropaFP.VarMap
import qualified AERN2.Linear.Vector.Type as V
import AERN2.Kleenean
import PropaFP.Translators.BoxFun
import AERN2.BoxFun.Optimisation
import Control.Parallel.Strategies

-- TODO: Remove traces
-- |Dummy trace function
trace :: p -> p -> p
trace p
a p
x = p
x

-- |Calculate the range of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'apply'.
applyExpression :: E.E -> VarMap -> Precision -> CN MPBall
applyExpression :: E -> VarMap -> Precision -> CN MPBall
applyExpression E
expression VarMap
varMap Precision
p =
  BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f (VarMap -> Precision -> Vector (CN MPBall)
varMapToBox VarMap
varMap Precision
p)
  where
    f :: BoxFun
f = E -> VarMap -> Precision -> BoxFun
expressionToBoxFun E
expression VarMap
varMap Precision
p

-- |Calculate the gradient of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'gradient'.
gradientExpression :: E.E -> VarMap -> Precision -> V.Vector (CN MPBall)
gradientExpression :: E -> VarMap -> Precision -> Vector (CN MPBall)
gradientExpression E
expression VarMap
varMap Precision
p =
  BoxFun -> Vector (CN MPBall) -> Vector (CN MPBall)
gradient BoxFun
f (VarMap -> Precision -> Vector (CN MPBall)
varMapToBox VarMap
varMap Precision
p)
  where
    f :: BoxFun
f = E -> VarMap -> Precision -> BoxFun
expressionToBoxFun E
expression VarMap
varMap Precision
p

-- |Run 'applyExpression' on each 'E.E' in a given list
applyExpressionList :: [E.E] -> VarMap -> Precision -> [CN MPBall]
applyExpressionList :: [E] -> VarMap -> Precision -> [CN MPBall]
applyExpressionList [E]
expressions VarMap
varMap Precision
p =
  (E -> CN MPBall) -> [E] -> [CN MPBall]
forall a b. (a -> b) -> [a] -> [b]
map
  (\E
e -> BoxFun -> Vector (CN MPBall) -> CN MPBall
apply (E -> VarMap -> Precision -> BoxFun
expressionToBoxFun E
e VarMap
varMap Precision
p) Vector (CN MPBall)
box)
  [E]
expressions
  where
    box :: Vector (CN MPBall)
box = VarMap -> Precision -> Vector (CN MPBall)
varMapToBox VarMap
varMap Precision
p

-- |Run 'gradientExpression' on each 'E.E' in a given list
gradientExpressionList :: [E.E] -> VarMap -> Precision -> [V.Vector (CN MPBall)]
gradientExpressionList :: [E] -> VarMap -> Precision -> [Vector (CN MPBall)]
gradientExpressionList [E]
expressions VarMap
varMap Precision
p =
  (E -> Vector (CN MPBall)) -> [E] -> [Vector (CN MPBall)]
forall a b. (a -> b) -> [a] -> [b]
map
  (\E
e -> E -> VarMap -> Precision -> Vector (CN MPBall)
gradientExpression E
e VarMap
varMap Precision
p)
  [E]
expressions

-- |Run 'applyExpressionList' on each '[E.E]' in a given list
applyExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[CN MPBall]]
applyExpressionDoubleList :: [[E]] -> VarMap -> Precision -> [[CN MPBall]]
applyExpressionDoubleList [[E]]
cnf VarMap
varMap Precision
p = ([E] -> [CN MPBall]) -> [[E]] -> [[CN MPBall]]
forall a b. (a -> b) -> [a] -> [b]
map (\[E]
d -> [E] -> VarMap -> Precision -> [CN MPBall]
applyExpressionList [E]
d VarMap
varMap Precision
p) [[E]]
cnf

-- |Run 'gradientExpressionList' on each '[E.E]' in a given list
gradientExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]
gradientExpressionDoubleList :: [[E]] -> VarMap -> Precision -> [[Vector (CN MPBall)]]
gradientExpressionDoubleList [[E]]
cnf VarMap
varMap Precision
p = ([E] -> [Vector (CN MPBall)]) -> [[E]] -> [[Vector (CN MPBall)]]
forall a b. (a -> b) -> [a] -> [b]
map (\[E]
d -> [E] -> VarMap -> Precision -> [Vector (CN MPBall)]
gradientExpressionList [E]
d VarMap
varMap Precision
p) [[E]]
cnf

-- |Run 'applyExpressionDoubleList' on an [['E.ESafe']]
applyESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[CN MPBall]]
applyESafeDoubleList :: [[ESafe]] -> VarMap -> Precision -> [[CN MPBall]]
applyESafeDoubleList [[ESafe]]
cnf  = [[E]] -> VarMap -> Precision -> [[CN MPBall]]
applyExpressionDoubleList (([ESafe] -> [E]) -> [[ESafe]] -> [[E]]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe -> E) -> [ESafe] -> [E]
forall a b. (a -> b) -> [a] -> [b]
map ESafe -> E
E.extractSafeE) [[ESafe]]
cnf)

-- |Run 'gradientExpressionDoubleList' on an [['E.ESafe']]
gradientESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]
gradientESafeDoubleList :: [[ESafe]] -> VarMap -> Precision -> [[Vector (CN MPBall)]]
gradientESafeDoubleList [[ESafe]]
cnf = [[E]] -> VarMap -> Precision -> [[Vector (CN MPBall)]]
gradientExpressionDoubleList (([ESafe] -> [E]) -> [[ESafe]] -> [[E]]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe -> E) -> [ESafe] -> [E]
forall a b. (a -> b) -> [a] -> [b]
map ESafe -> E
E.extractSafeE) [[ESafe]]
cnf)

-- |Evaluate an 'E.F' over some 'VarMap' with a given 'Precision' using 'applyExpression'
checkFWithApply :: E.F -> VarMap -> Precision -> CN Kleenean
checkFWithApply :: F -> VarMap -> Precision -> CN Kleenean
checkFWithApply (E.FComp Comp
op E
e1 E
e2) VarMap
varMap Precision
p =
  case Comp
op of
    Comp
E.Ge -> CN MPBall
e1Val CN MPBall -> CN MPBall -> OrderCompareType (CN MPBall) (CN MPBall)
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= CN MPBall
e2Val
    Comp
E.Gt -> CN MPBall
e1Val CN MPBall -> CN MPBall -> OrderCompareType (CN MPBall) (CN MPBall)
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>  CN MPBall
e2Val
    Comp
E.Le -> CN MPBall
e1Val CN MPBall -> CN MPBall -> OrderCompareType (CN MPBall) (CN MPBall)
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<= CN MPBall
e2Val
    Comp
E.Lt -> CN MPBall
e1Val CN MPBall -> CN MPBall -> OrderCompareType (CN MPBall) (CN MPBall)
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
<  CN MPBall
e2Val
    Comp
E.Eq -> CN MPBall
e1Val CN MPBall -> CN MPBall -> EqCompareType (CN MPBall) (CN MPBall)
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== CN MPBall
e2Val
  where
    e1Val :: CN MPBall
e1Val = E -> VarMap -> Precision -> CN MPBall
applyExpression E
e1 VarMap
varMap Precision
p
    e2Val :: CN MPBall
e2Val = E -> VarMap -> Precision -> CN MPBall
applyExpression E
e2 VarMap
varMap Precision
p
checkFWithApply (E.FConn Conn
op F
f1 F
f2) VarMap
varMap Precision
p =
  case Conn
op of
    Conn
E.And   -> CN Kleenean
f1Val CN Kleenean -> CN Kleenean -> AndOrType (CN Kleenean) (CN Kleenean)
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN Kleenean
f2Val
    Conn
E.Or    -> CN Kleenean
f1Val CN Kleenean -> CN Kleenean -> AndOrType (CN Kleenean) (CN Kleenean)
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| CN Kleenean
f2Val
    Conn
E.Impl  -> CN Kleenean -> NegType (CN Kleenean)
forall t. CanNeg t => t -> NegType t
not CN Kleenean
f1Val CN Kleenean -> CN Kleenean -> AndOrType (CN Kleenean) (CN Kleenean)
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| CN Kleenean
f2Val
  where
    f1Val :: CN Kleenean
f1Val = F -> VarMap -> Precision -> CN Kleenean
checkFWithApply F
f1 VarMap
varMap Precision
p
    f2Val :: CN Kleenean
f2Val = F -> VarMap -> Precision -> CN Kleenean
checkFWithApply F
f2 VarMap
varMap Precision
p
checkFWithApply (E.FNot F
f) VarMap
varMap Precision
p = CN Kleenean -> NegType (CN Kleenean)
forall t. CanNeg t => t -> NegType t
not (CN Kleenean -> NegType (CN Kleenean))
-> CN Kleenean -> NegType (CN Kleenean)
forall a b. (a -> b) -> a -> b
$ F -> VarMap -> Precision -> CN Kleenean
checkFWithApply F
f VarMap
varMap Precision
p
checkFWithApply F
E.FTrue VarMap
_ Precision
_         = Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
CertainTrue
checkFWithApply F
E.FFalse VarMap
_ Precision
_        = Kleenean -> CN Kleenean
forall v. v -> CN v
cn Kleenean
CertainFalse

-- |Filter out expressions in a list which are certainly false.
-- If an expression cannot be evaluated, do not filter it out.
filterOutFalseExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]
filterOutFalseExpressions :: [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
filterOutFalseExpressions =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    case ESafe
safeE of
      E.EStrict E
_ ->    CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<=! Integer
0) -- We cannot decide on ranges with errors, so do not filter them out
      E.ENonStrict E
_ -> CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
0)
  )

-- |Filter out expressions in a list which are certainly true.
-- If an expression cannot be evaluated, do not filter it out.
filterOutTrueExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]
filterOutTrueExpressions :: [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
filterOutTrueExpressions =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
forall a. (a -> Bool) -> [a] -> [a]
filter
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| -- Do not filter if there is an error
    (
      case ESafe
safeE of
        E.EStrict E
_ ->
          case CN MPBall -> MPBall
forall p. CN p -> p
unCN CN MPBall
range MPBall -> Integer -> OrderCompareType MPBall Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Integer
0 of
            Kleenean
OrderCompareType MPBall Integer
CertainTrue -> Bool
False
            OrderCompareType MPBall Integer
_ -> Bool
True
          -- We cannot decide on ranges with errors, so do not filter them out
        E.ENonStrict E
_ ->
          case CN MPBall -> MPBall
forall p. CN p -> p
unCN CN MPBall
range MPBall -> Integer -> OrderCompareType MPBall Integer
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Integer
0 of
            Kleenean
OrderCompareType MPBall Integer
CertainTrue -> Bool
False
            OrderCompareType MPBall Integer
_ -> Bool
True
    )
  )

-- |Returns true if any of the ranges of the given Expression have been evaluated to be greater than or equal to zero.
decideRangesGEZero :: [((E.E, BoxFun), CN MPBall)] -> Bool
decideRangesGEZero :: [((E, BoxFun), CN MPBall)] -> Bool
decideRangesGEZero = (((E, BoxFun), CN MPBall) -> Bool)
-> [((E, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\((E, BoxFun)
_, CN MPBall
range) -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! Integer
0)

-- |The mean of a list of 'CN Dyadic' numbers.
mean :: [CN Dyadic] -> CN Rational
mean :: [CN Dyadic] -> CN Rational
mean [CN Dyadic]
xs = [CN Dyadic] -> CN Dyadic
forall t.
(CanAddSameType t, ConvertibleExactly Integer t) =>
[t] -> t
sum [CN Dyadic]
xs CN Dyadic -> Integer -> DivType (CN Dyadic) Integer
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ [CN Dyadic] -> Integer
forall (t :: * -> *) a. Foldable t => t a -> Integer
length [CN Dyadic]
xs

-- |Safely find the maximum of a list of ordered elements, avoiding exceptions by ignoring anything with errors
safeMaximum :: (HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a), CanTestErrorsPresent a) =>
  a -> [a] -> a
safeMaximum :: forall a.
(HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a),
 CanTestErrorsPresent a) =>
a -> [a] -> a
safeMaximum a
currentMax [] = a
currentMax
safeMaximum a
currentMax (a
x : [a]
xs) =
  if a -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError a
x
    then a -> [a] -> a
forall a.
(HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a),
 CanTestErrorsPresent a) =>
a -> [a] -> a
safeMaximum a
currentMax [a]
xs
    else a -> [a] -> a
forall a.
(HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a),
 CanTestErrorsPresent a) =>
a -> [a] -> a
safeMaximum (if a
x a -> a -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>! a
currentMax then a
x else a
currentMax) [a]
xs

-- |Safely find the maximum centre of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors
safeMaximumCentre :: [BoxFun] -> Box -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre :: [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre []       Vector (CN MPBall)
_   Maybe (CN Dyadic)
mCurrentCentre = Maybe (CN Dyadic)
mCurrentCentre
safeMaximumCentre (BoxFun
f : [BoxFun]
fs) Vector (CN MPBall)
box Maybe (CN Dyadic)
mCurrentCentre =
  if CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range
    then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN Dyadic)
mCurrentCentre
    else
      case Maybe (CN Dyadic)
mCurrentCentre of
        Just CN Dyadic
currentMax ->
          if CN Dyadic
currentMax CN Dyadic -> CN Dyadic -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! CentreType (CN MPBall)
CN Dyadic
rangeCentre
            then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN Dyadic)
mCurrentCentre
            else [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre [BoxFun]
fs Vector (CN MPBall)
box (CN Dyadic -> Maybe (CN Dyadic)
forall a. a -> Maybe a
Just CentreType (CN MPBall)
CN Dyadic
rangeCentre)
        Maybe (CN Dyadic)
Nothing -> [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)
safeMaximumCentre [BoxFun]
fs Vector (CN MPBall)
box (CN Dyadic -> Maybe (CN Dyadic)
forall a. a -> Maybe a
Just CentreType (CN MPBall)
CN Dyadic
rangeCentre)
  where
    range :: CN MPBall
range = BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
box
    rangeCentre :: CentreType (CN MPBall)
rangeCentre = CN MPBall -> CentreType (CN MPBall)
forall t. IsBall t => t -> CentreType t
AERN2.MP.Ball.centre CN MPBall
range

-- |Safely find the maximum minimum of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors
safeMaximumMinimum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum :: [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum []       Vector (CN MPBall)
_   Maybe (CN MPBall)
mCurrentMin = Maybe (CN MPBall)
mCurrentMin
safeMaximumMinimum (BoxFun
f : [BoxFun]
fs) Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMin =
  if CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range
    then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMin
    else
      case Maybe (CN MPBall)
mCurrentMin of
        Just CN MPBall
currentMin ->
          if CN MPBall
currentMin CN MPBall -> CN MPBall -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! CN MPBall
rangeMin
            then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMin
            else [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box (CN MPBall -> Maybe (CN MPBall)
forall a. a -> Maybe a
Just CN MPBall
rangeMin)
        Maybe (CN MPBall)
Nothing -> [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box (CN MPBall -> Maybe (CN MPBall)
forall a. a -> Maybe a
Just CN MPBall
rangeMin)
  where
    range :: CN MPBall
range = BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
box
    rangeMin :: CN MPBall
rangeMin = (CN MPBall, CN MPBall) -> CN MPBall
forall a b. (a, b) -> a
fst ((CN MPBall, CN MPBall) -> CN MPBall)
-> (CN MPBall, CN MPBall) -> CN MPBall
forall a b. (a -> b) -> a -> b
$ CN MPBall -> (CN MPBall, CN MPBall)
forall i. IsInterval i => i -> (i, i)
endpointsAsIntervals CN MPBall
range

-- |Safely find the maximum maximum of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors
safeMaximumMaximum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMaximum :: [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMaximum []       Vector (CN MPBall)
_   Maybe (CN MPBall)
mCurrentMax = Maybe (CN MPBall)
mCurrentMax
safeMaximumMaximum (BoxFun
f : [BoxFun]
fs) Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMax =
  if CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range
    then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMaximum [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMax
    else
      case Maybe (CN MPBall)
mCurrentMax of
        Just CN MPBall
currentMax ->
          if CN MPBall
currentMax CN MPBall -> CN MPBall -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! CN MPBall
rangeMax
            then [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box Maybe (CN MPBall)
mCurrentMax
            else [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box (CN MPBall -> Maybe (CN MPBall)
forall a. a -> Maybe a
Just CN MPBall
rangeMax)
        Maybe (CN MPBall)
Nothing -> [BoxFun]
-> Vector (CN MPBall) -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
fs Vector (CN MPBall)
box (CN MPBall -> Maybe (CN MPBall)
forall a. a -> Maybe a
Just CN MPBall
rangeMax)
  where
    range :: CN MPBall
range = BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
box
    rangeMax :: CN MPBall
rangeMax = (CN MPBall, CN MPBall) -> CN MPBall
forall a b. (a, b) -> b
snd ((CN MPBall, CN MPBall) -> CN MPBall)
-> (CN MPBall, CN MPBall) -> CN MPBall
forall a b. (a -> b) -> a -> b
$ CN MPBall -> (CN MPBall, CN MPBall)
forall i. IsInterval i => i -> (i, i)
endpointsAsIntervals CN MPBall
range

-- TODO: Move to PropaFP
-- |Bisect the widest interval in a 'VarMap'
bisectWidestInterval :: VarMap -> (VarMap, VarMap)
bisectWidestInterval :: VarMap -> (VarMap, VarMap)
bisectWidestInterval [] = String -> (VarMap, VarMap)
forall a. HasCallStack => String -> a
error String
"Given empty box to bisect"
bisectWidestInterval VarMap
vm = VarMap -> String -> (VarMap, VarMap)
bisectVar VarMap
vm String
widestVar
  where
    (String
widestVar, (Rational, Rational)
_) = VarMap
-> (String, (Rational, Rational)) -> (String, (Rational, Rational))
widestInterval (VarMap -> VarMap
forall a. [a] -> [a]
tail VarMap
vm) (VarMap -> (String, (Rational, Rational))
forall a. [a] -> a
head VarMap
vm)

-- TODO: Move to PropaFP
-- |Bisect the widest interval in a 'TypedVarMap'
bisectWidestTypedInterval :: TypedVarMap -> (TypedVarMap, TypedVarMap)
bisectWidestTypedInterval :: TypedVarMap -> (TypedVarMap, TypedVarMap)
bisectWidestTypedInterval [] = String -> (TypedVarMap, TypedVarMap)
forall a. HasCallStack => String -> a
error String
"Given empty box to bisect"
bisectWidestTypedInterval TypedVarMap
vm = TypedVarMap -> String -> (TypedVarMap, TypedVarMap)
bisectTypedVar TypedVarMap
vm String
widestVar
  where
    (String
widestVar, (Rational, Rational)
_) = TypedVarMap
-> (String, (Rational, Rational)) -> (String, (Rational, Rational))
widestTypedInterval (TypedVarMap -> TypedVarMap
forall a. [a] -> [a]
tail TypedVarMap
vm) ((String, (Rational, Rational)) -> (String, (Rational, Rational)))
-> (String, (Rational, Rational)) -> (String, (Rational, Rational))
forall a b. (a -> b) -> a -> b
$ TypedVarInterval -> (String, (Rational, Rational))
typedVarIntervalToVarInterval (TypedVarMap -> TypedVarInterval
forall a. [a] -> a
head TypedVarMap
vm)

-- TODO: Move to PropaFP
-- |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)
ensureVarMapWithinVarMap :: VarMap -> VarMap -> VarMap
ensureVarMapWithinVarMap :: VarMap -> VarMap -> VarMap
ensureVarMapWithinVarMap [] [] = []
ensureVarMapWithinVarMap ((String
v, (Rational
roundedL, Rational
roundedR)) : VarMap
rvm) ((String
_, (Rational
originalL, Rational
originalR)) : VarMap
ovm) =
  (String
v, (if Rational
roundedL Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
< Rational
originalL then Rational
originalL else Rational
roundedL, if Rational
roundedR Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
> Rational
originalR then Rational
originalR else Rational
roundedR))
  (String, (Rational, Rational)) -> VarMap -> VarMap
forall a. a -> [a] -> [a]
: VarMap -> VarMap -> VarMap
ensureVarMapWithinVarMap VarMap
rvm VarMap
ovm
ensureVarMapWithinVarMap VarMap
_ VarMap
_ = String -> VarMap
forall a. HasCallStack => String -> a
error String
"Different sized varMaps"

-- |Version of 'computeCornerValuesAndDerivatives' that returns Nothing if a calculation contains an error
safelyComputeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> Maybe [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]
safelyComputeCornerValuesAndDerivatives :: [((ESafe, BoxFun), CN MPBall)]
-> Vector (CN MPBall)
-> Maybe [(CN MPBall, CN MPBall, Vector (CN MPBall))]
safelyComputeCornerValuesAndDerivatives [((ESafe, BoxFun), CN MPBall)]
esWithRanges Vector (CN MPBall)
box =
  if Bool
cornerRangesWithDerivativesHasError
    then Maybe [(CN MPBall, CN MPBall, Vector (CN MPBall))]
forall a. Maybe a
Nothing
    else [(CN MPBall, CN MPBall, Vector (CN MPBall))]
-> Maybe [(CN MPBall, CN MPBall, Vector (CN MPBall))]
forall a. a -> Maybe a
Just [(CN MPBall, CN MPBall, Vector (CN MPBall))]
cornerRangesWithDerivatives
  where
    boxL :: Vector (CN MPBall)
boxL = Vector (CN MPBall) -> Vector (CN MPBall)
lowerBounds Vector (CN MPBall)
box
    boxU :: Vector (CN MPBall)
boxU = Vector (CN MPBall) -> Vector (CN MPBall)
upperBounds Vector (CN MPBall)
box

    -- filteredCornerRangesWithDerivatives = 
    --   [
    --     value |
    --     value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,
    --     not (hasError value)
    --   ]

    cornerRangesWithDerivatives :: [(CN MPBall, CN MPBall, Vector (CN MPBall))]
cornerRangesWithDerivatives =
      Strategy (CN MPBall, CN MPBall, Vector (CN MPBall))
-> (((ESafe, BoxFun), CN MPBall)
    -> (CN MPBall, CN MPBall, Vector (CN MPBall)))
-> [((ESafe, BoxFun), CN MPBall)]
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (CN MPBall, CN MPBall, Vector (CN MPBall))
forall a. Strategy a
rseq
      (\ ((ESafe
_, BoxFun
f), CN MPBall
_) -> (BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
boxL, BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
boxU, BoxFun -> Vector (CN MPBall) -> Vector (CN MPBall)
gradient BoxFun
f Vector (CN MPBall)
box))
      [((ESafe, BoxFun), CN MPBall)]
esWithRanges

    -- Check if any function contains errors
    cornerRangesWithDerivativesHasError :: Bool
cornerRangesWithDerivativesHasError =
      ((CN MPBall, CN MPBall, Vector (CN MPBall)) -> Bool)
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
      (\(CN MPBall
l, CN MPBall
r, Vector (CN MPBall)
c) -> CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
l Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
r Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (CN MPBall -> Bool) -> Vector (CN MPBall) -> Bool
forall a. (a -> Bool) -> Vector a -> Bool
V.any CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError Vector (CN MPBall)
c)
      [(CN MPBall, CN MPBall, Vector (CN MPBall))]
cornerRangesWithDerivatives

-- |Return the value of the given 'E.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 minimum/maximum of every interval in a 'Box' for the left/right extreme corners respectively.
computeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]
computeCornerValuesAndDerivatives :: [((ESafe, BoxFun), CN MPBall)]
-> Vector (CN MPBall)
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))]
computeCornerValuesAndDerivatives [((ESafe, BoxFun), CN MPBall)]
esWithRanges Vector (CN MPBall)
box = [(CN MPBall, CN MPBall, Vector (CN MPBall))]
filteredCornerRangesWithDerivatives
  where
    boxL :: Vector (CN MPBall)
boxL = Vector (CN MPBall) -> Vector (CN MPBall)
lowerBounds Vector (CN MPBall)
box
    boxU :: Vector (CN MPBall)
boxU = Vector (CN MPBall) -> Vector (CN MPBall)
upperBounds Vector (CN MPBall)
box

    -- filteredCornerRangesWithDerivatives = 
    --   [
    --     value |
    --     value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,
    --     not (hasError value)
    --   ]

    cornerRangesWithDerivatives :: [(CN MPBall, CN MPBall, Vector (CN MPBall))]
cornerRangesWithDerivatives =
      Strategy (CN MPBall, CN MPBall, Vector (CN MPBall))
-> (((ESafe, BoxFun), CN MPBall)
    -> (CN MPBall, CN MPBall, Vector (CN MPBall)))
-> [((ESafe, BoxFun), CN MPBall)]
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (CN MPBall, CN MPBall, Vector (CN MPBall))
forall a. Strategy a
rseq
      (\ ((ESafe
_, BoxFun
f), CN MPBall
_) -> (BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
boxL, BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f Vector (CN MPBall)
boxU, BoxFun -> Vector (CN MPBall) -> Vector (CN MPBall)
gradient BoxFun
f Vector (CN MPBall)
box))
      [((ESafe, BoxFun), CN MPBall)]
esWithRanges

    -- Keep the functions where we can calculate all derivatives
    filteredCornerRangesWithDerivatives :: [(CN MPBall, CN MPBall, Vector (CN MPBall))]
filteredCornerRangesWithDerivatives =
      ((CN MPBall, CN MPBall, Vector (CN MPBall)) -> Bool)
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))]
-> [(CN MPBall, CN MPBall, Vector (CN MPBall))]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (\(CN MPBall
l, CN MPBall
r, Vector (CN MPBall)
c) -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
l Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
r Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
|| (CN MPBall -> Bool) -> Vector (CN MPBall) -> Bool
forall a. (a -> Bool) -> Vector a -> Bool
V.any CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError Vector (CN MPBall)
c)) -- Filter out functions where any partial derivative or corners contain an error
      [(CN MPBall, CN MPBall, Vector (CN MPBall))]
cornerRangesWithDerivatives

-- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is false in a standard manner
-- A range with an error is treated as false.
decideConjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesFalse :: [((ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesFalse =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    case ESafe
safeE of
      E.EStrict E
_     -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<=! Integer
0
      E.ENonStrict E
_  -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
0
  )

-- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is true in a standard manner
-- A range with an error is treated as false.
decideConjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesTrue :: [((ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesTrue =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    case ESafe
safeE of
      E.EStrict E
_     -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>! Integer
0
      E.ENonStrict E
_  -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! Integer
0
  )


-- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is true in a standard manner
-- A range with an error is treated as false.
decideDisjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool
decideDisjunctionRangesTrue :: [((ESafe, BoxFun), CN MPBall)] -> Bool
decideDisjunctionRangesTrue =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    case ESafe
safeE of
      E.EStrict E
_     -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>! Integer
0
      E.ENonStrict E
_  -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! Integer
0
  )

-- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is false in a standard manner
-- A range with an error is treated as false.
decideDisjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool
decideDisjunctionRangesFalse :: [((ESafe, BoxFun), CN MPBall)] -> Bool
decideDisjunctionRangesFalse =
  (((ESafe, BoxFun), CN MPBall) -> Bool)
-> [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
  (\((ESafe
safeE, BoxFun
_), CN MPBall
range) ->
    case ESafe
safeE of
      E.EStrict E
_     -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<=! Integer
0
      E.ENonStrict E
_  -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
0
  )

-- |Evaluate the range of each 'E.ESafe' expression in a disjunction and check if the disjunction is false in a standard manner. 
decideDisjunctionFalse :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideDisjunctionFalse :: [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideDisjunctionFalse [(ESafe, BoxFun)]
expressionsWithFunctions TypedVarMap
varMap Precision
p =
  ((ESafe, BoxFun) -> Bool) -> [(ESafe, BoxFun)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
  (\(ESafe
safeE, BoxFun
f) ->
    let
      range :: CN MPBall
range = BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f (TypedVarMap -> Precision -> Vector (CN MPBall)
typedVarMapToBox TypedVarMap
varMap Precision
p)
    in
      case ESafe
safeE of
        E.EStrict E
_    -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<=! Integer
0
        E.ENonStrict E
_ -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
0
  )
  [(ESafe, BoxFun)]
expressionsWithFunctions

-- |Evaluate the range of each 'E.ESafe' expression in a CNF and check if the CNF is false in a standard manner. 
decideCNFFalse :: [[(E.ESafe, BoxFun)]] -> TypedVarMap -> Precision -> Bool
decideCNFFalse :: [[(ESafe, BoxFun)]] -> TypedVarMap -> Precision -> Bool
decideCNFFalse [[(ESafe, BoxFun)]]
c TypedVarMap
v Precision
p = ([(ESafe, BoxFun)] -> Bool) -> [[(ESafe, BoxFun)]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[(ESafe, BoxFun)]
d -> [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideDisjunctionFalse [(ESafe, BoxFun)]
d TypedVarMap
v Precision
p) [[(ESafe, BoxFun)]]
c

-- |Evaluate the range of each 'E.ESafe' expression in a conjunction and check if the conjunction is true in a standard manner. 
decideConjunctionTrue :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideConjunctionTrue :: [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideConjunctionTrue [(ESafe, BoxFun)]
c TypedVarMap
v Precision
p =
  ((ESafe, BoxFun) -> Bool) -> [(ESafe, BoxFun)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(ESafe
safeE, BoxFun
f) ->
    let
      range :: CN MPBall
range = BoxFun -> Vector (CN MPBall) -> CN MPBall
apply BoxFun
f (TypedVarMap -> Precision -> Vector (CN MPBall)
typedVarMapToBox TypedVarMap
v Precision
p)
    in
      case ESafe
safeE of
        E.EStrict E
_    -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>! Integer
0
        E.ENonStrict E
_ -> Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not (CN MPBall -> Bool
forall es. CanTestErrorsPresent es => es -> Bool
hasError CN MPBall
range) Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& CN MPBall
range CN MPBall -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!>=! Integer
0
  )
  [(ESafe, BoxFun)]
c

-- |Check the results of a disjunction in a standard manner
checkDisjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults :: forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults [] Maybe potentialModel
Nothing = (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe potentialModel
forall a. Maybe a
Nothing)
checkDisjunctionResults [] indeterminateArea :: Maybe potentialModel
indeterminateArea@(Just potentialModel
_) = (Maybe Bool
forall a. Maybe a
Nothing, Maybe potentialModel
indeterminateArea)
checkDisjunctionResults ((Maybe Bool, Maybe potentialModel)
result : [(Maybe Bool, Maybe potentialModel)]
results) Maybe potentialModel
mIndeterminateArea =
  case (Maybe Bool, Maybe potentialModel)
result of
    r :: (Maybe Bool, Maybe potentialModel)
r@(Just Bool
True, Maybe potentialModel
_) -> (Maybe Bool, Maybe potentialModel)
r
    (Just Bool
False, Maybe potentialModel
_) ->
      [(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults [(Maybe Bool, Maybe potentialModel)]
results Maybe potentialModel
mIndeterminateArea
    (Maybe Bool
Nothing, indeterminateArea :: Maybe potentialModel
indeterminateArea@(Just potentialModel
_)) -> [(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults [(Maybe Bool, Maybe potentialModel)]
results Maybe potentialModel
indeterminateArea
    (Maybe Bool
Nothing, Maybe potentialModel
Nothing) -> (Maybe Bool, Maybe potentialModel)
forall a. HasCallStack => a
undefined

-- |Check the results of a conjunction in a standard manner
checkConjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkConjunctionResults :: forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkConjunctionResults [] Maybe potentialModel
Nothing = (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, Maybe potentialModel
forall a. Maybe a
Nothing)
checkConjunctionResults [] indeterminateArea :: Maybe potentialModel
indeterminateArea@(Just potentialModel
_) = (Maybe Bool
forall a. Maybe a
Nothing, Maybe potentialModel
indeterminateArea)
checkConjunctionResults ((Maybe Bool, Maybe potentialModel)
result : [(Maybe Bool, Maybe potentialModel)]
results) Maybe potentialModel
mIndeterminateArea =
  case (Maybe Bool, Maybe potentialModel)
result of
    (Just Bool
True, Maybe potentialModel
_) -> [(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkConjunctionResults [(Maybe Bool, Maybe potentialModel)]
results Maybe potentialModel
mIndeterminateArea
    r :: (Maybe Bool, Maybe potentialModel)
r@(Just Bool
False, Maybe potentialModel
_) -> (Maybe Bool, Maybe potentialModel)
r
    (Maybe Bool
Nothing, indeterminateArea :: Maybe potentialModel
indeterminateArea@(Just potentialModel
_)) -> [(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkConjunctionResults [(Maybe Bool, Maybe potentialModel)]
results Maybe potentialModel
indeterminateArea
    (Maybe Bool
Nothing, Maybe potentialModel
Nothing) -> (Maybe Bool, Maybe potentialModel)
forall a. HasCallStack => a
undefined

-- |Substitute all variable-defining equalities in a given conjunction.
-- Simplify the conjunction after substituting all variable-defining equalities.
substituteConjunctionEqualities :: [E.ESafe] -> [E.ESafe]
substituteConjunctionEqualities :: [ESafe] -> [ESafe]
substituteConjunctionEqualities [] = []
substituteConjunctionEqualities conjunction :: [ESafe]
conjunction@(ESafe
conjunctionHead : [ESafe]
conjunctionTail) =
  case [(String, E)]
equations of
    [] -> [ESafe] -> [ESafe]
forall a. Eq a => [a] -> [a]
nub ([ESafe] -> [ESafe]) -> [ESafe] -> [ESafe]
forall a b. (a -> b) -> a -> b
$ [ESafe]
conjunction
    [(String, E)]
_  -> [ESafe] -> [ESafe]
substituteConjunctionEqualities [ESafe]
substConj
  where
    -- these equalities will not have any contradictions, they should already have been dealt with by deriveBounds and simplifyFDNF.
    equations :: [(String, E)]
equations = ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
conjunctionHead [ESafe]
conjunctionTail [ESafe]
conjunctionTail
    ((String, E)
eq : [(String, E)]
eqs) = [(String, E)]
equations

    substConj :: [ESafe]
substConj = (String, E) -> [ESafe] -> [ESafe]
substituteAndSimplifyChosenEquation (String, E)
selectedDupe [ESafe]
conjunction
    -- simplifiedSubstitutedConjunction = map (E.fmapESafe E.simplifyE) conjunction

    -- find duplicates for the first equation
    ([(String, E)]
dupes, [(String, E)]
nonDupes) = (String, E) -> [(String, E)] -> ([(String, E)], [(String, E)])
findDuplicateEquations (String, E)
eq [(String, E)]
eqs

    -- sort duplicates based on length
    sortedDupes :: [(String, E)]
sortedDupes = ((String, E) -> (String, E) -> Ordering)
-> [(String, E)] -> [(String, E)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(String
_, E
y1) (String
_, E
y2) -> E -> E -> Ordering
forall a. Ord a => a -> a -> Ordering
P.compare E
y1 E
y2) ((String, E)
eq (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: [(String, E)]
dupes)

    -- partition duplicates based on whether or not they contain variables
    ([(String, E)]
varFreeDupes, [(String, E)]
varContainingDupes) = ((String, E) -> Bool)
-> [(String, E)] -> ([(String, E)], [(String, E)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(String
_, E
e) -> E -> Bool
E.hasVarsE E
e) [(String, E)]
sortedDupes

    -- Select an equality to substitute
    -- Selects the shortest var-free equality or, if a var-free equality does not exist, the shortest equality
    selectedDupe :: (String, E)
selectedDupe = [(String, E)] -> (String, E)
forall a. [a] -> a
head ([(String, E)] -> (String, E)) -> [(String, E)] -> (String, E)
forall a b. (a -> b) -> a -> b
$ [(String, E)]
varFreeDupes [(String, E)] -> [(String, E)] -> [(String, E)]
forall a. [a] -> [a] -> [a]
++ [(String, E)]
varContainingDupes

    -- Find other var-defining equations for the var in the given equation
    findDuplicateEquations :: (String, E.E) -> [(String, E.E)] -> ([(String, E.E)], [(String, E.E)])
    findDuplicateEquations :: (String, E) -> [(String, E)] -> ([(String, E)], [(String, E)])
findDuplicateEquations (String, E)
_ [] = ([],[])
    findDuplicateEquations (String
x1, E
y1) ((String
x2, E
y2) : [(String, E)]
es)
      | String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
x2 =
        ([(String, E)] -> [(String, E)])
-> ([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((String
x2, E
y2) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
:) (([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)]))
-> ([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)])
forall a b. (a -> b) -> a -> b
$ (String, E) -> [(String, E)] -> ([(String, E)], [(String, E)])
findDuplicateEquations (String
x1, E
y1) [(String, E)]
es
      | Bool
otherwise =
        ([(String, E)] -> [(String, E)])
-> ([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((String
x2, E
y2) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
:) (([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)]))
-> ([(String, E)], [(String, E)]) -> ([(String, E)], [(String, E)])
forall a b. (a -> b) -> a -> b
$ (String, E) -> [(String, E)] -> ([(String, E)], [(String, E)])
findDuplicateEquations (String
x1, E
y1) [(String, E)]
es

    -- substitute the given equation in the given conjunction
    substituteAndSimplifyChosenEquation :: (String, E.E) -> [E.ESafe] -> [E.ESafe]
    substituteAndSimplifyChosenEquation :: (String, E) -> [ESafe] -> [ESafe]
substituteAndSimplifyChosenEquation (String, E)
_ [] = []
    substituteAndSimplifyChosenEquation (String
x, E
y) (ESafe
e : [ESafe]
c) = (E -> E) -> ESafe -> ESafe
E.fmapESafe (\E
nonSafeE -> E -> E
E.simplifyE (E -> E -> E -> E
E.replaceEInE E
nonSafeE (String -> E
E.Var String
x) E
y)) ESafe
e ESafe -> [ESafe] -> [ESafe]
forall a. a -> [a] -> [a]
: (String, E) -> [ESafe] -> [ESafe]
substituteAndSimplifyChosenEquation (String
x, E
y) [ESafe]
c

    -- Find var equations
    -- Essentially, find Es in the conjunction of the form Var v >= e, Var v <= e
    -- The e is ignored if it contains Var v
    -- Else, store this equality as v, e in the resulting list 
    findVarDefiningEquations :: E.ESafe -> [E.ESafe] -> [E.ESafe] -> [(String, E.E)]
    findVarDefiningEquations :: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
_ [] [] = []
    findVarDefiningEquations ESafe
_ [] (ESafe
e : [ESafe]
conj) = ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e [ESafe]
conj [ESafe]
conj
    findVarDefiningEquations ESafe
e1 (ESafe
e2 : [ESafe]
es) [ESafe]
conj =
      case ESafe
e1 of
        -- x1 - y1 >= 0
        E.ENonStrict (E.EBinOp BinOp
E.Sub v :: E
v@(E.Var String
x1) E
y1) ->
          -- ignore circular equalities
          if String
x1 String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` E -> [String]
findVariablesInExpressions E
y1 then ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else
          case ESafe
e2 of
            -- x2 - y2 >= 0
            E.ENonStrict (E.EBinOp BinOp
E.Sub E
x2 (E.Var String
y2)) ->
              -- if we have x - y >= 0 && y - x >= 0, then y - x = 0, so y = x
              if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
y2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
y1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
x2
                then
                  (String
x1, E
y1) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
                else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            ESafe
_ -> ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
        -- y1 - x1 >= 0
        E.ENonStrict (E.EBinOp BinOp
E.Sub E
y1 v :: E
v@(E.Var String
x1)) ->
          -- ignore circular equalities
          if String
x1 String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` E -> [String]
findVariablesInExpressions E
y1 then ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else
          case ESafe
e2 of
            -- y2 - x2 >= 0
            E.ENonStrict (E.EBinOp BinOp
E.Sub (E.Var String
y2) E
x2) ->
              -- if we have y - x >= 0 && x - y >= 0, then y - x = 0, so y = x
              if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
y2 Bool -> Bool -> AndOrType Bool Bool
forall a b. CanAndOrAsymmetric a b => a -> b -> AndOrType a b
&& E
y1 E -> E -> Bool
forall a. Eq a => a -> a -> Bool
P.== E
x2
                then
                  (String
x1, E
y1) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
                else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            ESafe
_ -> ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
        -- x >= 0
        E.ENonStrict v1 :: E
v1@(E.Var String
x1) ->
          case ESafe
e2 of
            -- -x >= 0
            E.ENonStrict (E.EUnOp UnOp
E.Negate (E.Var String
x2)) -> if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
x2 then (String
x1, Rational -> E
E.Lit Rational
0.0) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            -- 0 - x
            E.ENonStrict (E.EBinOp BinOp
E.Sub (E.Lit Rational
0.0) (E.Var String
x2)) -> if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
x2 then (String
x1, Rational -> E
E.Lit Rational
0.0) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            -- -1 * x
            E.ENonStrict (E.EBinOp BinOp
E.Mul (E.Lit (-1.0)) (E.Var String
x2)) -> if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
x2 then (String
x1, Rational -> E
E.Lit Rational
0.0) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            -- (-(1)) * x
            E.ENonStrict (E.EBinOp BinOp
E.Mul (E.EUnOp UnOp
E.Negate (E.Lit (Rational
1.0))) (E.Var String
x2)) -> if String
x1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
P.== String
x2 then (String
x1, Rational -> E
E.Lit Rational
0.0) (String, E) -> [(String, E)] -> [(String, E)]
forall a. a -> [a] -> [a]
: ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj else ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
            ESafe
_ -> ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj
        ESafe
_ -> ESafe -> [ESafe] -> [ESafe] -> [(String, E)]
findVarDefiningEquations ESafe
e1 [ESafe]
es [ESafe]
conj