LPPaver (empty) → 0.0.3.1
raw patch · 12 files changed
+2062/−0 lines, 12 filesdep +LPPaverdep +PropaFPdep +aern2-mfunsetup-changed
Dependencies added: LPPaver, PropaFP, aern2-mfun, aern2-mp, base, collect-errors, containers, directory, mixed-types-num, optparse-applicative, parallel, pqueue, simplex-method
Files
- ChangeLog.md +27/−0
- LICENSE +373/−0
- LPPaver.cabal +130/−0
- README.md +45/−0
- Setup.hs +2/−0
- app/LPPaver.hs +173/−0
- src/LPPaver/Constraint/Type.hs +17/−0
- src/LPPaver/Constraint/Util.hs +55/−0
- src/LPPaver/Decide/Algorithm.hs +363/−0
- src/LPPaver/Decide/Linearisation.hs +258/−0
- src/LPPaver/Decide/Util.hs +476/−0
- test/Spec.hs +143/−0
+ ChangeLog.md view
@@ -0,0 +1,27 @@+# Changelog for LPPaver++## [v0.0.3.1](https://github.com/rasheedja/PropaFP/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)++- Deploy haddock documentation using GitHub pages+- Clean up and document new modules+- Split up single Type.hs module into smaller and better encapsulated modules+- 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)++- Replace minView with maxView in 'model search' mode+ - Higher ranges are more likely to produce models+- Add test suite+ - Uses PropaFP and 'Place' examples+- Update package dependencies++## [v0.0.1](https://github.com/rasheedja/LPPaver/tree/v0.0.1)++- Initial release
+ LICENSE view
@@ -0,0 +1,373 @@+Mozilla Public License Version 2.0+==================================++1. Definitions+--------------++1.1. "Contributor"+ means each individual or legal entity that creates, contributes to+ the creation of, or owns Covered Software.++1.2. "Contributor Version"+ means the combination of the Contributions of others (if any) used+ by a Contributor and that particular Contributor's Contribution.++1.3. "Contribution"+ means Covered Software of a particular Contributor.++1.4. "Covered Software"+ means Source Code Form to which the initial Contributor has attached+ the notice in Exhibit A, the Executable Form of such Source Code+ Form, and Modifications of such Source Code Form, in each case+ including portions thereof.++1.5. "Incompatible With Secondary Licenses"+ means++ (a) that the initial Contributor has attached the notice described+ in Exhibit B to the Covered Software; or++ (b) that the Covered Software was made available under the terms of+ version 1.1 or earlier of the License, but not also under the+ terms of a Secondary License.++1.6. "Executable Form"+ means any form of the work other than Source Code Form.++1.7. "Larger Work"+ means a work that combines Covered Software with other material, in+ a separate file or files, that is not Covered Software.++1.8. "License"+ means this document.++1.9. "Licensable"+ means having the right to grant, to the maximum extent possible,+ whether at the time of the initial grant or subsequently, any and+ all of the rights conveyed by this License.++1.10. "Modifications"+ means any of the following:++ (a) any file in Source Code Form that results from an addition to,+ deletion from, or modification of the contents of Covered+ Software; or++ (b) any new file in Source Code Form that contains any Covered+ Software.++1.11. "Patent Claims" of a Contributor+ means any patent claim(s), including without limitation, method,+ process, and apparatus claims, in any patent Licensable by such+ Contributor that would be infringed, but for the grant of the+ License, by the making, using, selling, offering for sale, having+ made, import, or transfer of either its Contributions or its+ Contributor Version.++1.12. "Secondary License"+ means either the GNU General Public License, Version 2.0, the GNU+ Lesser General Public License, Version 2.1, the GNU Affero General+ Public License, Version 3.0, or any later versions of those+ licenses.++1.13. "Source Code Form"+ means the form of the work preferred for making modifications.++1.14. "You" (or "Your")+ means an individual or a legal entity exercising rights under this+ License. For legal entities, "You" includes any entity that+ controls, is controlled by, or is under common control with You. For+ purposes of this definition, "control" means (a) the power, direct+ or indirect, to cause the direction or management of such entity,+ whether by contract or otherwise, or (b) ownership of more than+ fifty percent (50%) of the outstanding shares or beneficial+ ownership of such entity.++2. License Grants and Conditions+--------------------------------++2.1. Grants++Each Contributor hereby grants You a world-wide, royalty-free,+non-exclusive license:++(a) under intellectual property rights (other than patent or trademark)+ Licensable by such Contributor to use, reproduce, make available,+ modify, display, perform, distribute, and otherwise exploit its+ Contributions, either on an unmodified basis, with Modifications, or+ as part of a Larger Work; and++(b) under Patent Claims of such Contributor to make, use, sell, offer+ for sale, have made, import, and otherwise transfer either its+ Contributions or its Contributor Version.++2.2. Effective Date++The licenses granted in Section 2.1 with respect to any Contribution+become effective for each Contribution on the date the Contributor first+distributes such Contribution.++2.3. Limitations on Grant Scope++The licenses granted in this Section 2 are the only rights granted under+this License. No additional rights or licenses will be implied from the+distribution or licensing of Covered Software under this License.+Notwithstanding Section 2.1(b) above, no patent license is granted by a+Contributor:++(a) for any code that a Contributor has removed from Covered Software;+ or++(b) for infringements caused by: (i) Your and any other third party's+ modifications of Covered Software, or (ii) the combination of its+ Contributions with other software (except as part of its Contributor+ Version); or++(c) under Patent Claims infringed by Covered Software in the absence of+ its Contributions.++This License does not grant any rights in the trademarks, service marks,+or logos of any Contributor (except as may be necessary to comply with+the notice requirements in Section 3.4).++2.4. Subsequent Licenses++No Contributor makes additional grants as a result of Your choice to+distribute the Covered Software under a subsequent version of this+License (see Section 10.2) or under the terms of a Secondary License (if+permitted under the terms of Section 3.3).++2.5. Representation++Each Contributor represents that the Contributor believes its+Contributions are its original creation(s) or it has sufficient rights+to grant the rights to its Contributions conveyed by this License.++2.6. Fair Use++This License is not intended to limit any rights You have under+applicable copyright doctrines of fair use, fair dealing, or other+equivalents.++2.7. Conditions++Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted+in Section 2.1.++3. Responsibilities+-------------------++3.1. Distribution of Source Form++All distribution of Covered Software in Source Code Form, including any+Modifications that You create or to which You contribute, must be under+the terms of this License. You must inform recipients that the Source+Code Form of the Covered Software is governed by the terms of this+License, and how they can obtain a copy of this License. You may not+attempt to alter or restrict the recipients' rights in the Source Code+Form.++3.2. Distribution of Executable Form++If You distribute Covered Software in Executable Form then:++(a) such Covered Software must also be made available in Source Code+ Form, as described in Section 3.1, and You must inform recipients of+ the Executable Form how they can obtain a copy of such Source Code+ Form by reasonable means in a timely manner, at a charge no more+ than the cost of distribution to the recipient; and++(b) You may distribute such Executable Form under the terms of this+ License, or sublicense it under different terms, provided that the+ license for the Executable Form does not attempt to limit or alter+ the recipients' rights in the Source Code Form under this License.++3.3. Distribution of a Larger Work++You may create and distribute a Larger Work under terms of Your choice,+provided that You also comply with the requirements of this License for+the Covered Software. If the Larger Work is a combination of Covered+Software with a work governed by one or more Secondary Licenses, and the+Covered Software is not Incompatible With Secondary Licenses, this+License permits You to additionally distribute such Covered Software+under the terms of such Secondary License(s), so that the recipient of+the Larger Work may, at their option, further distribute the Covered+Software under the terms of either this License or such Secondary+License(s).++3.4. Notices++You may not remove or alter the substance of any license notices+(including copyright notices, patent notices, disclaimers of warranty,+or limitations of liability) contained within the Source Code Form of+the Covered Software, except that You may alter any license notices to+the extent required to remedy known factual inaccuracies.++3.5. Application of Additional Terms++You may choose to offer, and to charge a fee for, warranty, support,+indemnity or liability obligations to one or more recipients of Covered+Software. However, You may do so only on Your own behalf, and not on+behalf of any Contributor. You must make it absolutely clear that any+such warranty, support, indemnity, or liability obligation is offered by+You alone, and You hereby agree to indemnify every Contributor for any+liability incurred by such Contributor as a result of warranty, support,+indemnity or liability terms You offer. You may include additional+disclaimers of warranty and limitations of liability specific to any+jurisdiction.++4. Inability to Comply Due to Statute or Regulation+---------------------------------------------------++If it is impossible for You to comply with any of the terms of this+License with respect to some or all of the Covered Software due to+statute, judicial order, or regulation then You must: (a) comply with+the terms of this License to the maximum extent possible; and (b)+describe the limitations and the code they affect. Such description must+be placed in a text file included with all distributions of the Covered+Software under this License. Except to the extent prohibited by statute+or regulation, such description must be sufficiently detailed for a+recipient of ordinary skill to be able to understand it.++5. Termination+--------------++5.1. The rights granted under this License will terminate automatically+if You fail to comply with any of its terms. However, if You become+compliant, then the rights granted under this License from a particular+Contributor are reinstated (a) provisionally, unless and until such+Contributor explicitly and finally terminates Your grants, and (b) on an+ongoing basis, if such Contributor fails to notify You of the+non-compliance by some reasonable means prior to 60 days after You have+come back into compliance. Moreover, Your grants from a particular+Contributor are reinstated on an ongoing basis if such Contributor+notifies You of the non-compliance by some reasonable means, this is the+first time You have received notice of non-compliance with this License+from such Contributor, and You become compliant prior to 30 days after+Your receipt of the notice.++5.2. If You initiate litigation against any entity by asserting a patent+infringement claim (excluding declaratory judgment actions,+counter-claims, and cross-claims) alleging that a Contributor Version+directly or indirectly infringes any patent, then the rights granted to+You by any and all Contributors for the Covered Software under Section+2.1 of this License shall terminate.++5.3. In the event of termination under Sections 5.1 or 5.2 above, all+end user license agreements (excluding distributors and resellers) which+have been validly granted by You or Your distributors under this License+prior to termination shall survive termination.++************************************************************************+* *+* 6. Disclaimer of Warranty *+* ------------------------- *+* *+* Covered Software is provided under this License on an "as is" *+* basis, without warranty of any kind, either expressed, implied, or *+* statutory, including, without limitation, warranties that the *+* Covered Software is free of defects, merchantable, fit for a *+* particular purpose or non-infringing. The entire risk as to the *+* quality and performance of the Covered Software is with You. *+* Should any Covered Software prove defective in any respect, You *+* (not any Contributor) assume the cost of any necessary servicing, *+* repair, or correction. This disclaimer of warranty constitutes an *+* essential part of this License. No use of any Covered Software is *+* authorized under this License except under this disclaimer. *+* *+************************************************************************++************************************************************************+* *+* 7. Limitation of Liability *+* -------------------------- *+* *+* Under no circumstances and under no legal theory, whether tort *+* (including negligence), contract, or otherwise, shall any *+* Contributor, or anyone who distributes Covered Software as *+* permitted above, be liable to You for any direct, indirect, *+* special, incidental, or consequential damages of any character *+* including, without limitation, damages for lost profits, loss of *+* goodwill, work stoppage, computer failure or malfunction, or any *+* and all other commercial damages or losses, even if such party *+* shall have been informed of the possibility of such damages. This *+* limitation of liability shall not apply to liability for death or *+* personal injury resulting from such party's negligence to the *+* extent applicable law prohibits such limitation. Some *+* jurisdictions do not allow the exclusion or limitation of *+* incidental or consequential damages, so this exclusion and *+* limitation may not apply to You. *+* *+************************************************************************++8. Litigation+-------------++Any litigation relating to this License may be brought only in the+courts of a jurisdiction where the defendant maintains its principal+place of business and such litigation shall be governed by laws of that+jurisdiction, without reference to its conflict-of-law provisions.+Nothing in this Section shall prevent a party's ability to bring+cross-claims or counter-claims.++9. Miscellaneous+----------------++This License represents the complete agreement concerning the subject+matter hereof. If any provision of this License is held to be+unenforceable, such provision shall be reformed only to the extent+necessary to make it enforceable. Any law or regulation which provides+that the language of a contract shall be construed against the drafter+shall not be used to construe this License against a Contributor.++10. Versions of the License+---------------------------++10.1. New Versions++Mozilla Foundation is the license steward. Except as provided in Section+10.3, no one other than the license steward has the right to modify or+publish new versions of this License. Each version will be given a+distinguishing version number.++10.2. Effect of New Versions++You may distribute the Covered Software under the terms of the version+of the License under which You originally received the Covered Software,+or under the terms of any subsequent version published by the license+steward.++10.3. Modified Versions++If you create software not governed by this License, and you want to+create a new license for such software, you may create and use a+modified version of this License if you rename the license and remove+any references to the name of the license steward (except to note that+such modified license differs from this License).++10.4. Distributing Source Code Form that is Incompatible With Secondary+Licenses++If You choose to distribute Source Code Form that is Incompatible With+Secondary Licenses under the terms of this version of the License, the+notice described in Exhibit B of this License must be attached.++Exhibit A - Source Code Form License Notice+-------------------------------------------++ This Source Code Form is subject to the terms of the Mozilla Public+ License, v. 2.0. If a copy of the MPL was not distributed with this+ file, You can obtain one at http://mozilla.org/MPL/2.0/.++If it is not possible or desirable to put the notice in a particular+file, then You may include the notice in a location (such as a LICENSE+file in a relevant directory) where a recipient would be likely to look+for such a notice.++You may add additional accurate notices of copyright ownership.++Exhibit B - "Incompatible With Secondary Licenses" Notice+---------------------------------------------------------++ This Source Code Form is "Incompatible With Secondary Licenses", as+ defined by the Mozilla Public License, v. 2.0.
+ LPPaver.cabal view
@@ -0,0 +1,130 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name: LPPaver+version: 0.0.3.1+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+homepage: https://github.com/rasheedja/LPPaver#readme+bug-reports: https://github.com/rasheedja/LPPaver/issues+author: Junaid Rasheed+maintainer: rasheeja@aston.ac.uk+copyright: MPL-2.0+license: MPL-2.0+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md+ ChangeLog.md++source-repository head+ type: git+ location: https://github.com/rasheedja/LPPaver++library+ exposed-modules:+ LPPaver.Constraint.Type+ LPPaver.Constraint.Util+ LPPaver.Decide.Algorithm+ LPPaver.Decide.Linearisation+ LPPaver.Decide.Util+ other-modules:+ Paths_LPPaver+ hs-source-dirs:+ src+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ build-depends:+ PropaFP >=0.1.1 && <0.2+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , collect-errors ==0.1.*+ , containers ==0.6.*+ , directory ==1.3.*+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative ==0.16.*+ , parallel ==3.2.*+ , pqueue ==1.4.*+ , simplex-method ==0.1.*+ default-language: Haskell2010++executable lppaver+ main-is: app/LPPaver.hs+ other-modules:+ Paths_LPPaver+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ LPPaver+ , PropaFP+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , collect-errors ==0.1.*+ , containers ==0.6.*+ , directory ==1.3.*+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative ==0.16.*+ , parallel ==3.2.*+ , pqueue ==1.4.*+ , simplex-method ==0.1.*+ default-language: Haskell2010++test-suite LPPaver-test+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ other-modules:+ Paths_LPPaver+ hs-source-dirs:+ test+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ LPPaver+ , PropaFP >=0.1.1 && <0.2+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , collect-errors ==0.1.*+ , containers ==0.6.*+ , directory ==1.3.*+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative ==0.16.*+ , parallel ==3.2.*+ , pqueue ==1.4.*+ , simplex-method ==0.1.*+ default-language: Haskell2010
+ README.md view
@@ -0,0 +1,45 @@+# LPPaver++LPPaver is an automated prover which targets problems involving nonlinear real arithmetic.+A paper describing LPPaver in detail is coming soon.++## Documentation++[Haddock](https://haskell-haddock.readthedocs.io/en/latest/) documentation for LPPaver can be found at [Hackage](https://hackage.haskell.org/package/LPPaver).++## Reference++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)++## Building++LPPaver can be built with either [Stack](https://docs.haskellstack.org/en/stable/) or [Cabal](https://www.haskell.org/cabal/), though officially we only support Stack.++### Stack++```sh+stack build+```++### Cabal++```sh+cabal build+```++## 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.+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/).+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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/LPPaver.hs view
@@ -0,0 +1,173 @@+module Main where++import MixedTypesNumPrelude+import AERN2.MP.Ball+import LPPaver.Decide.Algorithm+import PropaFP.Expression+import PropaFP.Eliminator+import PropaFP.VarMap+import PropaFP.Parsers.Smt (parseSMT2, parseVCToF, ParsingMode (Why3, CNF))+import PropaFP.Parsers.DRealSmt+import Options.Applicative+import System.Directory+import Data.Ratio++data ProverOptions = ProverOptions+ {+ provingProcessDone :: Bool,+ ceMode :: Bool,+ depthCutoff :: Integer,+ bestFirstSearchCutoff :: Integer,+ precision :: Integer,+ -- relativeImprovementCutoff :: Rational, make this a flag, as a double is probably easier+ fileName :: String+ }++-- data DRealOptions = DRealOptions+-- {+-- dRealFileName :: String,+-- dRealTargetName :: String+-- }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> switch+ (+ long "propafp-done"+ <> short 'a'+ <> help "Add this option if the target file was generated by PropaFP"+ )+ <*> switch+ (+ long "ce-mode"+ <> short 'c'+ <> help "Tell LPPaver to focus on finding a counterexample"+ )+ <*> option auto+ (+ long "depth-cutoff"+ <> short 'd'+ <> help "How hard LPPaver 'works' until giving up. This option is ignored when ce-mode is on"+ <> showDefault+ <> value 100+ <> metavar "INT"+ )+ <*> option auto+ (+ long "best-first-search-cutoff"+ <> short 'b'+ <> help "How hard LPPaver 'works' until giving up when searching for a counterexample. This option is ignored when ce-mode is off"+ <> showDefault+ <> value 1000+ <> metavar "INT"+ )+ <*> option auto+ (+ long "precision"+ <> short 'p'+ <> help "Precision of floating-point numbers used within the prover. Higher precision slows down the prover but may be needed for more difficult problems"+ <> showDefault+ <> value 100+ <> metavar "INT"+ )+ <*> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "SMT2 file to be checked"+ <> metavar "filePath"+ )+main :: IO ()+main = + do + runProver =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "LPPaver - prover" )++runProver :: ProverOptions -> IO ()+runProver proverOptions@(ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) =+ do + if provingProcessDone+ then do+ parsedFile <- parseSMT2 filePath+ case parseDRealSmtToF parsedFile of+ (Just vc, typedVarMap) ->+ 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+ in do+ decideEDNFWithVarMap ednf typedVarMap proverOptions+ (_, _) -> error "Error - Issue parsing given SMT file"+ else do+ -- PATH needs to include folder containing FPTaylor binary after make+ -- symlink to the binary in somewhere like ~/.local/bin will NOT work reliably+ mFptaylorPath <- findExecutable "fptaylor"+ case mFptaylorPath of+ Nothing -> putStrLn "Error - fptaylor executable not in path"+ Just fptaylorPath -> do+ mParsedVC <- parseVCToF filePath fptaylorPath+ case mParsedVC of+ Just (vc, typedVarMap) ->+ 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+ in do+ decideEDNFWithVarMap ednf typedVarMap proverOptions+ Nothing -> do+ putStrLn "unknown"+ putStrLn "Issue parsing file"++decideEDNFWithVarMap :: [[ESafe]] -> TypedVarMap -> ProverOptions -> IO ()+decideEDNFWithVarMap ednf typedVarMap (ProverOptions provingProcessDone ceMode depthCutoff bestFirstSearchCutoff p filePath) = do+ let result =+ if ceMode+ then checkEDNFBestFirstWithSimplexCE ednf typedVarMap bestFirstSearchCutoff 1.2 (prec p)+ else checkEDNFDepthFirstWithSimplex ednf typedVarMap depthCutoff 1.2 (prec p)+ case result of+ (Just True, Just model) -> do+ putStrLn "sat"+ printSMTModel model+ prettyPrintCounterExample model+ (Just False, _) -> do+ putStrLn "unsat"+ r@(_, Just indeterminateExample) -> do+ putStrLn "unknown"+ printSMTModel indeterminateExample+ prettyPrintCounterExample indeterminateExample+ r@(_, _) -> do+ putStrLn "unknown"++prettyPrintCounterExample :: TypedVarMap -> IO ()+prettyPrintCounterExample [] = return ()+prettyPrintCounterExample ((TypedVar (v, (l, r)) t) : vs) = + if l == r+ then do + putStrLn (v ++ " = " ++ show (double l))+ prettyPrintCounterExample vs+ else do+ putStrLn (v ++ " = [" ++ show (double l) ++ ", " ++ show (double r) ++ "]")+ prettyPrintCounterExample vs++printSMTModel :: TypedVarMap -> IO ()+printSMTModel typedVarMap =+ do+ putStrLn "(model"+ printModels typedVarMap+ putStrLn ")"+ where+ printModels [] = return ()+ printModels ((TypedVar (v, (l, r)) t) : vs) = do+ putStrLn $ "(define-fun " ++ v ++ " () " ++ show t ++ " " ++ showNum (l) ++ ")"+ putStrLn $ "(define-fun " ++ v ++ "_vc_constant" ++ " () " ++ show t ++ " " ++ showNum (l) ++ ")" --FIXME: Only do this with a Why3 or similar flag?+ printModels vs++ showNum :: Rational -> String+ showNum num =+ if num < 0+ then "(/ " ++ "(" ++ show (numerator num) ++ ") " ++ show (denominator num) ++ ")"+ else "(/ " ++ show (numerator num) ++ " " ++ show (denominator num) ++ ")"
+ src/LPPaver/Constraint/Type.hs view
@@ -0,0 +1,17 @@+{-|+Module : LPPaver.Constraint.Type+Description : Defines the 'Constraint' type+Copyright : (c) Junaid Rasheed, 2021-2022+License : MPL+Maintainer : jrasheed178@gmail.com+Stability : experimental+Module defining the 'Constraint' data type.+-}+module LPPaver.Constraint.Type where++import MixedTypesNumPrelude++-- | The 'Constraint' data type is used to represent non-strict inequalities.+-- The LHS is a list of 'String' variables along with their 'Rational' coefficients.+-- The RHS is a 'Rational' number. +data Constraint = GEQ [(String, Rational)] Rational | LEQ [(String, Rational)] Rational
+ src/LPPaver/Constraint/Util.hs view
@@ -0,0 +1,55 @@+{-|+Module : LPPaver.Constraint.Util+Description : Utility functions for the 'Constraint' type+Copyright : (c) Junaid Rasheed, 2021-2022+License : MPL+Maintainer : jrasheed178@gmail.com+Stability : experimental+Module defining useful utility functions for the 'Constraint' data type.+-}+{-# LANGUAGE LambdaCase #-}++module LPPaver.Constraint.Util where++import MixedTypesNumPrelude+import LPPaver.Constraint.Type+import Data.List (nub)+import qualified Linear.Simplex.Types as LT+import qualified Data.Map as M+import Data.Maybe+import Linear.Simplex.Types (PolyConstraint)++-- | Get the LHS of a 'Constraint'+constraintLeftSide :: Constraint -> [(String, Rational)]+constraintLeftSide (GEQ lhs _) = lhs+constraintLeftSide (LEQ lhs _) = lhs++-- | Get the LHS of a 'Constraint'+constraintRightSide :: Constraint -> Rational+constraintRightSide (GEQ _ rhs) = rhs+constraintRightSide (LEQ _ rhs) = rhs++-- | Get a list of all variables in a list of 'Constraint's+constraintVars :: [Constraint] -> [String]+constraintVars cs = nub $ aux cs+ where+ aux :: [Constraint] -> [String]+ aux [] = []+ aux (x : xs) = map fst (constraintLeftSide x) ++ aux xs++-- | Convert a list of 'Constraint's into a list of 'LT.PolyConstraint's.+-- The function returns a pair with the first item being a list of 'LT.PolyConstraint's and the second item being a mapping of 'String' variables (from 'Constraint's) to 'Integer' variables (for 'LT.PolyConstraint's).+constraintsToSimplexConstraints :: [Constraint] -> ([LT.PolyConstraint], M.Map String Integer)+constraintsToSimplexConstraints constraints =+ (+ map+ (\case+ GEQ varsWithCoeffs rhs -> LT.GEQ (map (\(stringVar, coeff) -> (fromJust (M.lookup stringVar stringIntVarMap), coeff)) varsWithCoeffs) rhs+ LEQ varsWithCoeffs rhs -> LT.LEQ (map (\(stringVar, coeff) -> (fromJust (M.lookup stringVar stringIntVarMap), coeff)) varsWithCoeffs) rhs+ )+ constraints,+ stringIntVarMap+ )+ where+ stringVars = constraintVars constraints+ stringIntVarMap = M.fromList $ zip stringVars [1..]
+ src/LPPaver/Decide/Algorithm.hs view
@@ -0,0 +1,363 @@+{-|+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 view
@@ -0,0 +1,258 @@+{-|+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 view
@@ -0,0 +1,476 @@+{-|+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
@@ -0,0 +1,143 @@+module Main where++import Prelude+-- import TestFiles+import System.Directory+import PropaFP.Expression+import PropaFP.VarMap+import PropaFP.Parsers.Smt+import PropaFP.Translators.DReal+import PropaFP.Translators.MetiTarski+import System.Exit+import MixedTypesNumPrelude (ifThenElse)+import LPPaver.Decide.Algorithm+import PropaFP.Eliminator (minMaxAbsEliminatorF)+import PropaFP.Parsers.DRealSmt+import AERN2.MP++main :: IO ()+main = do+ putStrLn "Testing Place VCs"+ testPlaceVCs+ putStrLn "Place VCs passed"+ putStrLn "Testing PropaFP VCs"+ testPropaFPVCs+ putStrLn "PropaFP VCs passed"++testPropaFPVCs :: IO ()+testPropaFPVCs = do+ currentDirectory <- getCurrentDirectory+ let satisfiableVCsParentDirectory = currentDirectory ++ "/test/testFiles/PropaFP/sat/"+ let unsatisfiableVCsParentDirectory = currentDirectory ++ "/test/testFiles/PropaFP/unsat/"+ satisfiableVCs <- listDirectory satisfiableVCsParentDirectory+ unsatisfiableVCs <- listDirectory unsatisfiableVCsParentDirectory+ putStrLn "Testing satisfiable VCs with 'model search' mode"+ checkVCsSat satisfiableVCs satisfiableVCsParentDirectory+ putStrLn "Testing unsatisfiable VCs with 'proving' mode"+ checkVCsUnsat unsatisfiableVCs unsatisfiableVCsParentDirectory++testPlaceVCs :: IO ()+testPlaceVCs = do+ currentDirectory <- getCurrentDirectory+ let satisfiableVCsParentDirectory = currentDirectory ++ "/test/testFiles/Place/sat/"+ let unsatisfiableVCsParentDirectory = currentDirectory ++ "/test/testFiles/Place/unsat/"+ satisfiableVCs <- listDirectory satisfiableVCsParentDirectory+ unsatisfiableVCs <- listDirectory unsatisfiableVCsParentDirectory+ putStrLn "Testing satisfiable VCs with 'model search' mode"+ checkVCsSat satisfiableVCs satisfiableVCsParentDirectory+ putStrLn "Testing unsatisfiable VCs with 'proving' mode"+ checkVCsUnsat unsatisfiableVCs unsatisfiableVCsParentDirectory+++checkVCsSat :: [FilePath] -> FilePath -> IO ()+checkVCsSat [] _ = putStrLn "All satisfiable VCs are satisfiable"+checkVCsSat (file : files) fileParent = do+ mFptaylorPath <- findExecutable "fptaylor"+ case mFptaylorPath of+ Nothing -> putStrLn "Error - fptaylor executable not in path"+ Just fptaylorPath -> do+ mParsedVC <- parseVCToF (fileParent ++ file) fptaylorPath+ case mParsedVC of+ Just (vc, typedVarMap) ->+ 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+ putStrLn $ "Proved sat: " ++ file+ checkVCsSat files fileParent+ (Just False, _) -> do+ putStrLn $ "Satisfiable VC found to be unsatisfiable: " ++ file+ exitFailure+ (Nothing, _) -> do+ putStrLn $ "Satisfiable VC could not be decided: " ++ file+ exitFailure+ Nothing -> do+ putStrLn $ "Satisfiable VC could not be parsed: " ++ file+ exitFailure++checkVCsUnsat :: [FilePath] -> FilePath -> IO ()+checkVCsUnsat [] _ = putStrLn "All unsatisfiable VCs are unsatisfiable"+checkVCsUnsat (file : files) fileParent = do+ mFptaylorPath <- findExecutable "fptaylor"+ case mFptaylorPath of+ Nothing -> putStrLn "Error - fptaylor executable not in path"+ Just fptaylorPath -> do+ mParsedVC <- parseVCToF (fileParent ++ file) fptaylorPath+ case mParsedVC of+ Just (vc, typedVarMap) ->+ 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+ putStrLn $ "Proved unsat: " ++ file+ checkVCsUnsat files fileParent+ (Just True, _) -> do+ putStrLn $ "Unsatisfiable VC found to be satisfiable: " ++ file+ exitFailure+ (Nothing, _) -> do+ putStrLn $ "Unsatisfiable VC could not be decided: " ++ file+ exitFailure+ Nothing -> do+ putStrLn $ "Unsatisfiable VC could not be parsed: " ++ file+ exitFailure++-- -- |Take a list of input files, a prover for which PropaFP provides a translator, and a list of files unsupported by the translator.+-- -- Test if PropaFP generates the same file as the one stored (currently under PropaFP/examples/testParent/proverFolderName/testName.proverExt)+-- testProverTranslator :: [(String, String)] -> SupportedProver -> [(String, String)] -> IO ()+-- testProverTranslator [] _ _ = putStrLn "All tests passed"+-- testProverTranslator (test@(testParent, testName) : tests) prover unsupportedTests = do+-- mFptaylorPath <- findExecutable "fptaylor"+-- currentDirectory <- getCurrentDirectory+-- case mFptaylorPath of+-- Nothing -> putStrLn "FPTaylor executable not found in PATH"+-- Just fptaylorPath -> do+-- let vcToProcess = currentDirectory ++ "/examples/" ++ testParent ++ "/why3smt/" ++ testName ++ ".smt2"+-- let originalProcessedVCPath = currentDirectory ++ "/examples/" ++ testParent ++ "/" ++ getProverFolderName prover ++ "/" ++ testName ++ "." ++ getFileExtension prover+-- if test `elem` unsupportedTests+-- then do+-- putStrLn ("Test skipped (unsupported): " ++ vcToProcess) +-- testProverTranslator tests prover unsupportedTests+-- else do+-- originalProcessedVC <- readFile originalProcessedVCPath+-- mNewProcessedVC <- parseVCToSolver vcToProcess fptaylorPath (getTranslator prover) (getNegationStatus prover)+-- case mNewProcessedVC of+-- Just newProcessedVC -> +-- if newProcessedVC == originalProcessedVC+-- then do+-- putStrLn ("Test passed: " ++ vcToProcess)+-- testProverTranslator tests prover unsupportedTests+-- else do+-- putStrLn $ "Processing the following file for dReal: " ++ vcToProcess+-- putStrLn $ "Resulted in an output that differs from: " ++ originalProcessedVCPath+-- putStrLn $ "The incorrect output is:\n"+-- putStrLn newProcessedVC +-- putStrLn $ "The correct output is:\n"+-- putStrLn originalProcessedVC+-- putStrLn ("Test failed: " ++ vcToProcess)+-- exitFailure+-- Nothing -> do+-- putStrLn $ "Issue generating input for dReal using file: " ++ vcToProcess +-- exitFailure+