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
setupBestFirstCheckDNF
:: [(E.ESafe, BoxFun)]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
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
(CN MPBall
-> ([(ESafe, BoxFun)], TypedVarMap, Bool)
-> MaxPQueue (CN MPBall) ([(ESafe, BoxFun)], TypedVarMap, Bool)
forall k a. k -> a -> MaxPQueue k a
Q.singleton
(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))
Integer
0
Integer
bfsBoxesCutoff
Rational
relativeImprovementCutoff
Precision
p
checkEDNFDepthFirstWithSimplex
:: [[E.ESafe]]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
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
checkEDNFBestFirstWithSimplexCE
:: [[E.ESafe]]
-> TypedVarMap
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
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
decideConjunctionWithApply
:: [(E.ESafe, BoxFun)]
-> Box
-> Maybe Bool
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 :: [((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
decideConjunctionBestFirst
:: Q.MaxPQueue (CN MPBall) ([(E.ESafe, BoxFun)], TypedVarMap, Bool)
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
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),
([(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)
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)
decideConjunctionDepthFirstWithSimplex
:: [(E.ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Integer
-> Integer
-> Rational
-> Precision
-> (Maybe Bool, Maybe TypedVarMap)
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 :: [((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
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
((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
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
| (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)
(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
decideConjunctionWithSimplexCE
:: [(E.ESafe, BoxFun)]
-> TypedVarMap
-> TypedVarMap
-> Rational
-> Precision
-> Bool
-> (Maybe Bool, Maybe TypedVarMap, [(E.ESafe, BoxFun)], Bool)
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 :: [((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
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
| (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)
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
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)