LPPaver 0.0.3.1 → 0.0.5.0
raw patch · 12 files changed
+1436/−1141 lines, 12 filesdep +filepath
Dependencies added: filepath
Files
- ChangeLog.md +20/−3
- LPPaver.cabal +7/−5
- README.md +5/−5
- app/LPPaver.hs +144/−22
- src/LPPaver/Algorithm/DNF.hs +383/−0
- src/LPPaver/Algorithm/Linearisation.hs +255/−0
- src/LPPaver/Algorithm/Type.hs +34/−0
- src/LPPaver/Algorithm/Util.hs +577/−0
- src/LPPaver/Decide/Algorithm.hs +0/−363
- src/LPPaver/Decide/Linearisation.hs +0/−258
- src/LPPaver/Decide/Util.hs +0/−476
- test/Spec.hs +11/−9
ChangeLog.md view
@@ -1,12 +1,29 @@ # Changelog for LPPaver -## [v0.0.3.1](https://github.com/rasheedja/PropaFP/compare/v0.0.3.1...v0.0.3.1)+## [v0.0.5.0](https://github.com/rasheedja/LPPaver/compare/v0.0.4.0...v0.0.5.0)+- Use a new heuristic for the best-first search algorithm+ - Centre of averages of the ranges of each term in the conjunction is the heuristic+- Allow larger cutoffs in tests+ - Required for new heuristic+- Remove an unneeded variable when linearising functions +## [v0.0.4.0](https://github.com/rasheedja/LPPaver/compare/v0.0.3.1...v0.0.4.0)++- Rename LPPaver.Decide modules to LPPaver.Algorithm+ - LPPaver.Decide.Algorithm is now LPPaver.Algorithm.DNF+ - Other LPPaver.Decide.Name modules are now LPPaver.Algorithm.Name+- Polish documentation+- Add useful types for our decision algorithms+- Update decision algorithms to use these types, making them easier to read and maintain as well as returning pavings for each algorithm's result+- Add option -o to executable to write pavings to a JSON file.++## [v0.0.3.1](https://github.com/rasheedja/LPPaver/compare/v0.0.3.1...v0.0.3.1)+ - Write initial README.md and REFERENCE.md - Remove haddock documentation using GitHub pages - Issues with dependencies so using hackage instead -## [v0.0.3.0](https://github.com/rasheedja/PropaFP/compare/v0.0.3.0...v0.0.2.0)+## [v0.0.3.0](https://github.com/rasheedja/LPPaver/compare/v0.0.3.0...v0.0.2.0) - Deploy haddock documentation using GitHub pages - Clean up and document new modules@@ -14,7 +31,7 @@ - Add constraintRightSide to LPPaver.Constraint.Util - Document LPPaver.Constraint.Type and LPPaver.Constraint.Util -## [v0.0.2.0](https://github.com/rasheedja/PropaFP/compare/v0.0.2.0...v0.0.1)+## [v0.0.2.0](https://github.com/rasheedja/LPPaver/compare/v0.0.2.0...v0.0.1) - Replace minView with maxView in 'model search' mode - Higher ranges are more likely to produce models
LPPaver.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4.+-- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack name: LPPaver-version: 0.0.3.1+version: 0.0.5.0 synopsis: An automated prover targeting problems that involve nonlinear real arithmetic description: Please see the README on GitHub at <https://github.com/rasheedja/LPPaver#readme> category: Math, Maths, Mathematics, Formal methods, Theorem Provers, verification@@ -27,11 +27,12 @@ library exposed-modules:+ LPPaver.Algorithm.DNF+ LPPaver.Algorithm.Linearisation+ LPPaver.Algorithm.Type+ LPPaver.Algorithm.Util LPPaver.Constraint.Type LPPaver.Constraint.Util- LPPaver.Decide.Algorithm- LPPaver.Decide.Linearisation- LPPaver.Decide.Util other-modules: Paths_LPPaver hs-source-dirs:@@ -87,6 +88,7 @@ , collect-errors ==0.1.* , containers ==0.6.* , directory ==1.3.*+ , filepath , mixed-types-num >=0.5.10 && <0.6 , optparse-applicative ==0.16.* , parallel ==3.2.*
README.md view
@@ -12,7 +12,7 @@ LPPaver understands input that is similar to SMT2. LPPaver is designed to work with SMT2 `assert`s. If an `assert` contains anything that LPPaver does not understand, the `assert`ion is (currently) silently dropped.-The full list of accepted inputs can be found in [REFERENCE.md](https://github.com/rasheedja/LPPaver/tree/main/REFERENCE.md)+The full list of accepted inputs can be found in [REFERENCE.md](REFERENCE.md) ## Building @@ -32,14 +32,14 @@ ## Examples -Examples can be found in directory [test/testFiles](https://github.com/rasheedja/LPPaver/tree/main/test/testFiles).-The [Place](https://github.com/rasheedja/LPPaver/tree/main/test/testFiles/Place) directory contains examples that describe the problem of placing circles of a fixed size into a square of a fixed size in such a way that all of the circles are within the square none of the circles are touching each-other or the edges of the square.+Examples can be found in directory [test/testFiles](test/testFiles).+The [Place](test/testFiles/Place) directory contains examples that describe the problem of placing circles of a fixed size into a square of a fixed size in such a way that all of the circles are within the square none of the circles are touching each-other or the edges of the square. The problem has also been generalised to higher dimensions. A formula describing the problem is shown below: -+ -The [PropaFP](https://github.com/rasheedja/LPPaver/tree/main/test/testFiles/PropaFP) directory contains examples that came from [PropaFP](https://github.com/rasheedja/PropaFP/).+The [PropaFP](test/testFiles/PropaFP) directory contains examples that came from [PropaFP](https://github.com/rasheedja/PropaFP/). These examples are described in detail in a [preprint of a paper describing PropaFP](https://arxiv.org/abs/2207.00921). In both directories, the sat subdirectory holds files which should be satisfiable, the unsat subdirectory holds files which should be unsatisfiable, and the cannotDecide subdirectory holds files which LPPaver could not decide with default parameters.
app/LPPaver.hs view
@@ -2,7 +2,7 @@ import MixedTypesNumPrelude import AERN2.MP.Ball-import LPPaver.Decide.Algorithm+import LPPaver.Algorithm.DNF import PropaFP.Expression import PropaFP.Eliminator import PropaFP.VarMap@@ -10,7 +10,11 @@ import PropaFP.Parsers.DRealSmt import Options.Applicative import System.Directory+import System.FilePath import Data.Ratio+import LPPaver.Algorithm.Util+import LPPaver.Algorithm.Type+import Control.Monad data ProverOptions = ProverOptions {@@ -20,15 +24,10 @@ bestFirstSearchCutoff :: Integer, precision :: Integer, -- relativeImprovementCutoff :: Rational, make this a flag, as a double is probably easier- fileName :: String+ fileName :: String,+ outputPavings :: Bool } --- data DRealOptions = DRealOptions--- {--- dRealFileName :: String,--- dRealTargetName :: String--- }- proverOptions :: Parser ProverOptions proverOptions = ProverOptions <$> switch@@ -77,9 +76,16 @@ <> help "SMT2 file to be checked" <> metavar "filePath" )+ <*> switch+ (+ long "output-pavings"+ <> short 'o'+ <> help "When this flag is passed, LPPaver will produce JSON output of paved boxes."+ )+ main :: IO ()-main = - do +main =+ do runProver =<< execParser opts where opts = info (proverOptions <**> helper)@@ -88,14 +94,14 @@ <> header "LPPaver - prover" ) runProver :: ProverOptions -> IO ()-runProver proverOptions@(ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) =- do +runProver proverOptions@(ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath outputPavings) =+ do if provingProcessDone then do parsedFile <- parseSMT2 filePath case parseDRealSmtToF parsedFile of (Just vc, typedVarMap) ->- let + let -- If there are variable free comparisons here, we could not deal with them earlier in the proving process. -- LPPaver cannot perform any better with these so we safely remove them. ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc@@ -112,7 +118,7 @@ mParsedVC <- parseVCToF filePath fptaylorPath case mParsedVC of Just (vc, typedVarMap) ->- let + let -- If there are variable free comparisons here, we could not deal with them earlier in the proving process. -- LPPaver cannot perform any better with these so we safely remove them. ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc@@ -123,30 +129,146 @@ putStrLn "Issue parsing file" decideEDNFWithVarMap :: [[ESafe]] -> TypedVarMap -> ProverOptions -> IO ()-decideEDNFWithVarMap ednf typedVarMap (ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) = do+decideEDNFWithVarMap ednf typedVarMap (ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath outputPavings) = do let result = if ceMode then checkEDNFBestFirstWithSimplexCE ednf typedVarMap bestFirstSearchCutoff 1.2 (prec p) else checkEDNFDepthFirstWithSimplex ednf typedVarMap depthCutoff 1.2 (prec p)+ let vcFileWithoutExtension = takeFileName . dropExtensions $ filePath case result of- (Just True, Just model) -> do+ SatDNF model pavings -> do putStrLn "sat" printSMTModel model prettyPrintCounterExample model- (Just False, _) -> do+ when outputPavings $ do+ let jsonOutput = typedVarMapBoxPavingsToJSON pavings 0+ writeJSONFile vcFileWithoutExtension jsonOutput+ UnsatDNF listOfPavings -> do putStrLn "unsat"- r@(_, Just indeterminateExample) -> do+ when outputPavings $ do+ let jsonOutput = listOfTypedVarMapPavingsToJSON listOfPavings 0+ writeJSONFile vcFileWithoutExtension jsonOutput+ IndeterminateDNF indeterminateExample pavings -> do putStrLn "unknown" printSMTModel indeterminateExample prettyPrintCounterExample indeterminateExample- r@(_, _) -> do- putStrLn "unknown"+ when outputPavings $ do+ let jsonOutput = typedVarMapBoxPavingsToJSON pavings 0+ writeJSONFile vcFileWithoutExtension jsonOutput+ where+ -- Useful functions for converting our pavings into a JSON object + rationalToJSON :: Rational -> String+ rationalToJSON r = "[" ++ show n ++ "," ++ show d ++ "]"+ where+ n = numerator r+ d = denominator r++ listOfTypedVarMapPavingsToJSON :: [[BoxStep TypedVarMap]] -> Integer -> String+ listOfTypedVarMapPavingsToJSON listOfPavings tabCount =+ replicate tabCount '\t' ++ "[" ++ "\n" +++ aux listOfPavings ++ "\n" +++ replicate tabCount '\t' ++ "]"+ where+ aux [] = ""+ aux [ps] = typedVarMapBoxPavingsToJSON ps 1+ aux (ps : pss) = aux [ps] ++ ",\n" ++ aux pss++ typedVarMapBoxPavingsToJSON :: [BoxStep TypedVarMap] -> Integer -> String+ typedVarMapBoxPavingsToJSON pavings tabCount =+ replicate tabCount '\t' ++ "[" ++ "\n" +++ aux pavings ++ "\n" +++ replicate tabCount '\t' ++ "]"+ where+ tabCount' = tabCount + 1++ aux [] = ""+ aux [p] = typedVarMapBoxPavingToJSON p tabCount'+ aux (p : ps) = aux [p] ++ replicate tabCount' '\t' ++ ",\n" ++ aux ps++ typedVarMapBoxPavingToJSON :: BoxStep TypedVarMap -> Integer -> String+ typedVarMapBoxPavingToJSON boxStep tabCount =+ replicate tabCount '\t' ++ "{\n" +++ aux boxStep +++ replicate tabCount '\t' ++ "}\n"+ where+ tabCount' = tabCount + 1+ tabCount'' = tabCount' + 1+ tabCount''' = tabCount'' + 1+ tabCount'''' = tabCount''' + 1++ showTypedVarMap box boxName = + replicate tabCount' '\t' ++ "\"" ++ boxName ++ "\":\n" +++ replicate tabCount'' '\t' ++ "[\n" +++ aux box +++ replicate tabCount'' '\t' ++ "]"+ where+ aux [] = ""+ aux [TypedVar (v, (l, r)) t] =+ replicate tabCount''' '\t' ++ "{\n" +++ replicate tabCount'''' '\t' ++ "\"variableName\" : " ++ show v ++ ",\n" +++ replicate tabCount'''' '\t' ++ "\"variableType\" : " ++ "\"" ++ show t ++ "\"" ++ ",\n" +++ replicate tabCount'''' '\t' ++ "\"leftEndpoint\" : " ++ rationalToJSON l ++ ",\n" +++ replicate tabCount'''' '\t' ++ "\"rightEndpoint\" : " ++ rationalToJSON r ++ "\n" +++ replicate tabCount''' '\t' ++ "}\n"+ aux (v : vs) = aux [v] ++ replicate tabCount''' '\t' ++ "," ++ "\n" ++ aux vs++ aux (Initial box) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"Initial\",\n" +++ showTypedVarMap box "box" ++ "\n"+ aux (EvalTrue box) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"EvalTrue\",\n" +++ showTypedVarMap box "box" ++ "\n"+ aux (EvalFalse box) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"EvalFalse\",\n" +++ showTypedVarMap box "box" ++ "\n"+ aux (GaveUp box) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"GaveUp\",\n" +++ showTypedVarMap box "box" ++ "\n"+ aux (ContractEmpty box) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"ContractEmpty\",\n" +++ showTypedVarMap box "box" ++ "\n"+ aux (Contract box boxC) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"Contract\",\n" +++ showTypedVarMap box "box" ++ ",\n" +++ showTypedVarMap boxC "boxC" ++ "\n"+ aux (FoundModel box boxM) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"FoundModel\",\n" +++ showTypedVarMap box "box" ++ ",\n" +++ showTypedVarMap boxM "boxM" ++ "\n"+ aux (Split box boxL boxR) =+ replicate tabCount' '\t' ++ "\"boxStep\": \"Split\",\n" +++ showTypedVarMap box "box" ++ ",\n" +++ showTypedVarMap boxL "boxL" ++ ",\n" +++ showTypedVarMap boxR "boxR" ++ "\n"++ writeJSONFile :: String -> String -> IO ()+ writeJSONFile fileNameWithoutExtension jsonString = do+ putStr "Saving pavings information to "+ safeFile >>= putStrLn+ safeFile >>= (`writeFile` jsonString)+ putStrLn "Pavings information saved"+ where+ safeFile = do+ let jsonFileName = fileNameWithoutExtension ++ ".json"+ doesJSONFileNameExist <- doesFileExist jsonFileName+ if doesJSONFileNameExist+ then findSafeFile fileNameWithoutExtension 0+ else return jsonFileName++ -- |Chooses an empty/non-existant file to write to+ findSafeFile f appendCounter = do+ let currentF = f ++ show appendCounter ++ ".json"+ doesCurrentFExist <- doesFileExist currentF+ if doesCurrentFExist+ then findSafeFile f (appendCounter + 1)+ else return currentF+ prettyPrintCounterExample :: TypedVarMap -> IO () prettyPrintCounterExample [] = return ()-prettyPrintCounterExample ((TypedVar (v, (l, r)) t) : vs) = +prettyPrintCounterExample ((TypedVar (v, (l, r)) t) : vs) = if l == r- then do + then do putStrLn (v ++ " = " ++ show (double l)) prettyPrintCounterExample vs else do
+ src/LPPaver/Algorithm/DNF.hs view
@@ -0,0 +1,383 @@+{-|+Module : LPPaver.Algorithm.DNF+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.Algorithm.DNF 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.Algorithm.Type+import LPPaver.Algorithm.Util+import LPPaver.Algorithm.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.+ -> DNFConjunctionResult TypedVarMap -- ^ The return result for each conjunction is:+ -- (IndeterminateDNF indeterminateArea pavings) means that the algorithm could not make a decision and returns an example of an indeterminate area.+ -- (UnsatDNF listOfPavings) means that the algorithm has decided the DNF is unsatisfiable over the given area.+ -- (SatDNF satArea pavings) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.+ -- For indeterminate and sat DNFs, we return pavings from the conjunction that leads to the result.+ -- For an unsat dnf, we return a list of pavings for each conjunction in the DNF.+setupBestFirstCheckDNF expressionsWithFunctions typedVarMap bfsBoxesCutoff relativeImprovementCutoff p =+ decideConjunctionBestFirst+ -- (Q.singleton (maximum (map (\(_, f) -> (snd . endpointsAsIntervals) (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)+ (Q.singleton+ -- Maximum minimum + (fromMaybe (cn (mpBallP p 1000000000000)) (safeAverageDummy (map snd expressionsWithFunctions) (typedVarMapToBox typedVarMap p) Nothing))+ (expressionsWithFunctions, typedVarMap, True, [Initial typedVarMap]))+ -- (Q.singleton (maximum (map (\(_, f) -> AERN2.MP.Ball.centre (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)+ 0+ bfsBoxesCutoff+ relativeImprovementCutoff+ 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.+ -> DNFResult TypedVarMap -- ^ The return result for each conjunction is:+ -- (IndeterminateDNF indeterminateArea pavings) means that the algorithm could not make a decision and returns an example of an indeterminate area.+ -- (UnsatDNF listOfPavings) means that the algorithm has decided the DNF is unsatisfiable over the given area.+ -- (SatDNF satArea pavings) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.+ -- For indeterminate and sat DNFs, we return pavings from the conjunction that leads to the result.+ -- For an unsat dnf, we return a list of pavings for each conjunction in the DNF.+checkEDNFDepthFirstWithSimplex conjunctions typedVarMap depthCutoff relativeImprovementCutoff p =+ checkDisjunctionResults conjunctionResults Nothing []+ where+ conjunctionResults =+ parMap rseq+ (\conjunction ->+ let+ substitutedConjunction = substituteConjunctionEqualities conjunction+ substitutedConjunctionVars = nub $ concatMap (E.extractVariablesE . E.extractSafeE) substitutedConjunction+ filteredTypedVarMap =+ filter+ (\(TypedVar (v, (_, _)) _) -> v `elem` substitutedConjunctionVars)+ typedVarMap+ filteredVarMap = typedVarMapToVarMap filteredTypedVarMap+ in+ decideConjunctionDepthFirstWithSimplex (map (\e -> (e, expressionToBoxFun (E.extractSafeE e) filteredVarMap p)) substitutedConjunction) filteredTypedVarMap filteredTypedVarMap 0 depthCutoff relativeImprovementCutoff p [Initial typedVarMap])+ 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.+ -> DNFResult 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 conjunctions typedVarMap bfsBoxesCutoff relativeImprovementCutoff p =+ checkDisjunctionResults conjunctionResults Nothing []+ where+ conjunctionResults =+ parMap rseq+ (\conjunction ->+ let+ substitutedConjunction = substituteConjunctionEqualities conjunction+ substitutedConjunctionVars = nub $ concatMap (E.extractVariablesE . E.extractSafeE) substitutedConjunction+ filteredTypedVarMap =+ filter+ (\(TypedVar (v, (_, _)) _) -> v `elem` substitutedConjunctionVars)+ typedVarMap+ filteredVarMap = typedVarMapToVarMap filteredTypedVarMap+ in+ setupBestFirstCheckDNF (map (\e -> (e, expressionToBoxFun (E.extractSafeE e) filteredVarMap p)) substitutedConjunction) filteredTypedVarMap bfsBoxesCutoff relativeImprovementCutoff p+ )+ 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 expressionsWithFunctions box+ | null filterOutTrueTerms = Just True+ | checkIfEsFalseUsingApply = Just False+ | otherwise = Nothing+ where+ esWithRanges = parMap rseq (\ (e, f) -> ((e, f), apply f box)) expressionsWithFunctions+ -- filterOutTrueTerms = esWithRanges+ filterOutTrueTerms = filterOutTrueExpressions esWithRanges+ checkIfEsFalseUsingApply = decideConjunctionRangesFalse 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, [BoxStep TypedVarMap]) -- ^The priority queue. Maximal minimals are represented using CN MPBall.+ -- Each element in the queue is a tuple with four items.+ -- 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.+ -- The fourth item is a list of paved boxes for 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.+ -> [BoxStep TypedVarMap] -- ^ The boxes that we have checked so far.+ -> DNFConjunctionResult TypedVarMap -- ^ The return result.+ -- (IndetBox, indeterminateArea, pavedBoxes) means that the algorithm could not make a decision and returns an example of an indeterminate area.+ -- (UnsatBox, pavedBoxes) means that the algorithm has decided the DNF is unsatisfiable over the given area.+ -- (SatBox, satArea, pavedBoxes) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.+ -- pavedBoxes is a list storing the boxes that LPPaver has paved through to get to this result.+decideConjunctionBestFirst queue numberOfBoxesExamined numberOfBoxesCutoff relativeImprovementCutoff p currentPavings =+ case Q.maxView queue of+ Just ((expressionsWithFunctions, typedVarMap, isLeftCorner, expressionBoxPavings), queueWithoutFront) ->+ if numberOfBoxesExamined !<! numberOfBoxesCutoff then+ trace (show numberOfBoxesExamined) $+ case decideConjunctionWithSimplexCE expressionsWithFunctions typedVarMap typedVarMap relativeImprovementCutoff p isLeftCorner expressionBoxPavings of+ (UnsatBox pavedBoxes, QueueInfo {}) -> decideConjunctionBestFirst queueWithoutFront (numberOfBoxesExamined + 1) numberOfBoxesCutoff relativeImprovementCutoff p (currentPavings ++ pavedBoxes)+ (SatBox satArea pavedBoxes, QueueInfo {}) -> SatBox satArea (currentPavings ++ pavedBoxes)+ (IndetBox indeterminateVarMap pavedBoxes, QueueInfo filteredExpressionsWithFunctions newIsLeftCorner) ->+ let+ functions = map snd filteredExpressionsWithFunctions+ (leftVarMap, rightVarMap) = trace "bisecting" bisectWidestTypedInterval indeterminateVarMap++ -- createBoxPaving tvm = BoxPaving tvm (if wasPruned then IndetLin else IndetEval) Split++ leftVarMapWithExpressionsAndCornerAndMinimum = trace (show (map fst filteredExpressionsWithFunctions)) $ trace "left"+ (+ fromMaybe (cn (mpBallP p 1000000000000)) (safeAverageDummy functions (typedVarMapToBox leftVarMap p) Nothing),+ (filteredExpressionsWithFunctions, leftVarMap, not newIsLeftCorner, [])+ )+ rightVarMapWithExpressionsAndCornerAndMinimum = trace "right"+ (+ fromMaybe (cn (mpBallP p 1000000000000)) (safeAverageDummy functions (typedVarMapToBox rightVarMap p) Nothing),+ -- fromMaybe (cn (mpBallP p 100000000000)) (safeMaximumUpper functions (typedVarMapToBox rightVarMap p) Nothing),+ -- fromMaybe (cn (dyadic 1048576)) (safeMaximumCentre functions (typedVarMapToBox rightVarMap p) Nothing),+ (filteredExpressionsWithFunctions, rightVarMap, not newIsLeftCorner, [])+ )+ in+ decideConjunctionBestFirst+ (uncurry Q.insert rightVarMapWithExpressionsAndCornerAndMinimum (uncurry Q.insert leftVarMapWithExpressionsAndCornerAndMinimum queueWithoutFront))+ (numberOfBoxesExamined + 1) numberOfBoxesCutoff relativeImprovementCutoff p (currentPavings ++ pavedBoxes ++ [Split indeterminateVarMap leftVarMap rightVarMap])+ -- (_, _, _) -> error "Got unmatched case in decideConjunctionBestFirst"+ else IndetBox typedVarMap currentPavings -- Reached number of boxes cutoff+ Nothing -> UnsatBox currentPavings -- 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.+ -> [BoxStep TypedVarMap] -- The boxes that we have paved so far.+ -> DNFConjunctionResult TypedVarMap -- ^ The return result.+ -- (IndetBox, indeterminateArea, pavedBoxes) means that the algorithm could not make a decision and returns an example of an indeterminate area.+ -- (UnsatBox, pavedBoxes) means that the algorithm has decided the DNF is unsatisfiable over the given area.+ -- (SatBox, satArea, pavedBoxes) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.+ -- pavedBoxes is a list storing the boxes that LPPaver has paved through to get to this result.+decideConjunctionDepthFirstWithSimplex expressionsWithFunctions initialVarMap typedVarMap currentDepth depthCutoff relativeImprovementCutoff p pavedBoxes+ | null filterOutTrueTerms =+ trace ("proved sat with apply " ++ show roundedVarMap)+ SatBox roundedVarMap (pavedBoxes ++ [EvalTrue typedVarMap])+ | checkIfEsFalseUsingApply =+ trace "proved false with apply"+ UnsatBox (pavedBoxes ++ [EvalFalse typedVarMap])+ | otherwise = checkSimplex+ where+ box = typedVarMapToBox typedVarMap p+ varNamesWithTypes = getVarNamesWithTypes typedVarMap+ roundedVarMap =+ case safeBoxToTypedVarMap box varNamesWithTypes of+ Just rvm -> unsafeIntersectVarMap initialVarMap rvm+ Nothing -> error $ "Rounded the following varMap makes it inverted: " ++ show typedVarMap+ untypedRoundedVarMap = typedVarMapToVarMap roundedVarMap++ esWithRanges = parMap rseq (\ (e, f) -> ((e, f), apply f box)) expressionsWithFunctions+ -- filterOutTrueTerms = esWithRanges+ filterOutTrueTerms = filterOutTrueExpressions esWithRanges+ checkIfEsFalseUsingApply = decideConjunctionRangesFalse filterOutTrueTerms++ filteredExpressionsWithFunctions = map fst filterOutTrueTerms++ -- Filter out ranges/derivatives with errors.+ -- This is safe because we do not need every function to enclose the unsat area. + filteredCornerRangesWithDerivatives = computeCornerValuesAndDerivatives filterOutTrueTerms box++ bisectWidestDimensionAndRecurse varMapToBisect currentPavings =+ let+ (leftVarMap, rightVarMap) = bisectWidestTypedInterval varMapToBisect+ -- (leftVarMap, rightVarMap) = bimap (`unsafeIntersectVarMap` varMapToBisect) (`unsafeIntersectVarMap` varMapToBisect) $ bisectWidestTypedInterval varMapToBisect++ -- createBoxPaving tvm = BoxPaving tvm (if wasPruned then IndetLin else IndetEval) Split++ currentPavingsWithSplit = currentPavings ++ [Split varMapToBisect leftVarMap rightVarMap]++ (leftR, rightR) =+ withStrategy+ (parTuple2 rseq rseq)+ (+ decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap leftVarMap (currentDepth + 1) depthCutoff relativeImprovementCutoff p [],+ decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap rightVarMap (currentDepth + 1) depthCutoff relativeImprovementCutoff p [] + )+ in+ case leftR of+ SatBox satModel pavedBoxesLeft -> SatBox satModel $ currentPavingsWithSplit ++ pavedBoxesLeft+ IndetBox indetModel pavedBoxesLeft -> IndetBox indetModel $ currentPavingsWithSplit ++ pavedBoxesLeft+ UnsatBox pavedBoxesLeft+ -> case rightR of+ UnsatBox pavedBoxesRight -> UnsatBox $ currentPavingsWithSplit ++ pavedBoxesLeft ++ pavedBoxesRight+ SatBox satModel pavedBoxesRight -> SatBox satModel $ currentPavingsWithSplit ++ pavedBoxesLeft ++ pavedBoxesRight+ IndetBox indetModel pavedBoxesRight -> IndetBox indetModel $ currentPavingsWithSplit ++ pavedBoxesLeft ++ pavedBoxesRight+ + bisectUntilCutoff varMapToCheck newPavings =+ if currentDepth !<! depthCutoff -- Best first+ then+ bisectWidestDimensionAndRecurse varMapToCheck newPavings+ else+ IndetBox varMapToCheck $ newPavings ++ [GaveUp varMapToCheck]++ checkSimplex+ -- If we can calculate any derivatives+ | (not . null) filteredCornerRangesWithDerivatives = trace "decideWithSimplex start" $+ case removeConjunctionUnsatAreaWithSimplex filteredCornerRangesWithDerivatives untypedRoundedVarMap of+ (Just False, _) -> trace ("decideWithSimplex true: " ++ show roundedVarMap) UnsatBox (pavedBoxes ++ [ContractEmpty typedVarMap])+ (Nothing, Just newVarMap) -> trace "decideWithSimplex indet" $+ case safeVarMapToTypedVarMap newVarMap varNamesWithTypes of+ Just nvm -> recurseOnVarMap safeNvm (pavedBoxes ++ [Contract typedVarMap safeNvm]) where safeNvm = unsafeIntersectVarMap nvm roundedVarMap+ Nothing -> UnsatBox (pavedBoxes ++ [ContractEmpty typedVarMap]) -- This will only happen when all integers in an integer-only varMap have been decided+ _ -> undefined+ | otherwise = bisectUntilCutoff roundedVarMap pavedBoxes++ recurseOnVarMap recurseVarMap newPavings+ | typedMaxWidth recurseVarMap == 0 =+ case decideConjunctionWithApply filteredExpressionsWithFunctions (typedVarMapToBox recurseVarMap p) of+ Just True -> SatBox recurseVarMap (newPavings ++ [EvalTrue recurseVarMap])+ Just False -> UnsatBox (newPavings ++ [EvalFalse recurseVarMap]) + Nothing -> IndetBox recurseVarMap (newPavings ++ [GaveUp recurseVarMap])+ | typedMaxWidth roundedVarMap / typedMaxWidth recurseVarMap >= relativeImprovementCutoff =+ trace ("recursing with simplex with roundedVarMap: " ++ show recurseVarMap) $+ decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap recurseVarMap currentDepth depthCutoff relativeImprovementCutoff p newPavings+ | otherwise = bisectUntilCutoff recurseVarMap newPavings++-- |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.+ -> [BoxStep TypedVarMap] -- The boxes that we have paved so far.+ -> (DNFConjunctionResult TypedVarMap, DNFConjunctionQueueInfo) -- ^The return result is a pair.+ -- For the first element:+ -- (IndetBox, indeterminateArea, pavedBoxes) means that the algorithm could not make a decision and returns an example of an indeterminate area.+ -- (UnsatBox, pavedBoxes) means that the algorithm has decided the DNF is unsatisfiable over the given area.+ -- (SatBox, satArea, pavedBoxes) means that the algorithm has decided the DNF is satisfiable (with satArea being a model) over the given area.+ -- pavedBoxes is a list storing the boxes that LPPaver has paved through to get to this result.+ -- The second element is information useful for an efficient best-first algorithm+decideConjunctionWithSimplexCE expressionsWithFunctions initialVarMap typedVarMap relativeImprovementCutoff p isLeftCorner pavedBoxes+ | null filterOutTrueTerms =+ (SatBox roundedVarMap (pavedBoxes ++ [EvalTrue typedVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ | checkIfEsFalseUsingApply =+ (UnsatBox (pavedBoxes ++ [EvalFalse typedVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ | otherwise = checkSimplex+ where+ box = typedVarMapToBox typedVarMap p+ varNamesWithTypes = getVarNamesWithTypes typedVarMap+ roundedVarMap =+ case safeBoxToTypedVarMap box varNamesWithTypes of+ Just rvm -> unsafeIntersectVarMap initialVarMap rvm+ Nothing -> error $ "Rounded the following varMap makes it inverted: " ++ show typedVarMap+ untypedRoundedVarMap = typedVarMapToVarMap roundedVarMap++ esWithRanges = parMap rseq (\(e, f) -> ((e, f), apply f box)) expressionsWithFunctions+ -- filterOutTrueTerms = esWithRanges+ filterOutTrueTerms = filterOutTrueExpressions esWithRanges+ checkIfEsFalseUsingApply = decideConjunctionRangesFalse filterOutTrueTerms++ filteredExpressionsWithFunctions = map fst filterOutTrueTerms++ -- Filter out ranges/derivatives with errors.+ -- This is safe because we do not need every function to enclose the unsat area. + filteredCornerRangesWithDerivatives = computeCornerValuesAndDerivatives filterOutTrueTerms box++ checkSimplex :: (DNFConjunctionResult TypedVarMap, DNFConjunctionQueueInfo)+ checkSimplex+ -- If we can calculate any derivatives+ | (not . null) filteredCornerRangesWithDerivatives = trace "decideWithSimplex start" $+ trace "decideWithSimplex start" $+ case removeConjunctionUnsatAreaWithSimplex filteredCornerRangesWithDerivatives untypedRoundedVarMap of+ (Just False, _) -> trace ("decideWithSimplex true: " ++ show roundedVarMap) (UnsatBox (pavedBoxes ++ [ContractEmpty typedVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ (Nothing, Just newVarMap) -> trace "decideWithSimplex indet" $+ case safeVarMapToTypedVarMap newVarMap varNamesWithTypes of+ Nothing -> (UnsatBox (pavedBoxes ++ [ContractEmpty typedVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner) -- This will only happen when all integers in an integer-only varMap have been decided+ Just nvm ->+ let+ newTypedVarMap = unsafeIntersectVarMap nvm roundedVarMap+ newBox = typedVarMapToBox newTypedVarMap p+ newPavings = pavedBoxes ++ [Contract typedVarMap newTypedVarMap]++ -- 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 = safelyComputeCornerValuesAndDerivatives filterOutTrueTerms newBox+ in+ trace "findFalsePointWithSimplex start" $+ case mNewCornerRangesWithDerivatives of+ Just newCornerRangesWithDerivatives ->+ case findConjunctionSatAreaWithSimplex newCornerRangesWithDerivatives (typedVarMapToVarMap newTypedVarMap) isLeftCorner of+ Just satSolution ->+ case safeVarMapToTypedVarMap satSolution varNamesWithTypes of+ Just typedSatSolution ->+ if decideConjunctionTrue (map fst filterOutTrueTerms) typedSatSolution p+ then (SatBox typedSatSolution (newPavings ++ [FoundModel newTypedVarMap typedSatSolution]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ else recurseOnVarMap newTypedVarMap newPavings+ Nothing -> error $ "Found sat solution but encountered error when converting to typed sat solution" ++ show satSolution+ Nothing -> recurseOnVarMap newTypedVarMap newPavings+ Nothing -> recurseOnVarMap newTypedVarMap newPavings+ _ -> undefined+ | otherwise = recurseOnVarMap roundedVarMap pavedBoxes++ recurseOnVarMap recurseVarMap newPavings+ | typedMaxWidth recurseVarMap == 0 =+ case decideConjunctionWithApply filteredExpressionsWithFunctions (typedVarMapToBox recurseVarMap p) of+ Just True -> (SatBox recurseVarMap (newPavings ++ [EvalTrue recurseVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ Just False -> (UnsatBox (newPavings ++ [EvalFalse recurseVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ Nothing -> (IndetBox recurseVarMap (newPavings ++ [GaveUp recurseVarMap]), QueueInfo filteredExpressionsWithFunctions isLeftCorner)+ | typedMaxWidth roundedVarMap / typedMaxWidth recurseVarMap >= relativeImprovementCutoff =+ trace ("recursing with simplex with roundedVarMap: " ++ show recurseVarMap) $+ decideConjunctionWithSimplexCE filteredExpressionsWithFunctions initialVarMap recurseVarMap relativeImprovementCutoff p (not isLeftCorner) newPavings+ | otherwise = (IndetBox recurseVarMap newPavings, QueueInfo filteredExpressionsWithFunctions isLeftCorner)
+ src/LPPaver/Algorithm/Linearisation.hs view
@@ -0,0 +1,255 @@+{-|+Module : LPPaver.Algorithm.Linearisation+Description : Linearisations for conjunctions+Copyright : (c) Junaid Rasheed, 2021-2022+License : MPL+Maintainer : jrasheed178@gmail.com+Stability : experimental+Module defining linearisations for conjunctions of 'E.ESafe' terms.+-}+module LPPaver.Algorithm.Linearisation where++import MixedTypesNumPrelude+import qualified PropaFP.Expression as E+import PropaFP.VarMap+import AERN2.MP+import AERN2.MP.Precision+import AERN2.BoxFun.Type+import AERN2.BoxFun.Box+import qualified Data.PQueue.Prio.Max as Q+import Data.Maybe+import PropaFP.Translators.BoxFun+import Control.Parallel.Strategies+import Data.List+import qualified Data.Map as M+import Linear.Simplex.Simplex+import Linear.Simplex.Util+import qualified Linear.Simplex.Types as LT++import LPPaver.Algorithm.Util+import LPPaver.Constraint.Type+import LPPaver.Constraint.Util+import qualified AERN2.Linear.Vector.Type as V+import Data.Bifunctor++-- |Remove unsat areas from a conjunction arising from a DNF by weakening the conjunction using 'createConstraintsToRemoveConjunctionUnsatArea'.+-- The resulting linear system is solved and optimised by the two-phase simplex method.+-- If the linear system is infeasible, the entire conjunction was unsatisfiable.+removeConjunctionUnsatAreaWithSimplex + :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. + -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', + -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', + -- and the third item are partial derivatives of the term over a 'VarMap'.+ -> VarMap -- ^ The VarMap over which we are examining the conjunction.+ -> (Maybe Bool, Maybe VarMap) -- ^ The result of the simplex method on the resulting linear system.+ -- (Just False, Nothing) is returned if the system is infeasible.+ -- (Nothing, Just newArea) is returned if the system is feasible: newArea is an optimisation of the given 'VarMap'.+removeConjunctionUnsatAreaWithSimplex cornerValuesWithDerivatives varMap =+ case mOptimizedVars of+ Just optimizedVars -> (Nothing, Just optimizedVars)+ Nothing -> (Just False, Nothing)+ where+ (simplexSystem, stringIntVarMap) = constraintsToSimplexConstraints $ createConstraintsToRemoveConjunctionUnsatArea cornerValuesWithDerivatives varMap++ vars = map fst varMap++ mFeasibleSolution = findFeasibleSolution simplexSystem+++ -- Uses objective var to extract optimized values for each variable+ extractSimplexResult :: Maybe (Integer, [(Integer, Rational)]) -> Rational+ extractSimplexResult maybeResult =+ case maybeResult of+ Just (optimizedIntVar, result) -> -- optimizedIntVar refers to the objective variable. We extract the value of the objective+ -- variable from the result+ case lookup optimizedIntVar result of+ Just optimizedVarResult -> optimizedVarResult+ Nothing -> error "Extracting simplex result after finding feasible solution resulted in an infeasible result. This should not happen."+ Nothing -> error "Could not optimize feasible system. This should not happen."++ mOptimizedVars =+ case mFeasibleSolution of+ Just (feasibleSystem, slackVars, artificialVars, objectiveVar) ->+ Just $+ map -- Optimize (minimize and maximize) all variables in the varMap+ (\var ->+ case M.lookup var stringIntVarMap of+ Just intVar ->+ case lookup var varMap of+ Just (originalL, _) -> -- In the simplex system, the original lower bound of each var was shifted to 0. We undo this shift after optimization.+ (+ var,+ (+ originalL + extractSimplexResult (optimizeFeasibleSystem (LT.Min [(intVar, 1.0)]) feasibleSystem slackVars artificialVars objectiveVar),+ originalL + extractSimplexResult (optimizeFeasibleSystem (LT.Max [(intVar, 1.0)]) feasibleSystem slackVars artificialVars objectiveVar)+ )+ )+ Nothing -> error "Optimized var not found in original varMap. This should not happen."+ Nothing -> error "Integer version of var not found. This should not happen."+ )+ vars+ Nothing -> Nothing++-- |Find a satisfiable point from a conjunction arising from a DNF by strengthening the conjunction using 'createConstraintsToFindSatSolution'.+-- The resulting linear system is solved by the first phase of the two-phase simplex method.+findConjunctionSatAreaWithSimplex + :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. + -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', + -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', + -- and the third item are partial derivatives of the term over a 'VarMap'.+ -> VarMap -- ^ The VarMap over which we are examining the conjunction.+ -> Bool -- ^ A boolean used to determine which 'extreme' corner to strengthen the conjunction from.+ -- If true, linearise from the 'extreme' left corner and vice versa.+ -> Maybe VarMap -- ^ The result. If this is Nothing, no satisfiable point was found.+findConjunctionSatAreaWithSimplex cornerValuesWithDerivatives varMap isLeftCorner =+ case mFeasibleVars of+ Just newPoints ->+ Just+ $+ map+ (\var ->+ case M.lookup var stringIntVarMap of+ Just intVar ->+ case lookup var varMap of+ Just (originalL, _) -> -- In the simplex system, the original lower bound of each var was shifted to 0. We undo this shift after finding a feasible solution+ (+ var,+ let feasiblePoint = originalL + fromMaybe 0.0 (lookup intVar newPoints)+ in (feasiblePoint, feasiblePoint)+ )+ Nothing -> error "Optimized var not found in original varMap. This should not happen."+ Nothing -> error "Integer version of var not found. This should not happen."+ )+ vars+ Nothing -> trace "no sat solution" Nothing+ where+ (simplexSystem, stringIntVarMap) = constraintsToSimplexConstraints $ createConstraintsToFindSatSolution cornerValuesWithDerivatives varMap isLeftCorner++ vars = map fst varMap++ mFeasibleSolution = findFeasibleSolution simplexSystem++ mFeasibleVars =+ case mFeasibleSolution of+ Just (feasibleSystem, _slackVars, _artificialVars, _objectiveVar) -> Just $ displayDictionaryResults feasibleSystem+ Nothing -> Nothing++-- |Linearisations that weaken a conjunction of terms over some box.+createConstraintsToRemoveConjunctionUnsatArea + :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. + -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', + -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', + -- and the third item are partial derivatives of the term over a 'VarMap'.+ -> VarMap -- ^ The VarMap over which we are examining the conjunction.+ -> [Constraint] -- ^ An implicit linear system that is a weakening of the conjunction.+createConstraintsToRemoveConjunctionUnsatArea cornerValuesWithDerivatives varMap =+ domainConstraints ++ functionConstraints+ where+ vars = map fst varMap+ varsNewUpperBounds = map (\(_, (l, r)) -> r - l) varMap++ -- var >= varLower - varLower && var <= varUpper - varLower+ -- Since var >= 0 is assumed by the simplex method, var >= varLower - varLower is not needed+ domainConstraints =+ map+ (\(var, (varLower, varUpper)) ->+ LEQ [(var, 1.0)] $ varUpper - varLower+ )+ varMap++ -- The following constraints in this variable are...+ -- fn - (fnx1GradientR * x1) - .. - (fnxnGradientR * xn) <= fnLeftCorner + (fnx1GradientR * -x1L) + .. + (fnxnGradientR * -xnL)+ -- fn - (fnx1GradientL * x1) - .. - (fnxnGradientL * xn) <= fnRightCorner + (-fnx1GradientL * x1R) + .. + (-fnxnGradientL * xnR)+ -- and these are equivalent to...+ -- fn <= fnLeftCorner + (fnx1GradientR * (x1 - x1L)) + .. + (fnxnGradientR * (xn - xnL))+ -- fn <= fnRightCorner + (-fnx1GradientL * (x1R - x1)) + .. + (-fnxnGradientL * (xnR - xn))+ -- + functionConstraints =+ concatMap+ (\(fnInt, (fLeftRange, fRightRange, fPartialDerivatives)) ->+ let+ fNegatedPartialDerivativesLowerBounds = map (negate . fst . mpBallToRational) $ V.toList fPartialDerivatives+ fNegatedPartialDerivativesUpperBounds = map (negate . snd . mpBallToRational) $ V.toList fPartialDerivatives+ fLeftUpperBound = snd $ mpBallToRational fLeftRange+ fRightUpperBound = snd $ mpBallToRational fRightRange++ in+ [+ -- f is definitely below this line from the left corner+ -- Multiplication with left corner and partial derivatives omitted, since left corner is zero+ LEQ (zip vars fNegatedPartialDerivativesUpperBounds)+ fLeftUpperBound,+ -- f is definitely below this line from the right corner+ LEQ (zip vars fNegatedPartialDerivativesLowerBounds)+ $ foldl add fRightUpperBound $ zipWith mul varsNewUpperBounds fNegatedPartialDerivativesLowerBounds+ ]+ )+ $+ zip+ [1..]+ cornerValuesWithDerivatives++ mpBallToRational :: CN MPBall -> (Rational, Rational)+ mpBallToRational = bimap rational rational . endpoints . reducePrecionIfInaccurate . unCN++-- |Linearisations that strengthen a conjunction of terms over some box.+createConstraintsToFindSatSolution+ :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. + -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', + -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', + -- and the third item are partial derivatives of the term over a 'VarMap'.+ -> VarMap -- ^ The VarMap over which we are examining the conjunction.+ -> Bool -- ^ A boolean used to determine which 'extreme' corner to strengthen the conjunction from.+ -- If true, linearise from the 'extreme' left corner and vice versa.+ -> [Constraint] -- ^ An implicit linear system that is a weakening of the conjunction.+createConstraintsToFindSatSolution cornerValuesWithDerivatives varMap isLeftCorner =+ domainConstraints ++ functionConstraints+ where+ vars = map fst varMap+ varsNewUpperBounds = map (\(_, (l, r)) -> r - l) varMap++ -- var >= varLower - varLower && var <= varUpper - varLower+ -- Since var >= 0 is assumed by the simplex method, var >= varLower - varLower is not needed+ domainConstraints =+ map+ (\(var, (varLower, varUpper)) ->+ LEQ [(var, 1.0)] $ varUpper - varLower+ )+ varMap++ -- The following constraints in this variable are...+ -- Left corner: fn - (fnx1GradientL * x1) - .. - (fnxnGradientL * xn) <= fnLeftCorner - (fnx1GradientL * x1L) - .. - (fnx1GradientL * x1L)+ -- Right corner: fn - (fnx1GradientR * x1) - .. - (fnxnGradientR * xn) <= fnRightCorner - (fnx1GradientR * x1R) - .. - (fnx1GradientR * x1R)+ -- and these are equivalent to...+ -- Left corner: fn <= fnLeftCorner + (fnx1GradientL * (x1 - x1L)) + .. + (fnxnGradientL * (xn - xnL))+ -- Right corner: fn <= ynRightCorner + (-fnx1GradientR * (xR - x)) + .. + (-fnxnGradientR * (xnR - xn))+ functionConstraints =+ zipWith+ (curry+ (\(fnInt, (fLeftRange, fRightRange, fPartialDerivatives)) ->+ let+ fNegatedPartialDerivativesLowerBounds = map (negate . fst . mpBallToRational) $ V.toList fPartialDerivatives+ fNegatedPartialDerivativesUpperBounds = map (negate . snd . mpBallToRational) $ V.toList fPartialDerivatives+ fLeftLowerBound = fst $ mpBallToRational fLeftRange+ fRightLowerBound = fst $ mpBallToRational fRightRange++ --FIXME: make this safe. Check if vars contain ^fSimplex[0-9]+$. If so, try ^fSimplex1[0-9]+$ or something+ in+ if isLeftCorner+ then+ -- f is definitely above this line from the left corner+ -- Multiplication with left corner and partial derivatives omitted, since left corner is zero+ LEQ (zip vars fNegatedPartialDerivativesLowerBounds)+ fLeftLowerBound+ else+ -- f is definitely above this line from the right corner+ LEQ (zip vars fNegatedPartialDerivativesUpperBounds)+ $ foldl add fRightLowerBound $ zipWith mul varsNewUpperBounds fNegatedPartialDerivativesUpperBounds++ )+ )+ [1..]+ cornerValuesWithDerivatives++ mpBallToRational :: CN MPBall -> (Rational, Rational)+ mpBallToRational = bimap rational rational . endpoints . reducePrecionIfInaccurate . unCN
+ src/LPPaver/Algorithm/Type.hs view
@@ -0,0 +1,34 @@+{-|+Module : LPPaver.Algorithm.Type+Description : Defines types useful for our decision algorithms.+Copyright : (c) Junaid Rasheed, 2022+License : MPL+Maintainer : jrasheed178@gmail.com+Stability : experimental+Module defining the useful types for our decision algorithms.+-}+module LPPaver.Algorithm.Type where++import MixedTypesNumPrelude+import qualified Prelude as P+import LPPaver.Constraint.Type+import PropaFP.Expression (ESafe)+import AERN2.BoxFun.Type (BoxFun)++-- |The result of evaluating a box as well as a list of pavings that leads to said box+data BoxStep box = Initial box | EvalTrue box | EvalFalse box | GaveUp box | Split box box box | Contract box box | ContractEmpty box | FoundModel box box + deriving (P.Eq, Show)++-- |The result of a box against some conjunction as well as a list of steps that leads to said result.+data DNFConjunctionResult box = SatBox box [BoxStep box] | UnsatBox [BoxStep box] | IndetBox box [BoxStep box]+ deriving (P.Eq, Show)++-- |The result of a box against some DNF.+-- If sat, give a list of pavings that leads to the satisfiable box.+-- If indeterminate, give a list of pavings that leads to the indeterminate box for an arbitrary conjunction in the DNF.+-- If unsat, give a list of list of pavings. Each inner list show the steps for each conjunction that lead to the unsat result.+data DNFResult box = SatDNF box [BoxStep box] | UnsatDNF [[BoxStep box]] | IndeterminateDNF box [BoxStep box]+ deriving (P.Eq, Show)++-- |Information required for an efficient best-first queue algorithm+data DNFConjunctionQueueInfo = QueueInfo {expressionsWithFunctions :: [(ESafe, BoxFun)], wasLeftCornerLinearisedLast :: Bool}
+ src/LPPaver/Algorithm/Util.hs view
@@ -0,0 +1,577 @@+{-|+Module : LPPaver.Algorithm.Util+Description : Utility functions for LPPaver.Algorithm modules+Copyright : (c) Junaid Rasheed, 2021-2022+License : MPL+Maintainer : jrasheed178@gmail.com+Stability : experimental+Module defining useful utility functions for the LPPaver.Algorithm modules+-}+module LPPaver.Algorithm.Util where++import MixedTypesNumPrelude+import qualified Prelude as P+import Data.List (nub, sortBy, partition)+import Data.Bifunctor+import PropaFP.Parsers.Smt (findVariablesInExpressions)+import AERN2.MP.Dyadic+import Control.CollectErrors+import AERN2.MP.Ball+import qualified Numeric.CollectErrors as CN+import AERN2.BoxFun.Type+import AERN2.BoxFun.Box+import qualified PropaFP.Expression as E+import PropaFP.VarMap+import qualified AERN2.Linear.Vector.Type as V+import AERN2.Kleenean+import PropaFP.Translators.BoxFun+import AERN2.BoxFun.Optimisation+import Control.Parallel.Strategies+import LPPaver.Algorithm.Type++-- TODO: Remove traces+-- |Dummy trace function+trace a x = x++-- |Calculate the range of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'apply'.+applyExpression :: E.E -> VarMap -> Precision -> CN MPBall+applyExpression expression varMap p =+ apply f (varMapToBox varMap p)+ where+ f = expressionToBoxFun expression varMap p++-- |Calculate the gradient of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'gradient'.+gradientExpression :: E.E -> VarMap -> Precision -> V.Vector (CN MPBall)+gradientExpression expression varMap p =+ gradient f (varMapToBox varMap p)+ where+ f = expressionToBoxFun expression varMap p++-- |Run 'applyExpression' on each 'E.E' in a given list+applyExpressionList :: [E.E] -> VarMap -> Precision -> [CN MPBall]+applyExpressionList expressions varMap p =+ map+ (\e -> apply (expressionToBoxFun e varMap p) box)+ expressions+ where+ box = varMapToBox varMap p++-- |Run 'gradientExpression' on each 'E.E' in a given list+gradientExpressionList :: [E.E] -> VarMap -> Precision -> [V.Vector (CN MPBall)]+gradientExpressionList expressions varMap p =+ map+ (\e -> gradientExpression e varMap p)+ expressions++-- |Run 'applyExpressionList' on each '[E.E]' in a given list+applyExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[CN MPBall]]+applyExpressionDoubleList cnf varMap p = map (\d -> applyExpressionList d varMap p) cnf++-- |Run 'gradientExpressionList' on each '[E.E]' in a given list+gradientExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]+gradientExpressionDoubleList cnf varMap p = map (\d -> gradientExpressionList d varMap p) cnf++-- |Run 'applyExpressionDoubleList' on an [['E.ESafe']]+applyESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[CN MPBall]]+applyESafeDoubleList cnf = applyExpressionDoubleList (map (map E.extractSafeE) cnf)++-- |Run 'gradientExpressionDoubleList' on an [['E.ESafe']]+gradientESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]+gradientESafeDoubleList cnf = gradientExpressionDoubleList (map (map E.extractSafeE) cnf)++-- |Evaluate an 'E.F' over some 'VarMap' with a given 'Precision' using 'applyExpression'+checkFWithApply :: E.F -> VarMap -> Precision -> CN Kleenean+checkFWithApply (E.FComp op e1 e2) varMap p =+ case op of+ E.Ge -> e1Val >= e2Val+ E.Gt -> e1Val > e2Val+ E.Le -> e1Val <= e2Val+ E.Lt -> e1Val < e2Val+ E.Eq -> e1Val == e2Val+ where+ e1Val = applyExpression e1 varMap p+ e2Val = applyExpression e2 varMap p+checkFWithApply (E.FConn op f1 f2) varMap p =+ case op of+ E.And -> f1Val && f2Val+ E.Or -> f1Val || f2Val+ E.Impl -> not f1Val || f2Val+ where+ f1Val = checkFWithApply f1 varMap p+ f2Val = checkFWithApply f2 varMap p+checkFWithApply (E.FNot f) varMap p = not $ checkFWithApply f varMap p+checkFWithApply E.FTrue _ _ = cn CertainTrue+checkFWithApply E.FFalse _ _ = cn CertainFalse++-- |Filter out expressions in a list which are certainly false.+-- If an expression cannot be evaluated, do not filter it out.+filterOutFalseExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]+filterOutFalseExpressions =+ filter+ (\((safeE, _), range) ->+ case safeE of+ E.EStrict _ -> hasError range || not (range !<=! 0) -- We cannot decide on ranges with errors, so do not filter them out+ E.ENonStrict _ -> hasError range || not (range !<! 0)+ )++-- |Filter out expressions in a list which are certainly true.+-- If an expression cannot be evaluated, do not filter it out.+filterOutTrueExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]+filterOutTrueExpressions =+ filter+ (\((safeE, _), range) ->+ hasError range || -- Do not filter if there is an error+ (+ case safeE of+ E.EStrict _ ->+ case unCN range > 0 of+ CertainTrue -> False+ _ -> True+ -- We cannot decide on ranges with errors, so do not filter them out+ E.ENonStrict _ ->+ case unCN range >= 0 of+ CertainTrue -> False+ _ -> True+ )+ )++-- |Returns true if any of the ranges of the given Expression have been evaluated to be greater than or equal to zero.+decideRangesGEZero :: [((E.E, BoxFun), CN MPBall)] -> Bool+decideRangesGEZero = any (\(_, range) -> not (hasError range) && range !>=! 0)++-- |The mean of a list of 'CN Dyadic' numbers.+mean :: [CN Dyadic] -> CN Rational+mean xs = sum xs / length xs++-- |Safely find the maximum of a list of ordered elements, avoiding exceptions by ignoring anything with errors+safeMaximum :: (HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a), CanTestErrorsPresent a) =>+ a -> [a] -> a+safeMaximum currentMax [] = currentMax+safeMaximum currentMax (x : xs) =+ if hasError x+ then safeMaximum currentMax xs+ else safeMaximum (if x !>! currentMax then x else currentMax) xs++safeAverageDummy :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeAverageDummy a b _ = safeCentreAverage a b++-- |Safely find the centre of the average of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeCentreAverage :: [BoxFun] -> Box -> Maybe (CN MPBall)+safeCentreAverage fs b = (cnMPBall . AERN2.MP.Ball.centre) <$> aux fs b ((cn . mpBall) 0) 0+ where+ aux :: [BoxFun] -> Box -> CN MPBall -> Integer -> Maybe (CN MPBall)+ aux [] _ sum amount = + case amount of+ 0 -> Nothing+ _ -> Just (sum / amount)+ aux (f : fs) box sum amount =+ if hasError range+ then aux fs box sum amount+ else aux fs box (sum + range) (amount + 1)+ where+ range = apply f box++-- |Safely find the upper bound of the average of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeAverageUpper :: [BoxFun] -> Box -> Maybe (CN MPBall)+safeAverageUpper fs b = (snd . endpointsAsIntervals) <$> aux fs b ((cn . mpBall) 0) 0+ where+ aux :: [BoxFun] -> Box -> CN MPBall -> Integer -> Maybe (CN MPBall)+ aux [] _ sum amount = + case amount of+ 0 -> Nothing+ _ -> Just (sum / amount)+ aux (f : fs) box sum amount =+ if hasError range+ then aux fs box sum amount+ else aux fs box (sum + range) (amount + 1)+ where+ range = apply f box++-- |Safely find the lower bound of the average of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeAverageLower :: [BoxFun] -> Box -> Maybe (CN MPBall)+safeAverageLower fs b = (snd . endpointsAsIntervals) <$> aux fs b ((cn . mpBall) 0) 0+ where+ aux :: [BoxFun] -> Box -> CN MPBall -> Integer -> Maybe (CN MPBall)+ aux [] _ sum amount = + case amount of+ 0 -> Nothing+ _ -> Just (sum / amount)+ aux (f : fs) box sum amount =+ if hasError range+ then aux fs box sum amount+ else aux fs box (sum + range) (amount + 1)+ where+ range = apply f box++-- |Safely find the maximum of the centres of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMaximumCentre :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMaximumCentre [] _ mCurrentCentre = mCurrentCentre+safeMaximumCentre (f : fs) box mCurrentCentre =+ if hasError range+ then safeMaximumCentre fs box mCurrentCentre+ else+ case mCurrentCentre of+ Just currentCentre ->+ if currentCentre !>=! rangeCentre+ then safeMaximumCentre fs box mCurrentCentre+ else safeMaximumCentre fs box (Just rangeCentre)+ Nothing -> safeMaximumCentre fs box (Just rangeCentre)+ where+ range = apply f box+ rangeCentre = cnMPBall $ AERN2.MP.Ball.centre range++-- |Safely find the minimum of the centres of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMinimumCentre :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMinimumCentre [] _ mCurrentCentre = mCurrentCentre+safeMinimumCentre (f : fs) box mCurrentCentre =+ if hasError range+ then safeMinimumCentre fs box mCurrentCentre+ else+ case mCurrentCentre of+ Just currentCentre ->+ if currentCentre !>=! rangeCentre+ then safeMinimumCentre fs box mCurrentCentre+ else safeMinimumCentre fs box (Just rangeCentre)+ Nothing -> safeMinimumCentre fs box (Just rangeCentre)+ where+ range = apply f box+ rangeCentre = cnMPBall $ AERN2.MP.Ball.centre range++-- |Safely find the maximum of the lower bounds of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMaximumLower :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMaximumLower [] _ mCurrentMin = mCurrentMin+safeMaximumLower (f : fs) box mCurrentMin =+ if hasError range+ then safeMaximumLower fs box mCurrentMin+ else+ case mCurrentMin of+ Just currentMin ->+ if currentMin !>=! rangeMin+ then safeMaximumLower fs box mCurrentMin+ else safeMaximumLower fs box (Just rangeMin)+ Nothing -> safeMaximumLower fs box (Just rangeMin)+ where+ range = apply f box+ rangeMin = fst $ endpointsAsIntervals range++-- |Safely find the maximum of the upper bounds of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMaximumUpper :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMaximumUpper [] _ mCurrentMax = mCurrentMax+safeMaximumUpper (f : fs) box mCurrentMax =+ if hasError range+ then safeMaximumUpper fs box mCurrentMax+ else+ case mCurrentMax of+ Just currentMax ->+ if currentMax !>=! rangeMax+ then safeMaximumUpper fs box mCurrentMax+ else safeMaximumUpper fs box (Just rangeMax)+ Nothing -> safeMaximumUpper fs box (Just rangeMax)+ where+ range = apply f box+ rangeMax = snd $ endpointsAsIntervals range++-- |Safely find the minimum of the lower bounds of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMinimumLower :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMinimumLower [] _ mCurrentMin = mCurrentMin+safeMinimumLower (f : fs) box mCurrentMin =+ if hasError range+ then safeMinimumLower fs box mCurrentMin+ else+ case mCurrentMin of+ Just currentMin ->+ if currentMin !<=! rangeMin+ then safeMinimumLower fs box mCurrentMin+ else safeMinimumLower fs box (Just rangeMin)+ Nothing -> safeMinimumLower fs box (Just rangeMin)+ where+ range = apply f box+ rangeMin = fst $ endpointsAsIntervals range++-- |Safely find the minimum of the upper bounds of the ranges of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors+safeMinimumUpper :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)+safeMinimumUpper [] _ mCurrentMax = mCurrentMax+safeMinimumUpper (f : fs) box mCurrentMax =+ if hasError range+ then safeMinimumUpper fs box mCurrentMax+ else+ case mCurrentMax of+ Just currentMax ->+ if currentMax !<=! rangeMax+ then safeMinimumUpper fs box mCurrentMax+ else safeMinimumUpper fs box (Just rangeMax)+ Nothing -> safeMinimumUpper fs box (Just rangeMax)+ where+ range = apply f box+ rangeMax = snd $ endpointsAsIntervals range++-- TODO: Move to PropaFP+-- |Bisect the widest interval in a 'VarMap'+bisectWidestInterval :: VarMap -> (VarMap, VarMap)+bisectWidestInterval [] = error "Given empty box to bisect"+bisectWidestInterval vm = bisectVar vm widestVar+ where+ (widestVar, _) = widestInterval (tail vm) (head vm)++-- TODO: Move to PropaFP+-- |Bisect the widest interval in a 'TypedVarMap'+bisectWidestTypedInterval :: TypedVarMap -> (TypedVarMap, TypedVarMap)+bisectWidestTypedInterval [] = error "Given empty box to bisect"+bisectWidestTypedInterval vm = bisectTypedVar vm widestVar+ where+ (widestVar, _) = widestTypedInterval (tail vm) $ typedVarIntervalToVarInterval (head vm)++-- TODO: Move to PropaFP+-- |Ensures that the first varMap is within the second varMap+-- If it is, returns the first varMap.+-- If it isn't modifies the varMap so that the returned varMap is within the second varMap+-- Both varmaps must have the same number of vars in the same order (order of vars not checked)+ensureVarMapWithinVarMap :: VarMap -> VarMap -> VarMap+ensureVarMapWithinVarMap [] [] = []+ensureVarMapWithinVarMap ((v, (roundedL, roundedR)) : rvm) ((_, (originalL, originalR)) : ovm) =+ (v, (if roundedL < originalL then originalL else roundedL, if roundedR > originalR then originalR else roundedR))+ : ensureVarMapWithinVarMap rvm ovm+ensureVarMapWithinVarMap _ _ = error "Different sized varMaps"++-- |Version of 'computeCornerValuesAndDerivatives' that returns Nothing if a calculation contains an error+safelyComputeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> Maybe [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]+safelyComputeCornerValuesAndDerivatives esWithRanges box =+ if cornerRangesWithDerivativesHasError+ then Nothing+ else Just cornerRangesWithDerivatives+ where+ boxL = lowerBounds box+ boxU = upperBounds box++ -- filteredCornerRangesWithDerivatives = + -- [+ -- value |+ -- value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,+ -- not (hasError value)+ -- ]++ cornerRangesWithDerivatives =+ parMap rseq+ (\ ((_, f), _) -> (apply f boxL, apply f boxU, gradient f box))+ esWithRanges++ -- Check if any function contains errors+ cornerRangesWithDerivativesHasError =+ any+ (\(l, r, c) -> hasError l || hasError r || V.any hasError c)+ cornerRangesWithDerivatives++-- |Return the value of the given 'E.ESafe' expression/'BoxFun' at the extreme left corner and the extreme right corner as well as partial derivatives over the given 'Box'.+-- Extreme corners are defined as the minimum/maximum of every interval in a 'Box' for the left/right extreme corners respectively.+computeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]+computeCornerValuesAndDerivatives esWithRanges box = filteredCornerRangesWithDerivatives+ where+ boxL = lowerBounds box+ boxU = upperBounds box++ -- filteredCornerRangesWithDerivatives = + -- [+ -- value |+ -- value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,+ -- not (hasError value)+ -- ]++ cornerRangesWithDerivatives =+ parMap rseq+ (\ ((_, f), _) -> (apply f boxL, apply f boxU, gradient f box))+ esWithRanges++ -- Keep the functions where we can calculate all derivatives+ filteredCornerRangesWithDerivatives =+ filter+ (\(l, r, c) -> not (hasError l || hasError r || V.any hasError c)) -- Filter out functions where any partial derivative or corners contain an error+ cornerRangesWithDerivatives++-- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is false in a standard manner+-- A range with an error is treated as false.+decideConjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool+decideConjunctionRangesFalse =+ any+ (\((safeE, _), range) ->+ case safeE of+ E.EStrict _ -> not (hasError range) && range !<=! 0+ E.ENonStrict _ -> not (hasError range) && range !<! 0+ )++-- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is true in a standard manner+-- A range with an error is treated as false.+decideConjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool+decideConjunctionRangesTrue =+ all+ (\((safeE, _), range) ->+ case safeE of+ E.EStrict _ -> not (hasError range) && range !>! 0+ E.ENonStrict _ -> not (hasError range) && range !>=! 0+ )+++-- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is true in a standard manner+-- A range with an error is treated as false.+decideDisjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool+decideDisjunctionRangesTrue =+ any+ (\((safeE, _), range) ->+ case safeE of+ E.EStrict _ -> not (hasError range) && range !>! 0+ E.ENonStrict _ -> not (hasError range) && range !>=! 0+ )++-- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is false in a standard manner+-- A range with an error is treated as false.+decideDisjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool+decideDisjunctionRangesFalse =+ all+ (\((safeE, _), range) ->+ case safeE of+ E.EStrict _ -> not (hasError range) && not (hasError range) && range !<=! 0+ E.ENonStrict _ -> not (hasError range) && range !<! 0+ )++-- |Evaluate the range of each 'E.ESafe' expression in a disjunction and check if the disjunction is false in a standard manner. +decideDisjunctionFalse :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool+decideDisjunctionFalse expressionsWithFunctions varMap p =+ all+ (\(safeE, f) ->+ let+ range = apply f (typedVarMapToBox varMap p)+ in+ case safeE of+ E.EStrict _ -> not (hasError range) && range !<=! 0+ E.ENonStrict _ -> not (hasError range) && range !<! 0+ )+ expressionsWithFunctions++-- |Evaluate the range of each 'E.ESafe' expression in a CNF and check if the CNF is false in a standard manner. +decideCNFFalse :: [[(E.ESafe, BoxFun)]] -> TypedVarMap -> Precision -> Bool+decideCNFFalse c v p = any (\d -> decideDisjunctionFalse d v p) c++-- |Evaluate the range of each 'E.ESafe' expression in a conjunction and check if the conjunction is true in a standard manner. +decideConjunctionTrue :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool+decideConjunctionTrue c v p =+ all (\(safeE, f) ->+ let+ range = apply f (typedVarMapToBox v p)+ in+ case safeE of+ E.EStrict _ -> not (hasError range) && range !>! 0+ E.ENonStrict _ -> not (hasError range) && range !>=! 0+ )+ c++-- |Check the results of a disjunction of 'DNFConjunctionResult's in a standard manner+checkDisjunctionResults :: [DNFConjunctionResult box] -> Maybe (DNFConjunctionResult box) -> [[BoxStep box]] -> DNFResult box+checkDisjunctionResults [] (Just (IndetBox indeterminateArea indeterminatePavings)) _ = IndeterminateDNF indeterminateArea indeterminatePavings+checkDisjunctionResults [] _ unsatPavings = UnsatDNF unsatPavings+checkDisjunctionResults (result : results) mIndeterminateArea unsatPavings =+ case result of+ r@(SatBox potentialModel pavings) -> SatDNF potentialModel pavings+ (UnsatBox pavings) -> checkDisjunctionResults results mIndeterminateArea (unsatPavings ++ [pavings])+ r@(IndetBox _ _) -> checkDisjunctionResults results (Just r) unsatPavings++-- |Check the results of a conjunction in a standard manner+checkConjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)+checkConjunctionResults [] Nothing = (Just True, Nothing)+checkConjunctionResults [] indeterminateArea@(Just _) = (Nothing, indeterminateArea)+checkConjunctionResults (result : results) mIndeterminateArea =+ case result of+ (Just True, _) -> checkConjunctionResults results mIndeterminateArea+ r@(Just False, _) -> r+ (Nothing, indeterminateArea@(Just _)) -> checkConjunctionResults results indeterminateArea+ (Nothing, Nothing) -> undefined++-- |Substitute all variable-defining equalities in a given conjunction.+-- Simplify the conjunction after substituting all variable-defining equalities.+substituteConjunctionEqualities :: [E.ESafe] -> [E.ESafe]+substituteConjunctionEqualities [] = []+substituteConjunctionEqualities conjunction@(conjunctionHead : conjunctionTail) =+ case equations of+ [] -> nub $ conjunction+ _ -> substituteConjunctionEqualities substConj+ where+ -- these equalities will not have any contradictions, they should already have been dealt with by deriveBounds and simplifyFDNF.+ equations = findVarDefiningEquations conjunctionHead conjunctionTail conjunctionTail+ (eq : eqs) = equations++ substConj = substituteAndSimplifyChosenEquation selectedDupe conjunction+ -- simplifiedSubstitutedConjunction = map (E.fmapESafe E.simplifyE) conjunction++ -- find duplicates for the first equation+ (dupes, nonDupes) = findDuplicateEquations eq eqs++ -- sort duplicates based on length+ sortedDupes = sortBy (\(_, y1) (_, y2) -> P.compare y1 y2) (eq : dupes)++ -- partition duplicates based on whether or not they contain variables+ (varFreeDupes, varContainingDupes) = partition (\(_, e) -> E.hasVarsE e) sortedDupes++ -- Select an equality to substitute+ -- Selects the shortest var-free equality or, if a var-free equality does not exist, the shortest equality+ selectedDupe = head $ varFreeDupes ++ varContainingDupes++ -- Find other var-defining equations for the var in the given equation+ findDuplicateEquations :: (String, E.E) -> [(String, E.E)] -> ([(String, E.E)], [(String, E.E)])+ findDuplicateEquations _ [] = ([],[])+ findDuplicateEquations (x1, y1) ((x2, y2) : es)+ | x1 P.== x2 =+ first ((x2, y2) :) $ findDuplicateEquations (x1, y1) es+ | otherwise =+ second ((x2, y2) :) $ findDuplicateEquations (x1, y1) es++ -- substitute the given equation in the given conjunction+ substituteAndSimplifyChosenEquation :: (String, E.E) -> [E.ESafe] -> [E.ESafe]+ substituteAndSimplifyChosenEquation _ [] = []+ substituteAndSimplifyChosenEquation (x, y) (e : c) = E.fmapESafe (\nonSafeE -> E.simplifyE (E.replaceEInE nonSafeE (E.Var x) y)) e : substituteAndSimplifyChosenEquation (x, y) c++ -- Find var equations+ -- Essentially, find Es in the conjunction of the form Var v >= e, Var v <= e+ -- The e is ignored if it contains Var v+ -- Else, store this equality as v, e in the resulting list + findVarDefiningEquations :: E.ESafe -> [E.ESafe] -> [E.ESafe] -> [(String, E.E)]+ findVarDefiningEquations _ [] [] = []+ findVarDefiningEquations _ [] (e : conj) = findVarDefiningEquations e conj conj+ findVarDefiningEquations e1 (e2 : es) conj =+ case e1 of+ -- x1 - y1 >= 0+ E.ENonStrict (E.EBinOp E.Sub v@(E.Var x1) y1) ->+ -- ignore circular equalities+ if x1 `elem` findVariablesInExpressions y1 then findVarDefiningEquations e1 es conj else+ case e2 of+ -- x2 - y2 >= 0+ E.ENonStrict (E.EBinOp E.Sub x2 (E.Var y2)) ->+ -- if we have x - y >= 0 && y - x >= 0, then y - x = 0, so y = x+ if x1 P.== y2 && y1 P.== x2+ then+ (x1, y1) : findVarDefiningEquations e1 es conj+ else findVarDefiningEquations e1 es conj+ _ -> findVarDefiningEquations e1 es conj+ -- y1 - x1 >= 0+ E.ENonStrict (E.EBinOp E.Sub y1 v@(E.Var x1)) ->+ -- ignore circular equalities+ if x1 `elem` findVariablesInExpressions y1 then findVarDefiningEquations e1 es conj else+ case e2 of+ -- y2 - x2 >= 0+ E.ENonStrict (E.EBinOp E.Sub (E.Var y2) x2) ->+ -- if we have y - x >= 0 && x - y >= 0, then y - x = 0, so y = x+ if x1 P.== y2 && y1 P.== x2+ then+ (x1, y1) : findVarDefiningEquations e1 es conj+ else findVarDefiningEquations e1 es conj+ _ -> findVarDefiningEquations e1 es conj+ -- x >= 0+ E.ENonStrict v1@(E.Var x1) ->+ case e2 of+ -- -x >= 0+ E.ENonStrict (E.EUnOp E.Negate (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj+ -- 0 - x+ E.ENonStrict (E.EBinOp E.Sub (E.Lit 0.0) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj+ -- -1 * x+ E.ENonStrict (E.EBinOp E.Mul (E.Lit (-1.0)) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj+ -- (-(1)) * x+ E.ENonStrict (E.EBinOp E.Mul (E.EUnOp E.Negate (E.Lit (1.0))) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj+ _ -> findVarDefiningEquations e1 es conj+ _ -> findVarDefiningEquations e1 es conj
− src/LPPaver/Decide/Algorithm.hs
@@ -1,363 +0,0 @@-{-|-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 expressionsWithFunctions typedVarMap bfsBoxesCutoff relativeImprovementCutoff p =- decideConjunctionBestFirst- -- (Q.singleton (maximum (map (\(_, f) -> (snd . endpointsAsIntervals) (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)- (Q.singleton- -- Maximum minimum - (fromMaybe (cn (mpBallP p 1000000000000)) (safeMaximumMinimum (map snd expressionsWithFunctions) (typedVarMapToBox typedVarMap p) Nothing))- (expressionsWithFunctions, typedVarMap, True))- -- (Q.singleton (maximum (map (\(_, f) -> AERN2.MP.Ball.centre (apply f (typedVarMapToBox typedVarMap p))) expressionsWithFunctions)) typedVarMap)- 0- bfsBoxesCutoff- relativeImprovementCutoff- 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 conjunctions typedVarMap depthCutoff relativeImprovementCutoff p =- checkDisjunctionResults conjunctionResults Nothing- where- conjunctionResults =- parMap rseq- (\conjunction ->- let- substitutedConjunction = substituteConjunctionEqualities conjunction- substitutedConjunctionVars = nub $ concatMap (E.extractVariablesE . E.extractSafeE) substitutedConjunction- filteredTypedVarMap =- filter- (\(TypedVar (v, (_, _)) _) -> v `elem` substitutedConjunctionVars)- typedVarMap- filteredVarMap = typedVarMapToVarMap filteredTypedVarMap- in- decideConjunctionDepthFirstWithSimplex (map (\e -> (e, expressionToBoxFun (E.extractSafeE e) filteredVarMap p)) substitutedConjunction) filteredTypedVarMap filteredTypedVarMap 0 depthCutoff relativeImprovementCutoff p)- 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 conjunctions typedVarMap bfsBoxesCutoff relativeImprovementCutoff p =- checkDisjunctionResults conjunctionResults Nothing- where- conjunctionResults =- parMap rseq- (\conjunction ->- let- substitutedConjunction = substituteConjunctionEqualities conjunction- substitutedConjunctionVars = nub $ concatMap (E.extractVariablesE . E.extractSafeE) substitutedConjunction- filteredTypedVarMap =- filter- (\(TypedVar (v, (_, _)) _) -> v `elem` substitutedConjunctionVars)- typedVarMap- filteredVarMap = typedVarMapToVarMap filteredTypedVarMap- in- setupBestFirstCheckDNF (map (\e -> (e, expressionToBoxFun (E.extractSafeE e) filteredVarMap p)) substitutedConjunction) filteredTypedVarMap bfsBoxesCutoff relativeImprovementCutoff p- )- 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 expressionsWithFunctions box- | null filterOutTrueTerms = Just True- | checkIfEsFalseUsingApply = Just False- | otherwise = Nothing- where- esWithRanges = parMap rseq (\ (e, f) -> ((e, f), apply f box)) expressionsWithFunctions- -- filterOutTrueTerms = esWithRanges- filterOutTrueTerms = filterOutTrueExpressions esWithRanges- checkIfEsFalseUsingApply = decideConjunctionRangesFalse 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 queue numberOfBoxesExamined numberOfBoxesCutoff relativeImprovementCutoff p =- case Q.maxView queue of- Just ((expressionsWithFunctions, typedVarMap, isLeftCorner), queueWithoutVarMap) ->- if numberOfBoxesExamined !<! numberOfBoxesCutoff then- trace (show numberOfBoxesExamined) $- case decideConjunctionWithSimplexCE expressionsWithFunctions typedVarMap typedVarMap relativeImprovementCutoff p isLeftCorner of- (Just False, _, _, _) -> decideConjunctionBestFirst queueWithoutVarMap (numberOfBoxesExamined + 1) numberOfBoxesCutoff relativeImprovementCutoff p- (Just True, Just satArea, _, _) -> (Just True, Just satArea)- (Nothing, Just indeterminateVarMap, filteredExpressionsWithFunctions, newIsLeftCorner) -> trace "h" $- let- functions = map snd filteredExpressionsWithFunctions-- (leftVarMap, rightVarMap) = trace "bisecting" bisectWidestTypedInterval indeterminateVarMap-- leftVarMapWithExpressionsAndCornerAndMinimum = trace (show (map fst filteredExpressionsWithFunctions)) $ trace "left"- (- fromMaybe (cn (mpBallP p 1000000000000)) (safeMaximumMinimum functions (typedVarMapToBox leftVarMap p) Nothing),- (filteredExpressionsWithFunctions, leftVarMap, not newIsLeftCorner)- )- rightVarMapWithExpressionsAndCornerAndMinimum = trace "right"- (- fromMaybe (cn (mpBallP p 1000000000000)) (safeMaximumMinimum functions (typedVarMapToBox rightVarMap p) Nothing),- -- fromMaybe (cn (mpBallP p 100000000000)) (safeMaximumMaximum functions (typedVarMapToBox rightVarMap p) Nothing),- -- fromMaybe (cn (dyadic 1048576)) (safeMaximumCentre functions (typedVarMapToBox rightVarMap p) Nothing),- (filteredExpressionsWithFunctions, rightVarMap, not newIsLeftCorner)- )- in- decideConjunctionBestFirst- (uncurry Q.insert rightVarMapWithExpressionsAndCornerAndMinimum (uncurry Q.insert leftVarMapWithExpressionsAndCornerAndMinimum queueWithoutVarMap))- (numberOfBoxesExamined + 1) numberOfBoxesCutoff relativeImprovementCutoff p- (_, _, _, _) -> error "Got unmatched case in decideConjunctionBestFirst"- else (Nothing, Just typedVarMap) -- Reached number of boxes cutoff- Nothing -> (Just False, 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 expressionsWithFunctions initialVarMap typedVarMap currentDepth depthCutoff relativeImprovementCutoff p- | null filterOutTrueTerms =- trace ("proved sat with apply " ++ show roundedVarMap)- (Just True, Just roundedVarMap)- | checkIfEsFalseUsingApply =- trace "proved false with apply"- (Just False, Nothing)- | otherwise = checkSimplex- where- box = typedVarMapToBox typedVarMap p- varNamesWithTypes = getVarNamesWithTypes typedVarMap- roundedVarMap =- case safeBoxToTypedVarMap box varNamesWithTypes of- Just rvm -> unsafeIntersectVarMap initialVarMap rvm- Nothing -> error $ "Rounded the following varMap makes it inverted: " ++ show typedVarMap- untypedRoundedVarMap = typedVarMapToVarMap roundedVarMap-- esWithRanges = parMap rseq (\ (e, f) -> ((e, f), apply f box)) expressionsWithFunctions- -- filterOutTrueTerms = esWithRanges- filterOutTrueTerms = filterOutTrueExpressions esWithRanges- checkIfEsFalseUsingApply = decideConjunctionRangesFalse filterOutTrueTerms-- filteredExpressionsWithFunctions = map fst filterOutTrueTerms-- -- Filter out ranges/derivatives with errors.- -- This is safe because we do not need every function to enclose the unsat area. - filteredCornerRangesWithDerivatives = computeCornerValuesAndDerivatives filterOutTrueTerms box-- bisectWidestDimensionAndRecurse varMapToBisect =- let- (leftVarMap, rightVarMap) = bisectWidestTypedInterval varMapToBisect- -- (leftVarMap, rightVarMap) = bimap (`unsafeIntersectVarMap` varMapToBisect) (`unsafeIntersectVarMap` varMapToBisect) $ bisectWidestTypedInterval varMapToBisect-- (leftR, rightR) =- withStrategy- (parTuple2 rseq rseq)- (- decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap leftVarMap (currentDepth + 1) depthCutoff relativeImprovementCutoff p,- decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap rightVarMap (currentDepth + 1) depthCutoff relativeImprovementCutoff p- )- in- case leftR of- (Just False, _)- -> case rightR of- (Just False, _) -> (Just False, Nothing)- r -> r- r -> r-- bisectUntilCutoff varMapToCheck =- if currentDepth !<! depthCutoff -- Best first- then- bisectWidestDimensionAndRecurse varMapToCheck- else- (Nothing, Just varMapToCheck)-- checkSimplex- -- If we can calculate any derivatives- | (not . null) filteredCornerRangesWithDerivatives = trace "decideWithSimplex start" $- case removeConjunctionUnsatAreaWithSimplex filteredCornerRangesWithDerivatives untypedRoundedVarMap of- (Just False, _) -> trace ("decideWithSimplex true: " ++ show roundedVarMap) (Just False, Nothing)- (Nothing, Just newVarMap) -> trace "decideWithSimplex indet" $- case safeVarMapToTypedVarMap newVarMap varNamesWithTypes of- Just nvm -> recurseOnVarMap $ unsafeIntersectVarMap nvm roundedVarMap- Nothing -> (Just False, Nothing) -- This will only happen when all integers in an integer-only varMap have been decided- _ -> undefined- | otherwise = bisectUntilCutoff roundedVarMap-- recurseOnVarMap recurseVarMap- | typedMaxWidth recurseVarMap == 0 =- case decideConjunctionWithApply filteredExpressionsWithFunctions (typedVarMapToBox recurseVarMap p) of- Just True -> (Just True, Just recurseVarMap)- Just False -> (Just False, Nothing)- Nothing -> (Nothing, Just recurseVarMap)- | typedMaxWidth roundedVarMap / typedMaxWidth recurseVarMap >= relativeImprovementCutoff =- trace ("recursing with simplex with roundedVarMap: " ++ show recurseVarMap) $- decideConjunctionDepthFirstWithSimplex filteredExpressionsWithFunctions initialVarMap recurseVarMap currentDepth depthCutoff relativeImprovementCutoff p- | otherwise = bisectUntilCutoff 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 expressionsWithFunctions initialVarMap typedVarMap relativeImprovementCutoff p isLeftCorner- | null filterOutTrueTerms =- trace ("proved sat with apply " ++ show roundedVarMap)- (Just True, Just roundedVarMap, filteredExpressionsWithFunctions, isLeftCorner)- | checkIfEsFalseUsingApply =- trace "proved unsat with apply"- (Just False, Nothing, filteredExpressionsWithFunctions, isLeftCorner)- | otherwise = checkSimplex- where- box = typedVarMapToBox typedVarMap p- varNamesWithTypes = getVarNamesWithTypes typedVarMap- roundedVarMap =- case safeBoxToTypedVarMap box varNamesWithTypes of- Just rvm -> unsafeIntersectVarMap initialVarMap rvm- Nothing -> error $ "Rounded the following varMap makes it inverted: " ++ show typedVarMap- untypedRoundedVarMap = typedVarMapToVarMap roundedVarMap-- esWithRanges = parMap rseq (\(e, f) -> ((e, f), apply f box)) expressionsWithFunctions- -- filterOutTrueTerms = esWithRanges- filterOutTrueTerms = filterOutTrueExpressions esWithRanges- checkIfEsFalseUsingApply = decideConjunctionRangesFalse filterOutTrueTerms-- filteredExpressionsWithFunctions = map fst filterOutTrueTerms-- -- Filter out ranges/derivatives with errors.- -- This is safe because we do not need every function to enclose the unsat area. - filteredCornerRangesWithDerivatives = computeCornerValuesAndDerivatives filterOutTrueTerms box-- checkSimplex- -- If we can calculate any derivatives- | (not . null) filteredCornerRangesWithDerivatives = trace "decideWithSimplex start" $- trace "decideWithSimplex start" $- case removeConjunctionUnsatAreaWithSimplex filteredCornerRangesWithDerivatives untypedRoundedVarMap of- (Just False, _) -> trace ("decideWithSimplex true: " ++ show roundedVarMap) (Just False, Nothing, filteredExpressionsWithFunctions, isLeftCorner)- (Nothing, Just newVarMap) -> trace "decideWithSimplex indet" $- case safeVarMapToTypedVarMap newVarMap varNamesWithTypes of- Nothing -> (Just False, Nothing, filteredExpressionsWithFunctions, isLeftCorner) -- This will only happen when all integers in an integer-only varMap have been decided- Just nvm ->- let- newTypedVarMap = unsafeIntersectVarMap nvm roundedVarMap- newBox = typedVarMapToBox newTypedVarMap 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 = safelyComputeCornerValuesAndDerivatives filterOutTrueTerms newBox- in- trace "findFalsePointWithSimplex start" $- case mNewCornerRangesWithDerivatives of- Just newCornerRangesWithDerivatives ->- case findConjunctionSatAreaWithSimplex newCornerRangesWithDerivatives (typedVarMapToVarMap newTypedVarMap) isLeftCorner of- Just satSolution ->- case safeVarMapToTypedVarMap satSolution varNamesWithTypes of- Just typedSatSolution ->- if decideConjunctionTrue (map fst filterOutTrueTerms) typedSatSolution p- then (Just True, Just typedSatSolution, filteredExpressionsWithFunctions, isLeftCorner)- else recurseOnVarMap newTypedVarMap- Nothing -> error $ "Found sat solution but encountered error when converting to typed sat solution" ++ show satSolution- Nothing -> recurseOnVarMap newTypedVarMap- Nothing -> recurseOnVarMap newTypedVarMap- _ -> undefined- | otherwise = recurseOnVarMap roundedVarMap-- recurseOnVarMap recurseVarMap- | typedMaxWidth recurseVarMap == 0 =- case decideConjunctionWithApply filteredExpressionsWithFunctions (typedVarMapToBox recurseVarMap p) of- Just True -> (Just True, Just recurseVarMap, filteredExpressionsWithFunctions, isLeftCorner)- Just False -> (Just False, Nothing, filteredExpressionsWithFunctions, isLeftCorner)- Nothing -> (Nothing, Just recurseVarMap, filteredExpressionsWithFunctions, isLeftCorner)- | typedMaxWidth roundedVarMap / typedMaxWidth recurseVarMap >= relativeImprovementCutoff =- trace ("recursing with simplex with roundedVarMap: " ++ show recurseVarMap) $- decideConjunctionWithSimplexCE filteredExpressionsWithFunctions initialVarMap recurseVarMap relativeImprovementCutoff p (not isLeftCorner)- | otherwise = (Nothing, Just recurseVarMap, filteredExpressionsWithFunctions, isLeftCorner)
− src/LPPaver/Decide/Linearisation.hs
@@ -1,258 +0,0 @@-{-|-Module : LPPaver.Decide.Linearisation-Description : Linearisations for conjunctions-Copyright : (c) Junaid Rasheed, 2021-2022-License : MPL-Maintainer : jrasheed178@gmail.com-Stability : experimental-Module defining linearisations for conjunctions of 'E.ESafe' terms.--}-module LPPaver.Decide.Linearisation where--import MixedTypesNumPrelude-import qualified PropaFP.Expression as E-import PropaFP.VarMap-import AERN2.MP-import AERN2.MP.Precision-import AERN2.BoxFun.Type-import AERN2.BoxFun.Box-import qualified Data.PQueue.Prio.Max as Q-import Data.Maybe-import PropaFP.Translators.BoxFun-import Control.Parallel.Strategies-import Data.List-import qualified Data.Map as M-import Linear.Simplex.Simplex-import Linear.Simplex.Util-import qualified Linear.Simplex.Types as LT--import LPPaver.Decide.Util-import LPPaver.Constraint.Type-import LPPaver.Constraint.Util-import qualified AERN2.Linear.Vector.Type as V-import Data.Bifunctor---- |Remove unsat areas from a conjunction arising from a DNF by weakening the conjunction using 'createConstraintsToRemoveConjunctionUnsatArea'.--- The resulting linear system is solved and optimised by the two-phase simplex method.--- If the linear system is infeasible, the entire conjunction was unsatisfiable.-removeConjunctionUnsatAreaWithSimplex - :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. - -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', - -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', - -- and the third item are partial derivatives of the term over a 'VarMap'.- -> VarMap -- ^ The VarMap over which we are examining the conjunction.- -> (Maybe Bool, Maybe VarMap) -- ^ The result of the simplex method on the resulting linear system.- -- (Just False, Nothing) is returned if the system is infeasible.- -- (Nothing, Just newArea) is returned if the system is feasible: newArea is an optimisation of the given 'VarMap'.-removeConjunctionUnsatAreaWithSimplex cornerValuesWithDerivatives varMap =- case mOptimizedVars of- Just optimizedVars -> (Nothing, Just optimizedVars)- Nothing -> (Just False, Nothing)- where- (simplexSystem, stringIntVarMap) = constraintsToSimplexConstraints $ createConstraintsToRemoveConjunctionUnsatArea cornerValuesWithDerivatives varMap-- vars = map fst varMap-- mFeasibleSolution = findFeasibleSolution simplexSystem--- -- Uses objective var to extract optimized values for each variable- extractSimplexResult :: Maybe (Integer, [(Integer, Rational)]) -> Rational- extractSimplexResult maybeResult =- case maybeResult of- Just (optimizedIntVar, result) -> -- optimizedIntVar refers to the objective variable. We extract the value of the objective- -- variable from the result- case lookup optimizedIntVar result of- Just optimizedVarResult -> optimizedVarResult- Nothing -> error "Extracting simplex result after finding feasible solution resulted in an infeasible result. This should not happen."- Nothing -> error "Could not optimize feasible system. This should not happen."-- mOptimizedVars =- case mFeasibleSolution of- Just (feasibleSystem, slackVars, artificialVars, objectiveVar) ->- Just $- map -- Optimize (minimize and maximize) all variables in the varMap- (\var ->- case M.lookup var stringIntVarMap of- Just intVar ->- case lookup var varMap of- Just (originalL, _) -> -- In the simplex system, the original lower bound of each var was shifted to 0. We undo this shift after optimization.- (- var,- (- originalL + extractSimplexResult (optimizeFeasibleSystem (LT.Min [(intVar, 1.0)]) feasibleSystem slackVars artificialVars objectiveVar),- originalL + extractSimplexResult (optimizeFeasibleSystem (LT.Max [(intVar, 1.0)]) feasibleSystem slackVars artificialVars objectiveVar)- )- )- Nothing -> error "Optimized var not found in original varMap. This should not happen."- Nothing -> error "Integer version of var not found. This should not happen."- )- vars- Nothing -> Nothing---- |Find a satisfiable point from a conjunction arising from a DNF by strengthening the conjunction using 'createConstraintsToFindSatSolution'.--- The resulting linear system is solved by the first phase of the two-phase simplex method.-findConjunctionSatAreaWithSimplex - :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. - -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', - -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', - -- and the third item are partial derivatives of the term over a 'VarMap'.- -> VarMap -- ^ The VarMap over which we are examining the conjunction.- -> Bool -- ^ A boolean used to determine which 'extreme' corner to strengthen the conjunction from.- -- If true, linearise from the 'extreme' left corner and vice versa.- -> Maybe VarMap -- ^ The result. If this is Nothing, no satisfiable point was found.-findConjunctionSatAreaWithSimplex cornerValuesWithDerivatives varMap isLeftCorner =- case mFeasibleVars of- Just newPoints ->- Just- $- map- (\var ->- case M.lookup var stringIntVarMap of- Just intVar ->- case lookup var varMap of- Just (originalL, _) -> -- In the simplex system, the original lower bound of each var was shifted to 0. We undo this shift after finding a feasible solution- (- var,- let feasiblePoint = originalL + fromMaybe 0.0 (lookup intVar newPoints)- in (feasiblePoint, feasiblePoint)- )- Nothing -> error "Optimized var not found in original varMap. This should not happen."- Nothing -> error "Integer version of var not found. This should not happen."- )- vars- Nothing -> trace "no sat solution" Nothing- where- (simplexSystem, stringIntVarMap) = constraintsToSimplexConstraints $ createConstraintsToFindSatSolution cornerValuesWithDerivatives varMap isLeftCorner-- vars = map fst varMap-- mFeasibleSolution = findFeasibleSolution simplexSystem-- mFeasibleVars =- case mFeasibleSolution of- Just (feasibleSystem, _slackVars, _artificialVars, _objectiveVar) -> Just $ displayDictionaryResults feasibleSystem- Nothing -> Nothing---- |Linearisations that weaken a conjunction of terms over some box.-createConstraintsToRemoveConjunctionUnsatArea - :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. - -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', - -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', - -- and the third item are partial derivatives of the term over a 'VarMap'.- -> VarMap -- ^ The VarMap over which we are examining the conjunction.- -> [Constraint] -- ^ An implicit linear system that is a weakening of the conjunction.-createConstraintsToRemoveConjunctionUnsatArea cornerValuesWithDerivatives varMap =- domainConstraints ++ functionConstraints- where- vars = map fst varMap- varsNewUpperBounds = map (\(_, (l, r)) -> r - l) varMap-- -- var >= varLower - varLower && var <= varUpper - varLower- -- Since var >= 0 is assumed by the simplex method, var >= varLower - varLower is not needed- domainConstraints =- map- (\(var, (varLower, varUpper)) ->- LEQ [(var, 1.0)] $ varUpper - varLower- )- varMap-- -- The following constraints in this variable are...- -- fn - (fnx1GradientR * x1) - .. - (fnxnGradientR * xn) <= fnLeftCorner + (fnx1GradientR * -x1L) + .. + (fnxnGradientR * -xnL)- -- fn - (fnx1GradientL * x1) - .. - (fnxnGradientL * xn) <= fnRightCorner + (-fnx1GradientL * x1R) + .. + (-fnxnGradientL * xnR)- -- and these are equivalent to...- -- fn <= fnLeftCorner + (fnx1GradientR * (x1 - x1L)) + .. + (fnxnGradientR * (xn - xnL))- -- fn <= fnRightCorner + (-fnx1GradientL * (x1R - x1)) + .. + (-fnxnGradientL * (xnR - xn))- -- - functionConstraints =- concatMap- (\(fnInt, (fLeftRange, fRightRange, fPartialDerivatives)) ->- let- fNegatedPartialDerivativesLowerBounds = map (negate . fst . mpBallToRational) $ V.toList fPartialDerivatives- fNegatedPartialDerivativesUpperBounds = map (negate . snd . mpBallToRational) $ V.toList fPartialDerivatives- fLeftUpperBound = snd $ mpBallToRational fLeftRange- fRightUpperBound = snd $ mpBallToRational fRightRange-- --FIXME: make this safe. Check if vars contain ^fSimplex[0-9]+$. If so, try ^fSimplex1[0-9]+$ or something- fSimplexN = "fSimplex" ++ show fnInt- in- [- -- f is definitely below this line from the left corner- -- Multiplication with left corner and partial derivatives omitted, since left corner is zero- LEQ ((fSimplexN, 1.0) : zip vars fNegatedPartialDerivativesUpperBounds)- fLeftUpperBound,- -- f is definitely below this line from the right corner- LEQ ((fSimplexN, 1.0) : zip vars fNegatedPartialDerivativesLowerBounds)- $ foldl add fRightUpperBound $ zipWith mul varsNewUpperBounds fNegatedPartialDerivativesLowerBounds- ]- )- $- zip- [1..]- cornerValuesWithDerivatives-- mpBallToRational :: CN MPBall -> (Rational, Rational)- mpBallToRational = bimap rational rational . endpoints . reducePrecionIfInaccurate . unCN---- |Linearisations that strengthen a conjunction of terms over some box.-createConstraintsToFindSatSolution- :: [(CN MPBall, CN MPBall, Box)] -- ^ A list of values needed to linearise each term in the conjunction. - -- In each triple, the first item is the value of the term from the 'extreme' left corner of a 'VarMap', - -- the second item is the value of the term from the 'extreme' right corner of a 'VarMap', - -- and the third item are partial derivatives of the term over a 'VarMap'.- -> VarMap -- ^ The VarMap over which we are examining the conjunction.- -> Bool -- ^ A boolean used to determine which 'extreme' corner to strengthen the conjunction from.- -- If true, linearise from the 'extreme' left corner and vice versa.- -> [Constraint] -- ^ An implicit linear system that is a weakening of the conjunction.-createConstraintsToFindSatSolution cornerValuesWithDerivatives varMap isLeftCorner =- domainConstraints ++ functionConstraints- where- vars = map fst varMap- varsNewUpperBounds = map (\(_, (l, r)) -> r - l) varMap-- -- var >= varLower - varLower && var <= varUpper - varLower- -- Since var >= 0 is assumed by the simplex method, var >= varLower - varLower is not needed- domainConstraints =- map- (\(var, (varLower, varUpper)) ->- LEQ [(var, 1.0)] $ varUpper - varLower- )- varMap-- -- The following constraints in this variable are...- -- Left corner: fn - (fnx1GradientL * x1) - .. - (fnxnGradientL * xn) <= fnLeftCorner - (fnx1GradientL * x1L) - .. - (fnx1GradientL * x1L)- -- Right corner: fn - (fnx1GradientR * x1) - .. - (fnxnGradientR * xn) <= fnRightCorner - (fnx1GradientR * x1R) - .. - (fnx1GradientR * x1R)- -- and these are equivalent to...- -- Left corner: fn <= fnLeftCorner + (fnx1GradientL * (x1 - x1L)) + .. + (fnxnGradientL * (xn - xnL))- -- Right corner: fn <= ynRightCorner + (-fnx1GradientR * (xR - x)) + .. + (-fnxnGradientR * (xnR - xn))- functionConstraints =- zipWith- (curry- (\(fnInt, (fLeftRange, fRightRange, fPartialDerivatives)) ->- let- fNegatedPartialDerivativesLowerBounds = map (negate . fst . mpBallToRational) $ V.toList fPartialDerivatives- fNegatedPartialDerivativesUpperBounds = map (negate . snd . mpBallToRational) $ V.toList fPartialDerivatives- fLeftLowerBound = fst $ mpBallToRational fLeftRange- fRightLowerBound = fst $ mpBallToRational fRightRange-- --FIXME: make this safe. Check if vars contain ^fSimplex[0-9]+$. If so, try ^fSimplex1[0-9]+$ or something- fSimplexN = "fSimplex" ++ show fnInt- in- if isLeftCorner- then- -- f is definitely above this line from the left corner- -- Multiplication with left corner and partial derivatives omitted, since left corner is zero- LEQ ((fSimplexN, 1.0) : zip vars fNegatedPartialDerivativesLowerBounds)- fLeftLowerBound- else- -- f is definitely above this line from the right corner- LEQ ((fSimplexN, 1.0) : zip vars fNegatedPartialDerivativesUpperBounds)- $ foldl add fRightLowerBound $ zipWith mul varsNewUpperBounds fNegatedPartialDerivativesUpperBounds-- )- )- [1..]- cornerValuesWithDerivatives-- mpBallToRational :: CN MPBall -> (Rational, Rational)- mpBallToRational = bimap rational rational . endpoints . reducePrecionIfInaccurate . unCN
− src/LPPaver/Decide/Util.hs
@@ -1,476 +0,0 @@-{-|-Module : LPPaver.Decide.Util-Description : Utility functions for LPPaver.Decide modules-Copyright : (c) Junaid Rasheed, 2021-2022-License : MPL-Maintainer : jrasheed178@gmail.com-Stability : experimental-Module defining useful utility functions for the LPPaver.Decide modules--}-module LPPaver.Decide.Util where--import MixedTypesNumPrelude-import qualified Prelude as P-import Data.List (nub, sortBy, partition)-import Data.Bifunctor-import PropaFP.Parsers.Smt (findVariablesInExpressions)-import AERN2.MP.Dyadic-import Control.CollectErrors-import AERN2.MP.Ball-import qualified Numeric.CollectErrors as CN-import AERN2.BoxFun.Type-import AERN2.BoxFun.Box-import qualified PropaFP.Expression as E-import PropaFP.VarMap-import qualified AERN2.Linear.Vector.Type as V-import AERN2.Kleenean-import PropaFP.Translators.BoxFun-import AERN2.BoxFun.Optimisation-import Control.Parallel.Strategies---- TODO: Remove traces--- |Dummy trace function-trace a x = x---- |Calculate the range of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'apply'.-applyExpression :: E.E -> VarMap -> Precision -> CN MPBall-applyExpression expression varMap p =- apply f (varMapToBox varMap p)- where- f = expressionToBoxFun expression varMap p---- |Calculate the gradient of some 'E.E' expression over the given 'VarMap' with the given 'Precision' using 'gradient'.-gradientExpression :: E.E -> VarMap -> Precision -> V.Vector (CN MPBall)-gradientExpression expression varMap p =- gradient f (varMapToBox varMap p)- where- f = expressionToBoxFun expression varMap p---- |Run 'applyExpression' on each 'E.E' in a given list-applyExpressionList :: [E.E] -> VarMap -> Precision -> [CN MPBall]-applyExpressionList expressions varMap p =- map- (\e -> apply (expressionToBoxFun e varMap p) box)- expressions- where- box = varMapToBox varMap p---- |Run 'gradientExpression' on each 'E.E' in a given list-gradientExpressionList :: [E.E] -> VarMap -> Precision -> [V.Vector (CN MPBall)]-gradientExpressionList expressions varMap p =- map- (\e -> gradientExpression e varMap p)- expressions---- |Run 'applyExpressionList' on each '[E.E]' in a given list-applyExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[CN MPBall]]-applyExpressionDoubleList cnf varMap p = map (\d -> applyExpressionList d varMap p) cnf---- |Run 'gradientExpressionList' on each '[E.E]' in a given list-gradientExpressionDoubleList :: [[E.E]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]-gradientExpressionDoubleList cnf varMap p = map (\d -> gradientExpressionList d varMap p) cnf---- |Run 'applyExpressionDoubleList' on an [['E.ESafe']]-applyESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[CN MPBall]]-applyESafeDoubleList cnf = applyExpressionDoubleList (map (map E.extractSafeE) cnf)---- |Run 'gradientExpressionDoubleList' on an [['E.ESafe']]-gradientESafeDoubleList :: [[E.ESafe]] -> VarMap -> Precision -> [[V.Vector (CN MPBall)]]-gradientESafeDoubleList cnf = gradientExpressionDoubleList (map (map E.extractSafeE) cnf)---- |Evaluate an 'E.F' over some 'VarMap' with a given 'Precision' using 'applyExpression'-checkFWithApply :: E.F -> VarMap -> Precision -> CN Kleenean-checkFWithApply (E.FComp op e1 e2) varMap p =- case op of- E.Ge -> e1Val >= e2Val- E.Gt -> e1Val > e2Val- E.Le -> e1Val <= e2Val- E.Lt -> e1Val < e2Val- E.Eq -> e1Val == e2Val- where- e1Val = applyExpression e1 varMap p- e2Val = applyExpression e2 varMap p-checkFWithApply (E.FConn op f1 f2) varMap p =- case op of- E.And -> f1Val && f2Val- E.Or -> f1Val || f2Val- E.Impl -> not f1Val || f2Val- where- f1Val = checkFWithApply f1 varMap p- f2Val = checkFWithApply f2 varMap p-checkFWithApply (E.FNot f) varMap p = not $ checkFWithApply f varMap p-checkFWithApply E.FTrue _ _ = cn CertainTrue-checkFWithApply E.FFalse _ _ = cn CertainFalse---- |Filter out expressions in a list which are certainly false.--- If an expression cannot be evaluated, do not filter it out.-filterOutFalseExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]-filterOutFalseExpressions =- filter- (\((safeE, _), range) ->- case safeE of- E.EStrict _ -> hasError range || not (range !<=! 0) -- We cannot decide on ranges with errors, so do not filter them out- E.ENonStrict _ -> hasError range || not (range !<! 0)- )---- |Filter out expressions in a list which are certainly true.--- If an expression cannot be evaluated, do not filter it out.-filterOutTrueExpressions :: [((E.ESafe, BoxFun), CN MPBall)] -> [((E.ESafe, BoxFun), CN MPBall)]-filterOutTrueExpressions =- filter- (\((safeE, _), range) ->- hasError range || -- Do not filter if there is an error- (- case safeE of- E.EStrict _ ->- case unCN range > 0 of- CertainTrue -> False- _ -> True- -- We cannot decide on ranges with errors, so do not filter them out- E.ENonStrict _ ->- case unCN range >= 0 of- CertainTrue -> False- _ -> True- )- )---- |Returns true if any of the ranges of the given Expression have been evaluated to be greater than or equal to zero.-decideRangesGEZero :: [((E.E, BoxFun), CN MPBall)] -> Bool-decideRangesGEZero = any (\(_, range) -> not (hasError range) && range !>=! 0)---- |The mean of a list of 'CN Dyadic' numbers.-mean :: [CN Dyadic] -> CN Rational-mean xs = sum xs / length xs---- |Safely find the maximum of a list of ordered elements, avoiding exceptions by ignoring anything with errors-safeMaximum :: (HasOrderAsymmetric a a, CanTestCertainly (OrderCompareType a a), CanTestErrorsPresent a) =>- a -> [a] -> a-safeMaximum currentMax [] = currentMax-safeMaximum currentMax (x : xs) =- if hasError x- then safeMaximum currentMax xs- else safeMaximum (if x !>! currentMax then x else currentMax) xs---- |Safely find the maximum centre of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors-safeMaximumCentre :: [BoxFun] -> Box -> Maybe (CN Dyadic) -> Maybe (CN Dyadic)-safeMaximumCentre [] _ mCurrentCentre = mCurrentCentre-safeMaximumCentre (f : fs) box mCurrentCentre =- if hasError range- then safeMaximumCentre fs box mCurrentCentre- else- case mCurrentCentre of- Just currentMax ->- if currentMax !>=! rangeCentre- then safeMaximumCentre fs box mCurrentCentre- else safeMaximumCentre fs box (Just rangeCentre)- Nothing -> safeMaximumCentre fs box (Just rangeCentre)- where- range = apply f box- rangeCentre = AERN2.MP.Ball.centre range---- |Safely find the maximum minimum of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors-safeMaximumMinimum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)-safeMaximumMinimum [] _ mCurrentMin = mCurrentMin-safeMaximumMinimum (f : fs) box mCurrentMin =- if hasError range- then safeMaximumMinimum fs box mCurrentMin- else- case mCurrentMin of- Just currentMin ->- if currentMin !>=! rangeMin- then safeMaximumMinimum fs box mCurrentMin- else safeMaximumMinimum fs box (Just rangeMin)- Nothing -> safeMaximumMinimum fs box (Just rangeMin)- where- range = apply f box- rangeMin = fst $ endpointsAsIntervals range---- |Safely find the maximum maximum of a list of 'BoxFun's over a given 'Box', avoiding exceptions by ignoring anything with errors-safeMaximumMaximum :: [BoxFun] -> Box -> Maybe (CN MPBall) -> Maybe (CN MPBall)-safeMaximumMaximum [] _ mCurrentMax = mCurrentMax-safeMaximumMaximum (f : fs) box mCurrentMax =- if hasError range- then safeMaximumMaximum fs box mCurrentMax- else- case mCurrentMax of- Just currentMax ->- if currentMax !>=! rangeMax- then safeMaximumMinimum fs box mCurrentMax- else safeMaximumMinimum fs box (Just rangeMax)- Nothing -> safeMaximumMinimum fs box (Just rangeMax)- where- range = apply f box- rangeMax = snd $ endpointsAsIntervals range---- TODO: Move to PropaFP--- |Bisect the widest interval in a 'VarMap'-bisectWidestInterval :: VarMap -> (VarMap, VarMap)-bisectWidestInterval [] = error "Given empty box to bisect"-bisectWidestInterval vm = bisectVar vm widestVar- where- (widestVar, _) = widestInterval (tail vm) (head vm)---- TODO: Move to PropaFP--- |Bisect the widest interval in a 'TypedVarMap'-bisectWidestTypedInterval :: TypedVarMap -> (TypedVarMap, TypedVarMap)-bisectWidestTypedInterval [] = error "Given empty box to bisect"-bisectWidestTypedInterval vm = bisectTypedVar vm widestVar- where- (widestVar, _) = widestTypedInterval (tail vm) $ typedVarIntervalToVarInterval (head vm)---- TODO: Move to PropaFP--- |Ensures that the first varMap is within the second varMap--- If it is, returns the first varMap.--- If it isn't modifies the varMap so that the returned varMap is within the second varMap--- Both varmaps must have the same number of vars in the same order (order of vars not checked)-ensureVarMapWithinVarMap :: VarMap -> VarMap -> VarMap-ensureVarMapWithinVarMap [] [] = []-ensureVarMapWithinVarMap ((v, (roundedL, roundedR)) : rvm) ((_, (originalL, originalR)) : ovm) =- (v, (if roundedL < originalL then originalL else roundedL, if roundedR > originalR then originalR else roundedR))- : ensureVarMapWithinVarMap rvm ovm-ensureVarMapWithinVarMap _ _ = error "Different sized varMaps"---- |Version of 'computeCornerValuesAndDerivatives' that returns Nothing if a calculation contains an error-safelyComputeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> Maybe [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]-safelyComputeCornerValuesAndDerivatives esWithRanges box =- if cornerRangesWithDerivativesHasError- then Nothing- else Just cornerRangesWithDerivatives- where- boxL = lowerBounds box- boxU = upperBounds box-- -- filteredCornerRangesWithDerivatives = - -- [- -- value |- -- value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,- -- not (hasError value)- -- ]-- cornerRangesWithDerivatives =- parMap rseq- (\ ((_, f), _) -> (apply f boxL, apply f boxU, gradient f box))- esWithRanges-- -- Check if any function contains errors- cornerRangesWithDerivativesHasError =- any- (\(l, r, c) -> hasError l || hasError r || V.any hasError c)- cornerRangesWithDerivatives---- |Return the value of the given 'E.ESafe' expression/'BoxFun' at the extreme left corner and the extreme right corner as well as partial derivatives over the given 'Box'.--- Extreme corners are defined as the minimum/maximum of every interval in a 'Box' for the left/right extreme corners respectively.-computeCornerValuesAndDerivatives :: [((E.ESafe, BoxFun), CN MPBall)] -> Box -> [(CN MPBall, CN MPBall, V.Vector (CN MPBall))]-computeCornerValuesAndDerivatives esWithRanges box = filteredCornerRangesWithDerivatives- where- boxL = lowerBounds box- boxU = upperBounds box-- -- filteredCornerRangesWithDerivatives = - -- [- -- value |- -- value <- parMap rseq (\((_, f), _) -> (apply f boxL, apply f boxU, gradient f box)) esWithRanges,- -- not (hasError value)- -- ]-- cornerRangesWithDerivatives =- parMap rseq- (\ ((_, f), _) -> (apply f boxL, apply f boxU, gradient f box))- esWithRanges-- -- Keep the functions where we can calculate all derivatives- filteredCornerRangesWithDerivatives =- filter- (\(l, r, c) -> not (hasError l || hasError r || V.any hasError c)) -- Filter out functions where any partial derivative or corners contain an error- cornerRangesWithDerivatives---- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is false in a standard manner--- A range with an error is treated as false.-decideConjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool-decideConjunctionRangesFalse =- any- (\((safeE, _), range) ->- case safeE of- E.EStrict _ -> not (hasError range) && range !<=! 0- E.ENonStrict _ -> not (hasError range) && range !<! 0- )---- |Decide if the ranges of a conjunction of 'E.ESafe' expressions is true in a standard manner--- A range with an error is treated as false.-decideConjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool-decideConjunctionRangesTrue =- all- (\((safeE, _), range) ->- case safeE of- E.EStrict _ -> not (hasError range) && range !>! 0- E.ENonStrict _ -> not (hasError range) && range !>=! 0- )----- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is true in a standard manner--- A range with an error is treated as false.-decideDisjunctionRangesTrue :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool-decideDisjunctionRangesTrue =- any- (\((safeE, _), range) ->- case safeE of- E.EStrict _ -> not (hasError range) && range !>! 0- E.ENonStrict _ -> not (hasError range) && range !>=! 0- )---- |Decide if the ranges of a disjunction of 'E.ESafe' expressions is false in a standard manner--- A range with an error is treated as false.-decideDisjunctionRangesFalse :: [((E.ESafe, BoxFun), CN MPBall)] -> Bool-decideDisjunctionRangesFalse =- all- (\((safeE, _), range) ->- case safeE of- E.EStrict _ -> not (hasError range) && not (hasError range) && range !<=! 0- E.ENonStrict _ -> not (hasError range) && range !<! 0- )---- |Evaluate the range of each 'E.ESafe' expression in a disjunction and check if the disjunction is false in a standard manner. -decideDisjunctionFalse :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool-decideDisjunctionFalse expressionsWithFunctions varMap p =- all- (\(safeE, f) ->- let- range = apply f (typedVarMapToBox varMap p)- in- case safeE of- E.EStrict _ -> not (hasError range) && range !<=! 0- E.ENonStrict _ -> not (hasError range) && range !<! 0- )- expressionsWithFunctions---- |Evaluate the range of each 'E.ESafe' expression in a CNF and check if the CNF is false in a standard manner. -decideCNFFalse :: [[(E.ESafe, BoxFun)]] -> TypedVarMap -> Precision -> Bool-decideCNFFalse c v p = any (\d -> decideDisjunctionFalse d v p) c---- |Evaluate the range of each 'E.ESafe' expression in a conjunction and check if the conjunction is true in a standard manner. -decideConjunctionTrue :: [(E.ESafe, BoxFun)] -> TypedVarMap -> Precision -> Bool-decideConjunctionTrue c v p =- all (\(safeE, f) ->- let- range = apply f (typedVarMapToBox v p)- in- case safeE of- E.EStrict _ -> not (hasError range) && range !>! 0- E.ENonStrict _ -> not (hasError range) && range !>=! 0- )- c---- |Check the results of a disjunction in a standard manner-checkDisjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)-checkDisjunctionResults [] Nothing = (Just False, Nothing)-checkDisjunctionResults [] indeterminateArea@(Just _) = (Nothing, indeterminateArea)-checkDisjunctionResults (result : results) mIndeterminateArea =- case result of- r@(Just True, _) -> r- (Just False, _) ->- checkDisjunctionResults results mIndeterminateArea- (Nothing, indeterminateArea@(Just _)) -> checkDisjunctionResults results indeterminateArea- (Nothing, Nothing) -> undefined---- |Check the results of a conjunction in a standard manner-checkConjunctionResults :: [(Maybe Bool, Maybe potentialModel)] -> Maybe potentialModel -> (Maybe Bool, Maybe potentialModel)-checkConjunctionResults [] Nothing = (Just True, Nothing)-checkConjunctionResults [] indeterminateArea@(Just _) = (Nothing, indeterminateArea)-checkConjunctionResults (result : results) mIndeterminateArea =- case result of- (Just True, _) -> checkConjunctionResults results mIndeterminateArea- r@(Just False, _) -> r- (Nothing, indeterminateArea@(Just _)) -> checkConjunctionResults results indeterminateArea- (Nothing, Nothing) -> undefined---- |Substitute all variable-defining equalities in a given conjunction.--- Simplify the conjunction after substituting all variable-defining equalities.-substituteConjunctionEqualities :: [E.ESafe] -> [E.ESafe]-substituteConjunctionEqualities [] = []-substituteConjunctionEqualities conjunction@(conjunctionHead : conjunctionTail) =- case equations of- [] -> nub $ conjunction- _ -> substituteConjunctionEqualities substConj- where- -- these equalities will not have any contradictions, they should already have been dealt with by deriveBounds and simplifyFDNF.- equations = findVarDefiningEquations conjunctionHead conjunctionTail conjunctionTail- (eq : eqs) = equations-- substConj = substituteAndSimplifyChosenEquation selectedDupe conjunction- -- simplifiedSubstitutedConjunction = map (E.fmapESafe E.simplifyE) conjunction-- -- find duplicates for the first equation- (dupes, nonDupes) = findDuplicateEquations eq eqs-- -- sort duplicates based on length- sortedDupes = sortBy (\(_, y1) (_, y2) -> P.compare y1 y2) (eq : dupes)-- -- partition duplicates based on whether or not they contain variables- (varFreeDupes, varContainingDupes) = partition (\(_, e) -> E.hasVarsE e) sortedDupes-- -- Select an equality to substitute- -- Selects the shortest var-free equality or, if a var-free equality does not exist, the shortest equality- selectedDupe = head $ varFreeDupes ++ varContainingDupes-- -- Find other var-defining equations for the var in the given equation- findDuplicateEquations :: (String, E.E) -> [(String, E.E)] -> ([(String, E.E)], [(String, E.E)])- findDuplicateEquations _ [] = ([],[])- findDuplicateEquations (x1, y1) ((x2, y2) : es)- | x1 P.== x2 =- first ((x2, y2) :) $ findDuplicateEquations (x1, y1) es- | otherwise =- second ((x2, y2) :) $ findDuplicateEquations (x1, y1) es-- -- substitute the given equation in the given conjunction- substituteAndSimplifyChosenEquation :: (String, E.E) -> [E.ESafe] -> [E.ESafe]- substituteAndSimplifyChosenEquation _ [] = []- substituteAndSimplifyChosenEquation (x, y) (e : c) = E.fmapESafe (\nonSafeE -> E.simplifyE (E.replaceEInE nonSafeE (E.Var x) y)) e : substituteAndSimplifyChosenEquation (x, y) c-- -- Find var equations- -- Essentially, find Es in the conjunction of the form Var v >= e, Var v <= e- -- The e is ignored if it contains Var v- -- Else, store this equality as v, e in the resulting list - findVarDefiningEquations :: E.ESafe -> [E.ESafe] -> [E.ESafe] -> [(String, E.E)]- findVarDefiningEquations _ [] [] = []- findVarDefiningEquations _ [] (e : conj) = findVarDefiningEquations e conj conj- findVarDefiningEquations e1 (e2 : es) conj =- case e1 of- -- x1 - y1 >= 0- E.ENonStrict (E.EBinOp E.Sub v@(E.Var x1) y1) ->- -- ignore circular equalities- if x1 `elem` findVariablesInExpressions y1 then findVarDefiningEquations e1 es conj else- case e2 of- -- x2 - y2 >= 0- E.ENonStrict (E.EBinOp E.Sub x2 (E.Var y2)) ->- -- if we have x - y >= 0 && y - x >= 0, then y - x = 0, so y = x- if x1 P.== y2 && y1 P.== x2- then- (x1, y1) : findVarDefiningEquations e1 es conj- else findVarDefiningEquations e1 es conj- _ -> findVarDefiningEquations e1 es conj- -- y1 - x1 >= 0- E.ENonStrict (E.EBinOp E.Sub y1 v@(E.Var x1)) ->- -- ignore circular equalities- if x1 `elem` findVariablesInExpressions y1 then findVarDefiningEquations e1 es conj else- case e2 of- -- y2 - x2 >= 0- E.ENonStrict (E.EBinOp E.Sub (E.Var y2) x2) ->- -- if we have y - x >= 0 && x - y >= 0, then y - x = 0, so y = x- if x1 P.== y2 && y1 P.== x2- then- (x1, y1) : findVarDefiningEquations e1 es conj- else findVarDefiningEquations e1 es conj- _ -> findVarDefiningEquations e1 es conj- -- x >= 0- E.ENonStrict v1@(E.Var x1) ->- case e2 of- -- -x >= 0- E.ENonStrict (E.EUnOp E.Negate (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj- -- 0 - x- E.ENonStrict (E.EBinOp E.Sub (E.Lit 0.0) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj- -- -1 * x- E.ENonStrict (E.EBinOp E.Mul (E.Lit (-1.0)) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj- -- (-(1)) * x- E.ENonStrict (E.EBinOp E.Mul (E.EUnOp E.Negate (E.Lit (1.0))) (E.Var x2)) -> if x1 P.== x2 then (x1, E.Lit 0.0) : findVarDefiningEquations e1 es conj else findVarDefiningEquations e1 es conj- _ -> findVarDefiningEquations e1 es conj- _ -> findVarDefiningEquations e1 es conj
test/Spec.hs view
@@ -10,7 +10,9 @@ import PropaFP.Translators.MetiTarski import System.Exit import MixedTypesNumPrelude (ifThenElse)-import LPPaver.Decide.Algorithm+import LPPaver.Algorithm.DNF+import LPPaver.Algorithm.Util+import LPPaver.Algorithm.Type import PropaFP.Eliminator (minMaxAbsEliminatorF) import PropaFP.Parsers.DRealSmt import AERN2.MP@@ -62,14 +64,14 @@ let ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc in do- case checkEDNFBestFirstWithSimplexCE ednf typedVarMap 1000 1.2 (prec 100) of- (Just True, _) -> do+ case checkEDNFBestFirstWithSimplexCE ednf typedVarMap 1000000 1.2 (prec 100) of+ SatDNF _ _ -> do putStrLn $ "Proved sat: " ++ file checkVCsSat files fileParent- (Just False, _) -> do+ UnsatDNF _ -> do putStrLn $ "Satisfiable VC found to be unsatisfiable: " ++ file exitFailure- (Nothing, _) -> do+ IndeterminateDNF _ _ -> do putStrLn $ "Satisfiable VC could not be decided: " ++ file exitFailure Nothing -> do@@ -89,14 +91,14 @@ let ednf = fDNFToEDNF . simplifyFDNF . fToFDNF . simplifyF . minMaxAbsEliminatorF . simplifyF . removeVariableFreeComparisons $ vc in do- case checkEDNFDepthFirstWithSimplex ednf typedVarMap 100 1.2 (prec 100) of- (Just False, _) -> do+ case checkEDNFDepthFirstWithSimplex ednf typedVarMap 1000 1.2 (prec 100) of+ UnsatDNF _ -> do putStrLn $ "Proved unsat: " ++ file checkVCsUnsat files fileParent- (Just True, _) -> do+ SatDNF _ _ -> do putStrLn $ "Unsatisfiable VC found to be satisfiable: " ++ file exitFailure- (Nothing, _) -> do+ IndeterminateDNF _ _ -> do putStrLn $ "Unsatisfiable VC could not be decided: " ++ file exitFailure Nothing -> do