{-|
Module      : LPPaver.Decide.Algorithm
Description : Algorithms for deciding DNFs
Copyright   : (c) Junaid Rasheed, 2021-2022
License     : MPL
Maintainer  : jrasheed178@gmail.com
Stability   : experimental
Module defining algorithms that can decide DNFs of 'E.ESafe' terms.
-}
module LPPaver.Decide.Algorithm where

import MixedTypesNumPrelude
import qualified PropaFP.Expression as E
import PropaFP.VarMap
import AERN2.MP
import AERN2.MP.Precision
import AERN2.BoxFun.Type
import qualified Data.PQueue.Prio.Max as Q
import Data.Maybe
import PropaFP.Translators.BoxFun
import Control.Parallel.Strategies
import Data.List (nub)
import AERN2.BoxFun.Box


import LPPaver.Decide.Util
import LPPaver.Decide.Linearisation

-- |Start initial call to 'decideConjunctionBestFirst' for some conjunction in a DNF.
setupBestFirstCheckDNF 
  :: [(E.ESafe, BoxFun)]  -- ^ Each item is a term in the conjunction.
                          -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> TypedVarMap          -- ^ The area over which we are checking the conjunction.
  -> Integer              -- ^ The maximum number of boxes that should be examined before giving up. 
  -> Rational             -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
                          -- 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%
  -> Precision            -- ^'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> (Maybe Bool, Maybe TypedVarMap) -- ^ The return result.
                                     -- (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area.
                                     -- (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area.
                                     -- (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.
setupBestFirstCheckDNF :: [(ESafe, BoxFun)]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
setupBestFirstCheckDNF [(ESafe, BoxFun)]
expressionsWithFunctions TypedVarMap
typedVarMap Integer
bfsBoxesCutoff Rational
relativeImprovementCutoff Precision
p =
  MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionBestFirst
    -- (Q.singleton (maximum (map (\(_, f) -> (snd . endpointsAsIntervals) (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)
    (CN MPBall
-> ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall k a. k -> a -> MaxPQueue k a
Q.singleton
      -- Maximum minimum 
      (CN MPBall -> Maybe (CN MPBall) -> CN MPBall
forall a. a -> Maybe a -> a
fromMaybe (MPBall -> CN MPBall
forall v. v -> CN v
cn (Precision -> Integer -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p Integer
1000000000000)) ([BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum (((ESafe, BoxFun) -> BoxFun) -> [(ESafe, BoxFun)] -> [BoxFun]
forall a b. (a -> b) -> [a] -> [b]
map (ESafe, BoxFun) -> BoxFun
forall a b. (a, b) -> b
snd [(ESafe, BoxFun)]
expressionsWithFunctions) (TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
typedVarMap Precision
p) Maybe (CN MPBall)
forall a. Maybe a
Nothing))
      ([(ESafe, BoxFun)]
expressionsWithFunctions, TypedVarMap
typedVarMap, Bool
True))
    -- (Q.singleton (maximum (map (\(_, f) -> AERN2.MP.Ball.centre (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)
    Integer
0
    Integer
bfsBoxesCutoff
    Rational
relativeImprovementCutoff
    Precision
p

-- |Check a DNF of 'E.ESafe' terms using a depth-first branch-and-prune algorithm which tends to perform well when the problem is unsatisfiable.
checkEDNFDepthFirstWithSimplex 
  :: [[E.ESafe]]  -- ^ Each item is a term in the conjunction.
                  -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> TypedVarMap  -- ^ The area over which we are checking the conjunction.
  -> Integer      -- ^ The maximum depth that we can reach before giving up. 
  -> Rational     -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
                  -- 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%
  -> Precision    -- ^'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> (Maybe Bool, Maybe TypedVarMap) -- ^ The return result.
                                     -- (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area.
                                     -- (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area.
                                     -- (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.
checkEDNFDepthFirstWithSimplex :: [[ESafe]]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
checkEDNFDepthFirstWithSimplex [[ESafe]]
conjunctions TypedVarMap
typedVarMap Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p =
  [(Maybe Bool, Maybe TypedVarMap)]
-> Maybe TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults [(Maybe Bool, Maybe TypedVarMap)]
conjunctionResults Maybe TypedVarMap
forall a. Maybe a
Nothing
  where
    conjunctionResults :: [(Maybe Bool, Maybe TypedVarMap)]
conjunctionResults =
      Strategy (Maybe Bool, Maybe TypedVarMap)
-> ([ESafe] -> (Maybe Bool, Maybe TypedVarMap))
-> [[ESafe]]
-> [(Maybe Bool, Maybe TypedVarMap)]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (Maybe Bool, Maybe TypedVarMap)
forall a. Strategy a
rseq
      (\[ESafe]
conjunction ->
        let
          substitutedConjunction :: [ESafe]
substitutedConjunction = [ESafe] -> [ESafe]
substituteConjunctionEqualities [ESafe]
conjunction
          substitutedConjunctionVars :: [String]
substitutedConjunctionVars = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (ESafe -> [String]) -> [ESafe] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (E -> [String]
E.extractVariablesE (E -> [String]) -> (ESafe -> E) -> ESafe -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ESafe -> E
E.extractSafeE) [ESafe]
substitutedConjunction
          filteredTypedVarMap :: TypedVarMap
filteredTypedVarMap =
            (TypedVarInterval -> Bool) -> TypedVarMap -> TypedVarMap
forall a. (a -> Bool) -> [a] -> [a]
filter
            (\(TypedVar (String
v, (Rational
_, Rational
_)) VarType
_) -> String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
substitutedConjunctionVars)
            TypedVarMap
typedVarMap
          filteredVarMap :: VarMap
filteredVarMap = TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
filteredTypedVarMap
        in
          [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionDepthFirstWithSimplex ((ESafe -> (ESafe, BoxFun)) -> [ESafe] -> [(ESafe, BoxFun)]
forall a b. (a -> b) -> [a] -> [b]
map (\ESafe
e -> (ESafe
e, E -> VarMap -> Precision -> BoxFun
expressionToBoxFun (ESafe -> E
E.extractSafeE ESafe
e) VarMap
filteredVarMap Precision
p)) [ESafe]
substitutedConjunction) TypedVarMap
filteredTypedVarMap TypedVarMap
filteredTypedVarMap Integer
0 Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p)
      [[ESafe]]
conjunctions

-- |Check a DNF of 'E.ESafe' terms using a best-first branch-and-prune algorithm which tends to perform well when the problem is satisfiable.
checkEDNFBestFirstWithSimplexCE 
  :: [[E.ESafe]]  -- ^ Each item is a term in the conjunction.
                  -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> TypedVarMap  -- ^ The area over which we are checking the conjunction.
  -> Integer      -- ^ The maximum number of boxes that should be examined before giving up. 
  -> Rational     -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
                  -- 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%
  -> Precision    -- ^'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> (Maybe Bool, Maybe TypedVarMap) -- ^ The return result.
                                     -- (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area.
                                     -- (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area.
                                     -- (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.
checkEDNFBestFirstWithSimplexCE :: [[ESafe]]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
checkEDNFBestFirstWithSimplexCE [[ESafe]]
conjunctions TypedVarMap
typedVarMap Integer
bfsBoxesCutoff Rational
relativeImprovementCutoff Precision
p =
  [(Maybe Bool, Maybe TypedVarMap)]
-> Maybe TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
forall potentialModel.
[(Maybe Bool, Maybe potentialModel)]
-> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)
checkDisjunctionResults [(Maybe Bool, Maybe TypedVarMap)]
conjunctionResults Maybe TypedVarMap
forall a. Maybe a
Nothing
  where
    conjunctionResults :: [(Maybe Bool, Maybe TypedVarMap)]
conjunctionResults =
      Strategy (Maybe Bool, Maybe TypedVarMap)
-> ([ESafe] -> (Maybe Bool, Maybe TypedVarMap))
-> [[ESafe]]
-> [(Maybe Bool, Maybe TypedVarMap)]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy (Maybe Bool, Maybe TypedVarMap)
forall a. Strategy a
rseq
      (\[ESafe]
conjunction ->
        let
          substitutedConjunction :: [ESafe]
substitutedConjunction = [ESafe] -> [ESafe]
substituteConjunctionEqualities [ESafe]
conjunction
          substitutedConjunctionVars :: [String]
substitutedConjunctionVars = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (ESafe -> [String]) -> [ESafe] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (E -> [String]
E.extractVariablesE (E -> [String]) -> (ESafe -> E) -> ESafe -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ESafe -> E
E.extractSafeE) [ESafe]
substitutedConjunction
          filteredTypedVarMap :: TypedVarMap
filteredTypedVarMap =
            (TypedVarInterval -> Bool) -> TypedVarMap -> TypedVarMap
forall a. (a -> Bool) -> [a] -> [a]
filter
            (\(TypedVar (String
v, (Rational
_, Rational
_)) VarType
_) -> String
v String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
substitutedConjunctionVars)
            TypedVarMap
typedVarMap
          filteredVarMap :: VarMap
filteredVarMap = TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
filteredTypedVarMap
        in
          [(ESafe, BoxFun)]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
setupBestFirstCheckDNF ((ESafe -> (ESafe, BoxFun)) -> [ESafe] -> [(ESafe, BoxFun)]
forall a b. (a -> b) -> [a] -> [b]
map (\ESafe
e -> (ESafe
e, E -> VarMap -> Precision -> BoxFun
expressionToBoxFun (ESafe -> E
E.extractSafeE ESafe
e) VarMap
filteredVarMap Precision
p)) [ESafe]
substitutedConjunction) TypedVarMap
filteredTypedVarMap Integer
bfsBoxesCutoff Rational
relativeImprovementCutoff Precision
p
      )
      [[ESafe]]
conjunctions

-- |Attempt to decide a conjunction over some given box using basic interval evaluation via 'apply' 
decideConjunctionWithApply 
  :: [(E.ESafe, BoxFun)]  -- ^ Each item is a term in the conjunction.
                          -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> Box                  -- The box over which the conjunction is being examined.
  -> Maybe Bool           -- The result. 'Nothing' is given if a decision could not be made. 
decideConjunctionWithApply :: [(ESafe, BoxFun)] -> Box -> Maybe Bool
decideConjunctionWithApply [(ESafe, BoxFun)]
expressionsWithFunctions Box
box
  | [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms  = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
  | Bool
checkIfEsFalseUsingApply = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
  | Bool
otherwise                = Maybe Bool
forall a. Maybe a
Nothing
  where
    esWithRanges :: [((ESafe, BoxFun), CN MPBall)]
esWithRanges             = Strategy ((ESafe, BoxFun), CN MPBall)
-> ((ESafe, BoxFun) -> ((ESafe, BoxFun), CN MPBall))
-> [(ESafe, BoxFun)]
-> [((ESafe, BoxFun), CN MPBall)]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy ((ESafe, BoxFun), CN MPBall)
forall a. Strategy a
rseq (\ (ESafe
e, BoxFun
f) -> ((ESafe
e, BoxFun
f), BoxFun -> Box -> CN MPBall
apply BoxFun
f Box
box)) [(ESafe, BoxFun)]
expressionsWithFunctions
    -- filterOutTrueTerms       = esWithRanges
    filterOutTrueTerms :: [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms       = [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
filterOutTrueExpressions [((ESafe, BoxFun), CN MPBall)]
esWithRanges
    checkIfEsFalseUsingApply :: Bool
checkIfEsFalseUsingApply = [((ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesFalse [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms

-- |Decide a conjunction in a best-first manner using a priority queue. Maximal minimums over conjunctions are used to order them, with larger maximal minimums taking priority.
decideConjunctionBestFirst 
  :: Q.MaxPQueue (CN MPBall) ([(E.ESafe, BoxFun)], TypedVarMap, Bool) -- ^The priority queue. Maximal minimals are represented using CN MPBall.
                                                                      -- Each element in the queue is a triple.
                                                                      -- The first item is a pair where 'fst' is an 'E.ESafe' representation of the term and the 'snd' is a 'BoxFun' equivalent of the same term.
                                                                      -- The second item is the area over which the previous conjunction should be examined.
                                                                      -- The third item is a boolean used to determine from which 'extreme' corner to linearise the conjunction.
  -> Integer      -- ^ The number of boxes that have been examined.
  -> Integer      -- ^ The maximum number of boxes that should be examined before giving up. 
  -> Rational     -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
  -> Precision    -- ^'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> (Maybe Bool, Maybe TypedVarMap) -- ^ The return result.
                                     -- (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area.
                                     -- (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area.
                                     -- (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.
decideConjunctionBestFirst :: MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionBestFirst MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
queue Integer
numberOfBoxesExamined Integer
numberOfBoxesCutoff Rational
relativeImprovementCutoff Precision
p =
  case MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> Maybe
     (([(ESafe, BoxFun)], TypedVarMap, Bool),
      MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool))
forall k a. Ord k => MaxPQueue k a -> Maybe (a, MaxPQueue k a)
Q.maxView MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
queue of
    Just (([(ESafe, BoxFun)]
expressionsWithFunctions, TypedVarMap
typedVarMap, Bool
isLeftCorner), MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
queueWithoutVarMap) ->
      if Integer
numberOfBoxesExamined Integer -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
numberOfBoxesCutoff then
        String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace (Integer -> String
forall a. Show a => a -> String
show Integer
numberOfBoxesExamined) ((Maybe Bool, Maybe TypedVarMap)
 -> (Maybe Bool, Maybe TypedVarMap))
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$
        case [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Rational
-> Precision
-> Bool
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
decideConjunctionWithSimplexCE [(ESafe, BoxFun)]
expressionsWithFunctions TypedVarMap
typedVarMap TypedVarMap
typedVarMap Rational
relativeImprovementCutoff Precision
p Bool
isLeftCorner of
          (Just Bool
False, Maybe TypedVarMap
_, [(ESafe, BoxFun)]
_, Bool
_) -> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionBestFirst MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
queueWithoutVarMap (Integer
numberOfBoxesExamined Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) Integer
numberOfBoxesCutoff Rational
relativeImprovementCutoff Precision
p
          (Just Bool
True, Just TypedVarMap
satArea, [(ESafe, BoxFun)]
_, Bool
_) -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
satArea)
          (Maybe Bool
Nothing, Just TypedVarMap
indeterminateVarMap, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
newIsLeftCorner) -> String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"h" ((Maybe Bool, Maybe TypedVarMap)
 -> (Maybe Bool, Maybe TypedVarMap))
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$
            let
              functions :: [BoxFun]
functions = ((ESafe, BoxFun) -> BoxFun) -> [(ESafe, BoxFun)] -> [BoxFun]
forall a b. (a -> b) -> [a] -> [b]
map (ESafe, BoxFun) -> BoxFun
forall a b. (a, b) -> b
snd [(ESafe, BoxFun)]
filteredExpressionsWithFunctions

              (TypedVarMap
leftVarMap, TypedVarMap
rightVarMap) = String
-> (TypedVarMap -> (TypedVarMap, TypedVarMap))
-> TypedVarMap
-> (TypedVarMap, TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"bisecting" TypedVarMap -> (TypedVarMap, TypedVarMap)
bisectWidestTypedInterval TypedVarMap
indeterminateVarMap

              leftVarMapWithExpressionsAndCornerAndMinimum :: (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
leftVarMapWithExpressionsAndCornerAndMinimum  = String
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
forall {p1} {p2}. p1 -> p2 -> p2
trace ([ESafe] -> String
forall a. Show a => a -> String
show (((ESafe, BoxFun) -> ESafe) -> [(ESafe, BoxFun)] -> [ESafe]
forall a b. (a -> b) -> [a] -> [b]
map (ESafe, BoxFun) -> ESafe
forall a b. (a, b) -> a
fst [(ESafe, BoxFun)]
filteredExpressionsWithFunctions)) ((CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
 -> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool)))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
forall a b. (a -> b) -> a -> b
$ String
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"left"
                (
                  CN MPBall -> Maybe (CN MPBall) -> CN MPBall
forall a. a -> Maybe a -> a
fromMaybe (MPBall -> CN MPBall
forall v. v -> CN v
cn (Precision -> Integer -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p Integer
1000000000000)) ([BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
functions (TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
leftVarMap Precision
p) Maybe (CN MPBall)
forall a. Maybe a
Nothing),
                  ([(ESafe, BoxFun)]
filteredExpressionsWithFunctions, TypedVarMap
leftVarMap, Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
newIsLeftCorner)
                )
              rightVarMapWithExpressionsAndCornerAndMinimum :: (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
rightVarMapWithExpressionsAndCornerAndMinimum = String
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"right"
                (
                  CN MPBall -> Maybe (CN MPBall) -> CN MPBall
forall a. a -> Maybe a -> a
fromMaybe (MPBall -> CN MPBall
forall v. v -> CN v
cn (Precision -> Integer -> MPBall
forall t. CanBeMPBallP t => Precision -> t -> MPBall
mpBallP Precision
p Integer
1000000000000)) ([BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)
safeMaximumMinimum [BoxFun]
functions (TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
rightVarMap Precision
p) Maybe (CN MPBall)
forall a. Maybe a
Nothing),
                  -- fromMaybe (cn (mpBallP p 100000000000)) (safeMaximumMaximum functions (typedVarMapToBox rightVarMap p) Nothing),
                  -- fromMaybe (cn (dyadic 1048576)) (safeMaximumCentre functions (typedVarMapToBox rightVarMap p) Nothing),
                  ([(ESafe, BoxFun)]
filteredExpressionsWithFunctions, TypedVarMap
rightVarMap, Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
newIsLeftCorner)
                )
            in
              MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionBestFirst
              ((CN MPBall
 -> ([(ESafe, BoxFun)], TypedVarMap, Bool)
 -> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
 -> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CN MPBall
-> ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall k a. Ord k => k -> a -> MaxPQueue k a -> MaxPQueue k a
Q.insert (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
rightVarMapWithExpressionsAndCornerAndMinimum ((CN MPBall
 -> ([(ESafe, BoxFun)], TypedVarMap, Bool)
 -> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
 -> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CN MPBall
-> ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall k a. Ord k => k -> a -> MaxPQueue k a -> MaxPQueue k a
Q.insert (CN MPBall, ([(ESafe, BoxFun)], TypedVarMap, Bool))
leftVarMapWithExpressionsAndCornerAndMinimum MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
queueWithoutVarMap))
              (Integer
numberOfBoxesExamined Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) Integer
numberOfBoxesCutoff Rational
relativeImprovementCutoff Precision
p
          (Maybe Bool
_, Maybe TypedVarMap
_, [(ESafe, BoxFun)]
_, Bool
_) -> String -> (Maybe Bool, Maybe TypedVarMap)
forall a. HasCallStack => String -> a
error String
"Got unmatched case in decideConjunctionBestFirst"
      else (Maybe Bool
forall a. Maybe a
Nothing, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
typedVarMap)   -- Reached number of boxes cutoff
    Maybe
  (([(ESafe, BoxFun)], TypedVarMap, Bool),
   MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool))
Nothing -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing) -- All areas in queue disproved

-- |Decide a conjunction arising from a DNF over a given box using a depth-first branch-and-prune algorithm which tends to work well when the problem is unsatisfiable.
decideConjunctionDepthFirstWithSimplex
  :: [(E.ESafe, BoxFun)]  -- ^ Each item is a term in the conjunction.
                          -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> TypedVarMap          -- ^ The initial area over which the box is being examined. This remains unchanged during recursive calls to this function.
  -> TypedVarMap          -- ^ The current area over which the box is being examined.
  -> Integer              -- ^ The current depth.
  -> Integer              -- ^ The maximum allowed depth before giving up
  -> Rational             -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
                          -- 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%
  -> Precision            -- ^'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> (Maybe Bool, Maybe TypedVarMap) -- ^ The return result.
                                     -- (Nothing, Just indeterminateArea) means that the algorithm could not make a decision and returns an example of an indeterminate area.
                                     -- (Just False, Nothing) means that the algorithm has decided the DNF is unsatisfiable over the given area.
                                     -- (Just True, Just satArea) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.

decideConjunctionDepthFirstWithSimplex :: [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionDepthFirstWithSimplex [(ESafe, BoxFun)]
expressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
typedVarMap Integer
currentDepth Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p
  | [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms =
    String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"proved sat with apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
roundedVarMap)
    (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
roundedVarMap)
  | Bool
checkIfEsFalseUsingApply =
    String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"proved false with apply"
    (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing)
  | Bool
otherwise = (Maybe Bool, Maybe TypedVarMap)
checkSimplex
  where
      box :: Box
box  = TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
typedVarMap Precision
p
      varNamesWithTypes :: [(String, VarType)]
varNamesWithTypes = TypedVarMap -> [(String, VarType)]
getVarNamesWithTypes TypedVarMap
typedVarMap
      roundedVarMap :: TypedVarMap
roundedVarMap =
        case Box -> [(String, VarType)] -> Maybe TypedVarMap
safeBoxToTypedVarMap Box
box [(String, VarType)]
varNamesWithTypes of
          Just TypedVarMap
rvm -> TypedVarMap -> TypedVarMap -> TypedVarMap
unsafeIntersectVarMap TypedVarMap
initialVarMap TypedVarMap
rvm
          Maybe TypedVarMap
Nothing -> String -> TypedVarMap
forall a. HasCallStack => String -> a
error (String -> TypedVarMap) -> String -> TypedVarMap
forall a b. (a -> b) -> a -> b
$ String
"Rounded the following varMap makes it inverted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
typedVarMap
      untypedRoundedVarMap :: VarMap
untypedRoundedVarMap = TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
roundedVarMap

      esWithRanges :: [((ESafe, BoxFun), CN MPBall)]
esWithRanges             = Strategy ((ESafe, BoxFun), CN MPBall)
-> ((ESafe, BoxFun) -> ((ESafe, BoxFun), CN MPBall))
-> [(ESafe, BoxFun)]
-> [((ESafe, BoxFun), CN MPBall)]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy ((ESafe, BoxFun), CN MPBall)
forall a. Strategy a
rseq (\ (ESafe
e, BoxFun
f) -> ((ESafe
e, BoxFun
f), BoxFun -> Box -> CN MPBall
apply BoxFun
f Box
box)) [(ESafe, BoxFun)]
expressionsWithFunctions
      -- filterOutTrueTerms       = esWithRanges
      filterOutTrueTerms :: [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms       = [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
filterOutTrueExpressions [((ESafe, BoxFun), CN MPBall)]
esWithRanges
      checkIfEsFalseUsingApply :: Bool
checkIfEsFalseUsingApply = [((ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesFalse [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms

      filteredExpressionsWithFunctions :: [(ESafe, BoxFun)]
filteredExpressionsWithFunctions = (((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun))
-> [((ESafe, BoxFun), CN MPBall)] -> [(ESafe, BoxFun)]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun)
forall a b. (a, b) -> a
fst [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms

      -- Filter out ranges/derivatives with errors.
      -- This is safe because we do not need every function to enclose the unsat area. 
      filteredCornerRangesWithDerivatives :: [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives = [((ESafe, BoxFun), CN MPBall)]
-> Box -> [(CN MPBall, CN MPBall, Box)]
computeCornerValuesAndDerivatives [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms Box
box

      bisectWidestDimensionAndRecurse :: TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
bisectWidestDimensionAndRecurse TypedVarMap
varMapToBisect =
        let
          (TypedVarMap
leftVarMap, TypedVarMap
rightVarMap) = TypedVarMap -> (TypedVarMap, TypedVarMap)
bisectWidestTypedInterval TypedVarMap
varMapToBisect
          -- (leftVarMap, rightVarMap) = bimap (`unsafeIntersectVarMap` varMapToBisect) (`unsafeIntersectVarMap` varMapToBisect) $ bisectWidestTypedInterval varMapToBisect

          ((Maybe Bool, Maybe TypedVarMap)
leftR, (Maybe Bool, Maybe TypedVarMap)
rightR) =
            Strategy
  ((Maybe Bool, Maybe TypedVarMap), (Maybe Bool, Maybe TypedVarMap))
-> ((Maybe Bool, Maybe TypedVarMap),
    (Maybe Bool, Maybe TypedVarMap))
-> ((Maybe Bool, Maybe TypedVarMap),
    (Maybe Bool, Maybe TypedVarMap))
forall a. Strategy a -> a -> a
withStrategy
            (Strategy (Maybe Bool, Maybe TypedVarMap)
-> Strategy (Maybe Bool, Maybe TypedVarMap)
-> Strategy
     ((Maybe Bool, Maybe TypedVarMap), (Maybe Bool, Maybe TypedVarMap))
forall a b. Strategy a -> Strategy b -> Strategy (a, b)
parTuple2 Strategy (Maybe Bool, Maybe TypedVarMap)
forall a. Strategy a
rseq Strategy (Maybe Bool, Maybe TypedVarMap)
forall a. Strategy a
rseq)
            (
              [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionDepthFirstWithSimplex [(ESafe, BoxFun)]
filteredExpressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
leftVarMap (Integer
currentDepth Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p,
              [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionDepthFirstWithSimplex [(ESafe, BoxFun)]
filteredExpressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
rightVarMap (Integer
currentDepth Integer -> Integer -> AddType Integer Integer
forall t1 t2. CanAddAsymmetric t1 t2 => t1 -> t2 -> AddType t1 t2
+ Integer
1) Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p
            )
        in
          case (Maybe Bool, Maybe TypedVarMap)
leftR of
            (Just Bool
False, Maybe TypedVarMap
_)
              -> case (Maybe Bool, Maybe TypedVarMap)
rightR of
                (Just Bool
False, Maybe TypedVarMap
_) -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing)
                (Maybe Bool, Maybe TypedVarMap)
r -> (Maybe Bool, Maybe TypedVarMap)
r
            (Maybe Bool, Maybe TypedVarMap)
r -> (Maybe Bool, Maybe TypedVarMap)
r

      bisectUntilCutoff :: TypedVarMap -> IfThenElseType Bool (Maybe Bool, Maybe TypedVarMap)
bisectUntilCutoff TypedVarMap
varMapToCheck =
        if Integer
currentDepth Integer -> Integer -> Bool
forall a b. HasOrderCertainlyAsymmetric a b => a -> b -> Bool
!<! Integer
depthCutoff -- Best first
          then
              TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
bisectWidestDimensionAndRecurse TypedVarMap
varMapToCheck
          else
            (Maybe Bool
forall a. Maybe a
Nothing, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
varMapToCheck)

      checkSimplex :: (Maybe Bool, Maybe TypedVarMap)
checkSimplex
        -- If we can calculate any derivatives
        | (Bool -> Bool
forall t. CanNeg t => t -> NegType t
not (Bool -> Bool)
-> ([(CN MPBall, CN MPBall, Box)] -> Bool)
-> [(CN MPBall, CN MPBall, Box)]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(CN MPBall, CN MPBall, Box)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives = String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"decideWithSimplex start" ((Maybe Bool, Maybe TypedVarMap)
 -> (Maybe Bool, Maybe TypedVarMap))
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$
          case [(CN MPBall, CN MPBall, Box)]
-> VarMap -> (Maybe Bool, Maybe VarMap)
removeConjunctionUnsatAreaWithSimplex [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives VarMap
untypedRoundedVarMap of
            (Just Bool
False, Maybe VarMap
_) -> String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"decideWithSimplex true: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
roundedVarMap) (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing)
            (Maybe Bool
Nothing, Just VarMap
newVarMap) -> String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"decideWithSimplex indet" ((Maybe Bool, Maybe TypedVarMap)
 -> (Maybe Bool, Maybe TypedVarMap))
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$
              case VarMap -> [(String, VarType)] -> Maybe TypedVarMap
safeVarMapToTypedVarMap VarMap
newVarMap [(String, VarType)]
varNamesWithTypes of
                Just TypedVarMap
nvm -> TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
recurseOnVarMap (TypedVarMap -> (Maybe Bool, Maybe TypedVarMap))
-> TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$ TypedVarMap -> TypedVarMap -> TypedVarMap
unsafeIntersectVarMap TypedVarMap
nvm TypedVarMap
roundedVarMap
                Maybe TypedVarMap
Nothing -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing) -- This will only happen when all integers in an integer-only varMap have been decided
            (Maybe Bool, Maybe VarMap)
_ -> (Maybe Bool, Maybe TypedVarMap)
forall a. HasCallStack => a
undefined
        | Bool
otherwise = TypedVarMap -> IfThenElseType Bool (Maybe Bool, Maybe TypedVarMap)
bisectUntilCutoff TypedVarMap
roundedVarMap

      recurseOnVarMap :: TypedVarMap -> (Maybe Bool, Maybe TypedVarMap)
recurseOnVarMap TypedVarMap
recurseVarMap
        | TypedVarMap -> Rational
typedMaxWidth TypedVarMap
recurseVarMap Rational -> Integer -> EqCompareType Rational Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
0 =
          case [(ESafe, BoxFun)] -> Box -> Maybe Bool
decideConjunctionWithApply [(ESafe, BoxFun)]
filteredExpressionsWithFunctions (TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
recurseVarMap Precision
p) of
            Just Bool
True  -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
recurseVarMap)
            Just Bool
False -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing)
            Maybe Bool
Nothing    -> (Maybe Bool
forall a. Maybe a
Nothing, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
recurseVarMap)
        | TypedVarMap -> Rational
typedMaxWidth TypedVarMap
roundedVarMap Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ TypedVarMap -> Rational
typedMaxWidth TypedVarMap
recurseVarMap Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Rational
relativeImprovementCutoff =
          String
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"recursing with simplex with roundedVarMap: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
recurseVarMap) ((Maybe Bool, Maybe TypedVarMap)
 -> (Maybe Bool, Maybe TypedVarMap))
-> (Maybe Bool, Maybe TypedVarMap)
-> (Maybe Bool, Maybe TypedVarMap)
forall a b. (a -> b) -> a -> b
$
          [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
decideConjunctionDepthFirstWithSimplex [(ESafe, BoxFun)]
filteredExpressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
recurseVarMap Integer
currentDepth Integer
depthCutoff Rational
relativeImprovementCutoff Precision
p
        | Bool
otherwise = TypedVarMap -> IfThenElseType Bool (Maybe Bool, Maybe TypedVarMap)
bisectUntilCutoff TypedVarMap
recurseVarMap

-- |Decide a conjunction arising from a DNF over a given box using a best-first branch-and-prune algorithm which tends to work well when the problem is satisfiable.
decideConjunctionWithSimplexCE
  :: [(E.ESafe, BoxFun)]  -- ^ Each item is a term in the conjunction.
                          -- The first item of each pair is the 'E.ESafe' representation of the term and the second item is a 'BoxFun' equivalent of the same term.
  -> TypedVarMap          -- ^ The initial area over which the box is being examined. This remains unchanged during recursive calls to this function.
  -> TypedVarMap          -- ^ The current area over which the box is being examined.
  -> Rational             -- ^ A rational number used as a heuristic to determine when to recurse when pruning with the simplex method.
                          -- 1.2 (the recommended default) means the simplex method will recurse if the box being examined has shrunk by 20%
  -> Precision            -- ^ 'Precision' used for 'MPBall's. 'prec' 100 is the recommended default.
  -> Bool                 -- ^ A boolean used to determine the 'extreme' corner to linearise the conjunction from.
  -> (Maybe Bool, Maybe TypedVarMap, [(E.ESafe, BoxFun)], Bool) -- ^The return result
                                                                -- For the first item, Nothing means the algorithm could not decide, Just False means unsatisfiable and Just True means satisfiable.
                                                                -- The second item gives a counter-example/indeterminate area if appropriate.
                                                                -- The third item is a filtered conjunction: terms which interval evaluate to true are filtered out.
                                                                -- A boolean specifying the last corner from which the conjunction was linearised.
decideConjunctionWithSimplexCE :: [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Rational
-> Precision
-> Bool
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
decideConjunctionWithSimplexCE [(ESafe, BoxFun)]
expressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
typedVarMap Rational
relativeImprovementCutoff Precision
p Bool
isLeftCorner
  | [((ESafe, BoxFun), CN MPBall)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms =
    String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"proved sat with apply " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
roundedVarMap)
    (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
roundedVarMap, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
  | Bool
checkIfEsFalseUsingApply =
    String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"proved unsat with apply"
    (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
  | Bool
otherwise = (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
checkSimplex
  where
      box :: Box
box  = TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
typedVarMap Precision
p
      varNamesWithTypes :: [(String, VarType)]
varNamesWithTypes = TypedVarMap -> [(String, VarType)]
getVarNamesWithTypes TypedVarMap
typedVarMap
      roundedVarMap :: TypedVarMap
roundedVarMap =
        case Box -> [(String, VarType)] -> Maybe TypedVarMap
safeBoxToTypedVarMap Box
box [(String, VarType)]
varNamesWithTypes of
          Just TypedVarMap
rvm -> TypedVarMap -> TypedVarMap -> TypedVarMap
unsafeIntersectVarMap TypedVarMap
initialVarMap TypedVarMap
rvm
          Maybe TypedVarMap
Nothing -> String -> TypedVarMap
forall a. HasCallStack => String -> a
error (String -> TypedVarMap) -> String -> TypedVarMap
forall a b. (a -> b) -> a -> b
$ String
"Rounded the following varMap makes it inverted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
typedVarMap
      untypedRoundedVarMap :: VarMap
untypedRoundedVarMap = TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
roundedVarMap

      esWithRanges :: [((ESafe, BoxFun), CN MPBall)]
esWithRanges             = Strategy ((ESafe, BoxFun), CN MPBall)
-> ((ESafe, BoxFun) -> ((ESafe, BoxFun), CN MPBall))
-> [(ESafe, BoxFun)]
-> [((ESafe, BoxFun), CN MPBall)]
forall b a. Strategy b -> (a -> b) -> [a] -> [b]
parMap Strategy ((ESafe, BoxFun), CN MPBall)
forall a. Strategy a
rseq (\(ESafe
e, BoxFun
f) -> ((ESafe
e, BoxFun
f), BoxFun -> Box -> CN MPBall
apply BoxFun
f Box
box)) [(ESafe, BoxFun)]
expressionsWithFunctions
      -- filterOutTrueTerms       = esWithRanges
      filterOutTrueTerms :: [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms       = [((ESafe, BoxFun), CN MPBall)] -> [((ESafe, BoxFun), CN MPBall)]
filterOutTrueExpressions [((ESafe, BoxFun), CN MPBall)]
esWithRanges
      checkIfEsFalseUsingApply :: Bool
checkIfEsFalseUsingApply = [((ESafe, BoxFun), CN MPBall)] -> Bool
decideConjunctionRangesFalse [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms

      filteredExpressionsWithFunctions :: [(ESafe, BoxFun)]
filteredExpressionsWithFunctions = (((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun))
-> [((ESafe, BoxFun), CN MPBall)] -> [(ESafe, BoxFun)]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun)
forall a b. (a, b) -> a
fst [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms

      -- Filter out ranges/derivatives with errors.
      -- This is safe because we do not need every function to enclose the unsat area. 
      filteredCornerRangesWithDerivatives :: [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives = [((ESafe, BoxFun), CN MPBall)]
-> Box -> [(CN MPBall, CN MPBall, Box)]
computeCornerValuesAndDerivatives [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms Box
box

      checkSimplex :: (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
checkSimplex
        -- If we can calculate any derivatives
        | (Bool -> Bool
forall t. CanNeg t => t -> NegType t
not (Bool -> Bool)
-> ([(CN MPBall, CN MPBall, Box)] -> Bool)
-> [(CN MPBall, CN MPBall, Box)]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(CN MPBall, CN MPBall, Box)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives = String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"decideWithSimplex start" ((Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$
          String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"decideWithSimplex start" ((Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$
          case [(CN MPBall, CN MPBall, Box)]
-> VarMap -> (Maybe Bool, Maybe VarMap)
removeConjunctionUnsatAreaWithSimplex [(CN MPBall, CN MPBall, Box)]
filteredCornerRangesWithDerivatives VarMap
untypedRoundedVarMap of
            (Just Bool
False, Maybe VarMap
_) -> String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"decideWithSimplex true: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
roundedVarMap) (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
            (Maybe Bool
Nothing, Just VarMap
newVarMap) -> String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"decideWithSimplex indet" ((Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$
              case VarMap -> [(String, VarType)] -> Maybe TypedVarMap
safeVarMapToTypedVarMap VarMap
newVarMap [(String, VarType)]
varNamesWithTypes of
                Maybe TypedVarMap
Nothing -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner) -- This will only happen when all integers in an integer-only varMap have been decided
                Just TypedVarMap
nvm ->
                  let
                    newTypedVarMap :: TypedVarMap
newTypedVarMap = TypedVarMap -> TypedVarMap -> TypedVarMap
unsafeIntersectVarMap TypedVarMap
nvm TypedVarMap
roundedVarMap
                    newBox :: Box
newBox  = TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
newTypedVarMap Precision
p

                    -- When looking for a sat solution, we need to account for all ranges/derivatives
                    -- If any range/derivative has an error, we do not make a simplex system
                    mNewCornerRangesWithDerivatives :: Maybe [(CN MPBall, CN MPBall, Box)]
mNewCornerRangesWithDerivatives = [((ESafe, BoxFun), CN MPBall)]
-> Box -> Maybe [(CN MPBall, CN MPBall, Box)]
safelyComputeCornerValuesAndDerivatives [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms Box
newBox
                  in
                    String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace String
"findFalsePointWithSimplex start" ((Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$
                    case Maybe [(CN MPBall, CN MPBall, Box)]
mNewCornerRangesWithDerivatives of
                      Just [(CN MPBall, CN MPBall, Box)]
newCornerRangesWithDerivatives ->
                        case [(CN MPBall, CN MPBall, Box)] -> VarMap -> Bool -> Maybe VarMap
findConjunctionSatAreaWithSimplex [(CN MPBall, CN MPBall, Box)]
newCornerRangesWithDerivatives (TypedVarMap -> VarMap
typedVarMapToVarMap TypedVarMap
newTypedVarMap) Bool
isLeftCorner of
                          Just VarMap
satSolution ->
                            case VarMap -> [(String, VarType)] -> Maybe TypedVarMap
safeVarMapToTypedVarMap VarMap
satSolution [(String, VarType)]
varNamesWithTypes of
                              Just TypedVarMap
typedSatSolution ->
                                if [(ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool
decideConjunctionTrue ((((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun))
-> [((ESafe, BoxFun), CN MPBall)] -> [(ESafe, BoxFun)]
forall a b. (a -> b) -> [a] -> [b]
map ((ESafe, BoxFun), CN MPBall) -> (ESafe, BoxFun)
forall a b. (a, b) -> a
fst [((ESafe, BoxFun), CN MPBall)]
filterOutTrueTerms) TypedVarMap
typedSatSolution Precision
p
                                  then (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
typedSatSolution, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
                                  else TypedVarMap
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
recurseOnVarMap TypedVarMap
newTypedVarMap
                              Maybe TypedVarMap
Nothing -> String -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a. HasCallStack => String -> a
error (String
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$ String
"Found sat solution but encountered error when converting to typed sat solution" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VarMap -> String
forall a. Show a => a -> String
show VarMap
satSolution
                          Maybe VarMap
Nothing -> TypedVarMap
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
recurseOnVarMap TypedVarMap
newTypedVarMap
                      Maybe [(CN MPBall, CN MPBall, Box)]
Nothing -> TypedVarMap
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
recurseOnVarMap TypedVarMap
newTypedVarMap
            (Maybe Bool, Maybe VarMap)
_ -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a. HasCallStack => a
undefined
        | Bool
otherwise = TypedVarMap
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
recurseOnVarMap TypedVarMap
roundedVarMap

      recurseOnVarMap :: TypedVarMap
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
recurseOnVarMap TypedVarMap
recurseVarMap
        | TypedVarMap -> Rational
typedMaxWidth TypedVarMap
recurseVarMap Rational -> Integer -> EqCompareType Rational Integer
forall a b. HasEqAsymmetric a b => a -> b -> EqCompareType a b
== Integer
0 =
          case [(ESafe, BoxFun)] -> Box -> Maybe Bool
decideConjunctionWithApply [(ESafe, BoxFun)]
filteredExpressionsWithFunctions (TypedVarMap -> Precision -> Box
typedVarMapToBox TypedVarMap
recurseVarMap Precision
p) of
            Just Bool
True  -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
recurseVarMap, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
            Just Bool
False -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, Maybe TypedVarMap
forall a. Maybe a
Nothing, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
            Maybe Bool
Nothing    -> (Maybe Bool
forall a. Maybe a
Nothing, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
recurseVarMap, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)
        | TypedVarMap -> Rational
typedMaxWidth TypedVarMap
roundedVarMap Rational -> Rational -> DivType Rational Rational
forall t1 t2. CanDiv t1 t2 => t1 -> t2 -> DivType t1 t2
/ TypedVarMap -> Rational
typedMaxWidth TypedVarMap
recurseVarMap Rational -> Rational -> OrderCompareType Rational Rational
forall a b.
HasOrderAsymmetric a b =>
a -> b -> OrderCompareType a b
>= Rational
relativeImprovementCutoff =
          String
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall {p1} {p2}. p1 -> p2 -> p2
trace (String
"recursing with simplex with roundedVarMap: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypedVarMap -> String
forall a. Show a => a -> String
show TypedVarMap
recurseVarMap) ((Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
 -> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool))
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
forall a b. (a -> b) -> a -> b
$
          [(ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Rational
-> Precision
-> Bool
-> (Maybe Bool, Maybe TypedVarMap, [(ESafe, BoxFun)], Bool)
decideConjunctionWithSimplexCE [(ESafe, BoxFun)]
filteredExpressionsWithFunctions TypedVarMap
initialVarMap TypedVarMap
recurseVarMap Rational
relativeImprovementCutoff Precision
p (Bool -> NegType Bool
forall t. CanNeg t => t -> NegType t
not Bool
isLeftCorner)
        | Bool
otherwise = (Maybe Bool
forall a. Maybe a
Nothing, TypedVarMap -> Maybe TypedVarMap
forall a. a -> Maybe a
Just TypedVarMap
recurseVarMap, [(ESafe, BoxFun)]
filteredExpressionsWithFunctions, Bool
isLeftCorner)