PropaFP (empty) → 0.1.0.0
raw patch · 24 files changed
+5585/−0 lines, 24 filesdep +PropaFPdep +QuickCheckdep +aern2-mfun
Dependencies added: PropaFP, QuickCheck, aern2-mfun, aern2-mp, base, binary, bytestring, collect-errors, containers, directory, extra, ghc, mixed-types-num, optparse-applicative, process, regex-tdfa, scientific, temporary
Files
- ChangeLog.md +3/−0
- LICENSE +373/−0
- PropaFP.cabal +338/−0
- README.md +77/−0
- app/DRealRunner.hs +66/−0
- app/DRealTranslator.hs +54/−0
- app/LPPaverRunner.hs +73/−0
- app/MetiTarskiRunner.hs +79/−0
- app/MetiTarskiTranslator.hs +54/−0
- app/PrettifySMT2.hs +54/−0
- src/PropaFP/DeriveBounds.hs +478/−0
- src/PropaFP/EliminateFloats.hs +79/−0
- src/PropaFP/Eliminator.hs +243/−0
- src/PropaFP/Expression.hs +1271/−0
- src/PropaFP/Parsers/DRealSmt.hs +131/−0
- src/PropaFP/Parsers/Lisp/DataTypes.hs +108/−0
- src/PropaFP/Parsers/Lisp/Parser.hs +174/−0
- src/PropaFP/Parsers/Smt.hs +969/−0
- src/PropaFP/Translators/BoxFun.hs +74/−0
- src/PropaFP/Translators/DReal.hs +186/−0
- src/PropaFP/Translators/FPTaylor.hs +181/−0
- src/PropaFP/Translators/MetiTarski.hs +131/−0
- src/PropaFP/VarMap.hs +387/−0
- test/Spec.hs +2/−0
+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for PropaFP++## Unreleased changes
+ 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.
+ PropaFP.cabal view
@@ -0,0 +1,338 @@+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: PropaFP+version: 0.1.0.0+synopsis: Auto-active verification of floating-point programs+description: Please see the README on GitHub at <https://github.com/rasheedja/PropaFP#readme>+category: Math, Maths, Mathematics, Formal methods, Theorem Provers+homepage: https://github.com/rasheedja/PropaFP#readme+bug-reports: https://github.com/rasheedja/PropaFP/issues+author: Junaid Rasheed+maintainer: jrasheed178@gmail.com+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/PropaFP++library+ exposed-modules:+ PropaFP.DeriveBounds+ PropaFP.EliminateFloats+ PropaFP.Eliminator+ PropaFP.Expression+ PropaFP.Parsers.DRealSmt+ PropaFP.Parsers.Lisp.DataTypes+ PropaFP.Parsers.Lisp.Parser+ PropaFP.Parsers.Smt+ PropaFP.Translators.BoxFun+ PropaFP.Translators.DReal+ PropaFP.Translators.FPTaylor+ PropaFP.Translators.MetiTarski+ PropaFP.VarMap+ other-modules:+ Paths_PropaFP+ hs-source-dirs:+ src+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ build-depends:+ QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-prettify+ main-is: app/PrettifySMT2.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-run-dreal+ main-is: app/DRealRunner.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-run-lppaver+ main-is: app/LPPaverRunner.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-run-metitarski+ main-is: app/MetiTarskiRunner.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-translate-dreal+ main-is: app/DRealTranslator.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++executable propafp-translate-metitarski+ main-is: app/MetiTarskiTranslator.hs+ other-modules:+ Paths_PropaFP+ default-extensions:+ RebindableSyntax,+ ScopedTypeVariables,+ TypeFamilies,+ TypeOperators,+ ConstraintKinds,+ DefaultSignatures,+ MultiParamTypeClasses,+ FlexibleContexts,+ FlexibleInstances,+ UndecidableInstances+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall -O2+ build-depends:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010++test-suite PropaFP-test+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ other-modules:+ Paths_PropaFP+ 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:+ PropaFP+ , QuickCheck >=2.14.2 && <2.15+ , aern2-mfun >=0.2.9 && <0.3+ , aern2-mp >=0.2.9.1 && <0.3+ , base >=4.7 && <5+ , binary >=0.8.8.0 && <0.9+ , bytestring >=0.10.12.1 && <0.11+ , collect-errors >=0.1.5 && <0.2+ , containers >=0.6.4.1 && <0.7+ , directory >=1.3.6.2 && <1.4+ , extra >=1.7.10 && <1.8+ , ghc >=9.0.2 && <9.1+ , mixed-types-num >=0.5.10 && <0.6+ , optparse-applicative >=0.16.1.0 && <0.17+ , process >=1.6.13.2 && <1.7+ , regex-tdfa >=1.3.1.2 && <1.4+ , scientific >=0.3.7.0 && <0.3.8+ , temporary ==1.3.*+ default-language: Haskell2010
+ README.md view
@@ -0,0 +1,77 @@+# PropaFP++PropaFP is a tool used for auto-active verification of Floating-Point programs.+PropaFP can be used for the verification of [SPARK][1]/[Ada][2] floating-point programs and is integrated with [GNAT Studio 2022](https://www.adacore.com/gnatpro/toolsuite/gnatstudio).++PropaFP can take some Verification Condition (VC), and if PropaFP understands the VC, simplify it, derive bounds for variables, and safely eliminate floating-point operations using over-approximations on rounding errors.+A more detailed description of PropaFP can be found in [this paper](https://arxiv.org/abs/2207.00921).++Below is a diagram summarising the integration with PropaFP and SPARK.++++[1]: https://en.wikipedia.org/wiki/SPARK_(programming_language)+[2]: https://en.wikipedia.org/wiki/Ada_(programming_language)++## Requirements++All PropaFP executables require the [FPTaylor v0.9.3](https://github.com/soarlab/FPTaylor/releases/tag/v0.9.3) executable in your $PATH.++The 'propafp-run-$prover' executables require you to have $prover installed (but not necessarily in your $PATH).++To build PropaFP, we recommend [Stack](https://docs.haskellstack.org/en/stable/README/). We have built PropaFP with Stack version 2.7.5.++## Installation++- Download/Clone this repository+- cd into the repo+- Run `stack build`++Stack will then build the project and tell you where the PropaFP executables have been placed.++### Supported Provers++Currently, PropaFP supports:++- [dReal4](https://github.com/dreal/dreal4) (Tested on v4.21.06.2)+- [LPPaver](https://github.com/rasheedja/LPPaver) (Tested on v0.1.0.0)+- [MetiTarski](https://www.cl.cam.ac.uk/~lp15/papers/Arith/) (Tested on v2.4)++## Usage++PropaFP can work as a standalone program or with GNAT Studio 2022.++### PropaFP as a Standalone Program++To produce some input for PropaFP, see the [Reference](https://github.com/rasheedja/PropaFP/blob/c7680a48c9524768ac113ab5ca0e179dc2f315c6/REFERENCE.md).++#### Translator Executables++PropaFP contains 'translator' executables, which takes some input file, transforms the VC as described above, and produces another input file for the target prover.+The current 'translator' executables are:++- propafp-translate-dreal -f [smtFileContainingVC.smt2] -t [fileToWrite.smt2]+- propafp-translate-metitarski -f [smtFileContainingVC.smt2] -t [fileToWrite.smt2]++The propafp-translate-dreal executable can also be used for LPPaver.+If PropaFP does not understand the VC, it writes an empty file.++#### Runner Executables++'Runner' executables take some input file, transform the VC as described above, and calls the prover on the transformed VC.+'Runner' executables require the prover for each executable to be in your $PATH.+The current 'runner' executables are:++- propafp-run-dreal -f [smtFileContainingVC.smt2] -p [pathToDReal]+- propafp-run-lppaver -f [smtFileContainingVC.smt2] -p [pathToLPPaver]+- propafp-run-metitarski -f [smtFileContainingVC.smt2] -p [pathToMetiTarski]++To run LPPaver in a mode specialised to find counter-examples, you can pass the -c option.++### PropaFP with GNAT Studio++For instructions to use with GNAT Studio 2022, see [sparkFiles/INSTRUCTIONS.md](https://github.com/rasheedja/PropaFP/blob/c7680a48c9524768ac113ab5ca0e179dc2f315c6/sparkFiles/INSTRUCTIONS.md)++## Guided Example++[A guided example of using PropaFP with GNAT Studio.](https://github.com/rasheedja/PropaFP/blob/c7680a48c9524768ac113ab5ca0e179dc2f315c6/sparkFiles/EXAMPLE.md)
+ app/DRealRunner.hs view
@@ -0,0 +1,66 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Translators.DReal+import System.Process+import System.IO.Temp+import GHC.IO.Handle++data ProverOptions = ProverOptions+ {+ fileName :: String,+ dRealPath :: String+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "path to smt2 file to be checked"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "dreal-path"+ <> short 'p'+ <> help "path to dReal executable"+ <> metavar "filePath"+ )++runDReal :: ProverOptions -> IO ()+runDReal (ProverOptions filePath dRealPath) =+ 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 -> error "fptaylor executable not in path"+ Just fptaylorPath -> do+ mdRealInput <- parseVCToSolver filePath fptaylorPath formulaAndVarMapToDReal False+ case mdRealInput of+ Just dRealInput -> do+ (exitCode, output, errDetails) <- withSystemTempFile "dreal.smt2" handleDRealFile+ putStrLn output+ return ()+ where+ handleDRealFile fPath fHandle =+ do+ hPutStr fHandle dRealInput+ _ <- hGetContents fHandle -- Ensure handler has finished writing before calling DReal+ readProcessWithExitCode dRealPath [fPath, "--precision", "1e-100"] []+ Nothing -> error "Issue generating input for DReal"++main :: IO ()+main = + do + runDReal =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "fixme"+ <> header "DReal - runner" )
+ app/DRealTranslator.hs view
@@ -0,0 +1,54 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Translators.DReal++data ProverOptions = ProverOptions+ {+ fileName :: String,+ targetName :: String+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "SMT2 file to be checked"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "target-path"+ <> short 't'+ <> help "location to write dReal file"+ <> metavar "targetPath"+ )++runDRealTranslator :: ProverOptions -> IO ()+runDRealTranslator (ProverOptions filePath targetPath) =+ 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 "FPTaylor executable not found in path"+ Just fptaylorPath -> do+ mDRealInput <- parseVCToSolver filePath fptaylorPath formulaAndVarMapToDReal False+ case mDRealInput of+ Just dRealInput -> writeFile targetPath dRealInput+ Nothing -> error "Issue generating input for dReal"++main :: IO ()+main = + do + runDRealTranslator =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "DReal - translator" )
+ app/LPPaverRunner.hs view
@@ -0,0 +1,73 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Translators.DReal+import System.Process+import System.IO.Temp+import GHC.IO.Handle++data ProverOptions = ProverOptions+ {+ filePath :: String,+ lppaverPath :: String,+ ceMode :: Bool+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "path to smt2 file to be checked"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "lppaver-path"+ <> short 'p'+ <> help "path to LPPaver executable"+ <> metavar "filePath"+ )+ <*> switch+ (+ long "counter-example-mode"+ <> short 'c'+ <> help "Runs LPPaver in a specialised mode to find potential counter-examples"+ )++runLPPaver :: ProverOptions -> IO ()+runLPPaver (ProverOptions filePath lppaverPath ceMode) =+ 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 -> error "fptaylor executable not in path"+ Just fptaylorPath -> do+ mdRealInput <- parseVCToSolver filePath fptaylorPath formulaAndVarMapToDReal False+ case mdRealInput of+ Just dRealInput -> do+ (exitCode, output, errDetails) <- withSystemTempFile "lppaver.smt2" handleDRealFile+ putStrLn output+ return ()+ where+ handleDRealFile fPath fHandle =+ do+ hPutStr fHandle dRealInput+ _ <- hGetContents fHandle -- Ensure handler has finished writing before calling DReal+ readProcessWithExitCode lppaverPath (if ceMode then ["-f", fPath, "-c"] else ["-f", fPath]) []+ Nothing -> error "Issue generating input for LPPaver"++main :: IO ()+main = + do + runLPPaver =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "LPPaver - runner" )
+ app/MetiTarskiRunner.hs view
@@ -0,0 +1,79 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Translators.MetiTarski+import System.Process+import System.IO.Temp+import GHC.IO.Handle+import GHC.SysTools (isContainedIn)++data ProverOptions = ProverOptions+ {+ filePath :: String,+ metiTarskiPath :: String,+ convertForWhy3 :: Bool+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "path to smt2 file to be checked"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "metitarski-path"+ <> short 'p'+ <> help "path to MetiTarski executable"+ <> metavar "filePath"+ )+ <*> switch+ (+ long "convert-for-why3"+ <> short 'c'+ <> help "Converts MetiTarski output to SMT style output, so Why3 can understand the output (Theorem turns into 'unsat', anything else turns into 'unknown')"+ )+ +runMetiTarski :: ProverOptions -> IO ()+runMetiTarski (ProverOptions filePath' metiTarskiPath' convertForWhy3') =+ 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 -> error "fptaylor executable not in path"+ Just fptaylorPath -> do+ mMetiTarskiInput <- parseVCToSolver filePath' fptaylorPath formulaAndVarMapToMetiTarski True -- Negate the VC, MetiTarski does not give unsat, only sat or gave up, so make MetiTarski prove the contradiction+ case mMetiTarskiInput of+ Just metiTarskiInput -> do+ (exitCode, output, errDetails) <- withSystemTempFile "metitarski.tptp" handleMetiTarskiFile+ if convertForWhy3' then putStrLn (convertOutputToSMT output) else putStrLn output+ return ()+ where+ convertOutputToSMT outputToConvert = + if "Theorem" `isContainedIn` outputToConvert+ then "unsat"+ else "unknown"++ handleMetiTarskiFile fPath fHandle =+ do+ hPutStr fHandle metiTarskiInput+ _ <- hGetContents fHandle -- Ensure handler has finished writing before calling MetiTarski+ readProcessWithExitCode metiTarskiPath' ["--autoIncludeSuperExtended", fPath] []+ Nothing -> error "Issue generating input for MetiTarski"++main :: IO ()+main = + do + runMetiTarski =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "MetiTarski - runner" )
+ app/MetiTarskiTranslator.hs view
@@ -0,0 +1,54 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Translators.MetiTarski++data ProverOptions = ProverOptions+ {+ fileName :: String,+ targetName :: String+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "SMT2 file to be checked"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "target-path"+ <> short 't'+ <> help "location to write MetiTarski file"+ <> metavar "targetPath"+ )++runMetiTarskiTranslator :: ProverOptions -> IO ()+runMetiTarskiTranslator (ProverOptions filePath targetPath) =+ 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 "FPTaylor executable not found in path"+ Just fptaylorPath -> do+ mMetiTarskiInput <- parseVCToSolver filePath fptaylorPath formulaAndVarMapToMetiTarski True -- Negate the VC, MetiTarski does not give unsat, only sat or gave up, so make MetiTarski prove the contradiction+ case mMetiTarskiInput of+ Just metiTarskiInput -> writeFile targetPath metiTarskiInput+ Nothing -> error "Issue generating input for MetiTarski"++main :: IO ()+main = + do + runMetiTarskiTranslator =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "MetiTarski - translator" )
+ app/PrettifySMT2.hs view
@@ -0,0 +1,54 @@+module Main where++import MixedTypesNumPrelude+import Options.Applicative+import System.Directory+import PropaFP.Parsers.Smt+import PropaFP.Expression++data ProverOptions = ProverOptions+ {+ fileName :: String,+ targetName :: String+ }++proverOptions :: Parser ProverOptions+proverOptions = ProverOptions+ <$> strOption+ (+ long "file-path"+ <> short 'f'+ <> help "SMT2 file to be prettified"+ <> metavar "filePath"+ )+ <*> strOption+ (+ long "target-path"+ <> short 't'+ <> help "location to write prettified file"+ <> metavar "targetPath"+ )++runDRealTranslator :: ProverOptions -> IO ()+runDRealTranslator (ProverOptions filePath targetPath) =+ 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 "FPTaylor executable not found in path"+ Just fptaylorPath -> do+ mVC <- parseVCToF filePath fptaylorPath+ case mVC of+ Just (vc, vm) -> writeFile targetPath (prettyShowVC vc vm)+ Nothing -> error "Issue processing SMT2 file"++main :: IO ()+main = + do + runDRealTranslator =<< execParser opts+ where+ opts = info (proverOptions <**> helper)+ ( fullDesc+ <> progDesc "todo"+ <> header "SMT2 Prettifier" )
+ src/PropaFP/DeriveBounds.hs view
@@ -0,0 +1,478 @@+{-# LANGUAGE PartialTypeSignatures #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use camelCase" #-} +{-| + Module : PropaFP.DeriveBounds + Description : Deriving ranges for variables from hypotheses inside a formula + Copyright : (c) Michal Konecny 2013, 2021 + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + + Deriving ranges for variables from hypotheses inside a formula +-} +module PropaFP.DeriveBounds +where + +import MixedTypesNumPrelude +import qualified Numeric.CollectErrors as CN + +import qualified Prelude as P + +import qualified Data.Map as Map +import qualified Data.List as List +-- import qualified Data.Bifunctor as Bifunctor +import AERN2.MP.Ball +import AERN2.MP.Dyadic + +import PropaFP.Expression +import PropaFP.VarMap + +import Debug.Trace (trace) +import Data.List + +-- examples: + +_f1 :: F -- eliminates "x" +_f1 = FConn Impl (FConn And (FComp Le (Var "x") (Lit 1.0)) (FComp Le (Lit 0.0) (Var "x"))) (FComp Eq (Lit 0.0) (Lit 0.0)) + +_f2 :: F +_f2 = FConn Impl (FConn And (FComp Le (Var "x") (Lit 1.0)) (FComp Le (Lit 0.0) (Var "x"))) (FComp Eq (Var "x") (Lit 0.0)) + +_f3 :: F -- underivable "x" +_f3 = FConn Impl (FConn And (FComp Le (Var "x") (Lit 1.0)) (FComp Le (Var "x") (Lit 0.0))) (FComp Eq (Var "x") (Lit 0.0)) + +_f4 :: F -- nested implication containing bound on "x" guarded by a condition on "n" +_f4 = + FConn Impl + (FConn And + (FConn And + (FComp Le (Var "x") (Lit 1.0)) + (FComp Eq (Var "n") (Lit 1.0))) + (FConn Impl (FComp Eq (Var "n") (Lit 1.0)) (FComp Le (Lit 0.0) (Var "x")))) + (FComp Eq (Var "x") (Lit 0.0)) + +_f5 :: F -- two opposing implications which contain the same bound on "x" +_f5 = + FConn And + ( + FConn And + (FConn And + (FComp Ge (Var "n") (Lit 0.0)) + (FComp Le (Var "n") (Lit 2.0)) + ) + (FConn And + (FConn Impl + (FComp Le (Var "n") (Lit 1.0)) + (FConn And + (FComp Ge (Var "x") (Lit (-1.0))) + (FComp Le (Var "x") (Lit 1.0)) + ) + ) + (FConn Impl + ((FComp Gt (Var "n") (Lit 1.0))) + (FConn And + (FComp Ge (Var "x") (Lit (-1.0))) + (FComp Le (Var "x") (Lit 1.0)) + ) + ) + ) + ) + $ + FComp Ge (EUnOp Sin (Var "x")) (Lit 0.0) + +type VarName = String + +deriveBoundsAndSimplify :: F -> (F, VarMap, [VarName]) +deriveBoundsAndSimplify form' = + (finalSimplifiedF, derivedRangesWithoutPoints, map fst underivedRanges) + where + finalSimplifiedF = simplifyF simplifiedFWithSubstitutedPoints + + + simplifiedFWithSubstitutedPoints = substitutePoints simplifiedF varsWithPoints + + simplifiedF = (\(FConn Impl f FFalse) -> f) simplifiedFImpliesFalse + -- undo implies false on simplifiedFImpliesFalse + + (derivedRangesWithoutPoints, varsWithPoints) = seperatePoints derivedRanges + + derivedRanges = map removeJust mDerivedRanges + + (mDerivedRanges, underivedRanges) = List.partition isGood varRanges + + isPoint (l, r) = l == r + + + substitutePoints :: F -> [(String, Rational)] -> F + substitutePoints f [] = f + substitutePoints f ((var, val) : varPoints) = substitutePoints (substVarFWithLit f var val) varPoints + + seperatePoints :: VarMap -> (VarMap, [(String, Rational)]) + seperatePoints [] = ([], []) + seperatePoints ((var, bounds) : varMap) = + if isPoint bounds + then (resultingVarMap, (var, fst bounds) : resultingPoints) + else ((var, bounds) : resultingVarMap, resultingPoints) + where + (resultingVarMap, resultingPoints) = seperatePoints varMap + + form = FConn Impl form' FFalse -- Make the given form imply false for derivation of bounds + removeJust (v, (Just l, Just r)) = (v, (l, r)) + removeJust _ = error "deriveBounds: removeJust failed" + varRanges = Map.toList box + isGood (_v, (Just _,Just _)) = True + isGood _ = False + initBox = Map.fromList $ zip (extractVariablesF form) (repeat (Nothing, Nothing)) + (box, simplifiedFImpliesFalse) = aux initBox $ form + where + aux b f + | b P.== b2 = (b, f2) + | otherwise = aux b2 f2 + where + f2 = (\(FConn Impl form2 _falseTerm) -> FConn Impl (simplifyF form2) _falseTerm) (evalF_comparisons b f) + -- simplify where possible with the knowledge we are restricted to box b + -- avoid simplifying form2 -> false, only simplify form2 + b' = Map.intersection b $ Map.fromList $ zip (extractVariablesF f2) (repeat ()) + -- remove variables that do not appear in f2 + b2 = scanHypotheses f2 b' + -- attempt to improve the bounds on the variables + +type VarBoundMap = Map.Map VarName (Maybe Rational, Maybe Rational) + +-- TODO: Could refactor this to remove need of form -> false +scanHypotheses :: F -> VarBoundMap -> VarBoundMap +scanHypotheses (FConn Impl h c) = + scanHypotheses c . scanHypothesis h False +scanHypotheses _ = id + +scanHypothesis :: F -> Bool -> VarBoundMap -> VarBoundMap +scanHypothesis (FNot h) isNegated intervals = scanHypothesis h (not isNegated) intervals +scanHypothesis (FConn And (FConn Impl cond1 branch1) (FConn Impl (FNot cond2) branch2)) False intervals + | cond1 P.== cond2 = scanHypothesis (FConn Or branch1 branch2) False intervals + | sort (simplifyESafeDoubleList (fToEDNF (simplifyF cond1))) P.== sort (simplifyESafeDoubleList (fToEDNF (simplifyF cond2))) = scanHypothesis (FConn Or branch1 branch2) False intervals +-- scanHypothesis f@(FConn And h1@(FConn Impl cond1 branch1) h2@(FConn Impl cond2 branch2)) False intervals +-- = +-- trace (show f) $ +-- trace (show intervals) $ +-- trace (show (checkFWithEval cond1 intervals)) $ +-- trace (show (checkFWithEval cond2 intervals)) $ +-- -- doesn't work because cond1/2 is indeterminate most of the time +-- case checkFWithEval cond1 intervals of +-- Nothing -> (scanHypothesis h1 False . scanHypothesis h2 False) intervals +-- result1 -> +-- case checkFWithEval cond2 intervals of +-- Nothing -> (scanHypothesis h1 False . scanHypothesis h2 False) intervals +-- result2 -> +-- if result1 P./= result2 +-- then scanHypothesis (FConn Or branch1 branch2) False intervals +-- else (scanHypothesis h1 False . scanHypothesis h2 False) intervals +scanHypothesis (FConn And h1 h2) isNegated intervals = + if isNegated + then scanHypothesis (FConn Or (FNot h1) (FNot h2)) False intervals + else (scanHypothesis h1 isNegated . scanHypothesis h2 isNegated) intervals +scanHypothesis (FConn Or h1 h2) isNegated intervals = + if isNegated + then scanHypothesis (FConn And (FNot h1) (FNot h2)) False intervals + else Map.unionWith mergeWorse box1 box2 + where + box1 = iterateUntilNoChange (scanHypothesis h1 isNegated) intervals + box2 = iterateUntilNoChange (scanHypothesis h2 isNegated) intervals + mergeWorse (l1,r1) (l2,r2) = (min <$> l1 <*> l2, max <$> r1 <*> r2) + + -- mergeWorse (l1,r1) (l2,r2) = + -- case (l1, r1, l2, r2) of + -- (Nothing, Nothing, Just _, Just _) -> (l2, r2) -- FIXME: hack, should only do this if variable of interest only exists in one branch + -- (Just _, Just _, Nothing, Nothing) -> (l1, r1) -- FIXME: hack, should only do this if variable of interest only exists in one branch + -- _ -> (min <$> l1 <*> l2, max <$> r1 <*> r2) + + iterateUntilNoChange refineBox b1 + | b1 P.== b2 = b1 + | otherwise = iterateUntilNoChange refineBox b2 + where + b2 = refineBox b1 + -- iterateUntilNoChange b1 f + -- | b1 P.== b2 = b1 + -- | otherwise = scanHypothesis f isNegated b1 +scanHypothesis (FConn Impl h1 h2) isNegated intervals = scanHypothesis (FConn Or (FNot h1) h2) isNegated intervals +-- We need: data Comp = Gt | Ge | Lt | Le | Eq +scanHypothesis (FComp Eq _ _) True intervals = intervals +scanHypothesis (FComp Eq _e1@(Var v1) _e2@(Var v2)) False intervals = + Map.insert v1 val $ + Map.insert v2 val $ + intervals + where + Just val1 = Map.lookup v1 intervals + Just val2 = Map.lookup v2 intervals + val = updateUpper val1 $ updateLower val1 $ val2 + +scanHypothesis (FComp Eq (Var v) e) False intervals = + Map.insertWith updateUpper v val $ + Map.insertWith updateLower v val intervals + where + val = evalE_Rational intervals e + +scanHypothesis (FComp Eq e (Var v)) False intervals = + Map.insertWith updateUpper v val $ + Map.insertWith updateLower v val intervals + where + val = evalE_Rational intervals e + +-- Deal with negated inequalites +scanHypothesis (FComp Le e1 e2) True intervals = + scanHypothesis (FComp Gt e1 e2) False intervals + +scanHypothesis (FComp Lt e1 e2) True intervals = + scanHypothesis (FComp Ge e1 e2) False intervals + +scanHypothesis (FComp Gt e1 e2) True intervals = + scanHypothesis (FComp Le e1 e2) False intervals + +scanHypothesis (FComp Ge e1 e2) True intervals = + scanHypothesis (FComp Lt e1 e2) False intervals + +scanHypothesis (FComp Le _e1@(Var v1) _e2@(Var v2)) False intervals = + Map.insert v1 (updateUpper val2 val1) $ + Map.insert v2 (updateLower val1 val2) $ + intervals + where + Just val1 = Map.lookup v1 intervals + Just val2 = Map.lookup v2 intervals + +scanHypothesis (FComp Le (Var v) e) False intervals = + Map.insertWith updateUpper v (evalE_Rational intervals e) intervals +scanHypothesis (FComp Le e (Var v)) False intervals = + Map.insertWith updateLower v (evalE_Rational intervals e) intervals +-- Bounds for absolute values of Vars +scanHypothesis (FComp Le (EUnOp Abs (Var v)) e) False intervals = + -- trace (show bounds) + Map.insertWith updateLower v bounds $ Map.insertWith updateUpper v bounds intervals + where + (eValL, eValR) = evalE_Rational intervals e + bounds = (fmap negate eValL, eValR) +-- reduce Le, Geq, Ge on equivalent Leq (note that we treat strict and non-strict the same way): +-- Fixme: Some way to treat strict/non-strict with integer variables differently +scanHypothesis (FComp Lt e1 e2) False intervals = scanHypothesis (FComp Le e1 e2) False intervals +scanHypothesis (FComp Ge e1 e2) False intervals = scanHypothesis (FComp Le e2 e1) False intervals +scanHypothesis (FComp Gt e1 e2) False intervals = scanHypothesis (FComp Le e2 e1) False intervals +scanHypothesis _ _False intervals = intervals + +{-| + Replace within a formula some comparisons with FTrue/FFalse, namely + those comparisons that on the given box can be easily seen to be true/false. + -} +evalF_comparisons :: VarBoundMap -> F -> F +evalF_comparisons intervals = eC + where + eC FTrue = FTrue + eC FFalse = FFalse + eC (FNot f) = FNot (eC f) + eC (FConn op f1 f2) = FConn op (eC f1) (eC f2) + eC (FComp Gt e1 e2) = eC $ FComp Lt e2 e1 + eC (FComp Ge e1 e2) = eC $ FComp Le e2 e1 + eC (FComp Eq e1 e2) = eC $ FConn And (FComp Le e2 e1) (FComp Le e1 e2) + eC f@(FComp Le e1 e2) = + case (eE e1, eE e2) of + ((_, Just e1R), (Just e2L, _)) | e1R <= e2L -> FTrue + ((Just e1L, _), (_, Just e2R)) | e2R < e1L -> FFalse + _ -> f + eC f@(FComp Lt e1 e2) = + case (eE e1, eE e2) of + ((_, Just e1R), (Just e2L, _)) | e1R < e2L -> FTrue + ((Just e1L, _), (_, Just e2R)) | e2R <= e1L -> FFalse + _ -> f + eE = evalE_Rational intervals +-- x is inconsistent +-- since we have exists x in empty set +-- x > y is False +-- we use exists instead of forall because we're looking for a model for x + +evalE_Rational :: + VarBoundMap -> E -> (Maybe Rational, Maybe Rational) +evalE_Rational intervals = + rationalBounds . evalE (cn . mpBallP p) intervalsMPBall p + where + intervalsMPBall = Map.map toMPBall intervals + toMPBall :: (Maybe Rational, Maybe Rational) -> CN MPBall + toMPBall (Just l, Just r) = cn $ (mpBallP p l) `hullMPBall` (mpBallP p r) --FIXME: deal with contradictions, inconsistent intervals, directly + -- If we have an overlapping interval, turn conjunction into False + -- l = 1, r = 0 + toMPBall _ = CN.noValueNumErrorCertain $ CN.NumError "no bounds" + p = prec 60 -- Needs to be at least 54 for turning double pi from Why3 into real pi FIXME: behaviour with very high prec (say prec 1000)? + rationalBounds :: CN MPBall -> (Maybe Rational, Maybe Rational) + rationalBounds cnBall = + case CN.toEither cnBall of + Right ball -> + let (l,r) = endpoints ball in + (Just (rational l), Just (rational r)) + _ -> (Nothing, Nothing) + +updateUpper :: + CanMinMaxSameType a => + (t, Maybe a) -> (t1, Maybe a) -> (t1, Maybe a) +updateUpper (_,Just u2) (l, Just u1) = (l, Just $ min u1 u2) +updateUpper (_,Just u2) (l, Nothing) = (l, Just $ u2) +updateUpper (_,Nothing) (l, Just u1) = (l, Just $ u1) +updateUpper (_,Nothing) (l, Nothing) = (l, Nothing) +--updateUpper _ _ = error "DeriveBounds: updateUpper failed" + +updateLower :: + CanMinMaxSameType a => + (Maybe a, t) -> (Maybe a, t1) -> (Maybe a, t1) +updateLower (Just l2,_) (Just l1,u) = (Just $ max l1 l2, u) +updateLower (Just l2,_) (Nothing,u) = (Just $ l2, u) +updateLower (Nothing,_) (Just l1,u) = (Just $ l1, u) +updateLower (Nothing,_) (Nothing,u) = (Nothing, u) +--updateLower _ _ = error "DeriveBounds: updateLower failed" + +-- | compute the value of E with Vars at specified points +-- | (a generalised version of computeE) +evalE :: + (Ring v, CanDivSameType v, CanPowBy v Integer, + CanMinMaxSameType v, CanAbsSameType v, + CanPowBy v v, CanSqrtSameType v, CanSinCosSameType v, + IsInterval v, CanAddThis v Integer, HasDyadics v, CanMinMaxSameType (IntervalEndpoint v), _ + ) + => + (Rational -> v) -> + Map.Map VarName v -> Precision -> E -> v +evalE fromR (varMap :: Map.Map VarName v) p = evalVM + where + evalVM :: E -> v + evalVM (EBinOp op e1 e2) = + case op of + Min -> evalVM e1 `min` evalVM e2 + Max -> evalVM e1 `max` evalVM e2 + Add -> evalVM e1 + evalVM e2 + Sub -> evalVM e1 - evalVM e2 + Mul -> evalVM e1 * evalVM e2 + Div -> evalVM e1 / evalVM e2 + Pow -> evalVM e1 ^ evalVM e2 + Mod -> evalVM e1 `mod` evalVM e2 + evalVM (EUnOp op e) = + case op of + Abs -> abs (evalVM e) + Sqrt -> sqrt (evalVM e) + Negate -> negate (evalVM e) + Sin -> sin (evalVM e) + Cos -> cos (evalVM e) + evalVM (Var v) = + case Map.lookup v varMap of + Nothing -> + error ("evalE: varMap does not contain variable " ++ show v) + Just r -> r + evalVM Pi = cn (piBallP p) + evalVM (Lit i) = (fromR i) + evalVM (PowI e i) = evalVM e ^ i + evalVM (Float32 _ e) = (onePlusMinusEpsilon * (evalVM e)) + zeroPlusMinusEpsilon + where + eps :: v + eps = convertExactly $ dyadic $ 0.5^23 + onePlusMinusEpsilon :: v + onePlusMinusEpsilon = fromEndpointsAsIntervals (1 + (-eps)) (1 + eps) + epsD :: v + epsD = convertExactly $ dyadic $ 0.5^149 + zeroPlusMinusEpsilon :: v + zeroPlusMinusEpsilon = fromEndpointsAsIntervals (-epsD) epsD + evalVM (Float64 _ e) = (onePlusMinusEpsilon * (evalVM e)) + zeroPlusMinusEpsilon + where + eps :: v + eps = convertExactly $ dyadic $ 0.5^52 + onePlusMinusEpsilon :: v + onePlusMinusEpsilon = fromEndpointsAsIntervals (1 + (-eps)) (1 + eps) + epsD :: v + epsD = convertExactly $ dyadic $ 0.5^1074 + zeroPlusMinusEpsilon :: v + zeroPlusMinusEpsilon = fromEndpointsAsIntervals (-epsD) epsD + evalVM (RoundToInteger mode e) = fmap (roundMPBall mode) (evalVM e) + evalVM e = error $ "evalE: undefined for: " ++ show e + +roundMPBall :: (Real (IntervalEndpoint i), IsInterval i, IsInterval p, + ConvertibleExactly Integer (IntervalEndpoint p)) => + RoundingMode -> i -> p +roundMPBall mode i = + let + (l', r') = endpoints i + l = toRational l' + r = toRational r' + lFloor = floor l + lCeil = ceiling l + rFloor = floor r + rCeil = ceiling r + in case mode of + RNE -> + fromEndpoints + (if l - lFloor == 0.5 + then (if even lFloor then convertExactly lFloor else convertExactly lCeil) + else (if l - lFloor < 0.5 then convertExactly lFloor else convertExactly lCeil)) + (if r - rFloor == 0.5 + then (if even rFloor then convertExactly rFloor else convertExactly rCeil) + else (if r - rFloor < 0.5 then convertExactly rFloor else convertExactly rCeil)) + RTP -> fromEndpoints (convertExactly lCeil) (convertExactly rCeil) + RTN -> fromEndpoints (convertExactly lFloor) (convertExactly rFloor) + RTZ -> + fromEndpoints + (if isCertainlyPositive l then convertExactly lFloor else convertExactly lCeil) -- FIXME: check isCertainNegative? + (if isCertainlyPositive r then convertExactly rFloor else convertExactly rCeil) + RNA -> + fromEndpoints + (if l - lFloor == 0.5 + then (if isCertainlyPositive l then convertExactly lCeil else convertExactly lFloor) -- FIXME: check isCertainNegative? + else (if l - lFloor < 0.5 then convertExactly lFloor else convertExactly lCeil)) + (if r - rFloor == 0.5 + then (if isCertainlyPositive r then convertExactly rCeil else convertExactly rFloor) + else (if r - rFloor < 0.5 then convertExactly rFloor else convertExactly rCeil)) + +checkFWithEval :: F -> VarBoundMap -> Maybe Bool +checkFWithEval f' varBoundMap = aux f' + where + aux (FComp op e1 e2) = + case (mE1L, mE1R, mE2L, mE2R) of + (Just e1L, Just e1R, Just e2L, Just e2R) -> decideKleenean op (e1L, e1R) (e2L, e2R) + (_, _, _, _) -> Nothing + where + (mE1L, mE1R) = evalE_Rational varBoundMap e1 + (mE2L, mE2R) = evalE_Rational varBoundMap e2 + + decideKleenean Lt (l1, r1) (l2, r2) + | r1 < l2 = Just True + | r2 <= l1 = Just False + | otherwise = Nothing + decideKleenean Le (l1, r1) (l2, r2) + | r1 <= l2 = Just True + | r2 < l1 = Just False + | otherwise = Nothing + decideKleenean Ge x y = decideKleenean Le y x + decideKleenean Gt x y = decideKleenean Lt y x + decideKleenean Eq x y = --TODO: Use guards here + case decideKleenean Ge y x of + Just False -> Just False + Just True -> decideKleenean Le y x + Nothing -> + case decideKleenean Le y x of + Just False -> Just False + _ -> Nothing + + aux (FConn op f1 f2) = + case op of + And -> + case (f1Val, f2Val) of + (Just r1, Just r2) -> Just $ r1 && r2 + (_, _) -> Nothing + Or -> + case (f1Val, f2Val) of + (Just r1, Just r2) -> Just $ r1 || r2 + (_, _) -> Nothing + Impl -> + case (f1Val, f2Val) of + (Just r1, Just r2) -> Just $ not r1 || r2 + (_, _) -> Nothing + where + f1Val = aux f1 + f2Val = aux f2 + aux (FNot f) = not <$> aux f + aux FTrue = Just True + aux FFalse = Just False
+ src/PropaFP/EliminateFloats.hs view
@@ -0,0 +1,79 @@+module PropaFP.EliminateFloats where++import MixedTypesNumPrelude+import PropaFP.Expression+import PropaFP.Translators.FPTaylor+import System.Process+import System.IO.Unsafe+import PropaFP.VarMap (VarMap, prettyShowVarMap)+import System.Exit +import System.IO.Temp+import GHC.IO.Handle++removeFloats :: E -> E+removeFloats (Float _ e) = removeFloats e+removeFloats (Float32 _ e) = removeFloats e+removeFloats (Float64 _ e) = removeFloats e+removeFloats (EBinOp op e1 e2) = EBinOp op (removeFloats e1) (removeFloats e2)+removeFloats (EUnOp op e) = EUnOp op (removeFloats e)+removeFloats (PowI e i) = PowI (removeFloats e) i+removeFloats (Lit v) = Lit v+removeFloats (Var v) = Var v+removeFloats Pi = Pi+removeFloats (RoundToInteger m e) = RoundToInteger m (removeFloats e)++-- Bool True means 'strengthen' the formula, i.e. rnd(x) >= rnd(y) becomes x - rndErrorX >= y + rndErrorY.+-- Bool False means 'weaken' the formula , i.e. rnd(x) >= rnd(y) becomes x + rndErrorX >= y - rndErrorY+-- Eqs are turned into <= and >=, and then floats are eliminated+-- TODO: Test Max,Min+eliminateFloatsF :: F -> VarMap -> Bool -> FilePath -> IO F+eliminateFloatsF f varMap strengthenFormula fptaylorPath =+ aux f strengthenFormula+ where+ aux :: F -> Bool -> IO F+ aux (FConn Impl context goal) strengthenFormula =+ FConn Impl+ <$> aux context (not strengthenFormula)+ <*> aux goal strengthenFormula+ aux (FNot f) strengthenFormula = FNot <$> aux f (not strengthenFormula)+ aux (FComp op e1 e2) strengthenFormula =+ case op of+ Gt -> FComp op <$> eliminateFloatsFromExpression e1 strengthenFormula <*> eliminateFloatsFromExpression e2 (not strengthenFormula)+ Ge -> FComp op <$> eliminateFloatsFromExpression e1 strengthenFormula <*> eliminateFloatsFromExpression e2 (not strengthenFormula)+ Lt -> FComp op <$> eliminateFloatsFromExpression e1 (not strengthenFormula) <*> eliminateFloatsFromExpression e2 strengthenFormula+ Le -> FComp op <$> eliminateFloatsFromExpression e1 (not strengthenFormula) <*> eliminateFloatsFromExpression e2 strengthenFormula+ Eq -> aux (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) strengthenFormula+ aux (FConn op e1 e2) strengthenFormula = FConn op <$> aux e1 strengthenFormula <*> aux e2 strengthenFormula+ aux FTrue _ = return FTrue+ aux FFalse _ = return FFalse++ eliminateFloatsFromExpression e subtractError = + if hasFloatE e + then do+ absError <- findAbsoluteErrorUsingFPTaylor e varMap fptaylorPath+ let eWithoutFloats = removeFloats e+ if subtractError + then return $ EBinOp Sub eWithoutFloats $ Lit absError+ else return $ EBinOp Add eWithoutFloats $ Lit absError+ else+ return e++-- |Made for Float32/64 expressions+findAbsoluteErrorUsingFPTaylor :: E -> VarMap -> FilePath -> IO Rational+findAbsoluteErrorUsingFPTaylor e varMap fptaylorPath =+ do+ (exitCode, output, errDetails) <- withSystemTempFile "fptaylor" handleFPTaylorFile + case exitCode of+ ExitSuccess -> + case parseFPTaylorRational output of+ Just result -> return result+ Nothing -> error $ "Could not parse FPTaylor output" ++ show output+ ExitFailure _ -> error $ "Error when running FPTaylor on generated fptaylor.txt. Error message: " ++ show errDetails+ where+ fptaylorInput = expressionWithVarMapToFPTaylor e varMap+ -- fptaylorFile = "fptaylor.txt"+ handleFPTaylorFile filePath fileHandle = + do + hPutStr fileHandle fptaylorInput+ _ <- hGetContents fileHandle -- Ensure handler is finished writing before calling FPTaylor+ readProcessWithExitCode fptaylorPath [filePath] []
+ src/PropaFP/Eliminator.hs view
@@ -0,0 +1,243 @@+module PropaFP.Eliminator where++import MixedTypesNumPrelude+import qualified Prelude as P+import Data.List+import PropaFP.Expression++minMaxAbsEliminatorF :: F -> F+minMaxAbsEliminatorF f' = aux f'+ where+ -- hasMinMaxAbsE could be removed+ aux :: F -> F+ aux fToElim =+ case fToElim of+ FConn conn f1 f2 -> FConn conn (aux f1) (aux f2)+ FComp comp e1 e2 ->+ let+ qualifiedE1s = minMaxAbsEliminator $ ENonStrict e1+ qualifiedE2s = minMaxAbsEliminator $ ENonStrict e2++ eListToConjunction [] = error "undefined"+ eListToConjunction [ENonStrict e] = FComp Ge e (Lit 0.0)+ eListToConjunction [EStrict e] = FComp Gt e (Lit 0.0)+ eListToConjunction (e : es) = FConn And (eListToConjunction [e]) (eListToConjunction es)++ fListToConjunction [] = error "undefined"+ fListToConjunction [f] = f+ fListToConjunction (f : fs) = FConn And f (fListToConjunction fs)++ build :: ([ESafe], ESafe) -> [([ESafe], ESafe)] -> F+ build _ [] = error "Empty qualified list given in minMaxAbsEliminator"+ build e1Q@(e1C, e1G) [(e2C, e2G)] =+ let+ combinedL = e1C ++ e2C+ combinedF = eListToConjunction (nub combinedL)+ combinedG = FComp comp (extractSafeE e1G) (extractSafeE e2G)+ combinedQ = FConn Impl combinedF combinedG+ in+ if null combinedL+ then combinedG+ else combinedQ+ build e1Q@(e1C, e1G) ((e2C, e2G) : e2Qs) =+ let+ combinedL = e1C ++ e2C+ combinedF = eListToConjunction (nub combinedL)+ combinedG = FComp comp (extractSafeE e1G) (extractSafeE e2G)+ combinedQ = FConn Impl combinedF combinedG+ in+ if null combinedL+ then combinedG+ else FConn And combinedQ $ build e1Q e2Qs++ combinedQualifiedEsAsF = fListToConjunction $ map (`build` qualifiedE2s) qualifiedE1s+ in+ combinedQualifiedEsAsF++ FNot f -> FNot (aux f)+ FTrue -> FTrue+ FFalse -> FFalse++-- | Given an expression, eliminate all Min, Max, and Abs+-- occurences. This is done by:+-- +-- When we come across a Min e1 e2:+-- 1) We have two cases+-- 1a) if e2 >= e1, then choose e1+-- 1b) if e1 >= e2, then choose e2+-- 2) So, we eliminate min and add two elements to the qualified list+-- 2a) Add e2 - e1 to the list of premises, call the eliminiator on e1 and e2+-- recursively, add any new premises from the recursive call to the list of premises,+-- set the qualified value of e1 from the recursive call to be the qualified value+-- in this case+-- 2b) similar to 2a+-- +-- Max e1 e2 is similar to Min e1 e2+-- Abs is treated as Max e (-e)+-- +-- If we come across any other operator, recursively call the eliminator on any+-- expressions, add any resulting premises, and set the qualified value to be+-- the operator called on the resulting Es +minMaxAbsEliminator :: ESafe -> [([ESafe],ESafe)]+minMaxAbsEliminator (ENonStrict (EBinOp op e1 e2)) =+ case op of+ Min ->+ concat+ [+ [+ (nub ((p1 ++ p2) ++ [ENonStrict (EBinOp Sub (extractSafeE e2') (extractSafeE e1'))]), e1'), -- e2' >= e1'+ (nub ((p2 ++ p1) ++ [ENonStrict (EBinOp Sub (extractSafeE e1') (extractSafeE e2'))]), e2') -- e1' >= e2'+ ]+ |+ (p1, e1') <- branch1, (p2, e2') <- branch2+ ]+ Max ->+ concat+ [+ [+ (nub ((p1 ++ p2) ++ [ENonStrict (EBinOp Sub (extractSafeE e1') (extractSafeE e2'))]), e1'), -- e1' >= e2'+ (nub ((p2 ++ p1) ++ [ENonStrict (EBinOp Sub (extractSafeE e2') (extractSafeE e1'))]), e2') -- e2' >= e1'+ ]+ |+ (p1, e1') <- branch1, (p2, e2') <- branch2+ ]+ op' ->+ [(nub (p1 ++ p2), ENonStrict (EBinOp op' (extractSafeE e1') (extractSafeE e2'))) | (p1, e1') <- branch1, (p2, e2') <- branch2]+ where+ branch1 = minMaxAbsEliminator (ENonStrict e1)+ branch2 = minMaxAbsEliminator (ENonStrict e2)+minMaxAbsEliminator (ENonStrict (EUnOp op e)) =+ case op of+ Abs ->+ minMaxAbsEliminator (ENonStrict (EBinOp Max e (EUnOp Negate e)))+ op' ->+ [(p, ENonStrict (EUnOp op' (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator (ENonStrict (PowI e i)) =+ [(p, ENonStrict (PowI (extractSafeE e') i)) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator (ENonStrict (Float mode e)) =+ [(p, ENonStrict (Float mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator (ENonStrict (Float32 mode e)) =+ [(p, ENonStrict (Float32 mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator (ENonStrict (Float64 mode e)) =+ [(p, ENonStrict (Float64 mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator (ENonStrict (RoundToInteger mode e)) =+ [(p, ENonStrict (RoundToInteger mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator e@(ENonStrict (Lit _)) = [([],e)]+minMaxAbsEliminator e@(ENonStrict (Var _)) = [([],e)]+minMaxAbsEliminator e@(ENonStrict Pi) = [([],e)]+++minMaxAbsEliminator (EStrict (EBinOp op e1 e2)) =+ case op of+ Min ->+ concat+ [+ [ --Min/Max should always be non-strict here+ (nub ((p1 ++ p2) ++ [ENonStrict (EBinOp Sub (extractSafeE e2') (extractSafeE e1'))]), e1'), -- e2' > e1'+ (nub ((p2 ++ p1) ++ [ENonStrict (EBinOp Sub (extractSafeE e1') (extractSafeE e2'))]), e2') -- e1' > e2'+ ]+ |+ (p1, e1') <- branch1, (p2, e2') <- branch2+ ]+ Max ->+ concat+ [+ [+ (nub ((p1 ++ p2) ++ [ENonStrict (EBinOp Sub (extractSafeE e1') (extractSafeE e2'))]), e1'), -- e1' > e2'+ (nub ((p2 ++ p1) ++ [ENonStrict (EBinOp Sub (extractSafeE e2') (extractSafeE e1'))]), e2') -- e2' > e1'+ ]+ |+ (p1, e1') <- branch1, (p2, e2') <- branch2+ ]+ op' ->+ [(nub (p1 ++ p2), EStrict (EBinOp op' (extractSafeE e1') (extractSafeE e2'))) | (p1, e1') <- branch1, (p2, e2') <- branch2]+ where+ branch1 = minMaxAbsEliminator (EStrict e1)+ branch2 = minMaxAbsEliminator (EStrict e2)+minMaxAbsEliminator (EStrict (EUnOp op e)) =+ case op of+ Abs ->+ minMaxAbsEliminator (EStrict (EBinOp Max e (EUnOp Negate e)))+ op' ->+ [(p, EStrict (EUnOp op' (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (EStrict e)]+minMaxAbsEliminator (EStrict (PowI e i)) =+ [(p, EStrict (PowI (extractSafeE e') i)) | (p, e') <- minMaxAbsEliminator (EStrict e)]+minMaxAbsEliminator (EStrict (Float mode e)) =+ [(p, EStrict (Float mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (EStrict e)]+minMaxAbsEliminator (EStrict (Float32 mode e)) =+ [(p, EStrict (Float32 mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (EStrict e)]+minMaxAbsEliminator (EStrict (Float64 mode e)) =+ [(p, EStrict (Float64 mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (EStrict e)]+minMaxAbsEliminator (EStrict (RoundToInteger mode e)) =+ [(p, EStrict (RoundToInteger mode (extractSafeE e'))) | (p, e') <- minMaxAbsEliminator (ENonStrict e)]+minMaxAbsEliminator e@(EStrict (Lit _)) = [([],e)]+minMaxAbsEliminator e@(EStrict (Var _)) = [([],e)]+minMaxAbsEliminator e@(EStrict Pi) = [([],e)]+-- If we extractSafeE, then strictness does not matter++-- [[[[E]]]] where [[E]] = [e1 /\ (e2 \/ e3) /\ e4]+-- [[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]]+-- [[[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]] /\ [[[e1 /\ (e2 \/ e3) /\ e4]] \/ [e1 /\ (e2 \/ e3) /\ e4]]]+minMaxAbsEliminatorECNF :: [[ESafe]] -> [[ESafe]]+minMaxAbsEliminatorECNF ecnf = and $ map or (map (map (qualifiedEsToCNF2 . minMaxAbsEliminator)) ecnf)+ where+ and2 = (++)+ or2 ecnf1 ecnf2 = [d1 ++ d2 | d1 <- ecnf1, d2 <- ecnf2]+ and :: [[[ESafe]]] -> [[ESafe]]+ and = foldl and2 []+ or :: [[[ESafe]]] -> [[ESafe]]+ or = foldl or2 [[]]++-- | Translate the qualified Es list to a single expression+-- The qualified Es list is basically the following formula:+-- e >= 0 == (p1 >= 0 /\ p2 >= 0 /\ p3 >=0 -> q1 >= 0) /\ repeat...+-- where e is the expression passed to minMaxAbsEliminator+-- +-- This can be rewritten to+-- (-p1 >= 0 \/ - p2 >= 0 \/ -p3 >= 0 \/ q1 >= 0)+-- This is incorrect, strictness is not dealt with correctly+-- qualifiedEsToCNF :: [([E],E)] -> E+-- qualifiedEsToCNF [] = undefined+-- qualifiedEsToCNF [([], q)] = q+-- qualifiedEsToCNF [(ps, q)] = EBinOp Max (buildPs ps) q+-- where+-- buildPs :: [E] -> E+-- buildPs [] = undefined+-- buildPs [p] = (EUnOp Negate p)+-- buildPs (p : ps) = EBinOp Max (EUnOp Negate p) (buildPs ps) +-- qualifiedEsToCNF ((ps, q) : es) = EBinOp Min (qualifiedEsToCNF [(ps, q)]) (qualifiedEsToCNF es)++-- | Convert a list of qualified Es to a CNF represented as a list of lists+qualifiedEsToCNF2 :: [([ESafe],ESafe)] -> [[ESafe]]+qualifiedEsToCNF2 =+ map+ (\(ps,q) ->+ q : map negateSafeE ps+ )+ -- The negation of ps turns it into ps < 0, which is equivalent to -ps > 0++-- Disjunction of Conjunction of Disjunction ++qualifiedEsToDisjunction :: ([ESafe], ESafe) -> [ESafe]+qualifiedEsToDisjunction (context, goal) = goal : map negateSafeE context++qualifiedEsToF :: [([ESafe], ESafe)] -> F+qualifiedEsToF [] = undefined+qualifiedEsToF [qualifiedE] = qualifiedEToF qualifiedE+qualifiedEsToF (qualifiedE : qualifiedEs) = FConn And (qualifiedEToF qualifiedE) (qualifiedEsToF qualifiedEs)++qualifiedEToF :: ([ESafe], ESafe) -> F+qualifiedEToF ([], goal) = eSafeToF goal+qualifiedEToF (context, goal) = FConn Impl (aux context) $ eSafeToF goal+ where+ aux [] = undefined+ aux [c] = eSafeToF c+ aux (c : cs) = FConn And (eSafeToF c) (aux cs)+-- TODO:++-- Translate to this type+-- Vector (Differential (CN MPBall)) -> [[Differential (CN MPBall)]]+-- We'd give this type some domain++-- type EvalE = Vector (Differential (CN MPBall)) -> Differential (CN MPBall)+-- type EvalECNF = Vector (Differential (CN MPBall)) -> [[Differential (CN MPBall)]]
+ src/PropaFP/Expression.hs view
@@ -0,0 +1,1271 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LambdaCase #-}+module PropaFP.Expression where++import MixedTypesNumPrelude++import qualified Prelude as P++import qualified Data.Map as Map+import Data.List (nub, delete)++import Test.QuickCheck++import Debug.Trace (trace)+import Test.QuickCheck.State (State(randomSeed))+import Data.Ratio+import PropaFP.VarMap+import AERN2.Normalize (CanNormalize(normalize))++data BinOp = Add | Sub | Mul | Div | Min | Max | Pow | Mod+ deriving (Show, P.Eq, P.Ord)+data UnOp = Sqrt | Negate | Abs | Sin | Cos+ deriving (Show, P.Eq, P.Ord)++data RoundingMode = RNE | RTP | RTN | RTZ | RNA deriving (Show, P.Eq, P.Ord)+-- | The E type represents the inequality: expression :: E >= 0+-- TODO: Add rounding operator with certain epsilon/floating-point type+data E = EBinOp BinOp E E | EUnOp UnOp E | Lit Rational | Var String | PowI E Integer | Float32 RoundingMode E | Float64 RoundingMode E | Float RoundingMode E | Pi | RoundToInteger RoundingMode E+ deriving (Show, P.Eq, P.Ord)++data ESafe = EStrict E | ENonStrict E+ deriving (Show, P.Eq, P.Ord)+data Comp = Gt | Ge | Lt | Le | Eq+ deriving (Show, P.Eq, P.Ord)++data Conn = And | Or | Impl+ deriving (Show, P.Eq, P.Ord)++-- TODO: Could make prover work on 'Comp E E' (call it EComp)+-- Other method, add flag to E, whether or not it is strict++-- | The F type is used to specify comparisons between E types+-- and logical connectives between F types+data F = FComp Comp E E | FConn Conn F F | FNot F | FTrue | FFalse+ deriving (Show, P.Eq, P.Ord)++lengthF :: F -> Integer+lengthF (FConn _ f1 f2) = lengthF f1 + lengthF f2+lengthF (FComp _ e1 e2) = lengthE e1 + lengthE e2+lengthF (FNot f) = lengthF f+lengthF FTrue = 1+lengthF FFalse = 1++lengthE :: E -> Integer+lengthE (EBinOp _ e1 e2) = lengthE e1 + lengthE e2+lengthE (EUnOp _ e) = lengthE e+lengthE (Var _) = 1+lengthE (Lit _) = 1+lengthE (PowI e _) = lengthE e+lengthE (Float _ e) = lengthE e+lengthE (Float32 _ e) = lengthE e+lengthE (Float64 _ e) = lengthE e+lengthE Pi = 1+lengthE (RoundToInteger _ e) = lengthE e++newtype Name = Name String deriving Show++instance Arbitrary Name where+ arbitrary =+ oneof+ [+ return (Name "a"),+ return (Name "b"),+ return (Name "c"),+ return (Name "d"),+ return (Name "e"),+ return (Name "f"),+ return (Name "g"),+ return (Name "h"),+ return (Name "i"),+ return (Name "j"),+ return (Name "k"),+ return (Name "l")+ ]++instance Arbitrary UnOp where+ arbitrary =+ frequency [(int 11, return Negate), (int 1, return Abs), (int 4, return Sin), (int 4, return Cos)]++instance Arbitrary BinOp where+ arbitrary =+ frequency [(int 10, return Add), (int 10, return Sub), (int 10, return Mul), (int 10, return Div), (int 1, return Min), (int 1, return Max)]++instance Arbitrary RoundingMode where+ arbitrary =+ oneof [return RNE, return RTP, return RTN, return RTN]+instance Arbitrary E where+ arbitrary = sized eGenerator+ where+ varName :: Gen Name+ varName = arbitrary++ eGenerator :: Int -> Gen E+ eGenerator n | n>0 =+ oneof+ [+ Lit <$> fmap toRational (arbitrary :: Gen Integer),+ Var <$> show <$> varName,+ EUnOp <$> arbitrary <*> subE,+ EUnOp Sqrt . Lit <$> fmap getPositive (arbitrary :: Gen (Positive Rational)),+ EBinOp <$> arbitrary <*> subE <*> subE+ -- PowI <$> subE <*> fmap getPositive (arbitrary :: Gen (Positive Integer)) -- We do not allow Floats here+ ]+ where+ subE = eGenerator (int (floor (n / 20)))+ sqrtG x = EUnOp Sqrt (Lit x)+ eGenerator _ = oneof [Lit <$> (fmap toRational (arbitrary :: Gen Integer)), Var <$> show <$> varName]+ -- subE = eGenerator (pred n)++instance Arbitrary ESafe where+ arbitrary = randomStrictness <*> randomE+ where+ randomE :: Gen E+ randomE = arbitrary++ randomStrictness = oneof [return EStrict, return ENonStrict]++-- data Comp = Gt | Ge | Lt | Le | Eq+-- deriving (Show, P.Eq)++-- data Conn = And | Or | Impl | Equiv+-- deriving (Show, P.Eq)++-- -- | The F type is used to specify comparisons between E types+-- -- and logical connectives between F types+-- data F = FComp Comp E E | FConn Conn F F | FNot F | FTrue | FFalse+-- deriving (Show, P.Eq)++instance Arbitrary Comp where+ arbitrary = oneof [return Gt, return Ge, return Lt, return Le, return Eq]++instance Arbitrary Conn where+ arbitrary = oneof [return And, return Or, return Impl]++instance Arbitrary F where+ arbitrary = sized fGenerator+ where+ varName :: Gen Name+ varName = arbitrary++ fGenerator :: Int -> Gen F+ fGenerator 0 = oneof [FComp <$> arbitrary <*> arbitrary <*> arbitrary]+ fGenerator n =+ frequency+ [+ (int 10, FComp Eq <$> Var <$> show <$> varName <*> arbitrary),+ (int 30, FComp <$> arbitrary <*> arbitrary <*> arbitrary),+ (int 30, FConn <$> arbitrary <*> subF <*> subF),+ (int 30, FNot <$> subF)+ ]+ where+ subF = fGenerator (int (floor (n / 20)))+-- Note, does not generate FTrue, FFalse++flipStrictness :: ESafe -> ESafe+flipStrictness (EStrict e) = ENonStrict e+flipStrictness (ENonStrict e) = EStrict e++-- | Equivalent to E * -1+-- Example: ENonStrict e == e >= 0. negateSafeE (ENonStrict e) == e < 0 == -e > 0 == (EStrict (EUnOp Negate e))+negateSafeE :: ESafe -> ESafe+negateSafeE (EStrict e) = ENonStrict (EUnOp Negate e)+negateSafeE (ENonStrict e) = EStrict (EUnOp Negate e)++extractSafeE :: ESafe -> E+extractSafeE (EStrict e) = e+extractSafeE (ENonStrict e) = e++fmapESafe :: (E -> E) -> ESafe -> ESafe+fmapESafe f (EStrict e) = EStrict $ f e+fmapESafe f (ENonStrict e) = ENonStrict $ f e++fToECNF :: F -> [[ESafe]]+fToECNF = fToECNFB False+ where+ fToECNFB :: Bool -> F -> [[ESafe]]+ fToECNFB isNegated (FNot f) = fToECNFB (not isNegated) f+ fToECNFB True (FComp op e1 e2) = case op of+ Le -> fToECNFB False (FComp Gt e1 e2) -- !(f1 <= f2) -> (f1 > f2)+ Lt -> fToECNFB False (FComp Ge e1 e2)+ Ge -> fToECNFB False (FComp Lt e1 e2)+ Gt -> fToECNFB False (FComp Le e1 e2)+ Eq -> fToECNFB True (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) -- !(f1 = f2)+ fToECNFB False (FComp op e1 e2) = case op of+ Le -> fToECNFB False (FComp Ge e2 e1) -- f1 < f2 == f1 - f2 < 0 == -f1 + f2 >= 0+ Lt -> fToECNFB False (FComp Gt e2 e1) -- f1 <= f2 == f1 - f2 <= 0 == -f1 + f2 > 0+ Ge -> [[ENonStrict (EBinOp Sub e1 e2)]] -- f1 >= f2 == f1 - f2 >= 0 + Gt -> [[EStrict (EBinOp Sub e1 e2)]] -- f1 > f2 == f1 - f2 > 0 + Eq -> fToECNFB False (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) -- f1 = f2 == f1 >= f2 /\ f1 <= f2+ fToECNFB True (FConn op f1 f2) = case op of+ And -> [d1 ++ d2 | d1 <- fToECNFB True f1, d2 <- fToECNFB True f2]+ Or -> fToECNFB True f1 ++ fToECNFB True f2+ Impl -> fToECNFB False f1 ++ fToECNFB True f2 -- !(!p \/ q) == p /\ !q+ fToECNFB False (FConn op f1 f2) = case op of+ And -> fToECNFB False f1 ++ fToECNFB False f2 -- [e1 /\ e2 /\ (e3 \/ e4)] ++ [p1 /\ (p2 \/ p3) /\ p4] = [e1 /\ e2 /\ (e3 \/ e4) /\ p1 /\ (p2 \/ p3) /\ p4]+ Or -> [d1 ++ d2 | d1 <- fToECNFB False f1, d2 <- fToECNFB False f2] -- [e1 /\ e2 /\ (e3 \/ e4)] \/ [p1 /\ (p2 \/ p3) /\ p4] + Impl -> [d1 ++ d2 | d1 <- fToECNFB True f1, d2 <- fToECNFB False f2]+ -- fToECNFB isNegated FTrue _ = error "fToECNFB for FTrue undefined" $ Lit 1.0+ -- fToECNFB isNegated FFalse _ = error "fToECNFB for FFalse undefined" $ Lit $ -1.0+ fToECNFB True FTrue = fToECNFB False FFalse+ fToECNFB True FFalse = fToECNFB False FTrue+ fToECNFB False FTrue = [[ENonStrict (Lit 1.0)]]+ fToECNFB False FFalse = [[ENonStrict (Lit (-1.0))]]++fToEDNF :: F -> [[ESafe]]+fToEDNF = fToEDNFB False+ where+ fToEDNFB :: Bool -> F -> [[ESafe]]+ fToEDNFB isNegated (FNot f) = fToEDNFB (not isNegated) f+ fToEDNFB True (FComp op e1 e2) = case op of+ Le -> fToEDNFB False (FComp Gt e1 e2)+ Lt -> fToEDNFB False (FComp Ge e1 e2)+ Ge -> fToEDNFB False (FComp Lt e1 e2)+ Gt -> fToEDNFB False (FComp Le e1 e2)+ Eq -> fToEDNFB True (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) -- !(f1 = f2)+ -- Eq -> [[EStrict (EBinOp Sub e1 e2)], [EStrict (EBinOp Sub e2 e1)]]+ fToEDNFB False (FComp op e1 e2) = case op of+ Le -> fToEDNFB False (FComp Ge e2 e1)+ Lt -> fToEDNFB False (FComp Gt e2 e1)+ Ge -> [[ENonStrict (EBinOp Sub e1 e2)]]+ Gt -> [[EStrict (EBinOp Sub e1 e2)]]+ Eq -> fToEDNFB False (FConn And (FComp Ge e1 e2) (FComp Le e1 e2))+ -- Eq -> [[ENonStrict (EBinOp Sub e1 e2), ENonStrict (EBinOp Sub e2 e1)]]+ fToEDNFB True (FConn op f1 f2) = case op of+ And -> fToEDNFB True f1 ++ fToEDNFB True f2+ Or -> [d1 ++ d2 | d1 <- fToEDNFB True f1, d2 <- fToEDNFB True f2]+ Impl -> [d1 ++ d2 | d1 <- fToEDNFB False f1, d2 <- fToEDNFB True f2]+ fToEDNFB False (FConn op f1 f2) = case op of+ And -> [d1 ++ d2 | d1 <- fToEDNFB False f1, d2 <- fToEDNFB False f2]+ Or -> fToEDNFB False f1 ++ fToEDNFB False f2+ Impl -> fToEDNFB True f1 ++ fToEDNFB False f2+ fToEDNFB True FTrue = fToEDNFB False FFalse+ fToEDNFB True FFalse = fToEDNFB False FTrue+ fToEDNFB False FTrue = [[ENonStrict (Lit 1.0)]]+ fToEDNFB False FFalse = [[ENonStrict (Lit (-1.0))]]++-- Eq -> fToEDNFB True (FConn And (FComp Ge e1 e2) (FComp Le e1 e2)) -- !(f1 = f2)+-- Eq -> fToEDNFB False (FConn And (FComp Ge e1 e2) (FComp Le e1 e2))++fToFDNF :: F -> [[F]]+fToFDNF = fToFDNFB False+ where+ fToFDNFB :: Bool -> F -> [[F]]+ fToFDNFB isNegated (FNot f) = fToFDNFB (not isNegated) f+ fToFDNFB True f@FComp {} =+ case f of+ -- e1 < e2+ FComp Ge e1 e2 -> [[FComp Gt e2 e1]]+ -- e1 <= e2+ FComp Gt e1 e2 -> [[FComp Ge e2 e1]]+ -- e1 > e2+ FComp Le e1 e2 -> [[FComp Gt e1 e2]]+ -- e1 >= e2+ FComp Lt e1 e2 -> [[FComp Ge e1 e2]]+ FComp Eq e1 e2 -> fToFDNFB False $ FConn Or (FComp Gt e1 e2) (FComp Gt e2 e1)+ fToFDNFB False f@FComp {} =+ case f of+ FComp Ge _ _ -> [[f]]+ FComp Gt _ _ -> [[f]]+ FComp Le e1 e2 -> [[FComp Ge e2 e1]]+ FComp Lt e1 e2 -> [[FComp Gt e2 e1]]+ FComp Eq e1 e2 -> [[FComp Ge e1 e2, FComp Ge e2 e1]]+ -- fToFDNFB True f@FComp {} = [[FNot f]]+ -- fToFDNFB False f@FComp {} = [[f]]+ fToFDNFB True (FConn op f1 f2) = case op of+ And -> fToFDNFB True f1 ++ fToFDNFB True f2+ Or -> [d1 ++ d2 | d1 <- fToFDNFB True f1, d2 <- fToFDNFB True f2]+ Impl -> [d1 ++ d2 | d1 <- fToFDNFB False f1, d2 <- fToFDNFB True f2]+ fToFDNFB False (FConn op f1 f2) = case op of+ And -> [d1 ++ d2 | d1 <- fToFDNFB False f1, d2 <- fToFDNFB False f2]+ Or -> fToFDNFB False f1 ++ fToFDNFB False f2+ Impl -> fToFDNFB True f1 ++ fToFDNFB False f2+ fToFDNFB True FTrue = fToFDNFB False FFalse+ fToFDNFB True FFalse = fToFDNFB False FTrue+ fToFDNFB False FTrue = [[FTrue]]+ fToFDNFB False FFalse = [[FFalse]]++eSafeToF :: ESafe -> F+eSafeToF (EStrict e) = FComp Gt e (Lit 0.0)+eSafeToF (ENonStrict e) = FComp Ge e (Lit 0.0)++eSafeDisjToF :: [ESafe] -> F+eSafeDisjToF [] = error "empty disjunction given to eSafeDisjToF" -- Alternatively, this can be false?+eSafeDisjToF [e] = eSafeToF e+eSafeDisjToF (e : es) = FConn Or (eSafeToF e) (eSafeDisjToF es)++eSafeCNFToF :: [[ESafe]] -> F+eSafeCNFToF [] = error "empty disjunction given to eSafeCNFToF" -- Alternatively, this can be true?+eSafeCNFToF [disj] = eSafeDisjToF disj+eSafeCNFToF (disj : disjs) = FConn And (eSafeDisjToF disj) (eSafeCNFToF disjs)++eSafeCNFToDNF :: [[ESafe]] -> [[ESafe]]+eSafeCNFToDNF = fToEDNF . eSafeCNFToF++-- eSafeCNFToESafeDNF :: [[ESafe]] -> [[ESafe]]+-- eSafeCNFToESafeDNF [] = []+-- eSafeCNFToESafeDNF [disjunction] = map (\term -> [term]) disjunction++-- | Add bounds for any Float expressions+-- addRoundingBounds :: E -> [[E]]+-- addRoundingBounds (Float e significand) = [[exactExpression - machineEpsilon], [exactExpression + machineEpsilon]]+-- where+-- exactExpression = addRoundingBounds e+-- machineEpsilon = 2^(-23)+-- addRoundingBounds e = e++-- | Various rules to simplify expressions+simplifyE :: E -> E+simplifyE unsimplifiedE = if unsimplifiedE P.== simplifiedE then simplifiedE else simplifyE simplifiedE+ where+ simplifiedE = simplify unsimplifiedE++ simplify (EBinOp Div e (Lit 1.0)) = e+ simplify (EBinOp Div (Lit 0.0) _) = Lit 0.0+ simplify (EBinOp Mul (Lit (-1.0)) e) = simplify (EUnOp Negate e)+ simplify (EBinOp Mul e (Lit (-1.0))) = simplify (EUnOp Negate e)+ simplify (EBinOp Mul (Lit 0.0) _) = Lit 0.0+ simplify (EBinOp Mul _ (Lit 0.0)) = Lit 0.0+ simplify (EBinOp Mul (Lit 1.0) e) = e+ simplify (EBinOp Mul e (Lit 1.0)) = e+ simplify (EBinOp Add (Lit 0.0) e) = e+ simplify (EBinOp Add e (Lit 0.0)) = e+ simplify (EBinOp Sub e (Lit 0.0)) = e+ simplify (EBinOp Sub e1 e2) = if e1 P.== e2 then Lit 0.0 else EBinOp Sub (simplifyE e1) (simplifyE e2)+ simplify (EBinOp Pow _ (Lit 0.0)) = Lit 1.0+ simplify (EBinOp Pow e (Lit 1.0)) = e+ simplify (EBinOp Pow e (Lit n)) = if denominator n == 1 then PowI e (numerator n) else EBinOp Pow e (Lit n)+ simplify (PowI _e 0) = Lit 1.0+ simplify (PowI e 1) = e+ simplify (EUnOp Negate (Lit 0.0)) = Lit 0.0+ simplify (EUnOp Negate (EUnOp Negate e)) = e+ simplify (EUnOp Sqrt (Lit 0.0)) = Lit 0.0+ simplify (EUnOp Sqrt (Lit 1.0)) = Lit 1.0+ simplify (EUnOp Abs (Lit v)) = Lit (abs v)+ simplify (EBinOp Min e1 e2) = if e1 P.== e2 then e1 else EBinOp Min (simplifyE e1) (simplifyE e2)+ simplify (EBinOp Max e1 e2) = if e1 P.== e2 then e1 else EBinOp Max (simplifyE e1) (simplifyE e2)+ simplify (EBinOp op e1 e2) = EBinOp op (simplify e1) (simplify e2)+ simplify (EUnOp op e) = EUnOp op (simplify e)+ simplify e = e++simplifyF :: F -> F+-- Simplify Or+simplifyF unsimplifiedF = if unsimplifiedF P.== simplifiedF then simplifiedF else simplifyF simplifiedF+ where+ simplifiedF = simplify unsimplifiedF++ -- Collapse x < y OR x = y to x <= y (and similar)+ simplify (FConn Or f1@(FComp Lt l1 r1) f2@(FComp Eq l2 r2)) = if l1 P.== l2 P.&& r1 P.== r2 then FComp Le l1 r1 else FConn Or (simplify f1) (simplify f2)+ simplify (FConn Or f1@(FComp Eq l1 r1) f2@(FComp Lt l2 r2)) = if l1 P.== l2 P.&& r1 P.== r2 then FComp Le l1 r1 else FConn Or (simplify f1) (simplify f2)+ simplify (FConn Or f1@(FComp Gt l1 r1) f2@(FComp Eq l2 r2)) = if l1 P.== l2 P.&& r1 P.== r2 then FComp Ge l1 r1 else FConn Or (simplify f1) (simplify f2)+ simplify (FConn Or f1@(FComp Eq l1 r1) f2@(FComp Gt l2 r2)) = if l1 P.== l2 P.&& r1 P.== r2 then FComp Ge l1 r1 else FConn Or (simplify f1) (simplify f2)++ -- Eliminate implications with opposing conditions where the RHS is the same, replacing the two implications with the RHS+ simplify (FConn And f1@(FConn Impl cond1 branch1) f2@(FConn Impl (FNot cond2) branch2)) =+ if cond1 P.== cond2 && branch1 P.== branch2+ then simplify branch1+ else FConn And (simplify f1) (simplify f2)++ simplify (FConn And _ FFalse) = FFalse+ simplify (FConn And FFalse _) = FFalse+ simplify (FConn And f FTrue) = simplify f+ simplify (FConn And FTrue f) = simplify f++ -- Collapse x /\ (!x \/ y) into x /\ y+ simplify (FConn And x1 f2@(FConn Or (FNot x2) y)) = if x1 P.== x2 then simplify (FConn And x1 y) else FConn And (simplify x1) (simplify f2)+ -- Collapse (!x \/ y) /\ x into y /\ x+ simplify (FConn And f1@(FConn Or (FNot x1) y) x2) = if x1 P.== x2 then simplify (FConn And y x2) else FConn And (simplify f1) (simplify x2)+ -- Collapse x /\ (y \/ !x) into x /\ y+ simplify (FConn And x1 f2@(FConn Or y (FNot x2))) = if x1 P.== x2 then simplify (FConn And x1 y) else FConn And (simplify x1) (simplify f2)+ -- Collapse (y \/ !x) /\ x into y /\ x+ simplify (FConn And f1@(FConn Or y (FNot x1)) x2) = if x1 P.== x2 then simplify (FConn And y x2) else FConn And (simplify f1) (simplify x2)++ simplify (FConn And f1@(FConn Or v1 v2) f2@(FNot v3))+ -- Collapse (x \/ y) /\ !x into y /\ !x+ | v3 P.== v1 = simplify (FConn And v2 (FNot v3))+ -- Collapse (y \/ x) /\ !x into y /\ !x+ | v3 P.== v2 = simplify (FConn And v1 (FNot v3))+ -- Turn x /\ !x into false+ | f1 P.== v3 = FFalse+ | otherwise = FConn And (simplify f1) (simplify f2)++ simplify (FConn And f1@(FNot v1) f2@(FConn Or v2 v3))+ -- Collapse !x /\ (x \/ y) into !x /\ y+ | v1 P.== v2 = simplify (FConn And (FNot v1) v3)+ -- Collapse !x /\ (y \/ x) into !x /\ y+ | v1 P.== v3 = simplify (FConn And (FNot v1) v2)+ -- Turn !x /\ x into false+ | v1 P.== f2 = FFalse+ | otherwise = FConn And (simplify f1) (simplify f2)++ -- Collapse x /\ (x -> y) into x /\ y+ simplify (FConn And x1 f2@(FConn Impl x2 y)) = if x1 P.== x2 then simplify (FConn And x1 y) else FConn And (simplify x1) (simplify f2)+ -- Collapse (x -> y) /\ x into y /\ x+ simplify (FConn And f1@(FConn Impl x1 y) x2) = if x1 P.== x2 then simplify (FConn And y x2) else FConn And (simplify f1) (simplify x2)++ -- Boolean Rules+ -- And+ -- And contradictions and eliminations+ simplify (FConn And f1 fn2@(FNot f2)) = if f1 P.== f2 then FFalse else FConn And (simplify f1) (simplify fn2)+ simplify (FConn And fn1@(FNot f1) f2) = if f1 P.== f2 then FFalse else FConn And (simplify fn1) (simplify f2)+ -- And collapse to Eq+ simplify (FConn And f1@(FComp Ge l1 r1) f2@(FComp Ge l2 r2)) = if l1 P.== r2 && l2 P.== r1 then simplify (FComp Eq l1 r1) else FConn And (simplify f1) (simplify f2)+ -- simplify (FConn And f1@(FComp Ge e1 (Var v1)) f2@(FComp Ge (Var v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify f2)+ simplify (FConn And f1@(FComp Le l1 r1) f2@(FComp Le l2 r2)) = if l1 P.== r2 && l2 P.== r1 then simplify (FComp Eq l1 r1) else FConn And (simplify f1) (simplify f2)+ -- simplify (FConn And f1@(FComp Le e1 (Var v1)) f2@(FComp Le (Var v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify f2)+ simplify (FConn And f1@(FComp Ge l1 r1) f2@(FComp Le l2 r2)) = if l1 P.== l2 && r1 P.== r2 then simplify (FComp Eq l1 r1) else FConn And (simplify f1) (simplify f2)+ -- simplify (FConn And f1@(FComp Ge e1 (Var v1)) f2@(FComp Le e2 (Var v2))) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify f2)+ simplify (FConn And f1@(FComp Le l1 r1) f2@(FComp Ge l2 r2)) = if l1 P.== l2 && r1 P.== r2 then simplify (FComp Eq l1 r1) else FConn And (simplify f1) (simplify f2)+ -- simplify (FConn And f1@(FComp Le (v1) e1) f2@(FComp Ge (v2) e2)) = if e1 P.== e2 && v1 == v2 then simplify (FComp Eq (Var v1) e1) else FConn And (simplify f1) (simplify f2)+ simplify (FConn And f1 f2) = if f1 P.== f2 then simplify f1 else FConn And (simplify f1) (simplify f2)+ -- Or+ simplify (FConn Or _ FTrue) = FTrue+ simplify (FConn Or FTrue _) = FTrue+ simplify (FConn Or f FFalse) = simplify f+ simplify (FConn Or FFalse f) = simplify f++ simplify (FConn Or f1 fn2@(FNot f2)) = if f1 P.== f2 then FTrue else FConn Or (simplify f1) (simplify fn2)+ simplify (FConn Or fn1@(FNot f1) f2) = if f1 P.== f2 then FTrue else FConn Or (simplify fn1) (simplify f2)++ simplify (FConn Or f1 f2) = if f1 P.== f2 then simplify f1 else FConn Or (simplify f1) (simplify f2)+ -- Impl+ simplify (FConn Impl FFalse _) = FTrue+ simplify (FConn Impl _ FTrue) = FTrue+ simplify (FConn Impl f FFalse) = simplify (FNot f)+ simplify (FConn Impl FTrue f) = simplify f+ -- Impl tautologies and eliminations+ simplify (FConn Impl f1 fn2@(FNot f2)) = if f1 P.== f2 then simplify (FNot f1) else FConn Impl (simplify f1) (simplify fn2)+ simplify (FConn Impl fn1@(FNot f1) f2) = if f1 P.== f2 then simplify f1 else FConn Impl (simplify fn1) (simplify f2)+ simplify (FConn Impl f1 f2) = if f1 P.== f2 then FTrue else FConn Impl (simplify f1) (simplify f2)++ -- Evaluate rational comparisons+ simplify (FComp op (Lit l1) (Lit l2)) =+ case op of+ Gt -> boolToF $ l1 > l2+ Ge -> boolToF $ l1 >= l2+ Lt -> boolToF $ l1 < l2+ Le -> boolToF $ l1 <= l2+ Eq -> boolToF $ l1 == l2+ where+ boolToF True = FTrue+ boolToF False = FFalse+++ -- Comp tautologies and eliminations+ -- Eliminate double not+ simplify (FNot (FNot f)) = simplify f+ simplify (FComp Eq e1 e2) = if e1 P.== e2 || simplifyE e1 P.== simplifyE e2 then FTrue else FComp Eq (simplifyE e1) (simplifyE e2)+ simplify (FComp op e1 e2) = FComp op (simplifyE e1) (simplifyE e2)+ simplify FTrue = FTrue+ simplify FFalse = FFalse+ simplify (FNot FTrue) = FFalse+ simplify (FNot FFalse) = FTrue+ simplify (FNot f) = FNot (simplify f)+ -- simplifyF FTrue = error "FTrue was not eliminated"+ -- simplifyF FFalse = error "FFalse was not eliminated"++simplifyEDoubleList :: [[E]] -> [[E]]+simplifyEDoubleList = nub . map (nub . map simplifyE)++-- simplify all fs+-- look through, symbolic+-- f fnot, fnot f, etc.+-- nothing else, too complicated+++simplifyFDNF :: [[F]] -> [[F]]+simplifyFDNF [] = []+simplifyFDNF (c : cs) =+ case simplifyFConjunction c of+ Nothing -> simplifyFDNF cs+ Just [] -> simplifyFDNF cs+ Just [checkedConjunctionHead] -> [checkedConjunctionHead] : simplifyFDNF cs+ Just checkedConjunction@(checkedConjunctionHead : checkedConjunctionTail) ->+ let+ currentEqualities = findEqualities checkedConjunctionHead checkedConjunctionTail checkedConjunctionTail+ in+ case currentEqualities of+ [] -> checkedConjunction : simplifyFDNF cs+ [_eq1] -> checkedConjunction : simplifyFDNF cs+ (currentEqualitiesHead : currentEqualitiesTail) ->+ let+ newEqualities = findEqZero currentEqualitiesHead currentEqualitiesTail currentEqualitiesTail+ in+ nub (checkedConjunction ++ newEqualities) : simplifyFDNF cs+ where++ -- look for equalities like x == y and x == -y+ -- x == 0, y == 0+ findEqZero :: (E,E) -> [(E,E)] -> [(E,E)] -> [F]+ findEqZero _ [] [] = []+ findEqZero _ [] (eq : conj) = findEqZero eq conj conj+ findEqZero eq1 (eq2 : eqs) conj =+ case eq1 of+ (EUnOp Negate l1, EUnOp Negate r1) ->+ case eq2 of+ (EUnOp Negate l2, r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (l2, EUnOp Negate r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ _ -> findEqZero eq1 eqs conj+ (EUnOp Negate l1, r1) ->+ case eq2 of+ (EUnOp Negate l2, EUnOp Negate r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (l2, r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (l1, EUnOp Negate r1) ->+ case eq2 of+ (EUnOp Negate l2, EUnOp Negate r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (l2, r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (l1, r1) ->+ case eq2 of+ (l2, EUnOp Negate r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ (EUnOp Negate l2, r2)+ | l1 P.== l2 && r1 P.== r2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | l1 P.== r2 && r1 P.== l2 -> [FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge r1 (Lit 0.0), FComp Ge (Lit 0.0) r1] ++ findEqZero eq1 eqs conj+ | otherwise -> findEqZero eq1 eqs conj+ _ -> findEqZero eq1 eqs conj+++ -- finds equalities in a conjunction (x >= y and y >= x)+ findEqualities :: F -> [F] -> [F] -> [(E, E)]+ findEqualities _ [] [] = []+ findEqualities _ [] (f : conj) = findEqualities f conj conj+ findEqualities f1 (f2 : fs) conj =+ case f1 of+ -- say we have x >=y+ FComp Ge l1 r1 ->+ case f2 of+ -- y >= x is an equality+ FComp Ge l2 r2 ->+ if l1 P.== r2 && r1 P.== l2+ then (l1, r1) : findEqualities f1 fs conj+ else findEqualities f1 fs conj+ _ -> findEqualities f1 fs conj+ _ -> findEqualities f1 fs conj+++ simplifyFConjunction :: [F] -> Maybe [F]+ simplifyFConjunction [] = Just []+ simplifyFConjunction (simplifiedConjunctionHead : simplifiedConjunctionTail) =+ let+ -- Returns Nothing if a conjunction contains a contradiction+ removeContradictions :: F -> [F] -> [F] -> Maybe [F]+ removeContradictions f1 [] [] = Just [f1]+ removeContradictions f1 [] (f : conj) = (f1 :) <$> removeContradictions f conj conj+ removeContradictions f1 (f2 : fs) conj =+ -- Can be Ge or Gt+ case f1 of+ -- say this is x >= y+ FComp Ge l1 r1 ->+ case f2 of+ -- possible contradictions+ -- y > x+ FComp Gt l2 r2 ->+ if l1 P.== r2 && r1 P.== l2 then Nothing else removeContradictions f1 fs conj+ -- possible = 0+ -- y >= x (then x and y = 0)+ -- FComp Ge l2 r2 ->+ -- if l1 P.== r2 && r1 P.== l2 + -- then ([FComp Ge l1 (Lit 0.0), FComp Ge (Lit 0.0) l1, FComp Ge l2 (Lit 0.0), FComp Ge (Lit 0.0) l2] ++) <$> aux f1 fs conj+ -- else aux f1 fs conj+ _ -> removeContradictions f1 fs conj+ -- say this is x > y+ FComp Gt l1 r1 ->+ case f2 of+ -- possible contradictions+ -- y > x+ -- y >= x+ FComp Ge l2 r2 ->+ if l1 P.== r2 && r1 P.== l2 then Nothing else removeContradictions f1 fs conj+ FComp Gt l2 r2 ->+ if l1 P.== r2 && r1 P.== l2 then Nothing else removeContradictions f1 fs conj+ _ -> removeContradictions f1 fs conj+ _ -> removeContradictions f1 fs conj+ in+ nub <$> removeContradictions simplifiedConjunctionHead simplifiedConjunctionTail simplifiedConjunctionTail++fDNFToFDNFWithoutEq :: [[F]] -> [[F]] -> [[F]]+fDNFToFDNFWithoutEq [] dnf = dnf+fDNFToFDNFWithoutEq (c : cs) dnf =+ case mNewDNF of -- Same length means no FNot (FComp Eq _ _)+ Just newDNF -> fDNFToFDNFWithoutEq newDNF []+ Nothing -> fDNFToFDNFWithoutEq cs (cWithoutEq : dnf)+ where+ cWithoutEq = elimEq False c+ mNewDNF = elimNotEq cWithoutEq++ elimNotEq [] = Nothing+ elimNotEq (f@(FNot (FComp Eq e1 e2)) : _) = Just newDNF+ where+ currentDNF = c : cs ++ dnf+ currentDNFWithoutF = map (delete f) currentDNF+ newF1 = FNot (FComp Ge e1 e2)+ newF2 = FNot (FComp Ge e2 e1)++ newDNF = map (newF1 :) currentDNFWithoutF ++ map (newF2 :) currentDNFWithoutF+ -- cWithoutEqWithoutF = delete f cWithoutEq+ -- currentDNFWithoutC = cs ++ dnf+ -- newC1 = FNot (FComp Ge e1 e2) : cWithoutEqWithoutF+ -- newC2 = FNot (FComp Ge e2 e1) : cWithoutEqWithoutF+ -- newDNF = (newC1 : currentDNFWithoutC) ++ (newC2 : currentDNFWithoutC)+ elimNotEq (_ : fs) = elimNotEq fs++ elimEq _ [] = []+ elimEq isNegated (FNot f : fs) = elimEq (not isNegated) (f : fs)+ elimEq False (FComp Eq e1 e2 : fs) = FComp Ge e1 e2 : FComp Ge e2 e1 : elimEq False fs+ elimEq True (f : fs) = FNot f : elimEq False fs+ elimEq False (f : fs) = f : elimEq False fs++fDNFToEDNF :: [[F]] -> [[ESafe]]+fDNFToEDNF = map fConjToE+-- fDNFToEDNF = map (fConjToE False)+ where+ fConjToE :: [F] -> [ESafe]+ fConjToE [] = []+ fConjToE (FComp Ge e1 e2 : fs) = ENonStrict (EBinOp Sub e1 e2) : fConjToE fs+ fConjToE (FComp Gt e1 e2 : fs) = EStrict (EBinOp Sub e1 e2) : fConjToE fs+ fConjToE (FComp {} : _) = error "Non-normalized FComp found in DNF"+ fConjToE (FConn {} : _) = error "Non-atomic F found in DNF"+ fConjToE (FNot f : fs) = error "Negated f found in DNF"+ fConjToE (FTrue : fs) = ENonStrict (Lit 1.0) : fConjToE fs+ fConjToE (FFalse : fs) = ENonStrict (Lit (-1.0)) : fConjToE fs++ -- fConjToE :: Bool -> [F] -> [ESafe]+ -- fConjToE _ [] = []+ -- fConjToE True (FComp Eq e1 e2 : fs) = error "Negated FComp with Eq found in DNF" + -- fConjToE False (FComp Eq e1 e2 : fs) = fConjToE False $ [FComp Ge e1 e2, FComp Ge e2 e1] ++ fs+ -- fConjToE False (FComp Ge e1 e2 : fs) = ENonStrict (EBinOp Sub e1 e2) : fConjToE False fs+ -- fConjToE False (FComp Gt e1 e2 : fs) = EStrict (EBinOp Sub e1 e2) : fConjToE False fs+ -- fConjToE False (FComp Le e1 e2 : fs) = fConjToE False $ FComp Ge e2 e1 : fs+ -- fConjToE False (FComp Lt e1 e2 : fs) = fConjToE False $ FComp Gt e2 e1 : fs+ -- fConjToE True (FComp Ge e1 e2 : fs) = fConjToE False $ FComp Lt e1 e2 : fs+ -- fConjToE True (FComp Gt e1 e2 : fs) = fConjToE False $ FComp Le e1 e2 : fs+ -- fConjToE True (FComp Le e1 e2 : fs) = fConjToE False $ FComp Gt e1 e2 : fs+ -- fConjToE True (FComp Lt e1 e2 : fs) = fConjToE False $ FComp Ge e1 e2 : fs+ -- fConjToE _ (FConn {} : _) = error "non-atomic f found in DNF"+ -- fConjToE isNegated (FNot f : fs) = fConjToE (not isNegated) (f : fs)+ -- fConjToE False (FTrue : fs) = ENonStrict (Lit 1.0) : fConjToE False fs+ -- fConjToE False (FFalse : fs) = ENonStrict (Lit (-1.0)) : fConjToE False fs+ -- fConjToE True (FTrue : fs) = ENonStrict (Lit (-1.0)) : fConjToE False fs+ -- fConjToE True (FFalse : fs) = ENonStrict (Lit 1.0) : fConjToE False fs++ compFToE :: Bool -> F -> ESafe+ compFToE _ (FComp Eq _ _) = error "FComp with Eq found in DNF"+ compFToE False (FComp Ge e1 e2) = ENonStrict $ EBinOp Sub e1 e2+ compFToE False (FComp Gt e1 e2) = EStrict $ EBinOp Sub e1 e2+ compFToE False (FComp Le e1 e2) = compFToE False (FComp Ge e2 e1)+ compFToE False (FComp Lt e1 e2) = compFToE False (FComp Gt e2 e1)+ compFToE True (FComp Ge e1 e2) = compFToE False (FComp Lt e2 e1)+ compFToE True (FComp Gt e1 e2) = compFToE False (FComp Le e2 e1)+ compFToE True (FComp Le e1 e2) = compFToE False (FComp Gt e2 e1)+ compFToE True (FComp Lt e1 e2) = compFToE False (FComp Ge e2 e1)+ compFToE _ FConn {} = error "non-atomic f found in DNF"+ compFToE isNegated (FNot f) = compFToE (not isNegated) f+ compFToE False FTrue = ENonStrict $ Lit 1.0+ compFToE False FFalse = ENonStrict $ Lit $ -1.0+ compFToE True FTrue = ENonStrict $ Lit $ -1.0+ compFToE True FFalse = ENonStrict $ Lit 1.0+++simplifyFDoubleList :: [[F]] -> [[F]]+simplifyFDoubleList = nub . map (nub . map simplifyF)++simplifyESafeDoubleList :: [[ESafe]] -> [[ESafe]]+simplifyESafeDoubleList = nub . map (nub . map (fmapESafe simplifyE))++-- | compute the value of E with Vars at specified points+computeE :: E -> [(String, Rational)] -> CN Double+computeE (EBinOp op e1 e2) varMap =+ case op of+ Min -> computeE e1 varMap `min` computeE e2 varMap+ Max -> computeE e1 varMap `max` computeE e2 varMap+ Add -> computeE e1 varMap + computeE e2 varMap+ Sub -> computeE e1 varMap - computeE e2 varMap+ Mul -> computeE e1 varMap * computeE e2 varMap+ Div -> computeE e1 varMap / computeE e2 varMap+ Pow -> computeE e1 varMap ^ computeE e2 varMap+computeE (EUnOp op e) varMap =+ case op of+ Abs -> abs (computeE e varMap)+ Sqrt -> sqrt (computeE e varMap)+ Negate -> negate (computeE e varMap)+ Sin -> sin (computeE e varMap)+ Cos -> cos (computeE e varMap)+computeE (Var v) varMap =+ case Map.lookup v (Map.fromList varMap) of+ Nothing -> error ("map does not contain variable " ++ show v)+ Just r -> cn (double r)+computeE (Lit i) _ = cn (double i)+computeE (PowI e i) varMap = computeE e varMap ^ i+computeE (Float _ _) _ = error "computeE for Floats not supported"+computeE (Float32 _ _) _ = error "computeE for Floats not supported"+computeE (Float64 _ _) _ = error "computeE for Floats not supported"++-- | Given a list of qualified Es and points for all Vars,+-- compute a list of valid values. +-- +-- A value is the computed result of the second element of +-- the tuple and is valid if all the expressions in the list +-- at the first element of the tuple compute to be above 0.+computeQualifiedEs :: [([E], E)] -> [(String, Rational)] -> [CN Double]+computeQualifiedEs [] _ = []+computeQualifiedEs ((ps, q) : es) varMap =+ if all (\p -> computeE p varMap !>=! 0) ps+ then computeE q varMap : computeQualifiedEs es varMap+ else computeQualifiedEs es varMap++computeEDisjunction :: [E] -> [(String, Rational)] -> [CN Double]+computeEDisjunction es varMap = map (`computeE` varMap) es++computeECNF :: [[E]] -> [(String, Rational)] -> [[CN Double]]+computeECNF cnf varMap = map (`computeEDisjunction` varMap) cnf++prettyShowESafeCNF :: [[ESafe]] -> String+prettyShowESafeCNF cnf = "AND" ++ concatMap (\d -> "\n\t" ++ prettyShowDisjunction d) cnf+ where+ -- |Show a disjunction of expressions > 0 in a human-readable format+ -- This is shown as an OR with each term tabbed in+ -- If there is only one term, the expression is shown without an OR + prettyShowDisjunction :: [ESafe] -> String+ prettyShowDisjunction [] = []+ prettyShowDisjunction [e'] =+ case e' of+ EStrict e -> prettyShowE e ++ " > 0"+ ENonStrict e -> prettyShowE e ++ " >= 0"+ prettyShowDisjunction es =+ "OR" +++ concatMap+ (\case+ EStrict e -> "\n\t\t" ++ prettyShowE e ++ " > 0"+ ENonStrict e -> "\n\t\t" ++ prettyShowE e ++ " >= 0")+ es++prettyShowESafeDNF :: [[ESafe]] -> String+prettyShowESafeDNF cnf = "OR" ++ concatMap (\d -> "\n\t" ++ prettyShowDisjunction d) cnf+ where+ -- |Show a disjunction of expressions > 0 in a human-readable format+ -- This is shown as an OR with each term tabbed in+ -- If there is only one term, the expression is shown without an OR + prettyShowDisjunction :: [ESafe] -> String+ prettyShowDisjunction [] = []+ prettyShowDisjunction [e'] =+ case e' of+ EStrict e -> prettyShowE e ++ " > 0"+ ENonStrict e -> prettyShowE e ++ " >= 0"+ prettyShowDisjunction es =+ "AND" +++ concatMap+ (\case+ EStrict e -> "\n\t\t" ++ prettyShowE e ++ " > 0"+ ENonStrict e -> "\n\t\t" ++ prettyShowE e ++ " >= 0")+ es++prettyShowFSafeDNF :: [[F]] -> String+prettyShowFSafeDNF dnf = "OR" ++ concatMap (\c -> "\n\t" ++ prettyShowConjunction c) dnf+ where+ -- |Show a disjunction of expressions > 0 in a human-readable format+ -- This is shown as an OR with each term tabbed in+ -- If there is only one term, the expression is shown without an OR + prettyShowConjunction :: [F] -> String+ prettyShowConjunction [] = []+ prettyShowConjunction [f] = prettyShowF f 2+ prettyShowConjunction fs =+ "AND" +++ concatMap+ (\f -> "\n\t\t" ++ prettyShowF f 3)+ fs++-- prettyShowF :: F -> Integer -> String+-- prettyShowF (FComp op e1 e2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowE e1 ++ " " ++ prettyShowComp op ++ " " ++ prettyShowE e2+-- prettyShowF (FConn op f1 f2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowConn op ++ prettyShowF f1 (numTabs + 1) ++ prettyShowF f2 (numTabs + 1)+-- prettyShowF (FNot f) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "NOT" ++ prettyShowF f (numTabs + 1)+-- prettyShowF FTrue numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "True"+-- prettyShowF FFalse numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "False"++-- pretty show a Why3 VC which is typically a bunch of conjunctions+prettyShowVC :: F -> TypedVarMap -> String+prettyShowVC vc vm =+ "Bounds on variables: \n" +++ prettyShowRanges vm ++ "\n" +++ "exact NVC: \n" +++ prettyShowConjunction (conjunctionToList vc)+ where+ prettyShowRanges :: TypedVarMap -> String+ prettyShowRanges [] = ""+ prettyShowRanges ((TypedVar (vName, (vLower, vUpper)) vType) : vm) =+ vName ++ " (" ++ show vType ++ ")" ++ " in [" ++ showRational vLower ++ ", " ++ showRational vUpper ++ "]" ++ "\n" ++ prettyShowRanges vm++ showRational r =+ let+ numer = numerator r+ denom = denominator r+ in+ if denom == 1+ then show numer+ else show numer ++ " / " ++ show denom++ conjunctionToList :: F -> [F]+ conjunctionToList (FConn And f1 f2) = conjunctionToList f1 ++ conjunctionToList f2+ conjunctionToList f = [f]++ prettyShowConjunction :: [F] -> String+ prettyShowConjunction [] = []+ prettyShowConjunction [f] = prettyShowF f 2+ prettyShowConjunction fs =+ concatMap+ (\f -> prettyShowAssert f 0 ++ "\n\n")+ fs++ prettyShowAssert :: F -> Integer -> String+ prettyShowAssert (FComp op e1 e2) indentTracker = concat (replicate indentTracker " ") ++ prettyShowE e1 ++ " " ++ prettyShowComp op ++ " " ++ prettyShowE e2+ prettyShowAssert (FConn Impl f1 f2) indentTracker = concat (replicate indentTracker " ") ++ prettyShowConn Impl ++ "\n" ++ prettyShowAssert f1 (indentTracker + 1) ++ "\n" ++ concat (replicate (indentTracker + 1) " ") ++ "===========>\n" ++ prettyShowAssert f2 (indentTracker + 1)+ prettyShowAssert (FConn op f1 f2) indentTracker = concat (replicate indentTracker " ") ++ prettyShowConn op ++ "\n" ++ prettyShowAssert f1 (indentTracker + 1) ++ "\n" ++ prettyShowAssert f2 (indentTracker + 1)+ prettyShowAssert (FNot f) indentTracker = concat (replicate indentTracker " ") ++ "NOT" ++ "\n" ++ prettyShowAssert f (indentTracker + 1)+ prettyShowAssert FTrue indentTracker = concat (replicate indentTracker " ") ++ "True"+ prettyShowAssert FFalse indentTracker = concat (replicate indentTracker " ") ++ "False"++-- latexShowESafeCNF :: [[ESafe]] -> String+-- latexShowESafeCNF cnf = "AND" ++ concatMap (\d -> "\n\t" ++ prettyShowDisjunction d) cnf+-- where+-- -- |Show a disjunction of expressions > 0 in a human-readable format+-- -- This is shown as an OR with each term tabbed in+-- -- If there is only one term, the expression is shown without an OR +-- prettyShowDisjunction :: [ESafe] -> String+-- prettyShowDisjunction [] = []+-- prettyShowDisjunction [e'] = +-- case e' of+-- EStrict e -> prettyShowE e ++ " > 0"+-- ENonStrict e -> prettyShowE e ++ " >= 0"+-- prettyShowDisjunction es =+-- "OR" ++ +-- concatMap +-- (\case+-- EStrict e -> "\n\t\t" ++ prettyShowE e ++ " > 0" +-- ENonStrict e -> "\n\t\t" ++ prettyShowE e ++ " >= 0")+-- es++latexShowE :: E -> String+latexShowE (EBinOp op e1 e2) =+ case op of+ Add -> "$(" ++ latexShowE e1 ++ " + " ++ latexShowE e2 ++ ")$"+ Sub -> "$(" ++ latexShowE e1 ++ " - " ++ latexShowE e2 ++ ")$"+ Div -> "$(" ++ latexShowE e1 ++ " \\div " ++ latexShowE e2 ++ ")$"+ Mul -> "$(" ++ latexShowE e1 ++ " \\times " ++ latexShowE e2 ++ ")$"+ Pow -> "$(" ++ latexShowE e1 ++ "_{" ++ latexShowE e2 ++ ")}$"+ Min -> "$(min " ++ latexShowE e1 ++ " " ++ latexShowE e2 ++ ")$"+ Max -> "$(max " ++ latexShowE e1 ++ " " ++ latexShowE e2 ++ ")$"+ Mod -> "$(mod " ++ latexShowE e1 ++ " " ++ latexShowE e2 ++ ")$"+latexShowE (EUnOp op e) =+ case op of+ Abs -> "$|" ++ latexShowE e ++ "|$"+ Sqrt -> "$\\sqrt{" ++ latexShowE e ++ ")}"+ Negate -> "$(-1 \\times " ++ latexShowE e ++ ")$"+ Sin -> "$(sin " ++ latexShowE e ++ ")$"+ Cos -> "$(cos " ++ latexShowE e ++ ")$"+latexShowE (PowI e i) = "(" ++ latexShowE e ++ " ^ " ++ show i ++ ")"+latexShowE (Var v) = v+latexShowE (Lit v) = show (double v)+latexShowE (Float32 m e) =+ case m of+ RNE -> "(rnd32_ne " ++ latexShowE e ++ ")"+ RTP -> "(rnd32_tp " ++ latexShowE e ++ ")"+ RTN -> "(rnd32_tn " ++ latexShowE e ++ ")"+ RTZ -> "(rnd32_tz " ++ latexShowE e ++ ")"+ RNA -> "(rnd32_na " ++ latexShowE e ++ ")"+latexShowE (Float64 m e) =+ case m of+ RNE -> "(rnd64_ne " ++ latexShowE e ++ ")"+ RTP -> "(rnd64_tp " ++ latexShowE e ++ ")"+ RTN -> "(rnd64_tn " ++ latexShowE e ++ ")"+ RTZ -> "(rnd64_tz " ++ latexShowE e ++ ")"+ RNA -> "(rnd64_na " ++ latexShowE e ++ ")"+latexShowE (Float m e) =+ case m of+ RNE -> "(rnd_ne " ++ latexShowE e ++ ")"+ RTP -> "(rnd_tp " ++ latexShowE e ++ ")"+ RTN -> "(rnd_tn " ++ latexShowE e ++ ")"+ RTZ -> "(rnd_tz " ++ latexShowE e ++ ")"+ RNA -> "(rnd_na " ++ latexShowE e ++ ")"+latexShowE Pi = "$\\pi$"+latexShowE (RoundToInteger m e) =+ case m of+ RNE -> "(rndToInt_ne " ++ latexShowE e ++ ")"+ RTP -> "(rndToInt_tp " ++ latexShowE e ++ ")"+ RTN -> "(rndToInt_tn " ++ latexShowE e ++ ")"+ RTZ -> "(rndToInt_tz " ++ latexShowE e ++ ")"+ RNA -> "(rndToInt_ta " ++ latexShowE e ++ ")"++latexShowF :: F -> Integer -> String+latexShowF (FComp op e1 e2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ latexShowE e1 ++ " " ++ latexShowComp op ++ " " ++ latexShowE e2+latexShowF (FConn op f1 f2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ latexShowF f1 numTabs ++ " " ++ latexShowConn op ++ latexShowF f2 (numTabs + 1)+latexShowF (FNot f) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "$\\lnot$" ++ latexShowF f (numTabs + 1)+latexShowF FTrue numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "$\\top$"+latexShowF FFalse numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "$\\bot$"++latexShowComp :: Comp -> String+latexShowComp Gt = "$>$"+latexShowComp Ge = "$\\ge$"+latexShowComp Lt = "$<$"+latexShowComp Le = "$\\le$"+latexShowComp Eq = "$=$"++latexShowConn :: Conn -> String+latexShowConn And = "$\\wedge$"+latexShowConn Or = "$\\vee$"+latexShowConn Impl = "$\\implies$"++-- |Show an expression in a human-readable format+-- Rationals are converted into doubles+prettyShowE :: E -> String+prettyShowE (EBinOp op e1 e2) =+ case op of+ Add -> "(" ++ prettyShowE e1 ++ " + " ++ prettyShowE e2 ++ ")"+ Sub -> "(" ++ prettyShowE e1 ++ " - " ++ prettyShowE e2 ++ ")"+ Div -> "(" ++ prettyShowE e1 ++ " / " ++ prettyShowE e2 ++ ")"+ Mul -> "(" ++ prettyShowE e1 ++ " * " ++ prettyShowE e2 ++ ")"+ Pow -> "(" ++ prettyShowE e1 ++ " ^ " ++ prettyShowE e2 ++ ")"+ Min -> "(min " ++ prettyShowE e1 ++ " " ++ prettyShowE e2 ++ ")"+ Max -> "(max " ++ prettyShowE e1 ++ " " ++ prettyShowE e2 ++ ")"+ Mod -> "(mod " ++ prettyShowE e1 ++ " " ++ prettyShowE e2 ++ ")"+prettyShowE (EUnOp op e) =+ case op of+ Abs -> "|" ++ prettyShowE e ++ "|"+ Sqrt -> "(sqrt " ++ prettyShowE e ++ ")"+ Negate -> "(-1 * " ++ prettyShowE e ++ ")"+ Sin -> "(sin " ++ prettyShowE e ++ ")"+ Cos -> "(cos " ++ prettyShowE e ++ ")"+prettyShowE (PowI e i) = "(" ++ prettyShowE e ++ " ^ " ++ show i ++ ")"+prettyShowE (Var v) = v+prettyShowE (Lit v) =+ if denom == 1+ then show numer+ else show numer ++ " / " ++ show denom+ where+ numer = numerator v+ denom = denominator v+prettyShowE (Float32 m e) =+ case m of+ RNE -> "(rnd32_ne " ++ prettyShowE e ++ ")"+ RTP -> "(rnd32_tp " ++ prettyShowE e ++ ")"+ RTN -> "(rnd32_tn " ++ prettyShowE e ++ ")"+ RTZ -> "(rnd32_tz " ++ prettyShowE e ++ ")"+ RNA -> "(rnd32_na " ++ prettyShowE e ++ ")"+prettyShowE (Float64 m e) =+ case m of+ RNE -> "(rnd64_ne " ++ prettyShowE e ++ ")"+ RTP -> "(rnd64_tp " ++ prettyShowE e ++ ")"+ RTN -> "(rnd64_tn " ++ prettyShowE e ++ ")"+ RTZ -> "(rnd64_tz " ++ prettyShowE e ++ ")"+ RNA -> "(rnd64_na " ++ prettyShowE e ++ ")"+prettyShowE (Float m e) =+ case m of+ RNE -> "(rnd_ne " ++ prettyShowE e ++ ")"+ RTP -> "(rnd_tp " ++ prettyShowE e ++ ")"+ RTN -> "(rnd_tn " ++ prettyShowE e ++ ")"+ RTZ -> "(rnd_tz " ++ prettyShowE e ++ ")"+ RNA -> "(rnd_na " ++ prettyShowE e ++ ")"+prettyShowE Pi = "Pi"+prettyShowE (RoundToInteger m e) =+ case m of+ RNE -> "(rndToInt_ne " ++ prettyShowE e ++ ")"+ RTP -> "(rndToInt_tp " ++ prettyShowE e ++ ")"+ RTN -> "(rndToInt_tn " ++ prettyShowE e ++ ")"+ RTZ -> "(rndToInt_tz " ++ prettyShowE e ++ ")"+ RNA -> "(rndToInt_ta " ++ prettyShowE e ++ ")"++-- |Show a conjunction of expressions in a human-readable format+-- This is shown as an AND with each disjunction tabbed in with an OR+-- If there is only one term in a disjunction, the expression is shown without an OR +prettyShowECNF :: [[E]] -> String+prettyShowECNF cnf =+ "AND" ++ concatMap (\d -> "\n\t" ++ prettyShowDisjunction d) cnf+ where+ -- |Show a disjunction of expressions > 0 in a human-readable format+ -- This is shown as an OR with each term tabbed in+ -- If there is only one term, the expression is shown without an OR + prettyShowDisjunction :: [E] -> String+ prettyShowDisjunction [] = []+ prettyShowDisjunction [e] = prettyShowE e+ prettyShowDisjunction es =+ "OR" ++ concatMap (\e -> "\n\t\t" ++ prettyShowE e ++ " > 0") es++prettyShowF :: F -> Integer -> String+prettyShowF (FComp op e1 e2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowE e1 ++ " " ++ prettyShowComp op ++ " " ++ prettyShowE e2+prettyShowF (FConn op f1 f2) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ prettyShowConn op ++ prettyShowF f1 (numTabs + 1) ++ prettyShowF f2 (numTabs + 1)+prettyShowF (FNot f) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "NOT" ++ prettyShowF f (numTabs + 1)+prettyShowF FTrue numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "True"+prettyShowF FFalse numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "False"++prettyShowComp :: Comp -> String+prettyShowComp Gt = ">"+prettyShowComp Ge = ">="+prettyShowComp Lt = "<"+prettyShowComp Le = "<="+prettyShowComp Eq = "=="++prettyShowConn :: Conn -> String+prettyShowConn And = "AND"+prettyShowConn Or = "OR"+prettyShowConn Impl = "IMPL"++-- |Extract all variables in an expression+-- Will not return duplicationes+extractVariablesE :: E -> [String]+extractVariablesE = nub . findAllVars+ where+ findAllVars (Lit _) = []+ findAllVars Pi = []+ findAllVars (Var v) = [v]+ findAllVars (EUnOp _ e) = findAllVars e+ findAllVars (EBinOp _ e1 e2) = findAllVars e1 ++ findAllVars e2+ findAllVars (PowI e _) = findAllVars e+ findAllVars (Float32 _ e) = findAllVars e+ findAllVars (Float64 _ e) = findAllVars e+ findAllVars (Float _ e) = findAllVars e+ findAllVars (RoundToInteger _ e) = findAllVars e++-- |Extract all variables in an expression+-- Will not return duplicationes+extractVariablesF :: F -> [String]+extractVariablesF = nub . findAllVars+ where+ findAllVars (FComp _ e1 e2) = extractVariablesE e1 ++ extractVariablesE e2+ findAllVars (FConn _ f1 f2) = findAllVars f1 ++ findAllVars f2+ findAllVars (FNot f) = findAllVars f+ findAllVars FTrue = []+ findAllVars FFalse = []++extractVariablesECNF :: [[E]] -> [String]+extractVariablesECNF = nub . concatMap (concatMap extractVariablesE)++hasVarsE :: E -> Bool+hasVarsE (Float _ _) = False+hasVarsE (Float32 _ _) = False+hasVarsE (Float64 _ _) = False+hasVarsE (EBinOp _ e1 e2) = hasFloatE e1 || hasFloatE e2+hasVarsE (EUnOp _ e) = hasFloatE e+hasVarsE (PowI e _) = hasFloatE e+hasVarsE (Lit _) = False+hasVarsE (Var _) = True+hasVarsE Pi = False+hasVarsE (RoundToInteger _ e) = hasFloatE e++hasVarsF :: F -> Bool+hasVarsF (FConn _ f1 f2) = hasVarsF f1 || hasVarsF f2+hasVarsF (FComp _ e1 e2) = hasVarsE e1 || hasVarsE e2+hasVarsF (FNot f) = hasVarsF f+hasVarsF FTrue = False+hasVarsF FFalse = False++hasFloatE :: E -> Bool+hasFloatE (Float _ _) = True+hasFloatE (Float32 _ _) = True+hasFloatE (Float64 _ _) = True+hasFloatE (EBinOp _ e1 e2) = hasFloatE e1 || hasFloatE e2+hasFloatE (EUnOp _ e) = hasFloatE e+hasFloatE (PowI e _) = hasFloatE e+hasFloatE (Lit _) = False+hasFloatE (Var _) = False+hasFloatE Pi = False+hasFloatE (RoundToInteger _ e) = hasFloatE e++hasFloatF :: F -> Bool+hasFloatF (FConn _ f1 f2) = hasFloatF f1 || hasFloatF f2+hasFloatF (FComp _ e1 e2) = hasFloatE e1 || hasFloatE e2+hasFloatF (FNot f) = hasFloatF f+hasFloatF FTrue = False+hasFloatF FFalse = False++substVarEWithLit :: E -> String -> Rational -> E+substVarEWithLit (Var x) varToSubst valToSubst = if x == varToSubst then Lit valToSubst else Var x+substVarEWithLit (RoundToInteger m e) var val = RoundToInteger m (substVarEWithLit e var val)+substVarEWithLit Pi _ _ = Pi+substVarEWithLit l@(Lit _) _ _ = l+substVarEWithLit (EBinOp op e1 e2) var val = EBinOp op (substVarEWithLit e1 var val) (substVarEWithLit e2 var val)+substVarEWithLit (EUnOp op e) var val = EUnOp op (substVarEWithLit e var val)+substVarEWithLit (PowI e i) var val = PowI (substVarEWithLit e var val) i+substVarEWithLit (Float m e) var val = Float m (substVarEWithLit e var val)+substVarEWithLit (Float32 m e) var val = Float32 m (substVarEWithLit e var val)+substVarEWithLit (Float64 m e) var val = Float64 m (substVarEWithLit e var val)++substVarFWithLit :: F -> String -> Rational -> F+substVarFWithLit (FConn op f1 f2) var val = FConn op (substVarFWithLit f1 var val) (substVarFWithLit f2 var val)+substVarFWithLit (FComp op e1 e2) var val = FComp op (substVarEWithLit e1 var val) (substVarEWithLit e2 var val)+substVarFWithLit (FNot f) var val = FNot (substVarFWithLit f var val)+substVarFWithLit FTrue _ _ = FTrue+substVarFWithLit FFalse _ _ = FFalse++substVarEWithE :: String -> E -> E -> E+substVarEWithE varToSubst (EBinOp op e1 e2) eToSubst = EBinOp op (substVarEWithE varToSubst e1 eToSubst) (substVarEWithE varToSubst e2 eToSubst)+substVarEWithE varToSubst (EUnOp op e) eToSubst = EUnOp op (substVarEWithE varToSubst e eToSubst)+substVarEWithE varToSubst (Float mode e) eToSubst = Float mode $ substVarEWithE varToSubst e eToSubst+substVarEWithE varToSubst (Float32 mode e) eToSubst = Float32 mode $ substVarEWithE varToSubst e eToSubst+substVarEWithE varToSubst (Float64 mode e) eToSubst = Float64 mode $ substVarEWithE varToSubst e eToSubst+substVarEWithE varToSubst (RoundToInteger mode e) eToSubst = RoundToInteger mode $ substVarEWithE varToSubst e eToSubst+substVarEWithE varToSubst (PowI e i) eToSubst = PowI (substVarEWithE varToSubst e eToSubst) i+substVarEWithE _ Pi eToSubst = Pi+substVarEWithE _ e@(Lit _) eToSubst = e+substVarEWithE varToSubst (Var y) eToSubst = if varToSubst == y then eToSubst else Var y++substVarFWithE :: String -> F -> E -> F+substVarFWithE varToSubst (FConn op f1 f2) eToSubst = FConn op (substVarFWithE varToSubst f1 eToSubst) (substVarFWithE varToSubst f2 eToSubst)+substVarFWithE varToSubst (FComp op e1 e2) eToSubst = FComp op (substVarEWithE varToSubst e1 eToSubst) (substVarEWithE varToSubst e2 eToSubst)+substVarFWithE varToSubst (FNot f) eToSubst = FNot $ substVarFWithE varToSubst f eToSubst+substVarFWithE _ FTrue _ = FTrue+substVarFWithE _ FFalse _ = FFalse++-- Replaces implications with ORs, i.e. p -> q becomes !p \/ q+transformImplications :: F -> F+transformImplications (FConn Impl f1 f2) = FConn Or (transformImplications (FNot f1)) (transformImplications f2)+transformImplications (FConn op f1 f2) = FConn op (transformImplications f1) (transformImplications f2)+transformImplications f@(FComp op e1 e2) = f+transformImplications (FNot f) = FNot $ transformImplications f+transformImplications FTrue = FTrue+transformImplications FFalse = FFalse++removeVariableFreeComparisons :: F -> F+removeVariableFreeComparisons f =+ aux f False+ where+ expressionContainsVars :: E -> Bool+ expressionContainsVars (EBinOp _ e1 e2) = expressionContainsVars e1 || expressionContainsVars e2+ expressionContainsVars (EUnOp _ e) = expressionContainsVars e+ expressionContainsVars (PowI e _) = expressionContainsVars e+ expressionContainsVars (Float _ e) = expressionContainsVars e+ expressionContainsVars (Float32 _ e) = expressionContainsVars e+ expressionContainsVars (Float64 _ e) = expressionContainsVars e+ expressionContainsVars (RoundToInteger _ e) = expressionContainsVars e+ expressionContainsVars (Lit _) = False+ expressionContainsVars Pi = False+ expressionContainsVars (Var _) = True+++ -- When we say False (unsat), the VC MUST be False+ -- When we say True (sat), the VC might not be True+ -- We safely remove variableFreeComparisons by adhering to the above statements+ aux f'@(FConn And f1 f2) isNegated = FConn And (aux f1 isNegated) (aux f2 isNegated)+ aux f'@(FConn Or f1 f2) isNegated = FConn Or (aux f1 isNegated) (aux f2 isNegated)+ aux f'@(FConn Impl f1 f2) isNegated = FConn Impl (aux f1 (not isNegated)) (aux f2 isNegated)+ aux f'@(FComp _ e1 e2) isNegated =+ case (expressionContainsVars e1, expressionContainsVars e2) of+ (True, _) -> f'+ (_, True) -> f'+ _ -> if isNegated then FFalse else FTrue+ aux (FNot f') isNegated = FNot (aux f' (not isNegated))+ aux FTrue _ = FTrue+ aux FFalse _ = FFalse++hasMinMaxAbsE :: E -> Bool+hasMinMaxAbsE (EBinOp Max _ _) = True+hasMinMaxAbsE (EBinOp Min _ _) = True+hasMinMaxAbsE (EBinOp _ e1 e2) = hasMinMaxAbsE e1 || hasMinMaxAbsE e2+hasMinMaxAbsE (EUnOp Abs e) = True+hasMinMaxAbsE (EUnOp _ e) = hasMinMaxAbsE e+hasMinMaxAbsE (PowI e _) = hasMinMaxAbsE e+hasMinMaxAbsE (Float32 _ e) = hasMinMaxAbsE e+hasMinMaxAbsE (Float64 _ e) = hasMinMaxAbsE e+hasMinMaxAbsE (Float _ e) = hasMinMaxAbsE e+hasMinMaxAbsE (RoundToInteger _ e) = hasMinMaxAbsE e+hasMinMaxAbsE (Lit _) = False+hasMinMaxAbsE (Var _) = False+hasMinMaxAbsE (Pi) = False++hasMinMaxAbsF :: F -> Bool+hasMinMaxAbsF (FComp _ e1 e2) = hasMinMaxAbsE e1 || hasMinMaxAbsE e2+hasMinMaxAbsF (FConn _ f1 f2) = hasMinMaxAbsF f1 || hasMinMaxAbsF f2+hasMinMaxAbsF (FNot f) = hasMinMaxAbsF f+hasMinMaxAbsF FTrue = False+hasMinMaxAbsF FFalse = False++replaceEInE :: E -> E -> E -> E+replaceEInE eContainingE eToFind eToReplace =+ if eContainingE P.== eToFind+ then eToReplace+ else+ case eContainingE of+ EBinOp op e1 e2 -> EBinOp op (replaceEInE e1 eToFind eToReplace) (replaceEInE e2 eToFind eToReplace)+ EUnOp op e -> EUnOp op (replaceEInE e eToFind eToReplace)+ Float32 rnd e -> Float32 rnd (replaceEInE e eToFind eToReplace)+ Float64 rnd e -> Float64 rnd (replaceEInE e eToFind eToReplace)+ Float rnd e -> Float64 rnd (replaceEInE e eToFind eToReplace)+ RoundToInteger rnd e -> RoundToInteger rnd (replaceEInE e eToFind eToReplace)+ PowI e i -> PowI (replaceEInE e eToFind eToReplace) i+ Lit _ -> eContainingE+ Var _ -> eContainingE+ Pi -> eContainingE+++replaceEInF :: F -> E -> E -> F+replaceEInF fContainingE eToFind eToReplace =+ case fContainingE of+ FConn op f1 f2 -> FConn op (replaceEInF f1 eToFind eToReplace) (replaceEInF f2 eToFind eToReplace)+ FComp op e1 e2 -> FComp op (replaceEInE e1 eToFind eToReplace) (replaceEInE e2 eToFind eToReplace)+ FNot f -> FNot $ replaceEInF f eToFind eToReplace+ FTrue -> FTrue+ FFalse -> FFalse++-- |Normalize to and/or+-- aggressively apply elimination rules+normalizeBoolean :: F -> F+normalizeBoolean form =+ if form P.== simplifiedForm+ then simplifiedForm+ else normalizeBoolean simplifiedForm+ where+ simplifiedForm = aggressiveSimplify $ simplifyF $ normalizeToOr $ aux $ simplifyF form++ -- Turn and/or into or using demorgans laws+ normalizeToOr f =+ let+ -- convertAndToNegatedOr (FConn And (FNot x) y) = FNot $ FConn Or x $ convertAndToNegatedOr y+ convertAndToOr (FConn And x y) = FNot $ FConn Or (FNot x) $ convertAndToOr (FNot y)+ convertAndToOr (FConn Or x y) = FConn Or (convertAndToOr x) (convertAndToOr y)+ -- convertAndToNegatedOr (FNot y) = y+ convertAndToOr y = y+ in+ convertAndToOr f++ -- Aggressively simplify Ors+ aggressiveSimplify (FConn Or x f@(FNot (FConn Or y z)))+ | x P.== y = aggressiveSimplify (FConn Or x (FNot z))+ | x P.== z = aggressiveSimplify (FConn Or x (FNot y))+ | otherwise = FConn Or (aggressiveSimplify x) (aggressiveSimplify f)+ aggressiveSimplify (FConn Or f@(FNot (FConn Or y z)) x)+ | x P.== y = aggressiveSimplify (FConn Or (FNot z) x)+ | x P.== z = aggressiveSimplify (FConn Or (FNot y) x)+ | otherwise = FConn Or (aggressiveSimplify f) (aggressiveSimplify x)+ aggressiveSimplify (FNot (FNot f)) = aggressiveSimplify f+ -- aggressiveSimplify (FConn Or x f@(FConn And (FNot x') y)) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify x) (aggressiveSimplify f))+ -- aggressiveSimplify (FConn Or x f@(FConn And y (FNot x'))) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify x) (aggressiveSimplify f))+ -- aggressiveSimplify (FConn Or f@(FConn And (FNot x') y) x) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify f) (aggressiveSimplify x))+ -- aggressiveSimplify (FConn Or f@(FConn And y (FNot x')) x) = if x P.== x' then aggressiveSimplify (FConn Or x y) else (FConn Or (aggressiveSimplify f) (aggressiveSimplify x))+ aggressiveSimplify f = f++ -- aux (FConn Or x f@(FConn And (FNot x') y)) = if x P.== x' then FConn And x y else FConn Or (aux x) (aux f)+ aux (FConn Impl x y) = aux $ FConn Or (FNot x) y+ aux (FNot f@(FConn Impl x y)) = aux (FNot (aux f))+ aux (FNot (FConn Or x y)) = aux (FConn And (FNot x) (FNot y))+ aux (FNot (FConn And x y)) = aux (FConn Or (FNot x) (FNot y))+ aux (FConn Or x y) = FConn Or (aux x) (aux y)+ aux (FConn And x y) = FConn And (aux x) (aux y)+ aux (FNot (FNot f)) = aux f+ aux f = f
+ src/PropaFP/Parsers/DRealSmt.hs view
@@ -0,0 +1,131 @@+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LambdaCase #-}+module PropaFP.Parsers.DRealSmt where++import MixedTypesNumPrelude+import PropaFP.Expression+import qualified PropaFP.Parsers.Lisp.DataTypes as LD+import PropaFP.VarMap+import PropaFP.Parsers.Smt++-- | Parser for SMT files produced by the dReal Translator.+-- +-- The DReal SMT file will have the first line declaring the SMT logic, which we ignore.+-- The next few lines declare variables (if any)+-- A variable is declared in the following format+-- (declare-fun varName () varType) where varType can be Int or Real+-- (assert (<= lowerBound varName))+-- (assert (<= varName upperBound))+-- +-- Both lowerBound and upperBound will be rationals, though can be safely converted to Integer for Int vars+-- +-- Once the declare-fun lines end, we have an assert which contains the entire VC as an argument+-- The rest of the file can be ignored (it will be (check-sat), (get-model), and (exit))+parseDRealSmtToF :: [LD.Expression] -> (Maybe F, TypedVarMap)+parseDRealSmtToF parsedExpressions =+ (parseDRealVCs (findAssertions parsedVC), typedVarMap)+ where+ (_smtLogic : varsWithParsedVC) = parsedExpressions+ (parsedVC, typedVarMap) = parseDRealVariables varsWithParsedVC++parseDRealVCs :: [LD.Expression] -> Maybe F+parseDRealVCs [] = error "Processed parser: Given empty list of assertions"+parseDRealVCs [p1] = termDRealToF p1+parseDRealVCs (p1 : p2) = FConn And <$> termDRealToF p1 <*> parseDRealVCs p2++parseDRealVC :: LD.Expression -> Maybe F+parseDRealVC (LD.Application (LD.Variable "assert") [parsedVC]) = termDRealToF parsedVC+parseDRealVC _ = Nothing+-- | Parses variables from a parsed file.+-- First item must be a variable declaration+-- Continues parsing variables until it reaches a non-variable assertion+-- Returns a TypedVarMap and the rest of the parsed file.+parseDRealVariables :: [LD.Expression] -> ([LD.Expression], TypedVarMap)+parseDRealVariables + (+ LD.Application (LD.Variable "declare-fun") [LD.Variable varName, LD.Null, LD.Variable varType] :+ LD.Application (LD.Variable "assert") [LD.Application (LD.Variable "<=") [LD.Application (LD.Variable "/") [LD.Number lowerNumerator, LD.Number lowerDenominator], LD.Variable _]] :+ LD.Application (LD.Variable "assert") [LD.Application (LD.Variable "<=") [LD.Variable _, LD.Application (LD.Variable "/") [LD.Number upperNumerator, LD.Number upperDenominator]]] :+ parsedExpressions+ ) =+ let+ (remainingExpressions, parsedVarMap) = parseDRealVariables parsedExpressions+ parsedVarType = + case varType of+ "Real" -> Real+ "Int" -> Integer+ _ -> error "Unrecognized varType in given dReal SMT file"+ in+ (remainingExpressions, TypedVar (varName, (lowerNumerator / lowerDenominator, upperNumerator / upperDenominator)) parsedVarType : parsedVarMap)+parseDRealVariables parsedExpressions = (parsedExpressions, [])++termDRealToF :: LD.Expression -> Maybe F+-- FConn+termDRealToF (LD.Application (LD.Variable "and") [p1, p2]) = FConn And <$> termDRealToF p1 <*> termDRealToF p2+-- termDRealToF (LD.Application (LD.Variable "or") [LD.Application (LD.Variable "not") [p1], p2]) = FConn Impl <$> termDRealToF p1 <*> termDRealToF p2+termDRealToF (LD.Application (LD.Variable "or") [p1, p2]) = FConn Or <$> termDRealToF p1 <*> termDRealToF p2 --TODO: parse OR (NOT p1) p2 as impl? possible but is there any benefit?+-- Special case for =+termDRealToF (LD.Application (LD.Variable "=") [p1, p2]) = + case (termDRealToF p1, termDRealToF p2) of+ (Just f1, Just f2) -> Just $ FConn And (FConn Impl f1 f2) (FConn Impl f2 f1)+ (Nothing, Nothing) ->+ case (termDRealToE p1, termDRealToE p2) of+ (Just e1, Just e2) -> Just $ FComp Eq e1 e2+ (_, _) -> Nothing+ (_, _) -> Nothing+-- FComp+termDRealToF (LD.Application (LD.Variable ">=") [p1, p2]) = FComp Ge <$> termDRealToE p1 <*> termDRealToE p2+termDRealToF (LD.Application (LD.Variable ">") [p1, p2]) = FComp Gt <$> termDRealToE p1 <*> termDRealToE p2+termDRealToF (LD.Application (LD.Variable "<=") [p1, p2]) = FComp Le <$> termDRealToE p1 <*> termDRealToE p2+termDRealToF (LD.Application (LD.Variable "<") [p1, p2]) = FComp Lt <$> termDRealToE p1 <*> termDRealToE p2+termDRealToF (LD.Application (LD.Variable "not") [p]) = FNot <$> termDRealToF p+-- Bools+termDRealToF (LD.Variable "true") = Just FTrue+termDRealToF (LD.Variable "false") = Just FFalse+-- Unknown+termDRealToF _ = Nothing++termDRealToE :: LD.Expression -> Maybe E+-- Need to deal with Pi first+termDRealToE (LD.Application (LD.Variable "*") [LD.Number 4, LD.Application (LD.Variable "atan") [LD.Number 1]]) = Just $ Pi+-- EBinOp+termDRealToE (LD.Application (LD.Variable "+") [p1, p2]) = EBinOp Add <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "-") [p1, p2]) = EBinOp Sub <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "*") [p1, p2]) = EBinOp Mul <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "/") [p1, p2]) = EBinOp Div <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "min") [p1, p2]) = EBinOp Min <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "max") [p1, p2]) = EBinOp Max <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "^") [p1, p2]) = EBinOp Pow <$> termDRealToE p1 <*> termDRealToE p2+termDRealToE (LD.Application (LD.Variable "mod") [p1, p2]) = EBinOp Mod <$> termDRealToE p1 <*> termDRealToE p2+-- EUnOp+termDRealToE (LD.Application (LD.Variable "sqrt") [p]) = EUnOp Sqrt <$> termDRealToE p+-- TODO: understand negate?+termDRealToE (LD.Application (LD.Variable "abs") [p]) = EUnOp Abs <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "sin") [p]) = EUnOp Sin <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "cos") [p]) = EUnOp Cos <$> termDRealToE p+-- TODO: understand PowI? probably easier to add simplification rule+-- Variables+termDRealToE (LD.Variable v) = Just $ Var v+-- Literals+termDRealToE (LD.Number n) = Just $ Lit n+-- RoundToInt+termDRealToE (LD.Application (LD.Variable "to_int_rne") [p]) = RoundToInteger RNE <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "to_int_rtp") [p]) = RoundToInteger RTP <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "to_int_rtn") [p]) = RoundToInteger RTN <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "to_int_rtz") [p]) = RoundToInteger RTZ <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "to_int_rna") [p]) = RoundToInteger RNA <$> termDRealToE p+-- Float32+termDRealToE (LD.Application (LD.Variable "float32_rne") [p]) = Float32 RNE <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float32_rtp") [p]) = Float32 RTP <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float32_rtn") [p]) = Float32 RTN <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float32_rtz") [p]) = Float32 RTZ <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float32_rna") [p]) = Float32 RNA <$> termDRealToE p+-- Float64+termDRealToE (LD.Application (LD.Variable "float64_rne") [p]) = Float64 RNE <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float64_rtp") [p]) = Float64 RTP <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float64_rtn") [p]) = Float64 RTN <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float64_rtz") [p]) = Float64 RTZ <$> termDRealToE p+termDRealToE (LD.Application (LD.Variable "float64_rna") [p]) = Float64 RNA <$> termDRealToE p+-- Unknown+termDRealToE _ = Nothing
+ src/PropaFP/Parsers/Lisp/DataTypes.hs view
@@ -0,0 +1,108 @@+module PropaFP.Parsers.Lisp.DataTypes+( Frame+, Environment(..)+, Expression(..)+, addBinding+, lookupValue+, extendEnvironment+, pairToList+) where+import qualified Data.Map as Map+import qualified Data.List as List+import Prelude++-- A frame contains mappings from variable names to Lisp values.+type Frame = Map.Map String Expression++-- An Environment is a frame coupled with a parent environment.+data Environment = EmptyEnvironment+ | Environment Frame Environment++-- The Expression data type defines the elements of the abstract syntax tree+-- and the runtime types manipulated by the Lisp system.+data Expression = Null+ | Number Rational+ | Boolean Bool+ | Variable String+ | Pair Expression Expression+ | Exception String+ | Lambda [Expression] Expression+ | PrimitiveProcedure ([Expression] -> Expression)+ | Application Expression [Expression]+ | Definition Expression Expression+ | If Expression Expression Expression+ | Cond [(Expression, Expression)]++instance Show Expression where+ show = showExpression++instance Eq Expression where+ x == y = eqExpression x y++eqExpression :: Expression -> Expression -> Bool+eqExpression (Pair x1 x2) (Pair y1 y2) = eqExpression x1 y1 && eqExpression x2 y2+eqExpression (Lambda x1s x2) (Lambda y1s y2) = and (List.zipWith eqExpression x1s y1s) && eqExpression x2 y2+eqExpression (Application x1 y1s) (Application x2 y2s) = eqExpression x1 x2 && and (List.zipWith eqExpression y1s y2s)+eqExpression (Definition x1 y1) (Definition x2 y2) = eqExpression x1 y1 && eqExpression x2 y2+eqExpression (If x1 y1 z1) (If x2 y2 z2) = eqExpression x1 y1 && eqExpression x2 y2 && eqExpression z1 z2+eqExpression Null Null = True+eqExpression Null _ = False+eqExpression _ Null = False+eqExpression (Number x) (Number y) = x == y+eqExpression (Boolean x) (Boolean y) = x == y+eqExpression (Variable x) (Variable y) = x == y+eqExpression (Exception x) (Exception y) = x == y+eqExpression _ _ = False+-- A function that recursively converts a Lisp Expression to a+-- String representation.+showExpression :: Expression -> String+showExpression (Null) = "null"+showExpression (Number number) = show number+showExpression (Boolean bool)+ | bool == True = "#t"+ | otherwise = "#f"+showExpression (Variable variable) = variable+showExpression (Exception message) = "#Exception: " ++ "'" ++ message ++ "'"+showExpression pair@(Pair first second)+ | isList pair = "(" ++ (showPairList pair) ++ ")"+ | otherwise = "(" ++ (show first) ++ " . " ++ (show second) ++ ")"+showExpression (Lambda parameters body) = "#CompoundProcedure"+showExpression (PrimitiveProcedure _) = "#PrimitiveProcedure"+showExpression (Application operator operands) = "#Application " ++ show operator ++ " " ++ show operands+showExpression (Definition variable value) = "#Definition " ++ show variable ++ " " ++ show value+showExpression _ = "#Unknown"++showPairList :: Expression -> String+showPairList Null = ""+showPairList (Pair first (Null)) = (show first)+showPairList (Pair first second) = (show first) ++ " " ++ (showPairList second)++-- Helper functions for environment manipulation.+addBinding :: Environment -> String -> Expression -> Environment+addBinding EmptyEnvironment _ _ = EmptyEnvironment+addBinding (Environment frame parent) name value = Environment newFrame parent+ where newFrame = Map.insert name value frame++lookupValue :: Environment -> String -> Expression+lookupValue EmptyEnvironment variable = Exception ("Binding for " ++ variable ++ " not found.")+lookupValue (Environment frame parent) variable =+ case value of+ Just result -> result+ Nothing -> lookupValue parent variable+ where value = Map.lookup variable frame++extendEnvironment :: Environment -> [Expression] -> [Expression] -> Environment+extendEnvironment environment parameters arguments =+ let params = map show parameters+ in Environment (Map.fromList (zip params arguments)) environment++-- Helper functions for pair manipulation.+pairToList :: Expression -> [Expression]+pairToList Null = []+pairToList (Pair first rest) = first : pairToList rest++isList :: Expression -> Bool+isList Null = True+isList (Pair _ second) = isList second+isList _ = False+
+ src/PropaFP/Parsers/Lisp/Parser.hs view
@@ -0,0 +1,174 @@+module PropaFP.Parsers.Lisp.Parser+( tokenize+, parse+, parseSequence+, analyzeExpression+, analyzeExpressionSequence+, isScientificNumber) where+import PropaFP.Parsers.Lisp.DataTypes+import Prelude+import GHC.Utils.Misc (readRational)+import qualified Data.Scientific as S+import qualified Data.List as L+-- Constants.+symbolCharacters :: String+symbolCharacters = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_!?-+*/%<>#.=^"++numberCharacters :: String+numberCharacters = "0123456789."++isSymbolCharacter :: Char -> Bool+isSymbolCharacter ch = elem ch symbolCharacters++isNumberCharacter :: Char -> Bool+isNumberCharacter ch = elem ch numberCharacters++isSymbol :: String -> Bool+isSymbol = all isSymbolCharacter++-- Fixed issue with parsing -.1, multiple decimal points+isNumber :: String -> Bool+isNumber [] = True+isNumber [c] = elem c "0123456789"+isNumber ('-' : cs) = isNumber cs+isNumber (c : cs) = elem c "0123456789" && all isNumberCharacter cs && L.length (L.filter ('.' ==) cs) <= 1 ++isScientificNumber :: String -> Bool+isScientificNumber [] = True+isScientificNumber [_c] = False+isScientificNumber ('-' : cs) = isScientificNumber cs+isScientificNumber (c : cs) = + elem c "0123456789" &&+ case L.break (== 'e') cs of+ (_, []) -> False -- e is not in cs+ (beforeE, _e : afterE) ->+ all isNumberCharacter beforeE &&+ case afterE of+ [] -> False+ ('-' : ecs) -> all (`elem` "0123456789") ecs+ ecs -> all (`elem` "0123456789") ecs+ && L.length (L.filter ('.' ==) cs) <= 1 +-- The "tokenize" function is the first phase of converting the source code of+-- a Lisp program into an abstract syntax tree. It performs lexical analysis on+-- a String representation of a Lisp program by extracting a list of tokens.+tokenize :: String -> [String]+tokenize [] = []+tokenize (x:xs)+ | x == ';' = tokenize $ dropWhile (/= '\n') xs -- Remove comments+ | x == '(' = [x] : tokenize xs+ | x == ')' = [x] : tokenize xs+ | isNumberCharacter x = tokenizeNumber (x:xs) "" False+ | isSymbolCharacter x = tokenizeSymbol (x:xs) ""+ | otherwise = tokenize xs++tokenizeNumber :: String -> String -> Bool -> [String]+tokenizeNumber [] number foundE = [number]+tokenizeNumber (x:xs) number foundE+ | isNumberCharacter x = tokenizeNumber xs (number ++ [x]) foundE+ | ('e' == x) && not foundE = tokenizeNumber xs (number ++ [x]) True -- Support scientific numbers+ | otherwise = number : tokenize (x:xs)++tokenizeSymbol :: String -> String -> [String]+tokenizeSymbol [] symbol = [symbol]+tokenizeSymbol (x:xs) number+ | isSymbolCharacter x = tokenizeSymbol xs (number ++ [x])+ | otherwise = number : tokenize (x:xs)++-- The "parse" function is the second phase of converting the source code of+-- a Lisp program into an abstract syntax tree. It takes the list of tokens+-- generated by "tokenize" and scans it until a valid Expression is created.+-- The newly built expression along with the remaining tokens are returned.+-- The Expressions that are returned are "primitive". They are entirely+-- comprised of elements such as boolean and numeric constants with the only+-- compound element being a "pair".+parse :: [String] -> (Expression, [String])+parse [] = (Null, [])+parse (x:xs)+ | x == "(" = parseList xs+ | "#t" == x = ((Boolean True), xs)+ | "#f" == x = ((Boolean False), xs)+ | "null" == x = ((Null), xs)+ | isScientificNumber x = ((Number (toRational (read x :: S.Scientific))), xs)+ | isNumber x = ((Number (readRational x)), xs)+ | isSymbol x = ((Variable x), xs)+ | otherwise = (Null, [])++-- A helper function to parse a list. A list is defined as either+-- Null or a Pair who's second element is a list.+parseList :: [String] -> (Expression, [String])+parseList [] = (Null, [])+parseList tokens@(x:xs)+ | x == ")" = (Null, xs)+ | otherwise = ((Pair expr1 expr2), rest2)+ where (expr1, rest1) = parse tokens+ (expr2, rest2) = parseList rest1++-- A helper function that takes the list of tokens generated by "tokenize"+-- and continues parsing until all the constituent Expressions are extracted.+parseSequence :: [String] -> [Expression]+parseSequence [] = []+parseSequence tokens = expr : parseSequence rest+ where (expr, rest) = parse tokens++-- The "analyzeExpression" function implements the third and final phase of+-- converting the source code of a Lisp program into an abstract syntax tree.+-- It takes a "primitive" Expression as input and converts it into a more+-- sophisticated abstract syntax tree Expression such as Lambda, Application,+-- If, Define, etc.+analyzeExpression :: Expression -> Expression+analyzeExpression Null = Null+analyzeExpression (Number number) = (Number number)+analyzeExpression (Boolean bool) = (Boolean bool)+analyzeExpression (Variable variable) = (Variable variable)+analyzeExpression pair@(Pair first second)+ | isIfExpression pair = buildIfExpression pair+ | isLambdaExpression pair = buildLambdaExpression pair+ | isDefinitionExpression pair = buildDefinitionExpression pair+ | isCondExpression pair = buildCondExpression pair+ -- New special forms to be added here.+ | otherwise = buildApplicationExpression pair++isIfExpression :: Expression -> Bool+isIfExpression (Pair (Variable value) _) = value == "if"+isIfExpression _ = False++buildIfExpression :: Expression -> Expression+buildIfExpression (Pair _ (Pair predicate (Pair thenClause (Pair elseClause Null)))) =+ If (analyzeExpression predicate) (analyzeExpression thenClause) (analyzeExpression elseClause)++isLambdaExpression :: Expression -> Bool+isLambdaExpression (Pair (Variable value) _) = value == "lambda"+isLambdaExpression _ = False++buildLambdaExpression :: Expression -> Expression+buildLambdaExpression (Pair _ (Pair parameters (Pair body Null))) =+ Lambda (pairToList parameters) (analyzeExpression body)++isDefinitionExpression :: Expression -> Bool+isDefinitionExpression (Pair (Variable value) _) = value == "define"+isDefinitionExpression _ = False++buildDefinitionExpression :: Expression -> Expression+buildDefinitionExpression (Pair _ (Pair variable (Pair value Null))) =+ Definition variable (analyzeExpression value)++isCondExpression :: Expression -> Bool+isCondExpression (Pair (Variable value) _) = value == "cond"+isCondExpression _ = False++buildCondExpression :: Expression -> Expression+buildCondExpression (Pair _ second) = buildCondExpressionHelper second++buildCondExpressionHelper :: Expression -> Expression+buildCondExpressionHelper (Null) = (Cond [])+buildCondExpressionHelper (Pair (Pair predicate (Pair expression Null)) other) =+ (Cond ((analyzeExpression predicate, analyzeExpression expression) : cases))+ where (Cond cases) = buildCondExpressionHelper other++buildApplicationExpression :: Expression -> Expression+buildApplicationExpression (Pair operator operands) =+ Application (analyzeExpression operator) (map analyzeExpression (pairToList operands))++analyzeExpressionSequence :: [Expression] -> [Expression]+analyzeExpressionSequence = map analyzeExpression+
+ src/PropaFP/Parsers/Smt.hs view
@@ -0,0 +1,969 @@+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LambdaCase #-}+module PropaFP.Parsers.Smt where++import MixedTypesNumPrelude hiding (unzip)+import qualified Prelude as P+import System.IO.Unsafe++import PropaFP.Expression++import qualified PropaFP.Parsers.Lisp.Parser as LP+import qualified PropaFP.Parsers.Lisp.DataTypes as LD++import Data.Char (digitToInt)++import Data.Word+import qualified Data.ByteString.Lazy as B+import Data.Binary.Get+import Data.Maybe (mapMaybe)++import PropaFP.VarMap+import PropaFP.DeriveBounds+import PropaFP.EliminateFloats+import PropaFP.Eliminator (minMaxAbsEliminatorECNF, minMaxAbsEliminator)+import Data.List (nub, sort, isPrefixOf, sortBy, partition, foldl')+import Data.List.NonEmpty (unzip)+import Control.Arrow ((&&&))+import Debug.Trace+import PropaFP.Translators.DReal (formulaAndVarMapToDReal)+import Text.Regex.TDFA ( (=~) )+import Data.Ratio+import PropaFP.DeriveBounds+import qualified Data.Map as M+import AERN2.MP (endpoints, mpBallP, prec)++data ParsingMode = Why3 | CNF+parser :: String -> [LD.Expression]+parser = LP.analyzeExpressionSequence . LP.parseSequence . LP.tokenize++parseSMT2 :: FilePath -> IO [LD.Expression]+parseSMT2 filePath = fmap parser $ P.readFile filePath++-- |Find assertions in a parsed expression+-- Assertions are Application types with the operator being a Variable equal to "assert"+-- Assertions only have one 'operands'+findAssertions :: [LD.Expression] -> [LD.Expression]+findAssertions [] = []+-- findAssertions [LD.Application (LD.Variable "assert") [operands]] = [operands]+findAssertions ((LD.Application (LD.Variable "assert") [operands]) : expressions) = operands : findAssertions expressions+-- findAssertions ((LD.Application (LD.Variable var) [operands]) : expressions) = operands : findAssertions expressions+findAssertions (e : expressions) = findAssertions expressions++findFunctionInputsAndOutputs :: [LD.Expression] -> [(String, ([String], String))]+findFunctionInputsAndOutputs [] = []+findFunctionInputsAndOutputs ((LD.Application (LD.Variable "declare-fun") [LD.Variable fName, fInputsAsExpressions, LD.Variable fOutputs]) : expressions) =+ (fName, (expressionInputsAsString fInputsAsExpressions, fOutputs)) : findFunctionInputsAndOutputs expressions+ where+ expressionInputsAsString :: LD.Expression -> [String]+ expressionInputsAsString (LD.Application (LD.Variable inputTypeAsString) remainingInputsAsExpression) = inputTypeAsString : concatMap expressionInputsAsString remainingInputsAsExpression+ expressionInputsAsString (LD.Variable inputTypeAsString) = [inputTypeAsString]+ expressionInputsAsString _ = []+findFunctionInputsAndOutputs (_ : expressions) = findFunctionInputsAndOutputs expressions++-- |Find function declarations in a parsed expression+-- Function declarations are Application types with the operator being a Variable equal to "declare-fun"+-- Function declarations contain 3 operands+-- - Operand 1 is the name of the function+-- - Operand 2 is an Application type which can be thought of as the parameters of the functions+-- If the function has no paramters, this operand is LD.Null +-- - Operand 3 is the type of the function+findDeclarations :: [LD.Expression] -> [LD.Expression]+findDeclarations [] = []+findDeclarations (declaration@(LD.Application (LD.Variable "declare-fun") _) : expressions) = declaration : findDeclarations expressions+findDeclarations (_ : expressions) = findDeclarations expressions++findVariables :: [LD.Expression] -> [(String, String)]+findVariables [] = []+findVariables (LD.Application (LD.Variable "declare-const") [LD.Variable varName, LD.Variable varType] : expressions)+ = (varName, varType) : findVariables expressions+findVariables (LD.Application (LD.Variable "declare-fun") [LD.Variable varName, LD.Null, LD.Variable varType] : expressions)+ = (varName, varType) : findVariables expressions+findVariables (_ : expressions) = findVariables expressions++findIntegerVariables :: [(String, String)] -> [(String, VarType)]+findIntegerVariables [] = []+findIntegerVariables ((v,t) : vs) =+ if "Int" `isPrefixOf` t || "int" `isPrefixOf` t+ then (v, Integer) : findIntegerVariables vs+ else findIntegerVariables vs++-- |Finds goals in assertion operands+-- Goals are S-Expressions with a top level 'not'+findGoalsInAssertions :: [LD.Expression] -> [LD.Expression]+findGoalsInAssertions [] = []+findGoalsInAssertions ((LD.Application (LD.Variable operator) operands) : assertions) =+ if operator == "not"+ then head operands : findGoalsInAssertions assertions -- Take head of operands since not has only one operand+ else findGoalsInAssertions assertions+findGoalsInAssertions (_ : assertions) = findGoalsInAssertions assertions++-- |Takes the last element from a list of assertions+-- We assume that the last element is the goal+takeGoalFromAssertions :: [LD.Expression] -> (LD.Expression, [LD.Expression])+takeGoalFromAssertions asserts = (goal, assertsWithoutGoal)+ where+ numberOfAssertions = length asserts+ goal = last asserts -- FIXME: Unsafe. If asserts is empty, this will fail+ assertsWithoutGoal = take (numberOfAssertions - 1) asserts++-- safelyTypeExpression :: String -> [(String, ([String], String))] -> E -> E+-- safelyTypeExpression smtFunction functionsWithInputsAndOutputs exactExpression =+-- case lookup smtFunction functionsWithInputsAndOutputs of+-- Just (inputs, output)++-- |Attempts to parse FComp Ops, i.e. parse bool_eq to Just (FComp Eq)+parseFCompOp :: String -> Maybe (E -> E -> F)+parseFCompOp operator =+ case operator of+ n+ | n `elem` [">=", "fp.geq", "oge", "oge__logic"] || (n =~ "^bool_ge$|^bool_ge[0-9]+$" :: Bool) -> Just $ FComp Ge+ | n `elem` [">", "fp.gt", "ogt", "ogt__logic"] || (n =~ "^bool_gt$|^bool_gt[0-9]+$" :: Bool) -> Just $ FComp Gt+ | n `elem` ["<=", "fp.leq", "ole", "ole__logic"] || (n =~ "^bool_le$|^bool_le[0-9]+$" :: Bool) -> Just $ FComp Le+ | n `elem` ["<", "fp.lt", "olt", "olt__logic"] || (n =~ "^bool_lt$|^bool_lt[0-9]+$" :: Bool) -> Just $ FComp Lt+ | n `elem` ["=", "fp.eq"] || (n =~ "^bool_eq$|^bool_eq[0-9]+$|^user_eq$|^user_eq[0-9]+$" :: Bool) -> Just $ FComp Eq+ | "bool_neq" `isPrefixOf` n -> Just $ \e1 e2 -> FNot (FComp Eq e1 e2)+ _ -> Nothing++-- parseIte :: LD.Expression -> LD.Expression -> LD.Expression -> Maybe F+parseIte cond thenTerm elseTerm functionsWithInputsAndOutputs Nothing =+ case termToF cond functionsWithInputsAndOutputs of+ Just condF -> + case (termToF thenTerm functionsWithInputsAndOutputs, termToF elseTerm functionsWithInputsAndOutputs) of+ (Just thenTermF, Just elseTermF) -> + Just $ FConn And+ (FConn Impl condF thenTermF)+ (FConn Impl (FNot condF) elseTermF)+ (_, _) -> Nothing+ Nothing -> Nothing+parseIte cond thenTerm elseTerm functionsWithInputsAndOutputs (Just compTerm) =+ case termToF cond functionsWithInputsAndOutputs of+ (Just condF) ->+ case (termToE thenTerm functionsWithInputsAndOutputs, termToE elseTerm functionsWithInputsAndOutputs) of+ (Just thenTermE, Just elseTermE) ->+ Just $ FConn And+ (FConn Impl condF (compTerm thenTermE))+ (FConn Impl (FNot condF) (compTerm elseTermE))+ (Just thenTermE, _) ->+ case elseTerm of+ LD.Application (LD.Variable "ite") [elseCond, elseThenTerm, elseElseTerm] ->+ case parseIte elseCond elseThenTerm elseElseTerm functionsWithInputsAndOutputs (Just compTerm) of+ Just elseTermF -> Just $+ FConn And+ (FConn Impl condF (compTerm thenTermE))+ (FConn Impl (FNot condF) elseTermF)+ _ -> Nothing+ _ -> Nothing+ (_, Just elseTermE) ->+ case thenTerm of+ LD.Application (LD.Variable "ite") [thenCond, thenThenTerm, thenElseTerm] ->+ case parseIte thenCond thenThenTerm thenElseTerm functionsWithInputsAndOutputs (Just compTerm) of+ Just thenTermF -> Just $+ FConn And+ (FConn Impl condF thenTermF)+ (FConn Impl (FNot condF) (compTerm elseTermE))+ _ -> Nothing+ _ -> Nothing+ (_, _) -> + case (thenTerm, elseTerm) of+ (LD.Application (LD.Variable "ite") [thenCond, thenThenTerm, thenElseTerm], LD.Application (LD.Variable "ite") [elseCond, elseThenTerm, elseElseTerm]) ->+ case (parseIte thenCond thenThenTerm thenElseTerm functionsWithInputsAndOutputs (Just compTerm), parseIte elseCond elseThenTerm elseElseTerm functionsWithInputsAndOutputs (Just compTerm)) of+ (Just thenTermF, Just elseTermF) -> Just $+ FConn And+ (FConn Impl condF thenTermF)+ (FConn Impl (FNot condF) elseTermF)+ (_, _) -> Nothing+ (_, _) -> Nothing+ Nothing -> Nothing++termToF :: LD.Expression -> [(String, ([String], String))] -> Maybe F+termToF (LD.Application (LD.Variable operator) [op]) functionsWithInputsAndOutputs = -- Single param operators+ case termToE op functionsWithInputsAndOutputs of -- Ops with E params+ Just e ->+ case operator of+ "fp.isFinite32" ->+ let maxFloat = (2.0 - (1/(2^23))) * (2^127)+ minFloat = negate maxFloat+ in+ Just $ FConn And (FComp Le (Lit minFloat) e) (FComp Le e (Lit maxFloat))+ "fp.isFinite64" ->+ let maxFloat = (2.0 - (1/(2^52))) * (2^1023)+ minFloat = negate maxFloat+ in+ Just $ FConn And (FComp Le (Lit minFloat) e) (FComp Le e (Lit maxFloat))+ _ -> Nothing+ Nothing ->+ case termToF op functionsWithInputsAndOutputs of+ Just f ->+ case operator of+ "not" -> Just $ FNot f+ _ -> Nothing+ _ -> Nothing+termToF (LD.Application (LD.Variable operator) [op1, op2]) functionsWithInputsAndOutputs = -- Two param operations+ case (termToE op1 functionsWithInputsAndOutputs, termToE op2 functionsWithInputsAndOutputs) of+ (Just e1, Just e2) ->+ case parseFCompOp operator of+ Just fCompOp -> Just $ fCompOp e1 e2 + _ -> Nothing+ (_, _) ->+ case (termToF op1 functionsWithInputsAndOutputs, termToF op2 functionsWithInputsAndOutputs) of+ (Just f1, Just f2) ->+ case operator of+ "and" -> Just $ FConn And f1 f2+ "or" -> Just $ FConn Or f1 f2+ "=>" -> Just $ FConn Impl f1 f2+ "=" -> Just $ FConn And (FConn Impl f1 f2) (FConn Impl f2 f1)+ n+ | "bool_eq" `isPrefixOf` n -> Just $ FConn And (FConn Impl f1 f2) (FConn Impl f2 f1)+ | "bool_neq" `isPrefixOf` n -> Just $ FNot $ FConn And (FConn Impl f1 f2) (FConn Impl f2 f1)+ | "user_eq" `isPrefixOf` n -> Just $ FConn And (FConn Impl f1 f2) (FConn Impl f2 f1)+ _ -> Nothing+ -- Parse ite where it is used as an expression+ (_, _) ->+ case (op1, termToE op2 functionsWithInputsAndOutputs) of+ (LD.Application (LD.Variable "ite") [cond, thenTerm, elseTerm], Just e2) ->+ case parseFCompOp operator of+ Just fCompOp -> parseIte cond thenTerm elseTerm functionsWithInputsAndOutputs (Just (\e -> fCompOp e e2))+ Nothing -> Nothing+ (_, _) ->+ case (termToE op1 functionsWithInputsAndOutputs, op2) of+ (Just e1, LD.Application (LD.Variable "ite") [cond, thenTerm, elseTerm]) ->+ case parseFCompOp operator of+ Just fCompOp -> parseIte cond thenTerm elseTerm functionsWithInputsAndOutputs (Just (\e -> fCompOp e1 e))+ Nothing -> Nothing+ (_, _) -> Nothing++termToF (LD.Application (LD.Variable "ite") [cond, thenTerm, elseTerm]) functionsWithInputsAndOutputs = -- if-then-else operator with F types+ parseIte cond thenTerm elseTerm functionsWithInputsAndOutputs Nothing+termToF (LD.Variable "true") functionsWithInputsAndOutputs = Just FTrue+termToF (LD.Variable "false") functionsWithInputsAndOutputs = Just FFalse+termToF _ _ = Nothing++termToE :: LD.Expression -> [(String, ([String], String))] -> Maybe E+-- Parse 4 * atan(1) as Pi (used by our dReal SMT translator)+termToE (LD.Application (LD.Variable "*") [LD.Number 4, LD.Application (LD.Variable "atan") [LD.Number 1]]) functionsWithInputsAndOutputs = Just $ Pi+-- Symbols/Literals+termToE (LD.Variable "true") functionsWithInputsAndOutputs = Nothing -- These should be parsed to F+termToE (LD.Variable "false") functionsWithInputsAndOutputs = Nothing -- These should be parsed to F+termToE (LD.Variable var) functionsWithInputsAndOutputs = Just $ Var var+termToE (LD.Number num) functionsWithInputsAndOutputs = Just $ Lit num+-- one param PropaFP translator functions+-- RoundToInt+termToE (LD.Application (LD.Variable "to_int_rne") [p]) functionsWithInputsAndOutputs = RoundToInteger RNE <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "to_int_rtp") [p]) functionsWithInputsAndOutputs = RoundToInteger RTP <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "to_int_rtn") [p]) functionsWithInputsAndOutputs = RoundToInteger RTN <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "to_int_rtz") [p]) functionsWithInputsAndOutputs = RoundToInteger RTZ <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "to_int_rna") [p]) functionsWithInputsAndOutputs = RoundToInteger RNA <$> termToE p functionsWithInputsAndOutputs+-- Float32+termToE (LD.Application (LD.Variable "float32_rne") [p]) functionsWithInputsAndOutputs = Float32 RNE <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float32_rtp") [p]) functionsWithInputsAndOutputs = Float32 RTP <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float32_rtn") [p]) functionsWithInputsAndOutputs = Float32 RTN <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float32_rtz") [p]) functionsWithInputsAndOutputs = Float32 RTZ <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float32_rna") [p]) functionsWithInputsAndOutputs = Float32 RNA <$> termToE p functionsWithInputsAndOutputs+-- Float64+termToE (LD.Application (LD.Variable "float64_rne") [p]) functionsWithInputsAndOutputs = Float64 RNE <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float64_rtp") [p]) functionsWithInputsAndOutputs = Float64 RTP <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float64_rtn") [p]) functionsWithInputsAndOutputs = Float64 RTN <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float64_rtz") [p]) functionsWithInputsAndOutputs = Float64 RTZ <$> termToE p functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "float64_rna") [p]) functionsWithInputsAndOutputs = Float64 RNA <$> termToE p functionsWithInputsAndOutputs+-- one param functions+termToE (LD.Application (LD.Variable operator) [op]) functionsWithInputsAndOutputs =+ case termToE op functionsWithInputsAndOutputs of+ Nothing -> Nothing+ Just e -> case operator of+ n+ | (n =~ "^real_pi$|^real_pi[0-9]+$" :: Bool) -> Just Pi+ | (n =~ "^abs$|^abs[0-9]+$" :: Bool) -> Just $ EUnOp Abs e+ | (n =~ "^sin$|^sin[0-9]+$|^real_sin$|^real_sin[0-9]+$" :: Bool) -> Just $ EUnOp Sin e+ | (n =~ "^cos$|^cos[0-9]+$|^real_cos$|^real_cos[0-9]+$" :: Bool) -> Just $ EUnOp Cos e+ | (n =~ "^sqrt$|^sqrt[0-9]+$|^real_square_root$|^real_square_root[0-9]+$" :: Bool) -> Just $ EUnOp Sqrt e+ | (n =~ "^fp.to_real$|^fp.to_real[0-9]+$|^to_real$|^to_real[0-9]+$" :: Bool) -> Just e+ "-" -> Just $ EUnOp Negate e+ -- SPARK Reals functions+ "from_int" -> Just e+ -- Some to_int functions. different suffixes (1, 2, etc.)+ -- e.g. In one file, to_int1 :: Float -> Int+ -- to_int2 :: Bool -> Int+ -- Are these suffixes consistent?+ -- Float functions+ "fp.abs" -> Just $ EUnOp Abs e+ "fp.neg" -> Just $ EUnOp Negate e+ -- "fp.to_real" -> Just e+ -- "to_real" -> Just e+ -- "value" -> Just e+ -- Undefined functions+ "fp.isNormal" -> Nothing+ "fp.isSubnormal" -> Nothing+ "fp.isZero" -> Nothing+ "fp.isNaN" -> Nothing+ "fp.isPositive" -> Nothing+ "fp.isNegative" -> Nothing+ "fp.isIntegral32" -> Nothing+ "fp.isIntegral64" -> Nothing+ _ -> Nothing+ where+ deriveTypeForOneArgFunctions :: String -> (E -> E) -> E -> Maybe E+ deriveTypeForOneArgFunctions functionName functionAsExpression functionArg =+ -- case lookup functionName functionsWithInputsAndOutputs of+ -- Just ([inputType], outputType) ->+ let+ (mInputTypes, mOutputType) = unzip $ lookup functionName functionsWithInputsAndOutputs+ -- case lookup functionName functionsWithInputsAndOutputs of+ -- Just (inputTypes, outputType) -> (Just inputTypes, Just outputType)+ -- Nothing -> (Nothing, Nothing)++ newFunctionArg = functionArg+ -- case mInputTypes of+ -- Just [inputType] ->+ -- case inputType of+ -- -- "Float32" -> Float32 RNE functionArg+ -- -- "Float64" -> Float64 RNE functionArg+ -- _ -> functionArg -- Do not deal with multiple param args for one param functions. TODO: Check if these can occur, i.e. something like RoundingMode Float32++ mNewFunctionAsExpression =+ case mOutputType of+ Just outputType ->+ case outputType of+ -- "Float32" -> Float32 RNE . functionAsExpression -- TODO: Make these Nothing if we can't deal with them+ -- "Float64" -> Float64 RNE . functionAsExpression -- TODO: Make these Nothing if we can't deal with them+ "Real" -> Just functionAsExpression --FIXME: Should match on other possible names. Real/real Int/int/integer, etc. I've only seen these alt names in function definitions/axioms, not assertions, but would still be more safe.+ "Int" -> Just functionAsExpression -- FIXME: Round here?+ _ -> Nothing -- These should be floats, which we cannot deal with for now+ Nothing -> Just functionAsExpression -- No type given, assume real+ in+ case mNewFunctionAsExpression of+ Just newFunctionAsExpression -> Just $ newFunctionAsExpression newFunctionArg+ Nothing -> Nothing+ -- Nothing -> functionAsExpression functionArg+-- two param PropaFP translator functions+termToE (LD.Application (LD.Variable "min") [p1, p2]) functionsWithInputsAndOutputs = EBinOp Min <$> termToE p1 functionsWithInputsAndOutputs <*> termToE p2 functionsWithInputsAndOutputs+termToE (LD.Application (LD.Variable "max") [p1, p2]) functionsWithInputsAndOutputs = EBinOp Max <$> termToE p1 functionsWithInputsAndOutputs <*> termToE p2 functionsWithInputsAndOutputs+-- two param functions +-- params are either two different E types, or one param is a rounding mode and another is the arg+termToE (LD.Application (LD.Variable operator) [op1, op2]) functionsWithInputsAndOutputs =+ case (parseRoundingMode op1, termToE op2 functionsWithInputsAndOutputs) of+ (Just roundingMode, Just e) ->+ case operator of+ n+ | (n =~ "^round$|^round[0-9]+$" :: Bool) -> Just $ Float roundingMode e --FIXME: remove this? not used with cvc4 driver?+ | (n =~ "^to_int$|^to_int[0-9]+$" :: Bool) -> Just $ RoundToInteger roundingMode e+ | (n =~ "^of_int$|^of_int[0-9]+$" :: Bool) ->+ case lookup n functionsWithInputsAndOutputs of+ Just (_, outputType) ->+ case outputType of+ o -- Why3 will type check that the input is an integer, making these safe+ | o `elem` ["Float32", "single"] -> Just $ Float32 roundingMode e+ | o `elem` ["Float64", "double"] -> Just $ Float64 roundingMode e+ | o `elem` ["Real", "real"] -> Just e+ _ -> Nothing+ _ -> Nothing+ "fp.roundToIntegral" -> Just $ RoundToInteger roundingMode e+ _ -> Nothing+ _ ->+ case (termToE op1 functionsWithInputsAndOutputs, termToE op2 functionsWithInputsAndOutputs) of+ (Just e1, Just e2) ->+ case operator of+ n+ -- "o..." functions are from SPARK Reals+ | n `elem` ["+", "oadd", "oadd__logic"] -> Just $ EBinOp Add e1 e2+ | n `elem` ["-", "osubtract", "osubtract__logic"] -> Just $ EBinOp Sub e1 e2+ | n `elem` ["*", "omultiply", "omultiply__logic"] -> Just $ EBinOp Mul e1 e2+ | n `elem` ["/", "odivide", "odivide__logic"] -> Just $ EBinOp Div e1 e2+ | (n =~ "^pow$|^pow[0-9]+$|^power$|^power[0-9]+$" :: Bool) -> Just $ EBinOp Pow e1 e2 --FIXME: remove int pow? only use int pow if actually specified?+ | n == "^" -> Just $ EBinOp Pow e1 e2+ -- case lookup n functionsWithInputsAndOutputs of+ -- Just (["Real", "Real"], "Real") -> Just $ EBinOp Pow e1 e2+ -- Just ([input1, "Int"], output) ->+ -- let+ -- mExactPowExpression =+ -- if input1 == "Int" || input1 == "Real"+ -- then case e2 of+ -- Lit l2 -> if denominator l2 == 1.0 then Just $ PowI e1 (numerator l2) else Just $ EBinOp Pow e1 e2+ -- _ -> Just $ EBinOp Pow e1 e2+ -- else Nothing+ -- in case mExactPowExpression of+ -- Just exactPowExpression -> case output of+ -- "Real" -> Just exactPowExpression+ -- "Int" -> Just $ RoundToInteger RNE exactPowExpression++ -- _ -> Nothing+ -- Nothing -> Nothing+ -- Nothing -> -- No input/output, treat as real pow+ -- case e2 of+ -- Lit l2 -> if denominator l2 == 1.0 then Just $ PowI e1 (numerator l2) else Just $ EBinOp Pow e1 e2+ -- _ -> Just $ EBinOp Pow e1 e2+ -- _ -> Nothing+ | (n =~ "^mod$|^mod[0-9]+$" :: Bool) -> Just $ EBinOp Mod e1 e2+ -- case lookup n functionsWithInputsAndOutputs of+ -- Just (["Real", "Real"], "Real") -> Just $ EBinOp Mod e1 e2+ -- Just (["Int", "Int"], "Int") -> Just $ RoundToInteger RNE $ EBinOp Mod e1 e2 --TODO: might be worth implementing Int Mod+ -- -- No input/output, treat as real mod+ -- Nothing -> Just $ EBinOp Mod e1 e2+ -- _ -> Nothing+ _ -> Nothing+ (_, _) -> Nothing++-- Float bits to Rational+termToE (LD.Application (LD.Variable "fp") [LD.Variable sSign, LD.Variable sExponent, LD.Variable sMantissa]) functionsWithInputsAndOutputs =+ let+ bSign = drop 2 sSign+ bExponent = drop 2 sExponent+ bMantissa = drop 2 sMantissa++ bFull = bSign ++ bExponent ++ bMantissa++ -- Read a string of Bits ('1' or '0') where the first digit is the most significant+ -- The digit parameter denotes the current digit, should be equal to length of the first param at all times+ readBits :: String -> Integer -> Integer+ readBits [] _ = 0+ readBits (bit : bits) digit = digitToInt bit * (2 ^ (digit - 1)) + readBits bits (digit - 1)++ bitsToWord8 :: String -> [Word8]+ bitsToWord8 bits =+ let wordS = take 8 bits+ rem = drop 8 bits+ wordV = readBits wordS 8+ in+ P.fromInteger wordV : bitsToWord8 rem++ bsFloat = B.pack $ bitsToWord8 bFull+ in+ if all (`elem` "01") bFull+ then+ case length bFull of+ 32 -> Just $ Lit $ toRational $ runGet getFloatbe bsFloat+ 64 -> Just $ Lit $ toRational $ runGet getDoublebe bsFloat+ -- 32 -> Just $ Float32 RNE $ Lit $ toRational $ runGet getFloatbe bsFloat + -- 64 -> Just $ Float64 RNE $ Lit $ toRational $ runGet getDoublebe bsFloat+ _ -> Nothing+ else Nothing++-- Float functions, three params. Other three param functions should be placed before here+termToE (LD.Application (LD.Variable operator) [roundingMode, op1, op2]) functionsWithInputsAndOutputs =+ -- case operator of+ -- -- SPARK Reals+ -- "fp.to_real" -> Nothing + -- _ -> -- Known ops+ case (termToE op1 functionsWithInputsAndOutputs, termToE op2 functionsWithInputsAndOutputs) of+ (Just e1, Just e2) ->+ case parseRoundingMode roundingMode of -- Floating-point ops+ Just mode ->+ case operator of+ "fp.add" -> Just $ Float mode $ EBinOp Add e1 e2+ "fp.sub" -> Just $ Float mode $ EBinOp Sub e1 e2+ "fp.mul" -> Just $ Float mode $ EBinOp Mul e1 e2+ "fp.div" -> Just $ Float mode $ EBinOp Div e1 e2+ _ -> Nothing+ Nothing -> Nothing+ (_, _) -> Nothing+termToE _ _ = Nothing++collapseOrs :: [LD.Expression] -> [LD.Expression]+collapseOrs = map collapseOr++collapseOr :: LD.Expression -> LD.Expression+collapseOr orig@(LD.Application (LD.Variable "or") [LD.Application (LD.Variable "<") args1, LD.Application (LD.Variable "=") args2]) =+ if args1 P.== args2+ then LD.Application (LD.Variable "<=") args1+ else orig+collapseOr orig@(LD.Application (LD.Variable "or") [LD.Application (LD.Variable "=") args1, LD.Application (LD.Variable "<") args2]) =+ if args1 P.== args2+ then LD.Application (LD.Variable "<=") args1+ else orig+collapseOr orig@(LD.Application (LD.Variable "or") [LD.Application (LD.Variable ">") args1, LD.Application (LD.Variable "=") args2]) =+ if args1 P.== args2+ then LD.Application (LD.Variable ">=") args1+ else orig+collapseOr orig@(LD.Application (LD.Variable "or") [LD.Application (LD.Variable "=") args1, LD.Application (LD.Variable ">") args2]) =+ if args1 P.== args2+ then LD.Application (LD.Variable ">=") args1+ else orig+collapseOr (LD.Application operator args) = LD.Application operator (collapseOrs args)+collapseOr e = e++-- |Replace function guards which are known to be always true with true.+eliminateKnownFunctionGuards :: [LD.Expression] -> [LD.Expression]+eliminateKnownFunctionGuards = map eliminateKnownFunctionGuard++-- |Replace function guard which is known to be always true with true.+eliminateKnownFunctionGuard :: LD.Expression -> LD.Expression+eliminateKnownFunctionGuard orig@(LD.Application operator@(LD.Variable var) args@(guardedFunction : _)) =+ let+ knownGuardsRegex = + "^real_sin__function_guard$|^real_sin__function_guard[0-9]+$|" +++ "^real_cos__function_guard$|^real_cos__function_guard[0-9]+$|" +++ "^real_square_root__function_guard$|^real_square_root__function_guard[0-9]+$|" +++ "^real_pi__function_guard$|^real_pi__function_guard[0-9]+$"+ in+ if (var =~ knownGuardsRegex :: Bool)+ then LD.Variable "true"+ else LD.Application operator (eliminateKnownFunctionGuards args)+eliminateKnownFunctionGuard (LD.Application operator args) = LD.Application operator (eliminateKnownFunctionGuards args)+eliminateKnownFunctionGuard e = e++termsToF :: [LD.Expression] -> [(String, ([String], String))] -> [F]+termsToF es fs = mapMaybe (`termToF` fs) es++determineFloatTypeE :: E -> [(String, String)] -> Maybe E+determineFloatTypeE (EBinOp op e1 e2) varTypeMap = case determineFloatTypeE e1 varTypeMap of+ Just p1 ->+ case determineFloatTypeE e2 varTypeMap of+ Just p2 -> Just $ EBinOp op p1 p2+ Nothing -> Nothing+ Nothing -> Nothing+determineFloatTypeE (EUnOp op e) varTypeMap = case determineFloatTypeE e varTypeMap of+ Just p -> Just $ EUnOp op p+ Nothing -> Nothing+determineFloatTypeE (PowI e i) varTypeMap = case determineFloatTypeE e varTypeMap of+ Just p -> Just $ PowI p i+ Nothing -> Nothing+determineFloatTypeE (Float r e) varTypeMap = case mVariableType of+ Just variableType ->+ case variableType of+ t+ | t `elem` ["Float32", "single"] ->+ case determineFloatTypeE e varTypeMap of+ Just p -> Just $ Float32 r p+ Nothing -> Nothing+ | t `elem` ["Float64", "double"] ->+ case determineFloatTypeE e varTypeMap of+ Just p -> Just $ Float64 r p+ Nothing -> Nothing+ _ -> Nothing+ Nothing -> Nothing+ where+ allVars = findVariablesInExpressions e+ knownVarsWithPrecision = knownFloatVars e+ knownVars = map fst knownVarsWithPrecision+ unknownVars = filter (`notElem` knownVars) allVars+ mVariableType = findVariableType unknownVars varTypeMap knownVarsWithPrecision Nothing+determineFloatTypeE (Float32 r e) varTypeMap = case determineFloatTypeE e varTypeMap of+ Just p -> Just $ Float32 r p+ Nothing -> Nothing+determineFloatTypeE (Float64 r e) varTypeMap = case determineFloatTypeE e varTypeMap of+ Just p -> Just $ Float64 r p+ Nothing -> Nothing+determineFloatTypeE (RoundToInteger r e) varTypeMap = case determineFloatTypeE e varTypeMap of+ Just p -> Just $ RoundToInteger r p+ Nothing -> Nothing+determineFloatTypeE Pi _ = Just Pi+determineFloatTypeE (Var v) varTypeMap = case lookup v varTypeMap of+ Just variableType ->+ case variableType of+ -- t+ -- | t `elem` ["Float32", "single"] -> Just $ Float32 RNE $ Var v+ -- | t `elem` ["Float64", "double"] -> Just $ Float64 RNE $ Var v+ _ -> Just $ Var v -- It is safe to treat integers and rationals as reals+ _ -> Just $ Var v+determineFloatTypeE (Lit n) _ = Just $ Lit n++-- |Tries to determine whether a Float operation is single or double precision+-- by searching for the type of all variables appearing in the function. If the+-- types match and are all either Float32/Float64, we can determine the type.+determineFloatTypeF :: F -> [(String, String)] -> Maybe F+determineFloatTypeF (FComp op e1 e2) varTypeMap = case (determineFloatTypeE e1 varTypeMap, determineFloatTypeE e2 varTypeMap) of+ (Just p1, Just p2) -> Just $ FComp op p1 p2+ (_, _) -> Nothing+determineFloatTypeF (FConn op f1 f2) varTypeMap = case (determineFloatTypeF f1 varTypeMap, determineFloatTypeF f2 varTypeMap) of+ (Just p1, Just p2) -> Just $ FConn op p1 p2+ (_, _) -> Nothing+determineFloatTypeF (FNot f) varTypeMap = case determineFloatTypeF f varTypeMap of+ Just p -> Just $ FNot p+ Nothing -> Nothing+determineFloatTypeF FTrue _ = Just FTrue+determineFloatTypeF FFalse _ = Just FFalse++-- |Find the type for the given variables+-- Type is looked for in the supplied map+-- If all found types match, return this type+findVariableType :: [String] -> [(String, String)] -> [(String, Integer)] -> Maybe String -> Maybe String+findVariableType [] _ [] mFoundType = mFoundType+findVariableType [] _ ((_, precision) : vars) mFoundType =+ case mFoundType of+ Just t ->+ if (t `elem` ["Float32", "single"] && precision == 32) || ((t `elem` ["Float64", "double"]) && (precision == 64))+ then findVariableType [] [] vars mFoundType+ else Nothing+ Nothing ->+ case precision of+ 32 -> findVariableType [] [] vars (Just "Float32")+ 64 -> findVariableType [] [] vars (Just "Float64")+ _ -> Nothing++findVariableType (v: vs) varTypeMap knownVarsWithPrecision mFoundType =+ case lookup v varTypeMap of+ Just t ->+ if "Int" `isPrefixOf` t then+ findVariableType vs varTypeMap knownVarsWithPrecision mFoundType+ else+ case mFoundType of+ Just f -> if f == t then findVariableType vs varTypeMap knownVarsWithPrecision (Just t) else Nothing+ Nothing -> findVariableType vs varTypeMap knownVarsWithPrecision (Just t)+ Nothing -> Nothing++knownFloatVars :: E -> [(String, Integer)]+knownFloatVars e = removeConflictingVars . nub $ findAllFloatVars e+ where+ removeConflictingVars :: [(String, Integer)] -> [(String, Integer)]+ removeConflictingVars [] = []+ removeConflictingVars ((v, t) : vs) =+ if v `elem` map fst vs+ then removeConflictingVars $ filter (\(v', _) -> v /= v') vs+ else (v, t) : removeConflictingVars vs++ findAllFloatVars (EBinOp _ e1 e2) = knownFloatVars e1 ++ knownFloatVars e2+ findAllFloatVars (EUnOp _ e) = knownFloatVars e+ findAllFloatVars (PowI e _) = knownFloatVars e+ findAllFloatVars (Float _ e) = knownFloatVars e+ findAllFloatVars (Float32 _ (Var v)) = [(v, 32)]+ findAllFloatVars (Float64 _ (Var v)) = [(v, 64)]+ findAllFloatVars (Float32 _ e) = knownFloatVars e+ findAllFloatVars (Float64 _ e) = knownFloatVars e+ findAllFloatVars (RoundToInteger _ e) = knownFloatVars e+ findAllFloatVars (Var _) = []+ findAllFloatVars (Lit _) = []+ findAllFloatVars Pi = []++findVariablesInFormula :: F -> [String]+findVariablesInFormula f = nub $ findVars f+ where+ findVars (FConn _ f1 f2) = findVars f1 ++ findVars f2+ findVars (FComp _ e1 e2) = findVariablesInExpressions e1 ++ findVariablesInExpressions e2+ findVars (FNot f1) = findVars f1+ findVars FTrue = []+ findVars FFalse = []++findVariablesInExpressions :: E -> [String]+findVariablesInExpressions (EBinOp _ e1 e2) = findVariablesInExpressions e1 ++ findVariablesInExpressions e2+findVariablesInExpressions (EUnOp _ e) = findVariablesInExpressions e+findVariablesInExpressions (PowI e _) = findVariablesInExpressions e+findVariablesInExpressions (Float _ e) = findVariablesInExpressions e+findVariablesInExpressions (Float32 _ e) = findVariablesInExpressions e+findVariablesInExpressions (Float64 _ e) = findVariablesInExpressions e+findVariablesInExpressions (RoundToInteger _ e) = findVariablesInExpressions e+findVariablesInExpressions (Var v) = [v]+findVariablesInExpressions (Lit _) = []+findVariablesInExpressions Pi = []++parseRoundingMode :: LD.Expression -> Maybe RoundingMode+parseRoundingMode (LD.Variable mode) =+ case mode of+ m+ | m `elem` ["RNE", "NearestTiesToEven"] -> Just RNE+ | m `elem` ["RTP", "Up"] -> Just RTP+ | m `elem` ["RTN", "Down"] -> Just RTN+ | m `elem` ["RTZ", "ToZero"] -> Just RTZ+ | m `elem` ["RNA"] -> Just RNA+ _ -> Nothing+parseRoundingMode _ = Nothing++-- |Process a parsed list of expressions to a VC. +-- +-- If the parsing mode is Why3, everything in the context implies the goal (empty context means we only have a goal). +-- If the goal cannot be parsed, we return Nothing.+-- +-- If the parsing mode is CNF, parse all assertions into a CNF. If any assertion cannot be parsed, return Nothing.+-- If any assertion contains Floats, return Nothing.+processVC :: [LD.Expression] -> Maybe (F, [(String, String)])+processVC parsedExpressions =+ Just (foldAssertionsF assertionsF, variablesWithTypes)+ where+ assertions = findAssertions parsedExpressions+ assertionsF = mapMaybe (`determineFloatTypeF` variablesWithTypes) $ (termsToF . eliminateKnownFunctionGuards . collapseOrs) assertions functionsWithInputsAndOutputs++ variablesWithTypes = findVariables parsedExpressions+ functionsWithInputsAndOutputs = findFunctionInputsAndOutputs parsedExpressions++ foldAssertionsF :: [F] -> F+ foldAssertionsF [] = error "processVC - foldAssertionsF: Empty list given"+ foldAssertionsF [f] = f+ foldAssertionsF (f : fs) = FConn And f (foldAssertionsF fs)++-- |Looks for pi vars (vars named pi/pi{i} where {i} is some integer) and symbolic bounds.+-- If the bounds are better than those given to the real pi in Why3, replace the variable with exact pi.+symbolicallySubstitutePiVars :: F -> F+symbolicallySubstitutePiVars f = substVarsWithPi piVars f+ where+ piVars = nub (aux f)++ substVarsWithPi :: [String] -> F -> F+ substVarsWithPi [] f' = f'+ substVarsWithPi (v : _) f' = substVarFWithE v f' Pi++ aux :: F -> [String]+ aux (FConn And f1 f2) = aux f1 ++ aux f2+ aux (FComp Lt (EBinOp Div (Lit numer) (Lit denom)) (Var var)) =+ [var | + -- If variable is pi or pi# where # is a number+ (var =~ "^pi$|^pi[0-9]+$" :: Bool) &&+ -- And bounds are equal or better than the bounds given by Why3 for Pi+ lb >= (7074237752028440.0 / 2251799813685248.0) &&+ hasUB var f]+ where+ lb = numer / denom+ aux (FComp {}) = []+ aux (FConn {}) = []+ aux (FNot _) = []+ aux FTrue = []+ aux FFalse = []++ hasUB :: String -> F -> Bool+ hasUB piVar (FComp Lt (Var otherVar) (EBinOp Div (Lit numer) (Lit denom))) = + piVar == otherVar && ub <= (7074237752028441.0 / 2251799813685248.0)+ where+ ub = numer / denom+ hasUB piVar (FConn And f1 f2) = hasUB piVar f1 || hasUB piVar f2+ hasUB _ (FComp {}) = False+ hasUB _ (FConn {}) = False+ hasUB _ (FNot _) = False+ hasUB _ FTrue = False+ hasUB _ FFalse = False+++-- |Derive ranges for a VC (Implication where a CNF implies a goal)+-- Remove anything which refers to a variable for which we cannot derive ranges+-- If the goal contains underivable variables, return Nothing+deriveVCRanges :: F -> [(String, String)] -> Maybe (F, TypedVarMap)+deriveVCRanges vc varsWithTypes =+ case filterOutVars simplifiedF underivableVariables False of+ Just filteredF -> Just (filteredF, safelyRoundTypedVarMap typedDerivedVarMap)+ Nothing -> Nothing+ where+ integerVariables = findIntegerVariables varsWithTypes++ (simplifiedFUnchecked, derivedVarMapUnchecked, underivableVariables) = deriveBoundsAndSimplify vc++ -- (piVars, derivedVarMap) = findRealPiVars derivedVarMapUnchecked+ (piVars, derivedVarMap) = ([], derivedVarMapUnchecked)++ typedDerivedVarMap = unsafeVarMapToTypedVarMap derivedVarMap integerVariables++ -- safelyRoundTypedVarMap = id+ safelyRoundTypedVarMap [] = []+ safelyRoundTypedVarMap ((TypedVar (varName, (leftBound, rightBound)) Real) : vars) =+ let+ leftBoundRoundedDown = rational . fst . endpoints $ mpBallP (prec 23) leftBound+ rightBoundRoundedUp = rational . snd . endpoints $ mpBallP (prec 23) rightBound+ newBound = TypedVar (varName, (leftBoundRoundedDown, rightBoundRoundedUp)) Real+ in+ newBound : safelyRoundTypedVarMap vars+ safelyRoundTypedVarMap (vi@(TypedVar _ Integer) : vars) = vi : safelyRoundTypedVarMap vars++ -- simplifiedF = substVarsWithPi piVars simplifiedFUnchecked+ simplifiedF = simplifiedFUnchecked++ -- TODO: Would be good to include a warning when this happens+ -- Could also make this an option+ -- First elem are the variables which can be assumed to be real pi+ -- Second elem is the varMap without the real pi vars+ findRealPiVars :: VarMap -> ([String], VarMap)+ findRealPiVars [] = ([], [])+ findRealPiVars (varWithBounds@(var, (l, r)) : vars) =+ if+ -- If variable is pi or pi# where # is a number+ (var =~ "^pi$|^pi[0-9]+$" :: Bool) &&+ -- And bounds are equal or better than the bounds given by Why3 for Pi+ l >= (7074237752028440.0 / 2251799813685248.0) && r <= (7074237752028441.0 / 2251799813685248.0) &&+ -- And the type of the variable is Real+ (lookup var varsWithTypes == Just "Real")+ then (\(foundPiVars, varMapWithoutPi) -> ((var : foundPiVars), varMapWithoutPi)) $ findRealPiVars vars+ else (\(foundPiVars, varMapWithoutPi) -> (foundPiVars, (varWithBounds : varMapWithoutPi))) $ findRealPiVars vars++ substVarsWithPi :: [String] -> F -> F+ substVarsWithPi [] f = f+ substVarsWithPi (v : _) f = substVarFWithE v f Pi+++ -- |Safely filter our terms that contain underivable variables.+ -- Need to preserve unsat terms, so we can safely remove x in FConn And x y if x contains underivable variables.+ -- We cannot safely remove x from FConn Or x y if x contains underivable variables+ -- (since x may be sat and y may be unsat, filtering out x would give an incorrect unsat result), so we remove the whole term+ -- Reverse logic as appropriate when a term is negated+ filterOutVars :: F -> [String] -> Bool -> Maybe F+ filterOutVars (FConn And f1 f2) vars False =+ case (filterOutVars f1 vars False, filterOutVars f2 vars False) of+ (Just ff1, Just ff2) -> Just $ FConn And ff1 ff2+ (Just ff1, _) -> Just ff1+ (_, Just ff2) -> Just ff2+ (_, _) -> Nothing+ filterOutVars (FConn Or f1 f2) vars False =+ case (filterOutVars f1 vars False, filterOutVars f2 vars False) of+ (Just ff1, Just ff2) -> Just $ FConn Or ff1 ff2+ (_, _) -> Nothing+ filterOutVars (FConn Impl f1 f2) vars False =+ case (filterOutVars f1 vars False, filterOutVars f2 vars False) of+ (Just ff1, Just ff2) -> Just $ FConn Impl ff1 ff2+ (_, _) -> Nothing+ filterOutVars (FConn And f1 f2) vars True =+ case (filterOutVars f1 vars True, filterOutVars f2 vars True) of+ (Just ff1, Just ff2) -> Just $ FConn And ff1 ff2+ (_, _) -> Nothing+ filterOutVars (FConn Or f1 f2) vars True =+ case (filterOutVars f1 vars True, filterOutVars f2 vars True) of+ (Just ff1, Just ff2) -> Just $ FConn Or ff1 ff2+ (Just ff1, _) -> Just ff1+ (_, Just ff2) -> Just ff2+ (_, _) -> Nothing+ filterOutVars (FConn Impl f1 f2) vars True =+ case (filterOutVars f1 vars True, filterOutVars f2 vars True) of+ (Just ff1, Just ff2) -> Just $ FConn Impl ff1 ff2+ (Just ff1, _) -> Just ff1+ (_, Just ff2) -> Just ff2+ (_, _) -> Nothing+ filterOutVars (FNot f) vars isNegated = FNot <$> filterOutVars f vars (not isNegated)++ filterOutVars (FComp op e1 e2) vars _isNegated =+ if eContainsVars vars e1 || eContainsVars vars e2+ then Nothing+ else Just (FComp op e1 e2)++ filterOutVars FTrue _ _ = Just FTrue+ filterOutVars FFalse _ _ = Just FFalse++eContainsVars :: [String] -> E -> Bool+eContainsVars vars (Var var) = var `elem` vars+eContainsVars _ (Lit _) = False+eContainsVars _ Pi = False++eContainsVars vars (EBinOp _ e1 e2) = eContainsVars vars e1 || eContainsVars vars e2+eContainsVars vars (EUnOp _ e) = eContainsVars vars e+eContainsVars vars (PowI e _) = eContainsVars vars e+eContainsVars vars (Float32 _ e) = eContainsVars vars e+eContainsVars vars (Float64 _ e) = eContainsVars vars e+eContainsVars vars (Float _ e) = eContainsVars vars e+eContainsVars vars (RoundToInteger _ e) = eContainsVars vars e++fContainsVars :: [String] -> F -> Bool+fContainsVars vars (FConn _ f1 f2) = fContainsVars vars f1 || fContainsVars vars f2+fContainsVars vars (FComp _ e1 e2) = eContainsVars vars e1 || eContainsVars vars e2+fContainsVars vars (FNot f) = fContainsVars vars f+fContainsVars _ FTrue = False+fContainsVars _ FFalse = False++inequalityEpsilon :: Rational+inequalityEpsilon = 0.000000001+-- inequalityEpsilon = 1/(2^23)++findVarEqualities :: F -> [(String, E)]+findVarEqualities (FConn And f1 f2) = findVarEqualities f1 ++ findVarEqualities f2+findVarEqualities FConn {} = []+findVarEqualities (FComp Eq (Var v) e2) = [(v, e2)]+findVarEqualities (FComp Eq e1 (Var v)) = [(v, e1)]+findVarEqualities FComp {} = []+findVarEqualities (FNot _) = [] -- Not EQ, means we can't do anything here?+findVarEqualities FTrue = []+findVarEqualities FFalse = []++-- |Filter out var equalities which rely on themselves+filterOutCircularVarEqualities :: [(String, E)] -> [(String, E)]+filterOutCircularVarEqualities = filter (\(v, e) -> v `notElem` findVariablesInExpressions e)++-- |Filter out var equalities which occur multiple times by choosing the var equality with the smallest length+filterOutDuplicateVarEqualities :: [(String, E)] -> [(String, E)]+filterOutDuplicateVarEqualities [] = []+filterOutDuplicateVarEqualities ((v, e) : vs) =+ case partition (\(v',_) -> v == v') vs of+ ([], _) -> (v, e) : filterOutDuplicateVarEqualities vs+ (matchingEqualities, otherEqualities) ->+ let shortestVarEquality = head $ sortBy (\(_, e1) (_, e2) -> P.compare (lengthE e1) (lengthE e2)) $ (v, e) : matchingEqualities+ in shortestVarEquality : filterOutDuplicateVarEqualities otherEqualities++-- FIXME: subst one at a time+substAllEqualities :: F -> F+substAllEqualities = recursivelySubstVars+ where+ recursivelySubstVars f@(FConn Impl context _) =+ case filteredVarEqualities of+ [] -> f+ _ -> if f P.== substitutedF then f else recursivelySubstVars . simplifyF $ substitutedF -- TODO: make this a var+ where+ substitutedF = substVars filteredVarEqualities f+ filteredVarEqualities = (filterOutDuplicateVarEqualities . filterOutCircularVarEqualities) varEqualities+ varEqualities = findVarEqualities context++ recursivelySubstVars f =+ case filteredVarEqualities of+ [] -> f+ _ -> if f P.== substitutedF then f else recursivelySubstVars . simplifyF $ substitutedF+ where+ substitutedF = substVars filteredVarEqualities f+ filteredVarEqualities = (filterOutDuplicateVarEqualities . filterOutCircularVarEqualities) varEqualities+ varEqualities = findVarEqualities f++ substVars [] f = f+ substVars ((v, e) : _) f = substVarFWithE v f e++addVarMapBoundsToF :: F -> TypedVarMap -> F+addVarMapBoundsToF f [] = f+addVarMapBoundsToF f (TypedVar (v, (l, r)) _ : vm) = FConn And boundAsF $ addVarMapBoundsToF f vm+ where+ boundAsF = FConn And (FComp Ge (Var v) (Lit l)) (FComp Le (Var v) (Lit r))++eliminateFloatsAndSimplifyVC :: F -> TypedVarMap -> Bool -> FilePath -> IO F+eliminateFloatsAndSimplifyVC vc typedVarMap strengthenVC fptaylorPath =+ do+ vcWithoutFloats <- eliminateFloatsF vc (typedVarMapToVarMap typedVarMap) strengthenVC fptaylorPath+ let typedVarMapAsMap = M.fromList $ map (\(TypedVar (varName, (leftBound, rightBound)) _) -> (varName, (Just leftBound, Just rightBound))) typedVarMap+ let simplifiedVCWithoutFloats = (simplifyF . evalF_comparisons typedVarMapAsMap) vcWithoutFloats+ return simplifiedVCWithoutFloats++parseVCToF :: FilePath -> FilePath -> IO (Maybe (F, TypedVarMap))+parseVCToF filePath fptaylorPath =+ do+ parsedFile <- parseSMT2 filePath++ case processVC parsedFile of+ Just (vc, varTypes) ->+ let+ simplifiedVC = (symbolicallySubstitutePiVars . substAllEqualities . simplifyF) vc+ mDerivedVCWithRanges = deriveVCRanges simplifiedVC varTypes+ in+ case mDerivedVCWithRanges of+ Just (derivedVC, derivedRanges) ->+ do+ -- The file we are given is assumed to be a contradiction, so weaken the VC+ let strengthenVC = False+ vcWithoutFloats <- eliminateFloatsF derivedVC (typedVarMapToVarMap derivedRanges) strengthenVC fptaylorPath+ let vcWithoutFloatsWithBounds = addVarMapBoundsToF vcWithoutFloats derivedRanges+ case deriveVCRanges vcWithoutFloatsWithBounds varTypes of+ Just (simplifiedVCWithoutFloats, finalDerivedRanges) -> return $ Just (simplifiedVCWithoutFloats, finalDerivedRanges)+ Nothing -> error "Error deriving bounds again after floating-point elimination"+ Nothing -> return Nothing+ Nothing -> return Nothing++parseVCToSolver :: FilePath -> FilePath -> (F -> TypedVarMap -> String) -> Bool -> IO (Maybe String)+parseVCToSolver filePath fptaylorPath proverTranslator negateVC =+ do+ parsedFile <- parseSMT2 filePath++ case processVC parsedFile of+ Just (vc, varTypes) ->+ let+ simplifiedVC = (substAllEqualities . simplifyF) vc+ mDerivedVCWithRanges = deriveVCRanges simplifiedVC varTypes+ in+ case mDerivedVCWithRanges of+ Just (derivedVC, derivedRanges) ->+ do+ let strengthenVC = False+ vcWithoutFloats <- eliminateFloatsF derivedVC (typedVarMapToVarMap derivedRanges) strengthenVC fptaylorPath+ let vcWithoutFloatsWithBounds = addVarMapBoundsToF vcWithoutFloats derivedRanges+ case deriveVCRanges vcWithoutFloatsWithBounds varTypes of+ Just (simplifiedVCWithoutFloats, finalDerivedRanges) ->+ return $ Just (+ proverTranslator+ (+ if negateVC+ then+ case simplifiedVCWithoutFloats of+ FNot f -> f -- Eliminate double not+ _ -> FNot simplifiedVCWithoutFloats+ else simplifiedVCWithoutFloats+ )+ finalDerivedRanges+ )+ Nothing -> error "Error deriving bounds again after floating-point elimination"+ -- return $ Just (proverTranslator (if negateVC then simplifyF (FNot simplifiedVCWithoutFloats) else simplifiedVCWithoutFloats) derivedRanges)+ Nothing -> return Nothing+ Nothing -> return Nothing
+ src/PropaFP/Translators/BoxFun.hs view
@@ -0,0 +1,74 @@+module PropaFP.Translators.BoxFun where++import MixedTypesNumPrelude++import AERN2.AD.Differential+import AERN2.BoxFun.Type+import AERN2.BoxFun.TestFunctions (fromListDomain)+import PropaFP.Expression+import PropaFP.VarMap+import AERN2.MP.Ball+import AERN2.MP.Float+import qualified AERN2.Linear.Vector.Type as V+import qualified Prelude as P+import Data.List+import Numeric.CollectErrors+import PropaFP.DeriveBounds+++expressionToBoxFun :: E -> VarMap -> Precision -> BoxFun+expressionToBoxFun expression domain p =+ BoxFun+ (fromIntegral (Data.List.length domain))+ (expressionToDifferential expression)+ vectorDomain+ where++ expressionToDifferential2 :: E -> V.Vector (Differential (CN MPBall)) -> Differential (CN MPBall)+ expressionToDifferential2 e v = expressionToDifferential e v+ where+ ev = expressionToDifferential e v+ evc = expressionToDifferential e vc+ vc = V.map (fmap (fmap centreAsBall)) v+ ++ -- TODO: Change to bfEval+ expressionToDifferential :: E -> V.Vector (Differential (CN MPBall)) -> Differential (CN MPBall)+ expressionToDifferential e@(Float _ _) _ = error $ "Cannot translate expression containing float to BoxFun: " ++ prettyShowE e+ expressionToDifferential e@(Float32 _ _) _ = error $ "Cannot translate expression containing float32 to BoxFun: " ++ prettyShowE e+ expressionToDifferential e@(Float64 _ _) _ = error $ "Cannot translate expression containing float64 to BoxFun: " ++ prettyShowE e+ expressionToDifferential (RoundToInteger mode e) v = --FIXME: add round to AD+ case expressionToDifferential e v of+ OrderZero x -> OrderZero $ roundMPBall mode x+ OrderOne x _ -> OrderOne (roundMPBall mode x) err+ OrderTwo x _ _ _ -> OrderTwo (roundMPBall mode x) err err err+ where+ err = noValueNumErrorCertain $ NumError "No derivatives after rounding to integer"++ expressionToDifferential (EBinOp op e1 e2) v = + case op of+ Min -> min (expressionToDifferential e1 v) (expressionToDifferential e2 v)+ Max -> max (expressionToDifferential e1 v) (expressionToDifferential e2 v)+ Pow -> pow (expressionToDifferential e1 v) (expressionToDifferential e2 v)+ Add -> expressionToDifferential e1 v + expressionToDifferential e2 v+ Sub -> expressionToDifferential e1 v - expressionToDifferential e2 v+ Mul -> expressionToDifferential e1 v * expressionToDifferential e2 v+ Div -> expressionToDifferential e1 v / expressionToDifferential e2 v+ Mod -> expressionToDifferential e1 v `mod` expressionToDifferential e2 v+ expressionToDifferential (EUnOp op e) v = + case op of+ Abs -> abs (expressionToDifferential e v)+ Sqrt -> sqrt (expressionToDifferential e v)+ Negate -> negate (expressionToDifferential e v)+ Sin -> sin (expressionToDifferential e v)+ Cos -> cos (expressionToDifferential e v)+ expressionToDifferential (Lit e) _ = differential 2 $ cn (mpBallP p e)+ expressionToDifferential (Var e) v = + case elemIndex e variableOrder of+ Nothing -> error $ "Variable: " ++ show e ++ " not found in varMap: " ++ show domain ++ " when translating expression: " ++ show e + Just i -> v V.! (fromIntegral i)+ expressionToDifferential Pi _ = differential 2 $ cn (piBallP p)+ expressionToDifferential (PowI e i) v = expressionToDifferential e v ^ i++ variableOrder = map fst domain+ vectorDomain = fromListDomain (map snd domain)
+ src/PropaFP/Translators/DReal.hs view
@@ -0,0 +1,186 @@+{-# LANGUAGE LambdaCase #-}+module PropaFP.Translators.DReal where++import MixedTypesNumPrelude++import PropaFP.Expression++import Data.Ratio+import System.IO.Unsafe (unsafePerformIO)+import PropaFP.VarMap (TypedVarInterval(TypedVar), VarType (Real, Integer), TypedVarMap)++fToConjunction :: F -> [F]+fToConjunction (FConn And f1 f2) = fToConjunction f1 ++ fToConjunction f2+fToConjunction (FNot (FConn Or f1 f2)) = fToConjunction (FNot f1) ++ fToConjunction (FNot f2)+fToConjunction (FNot (FConn Impl f1 f2)) = fToConjunction f1 ++ fToConjunction (FNot f2)+fToConjunction f = [f]++conjunctionToSMT :: [F] -> String+conjunctionToSMT [] = ""+conjunctionToSMT (f : fs) = "(assert " ++ formulaToSMT f 1 ++ ")\n" ++ conjunctionToSMT fs++formulaToSMT :: F -> Integer -> String+formulaToSMT (FConn op f1 f2) numTabs = + case op of+ And -> "\n" ++ concat (replicate numTabs "\t") ++ "(and " ++ formulaToSMT f1 (numTabs + 1) ++ " " ++ formulaToSMT f2 (numTabs + 1) ++ ")"+ Or -> "\n" ++ concat (replicate numTabs "\t") ++ "(or " ++ formulaToSMT f1 (numTabs + 1) ++ " " ++ formulaToSMT f2 (numTabs + 1) ++ ")"+ Impl -> "\n" ++ concat (replicate numTabs "\t") ++ "(or " ++ formulaToSMT (FNot f1) (numTabs + 1) ++ formulaToSMT f2 (numTabs + 1) ++ ")"+formulaToSMT (FComp op e1 e2) numTabs = + case op of+ Ge -> "\n" ++ concat (replicate numTabs "\t") ++ "(>= " ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e1 ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e2 ++ ")"+ Gt -> "\n" ++ concat (replicate numTabs "\t") ++ "(> " ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e1 ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e2 ++ ")"+ Lt -> "\n" ++ concat (replicate numTabs "\t") ++ "(< " ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e1 ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e2 ++ ")"+ Le -> "\n" ++ concat (replicate numTabs "\t") ++ "(<= " ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e1 ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e2 ++ ")"+ Eq -> "\n" ++ concat (replicate numTabs "\t") ++ "(= " ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e1 ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToSMT e2 ++ ")"+formulaToSMT (FNot f) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "(not " ++ formulaToSMT f (numTabs + 1) ++ ")"+formulaToSMT FTrue numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "true"+formulaToSMT FFalse numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "false"++expressionToSMT :: E -> String+expressionToSMT (EBinOp op e1 e2) =+ case op of+ Add -> "(+ " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Sub -> "(- " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Mul -> "(* " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Div -> "(/ " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Min -> "(min " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Max -> "(max " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Pow -> "(^ " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")"+ Mod -> "(mod " ++ expressionToSMT e1 ++ " " ++ expressionToSMT e2 ++ ")" --TODO: Warn dreal users+expressionToSMT (EUnOp op e) =+ case op of+ Sqrt -> "(sqrt " ++ expressionToSMT e ++ ")"+ Negate -> "(* -1 " ++ expressionToSMT e ++ ")"+ Abs -> "(abs " ++ expressionToSMT e ++ ")"+ Sin -> "(sin " ++ expressionToSMT e ++ ")"+ Cos -> "(cos " ++ expressionToSMT e ++ ")"+expressionToSMT (PowI e i) = "(^ " ++ expressionToSMT e ++ " " ++ show i ++ ")"+expressionToSMT (Var e) = e+expressionToSMT (Lit e) = + case denominator e of+ 1 -> show numE+ _ -> "(/ " ++ show numE ++ " " ++ show denE ++ ")"+ where+ numE = numerator e+ denE = denominator e+expressionToSMT Pi = "(* 4.0 (atan 1.0))" -- Equivalent to pi+expressionToSMT (RoundToInteger mode e) = + -- TODO: Warn about non-standard SMT+ case mode of+ RNE -> "(to_int_rne " ++ expressionToSMT e ++ ")"+ RTP -> "(to_int_rtp " ++ expressionToSMT e ++ ")"+ RTN -> "(to_int_rtn " ++ expressionToSMT e ++ ")"+ RTZ -> "(to_int_rtz " ++ expressionToSMT e ++ ")"+ RNA -> "(to_int_rna " ++ expressionToSMT e ++ ")"+expressionToSMT (Float mode e) = error "Float with unknown precision not supported"+ -- TODO: Warn about non-standard SMT+-- case mode of+-- RNE -> "(float_rne " ++ expressionToSMT e ++ ")"+-- RTP -> "(float_rtp " ++ expressionToSMT e ++ ")"+-- RTN -> "(float_rtn " ++ expressionToSMT e ++ ")"+-- RTZ -> "(float_rtz " ++ expressionToSMT e ++ ")"+-- RNA -> "(float_rne " ++ expressionToSMT e ++ ")"+expressionToSMT (Float32 mode e) =+ -- TODO: Warn about non-standard SMT+ case mode of+ RNE -> "(float32_rne " ++ expressionToSMT e ++ ")"+ RTP -> "(float32_rtp " ++ expressionToSMT e ++ ")"+ RTN -> "(float32_rtn " ++ expressionToSMT e ++ ")"+ RTZ -> "(float32_rtz " ++ expressionToSMT e ++ ")"+ RNA -> "(float32_rne " ++ expressionToSMT e ++ ")"+expressionToSMT (Float64 mode e) =+ -- TODO: Warn about non-standard SMT+ case mode of+ RNE -> "(float64_rne " ++ expressionToSMT e ++ ")"+ RTP -> "(float64_rtp " ++ expressionToSMT e ++ ")"+ RTN -> "(float64_rtn " ++ expressionToSMT e ++ ")"+ RTZ -> "(float64_rtz " ++ expressionToSMT e ++ ")"+ RNA -> "(float64_rne " ++ expressionToSMT e ++ ")"++formulaAndVarMapToDReal :: F -> TypedVarMap -> String+formulaAndVarMapToDReal f typedVarMap =+ "(set-logic QF_NRA)\n" +++ variablesAsString typedVarMap +++ (conjunctionToSMT . fToConjunction) f +++ "(check-sat)\n" +++ "(get-model)\n" +++ "(exit)\n"+ where+ showVarType Integer = "Int"+ showVarType Real = "Real"+ + showRational x = "(/ " ++ show (numerator x) ++ " " ++ show (denominator x) ++ ")"++ variablesAsString [] = ""+ variablesAsString ((TypedVar (varName, (leftBound, rightBound)) varType) : typedVarIntervals) =+ "(declare-fun " ++ varName ++ " () " ++ showVarType varType ++ ")\n" +++ "(assert (<= " ++ showRational leftBound ++ " " ++ varName ++ "))\n" +++ "(assert (<= " ++ varName ++ " " ++ showRational rightBound ++ "))\n" ++ variablesAsString typedVarIntervals++disjunctionExpressionsToSMT :: [ESafe] -> String+disjunctionExpressionsToSMT es = + "\n\t\t\t(or " ++ + concatMap + (\case+ EStrict e -> "\n\t\t\t\t(> " ++ expressionToSMT e ++ " 0)"+ ENonStrict e -> "\n\t\t\t\t(>= " ++ expressionToSMT e ++ " 0)"+ ) + es ++ + ")"++cnfExpressionsToSMT :: [[ESafe]] -> String+cnfExpressionsToSMT disjunctions = "\n\t\t(and " ++ concatMap disjunctionExpressionsToSMT disjunctions ++ ")"++cnfExpressionAndDomainsToDreal :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> String+cnfExpressionAndDomainsToDreal cnf realDomains intDomains =+ "(set-option :precision 1e-300)" +++ "\n(assert " ++ forAll (cnfExpressionsToSMT cnf) ++ ")\n(check-sat)\n(exit)"+ where+ forAll vc =+ "\n(forall (" ++ concatMap (\(v, (_, _)) -> "\n\t(" ++ v ++ " Real)") realDomains ++ concatMap (\(v, (_, _)) -> "\n\t(" ++ v ++ " Int)") intDomains ++ "\n)" ++ + "\n\t(=>" ++ + "\n\t\t(and " ++ concatMap (\(v, (vL, vR)) -> "\n\t\t\t(>= " ++ v ++ " " ++ expressionToSMT (Lit vL) ++ ") (<= " ++ v ++ " " ++ expressionToSMT (Lit vR) ++ ")") (realDomains ++ intDomains) ++ "\n\t\t)" +++ vc ++ "))" + -- forAll vc =+ -- "(forall (" ++ concatMap (\(v, (_, _)) -> "(" ++ v ++ " Real)") realDomains ++ concatMap (\(v, (_, _)) -> "(" ++ v ++ " Int)") intDomains ++ ")" ++ + -- "(=>" ++ + -- "(and " ++ concatMap (\(v, (vL, vR)) -> "(>= " ++ v ++ " " ++ expressionToSMT (Lit vL) ++ ")(<= " ++ v ++ " " ++ expressionToSMT (Lit vR) ++ ")") (realDomains ++ intDomains) ++ ")" +++ -- vc ++ "))"++runDRealTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> [(String, (Rational, Rational))] -> IO ()+runDRealTranslatorCNFWithVarMap cnf realVarMap intVarMap =+ do+ putStrLn "Running Haskell to dReal translator for Expressions"+ putStr "Enter target file name: "+ fileName <- getLine+ writeFile fileName $ cnfExpressionAndDomainsToDreal cnf realVarMap intVarMap++runDRealTranslatorCNF :: [[ESafe]] -> IO ()+runDRealTranslatorCNF cnf = do+ putStrLn "Running Haskell to dReal translator for Expressions"+ -- PutStr "Enter tool: "+ putStr "Enter target file name: "+ fileName <- getLine+ putStr "How many Real vars in expression? "+ numReals <- getLine+ putStr "How many Int vars in expression? "+ numInts <- getLine+ writeFile fileName (cnfExpressionAndDomainsToDreal cnf (parseDomains "real var name? " (read numReals)) (parseDomains "integer var name? " (read numInts)))+ where+ parseDomains :: String -> Integer -> [(String, (Rational, Rational))]+ parseDomains _ 0 = []+ parseDomains msg n =++ (unsafePerformIO (getVar msg), (unsafePerformIO (parseRational "lower bound") :: Rational, unsafePerformIO (parseRational "upper bound") :: Rational))+ : parseDomains msg (n - 1)++ getVar message = do+ putStr message+ getLine++ parseRational message = do+ putStr (message ++ " numerator? ")+ num <- getLine+ putStr (message ++ " denominator? ")+ den <- getLine+ return ((read num :: Integer) / (read den :: Integer))
+ src/PropaFP/Translators/FPTaylor.hs view
@@ -0,0 +1,181 @@+module PropaFP.Translators.FPTaylor where++import MixedTypesNumPrelude++import PropaFP.Expression++import Data.List+import Data.Ratio+import System.IO.Unsafe (unsafePerformIO)+import PropaFP.VarMap++import System.IO+import Debug.Trace+import Data.Scientific+import AERN2.MP.Precision+import AERN2.MP.Ball (piBallP)+import Data.Bifunctor++-- | All variables must appear in the VarMap+expressionToFPTaylor :: E -> String+expressionToFPTaylor (EBinOp op e1 e2) =+ case op of+ Add -> "(" ++ expressionToFPTaylor e1 ++ " + " ++ expressionToFPTaylor e2 ++ ")"+ Sub -> "(" ++ expressionToFPTaylor e1 ++ " - " ++ expressionToFPTaylor e2 ++ ")"+ Mul -> "(" ++ expressionToFPTaylor e1 ++ " * " ++ expressionToFPTaylor e2 ++ ")"+ Div -> "(" ++ expressionToFPTaylor e1 ++ " / " ++ expressionToFPTaylor e2 ++ ")"+ Mod -> "(" ++ expressionToFPTaylor e1 ++ " / " ++ expressionToFPTaylor e2 ++ ")" -- FIXME: not safe+ Min ->+ let+ fpE1 = expressionToFPTaylor e1+ fpE2 = expressionToFPTaylor e2+ in+ "((" ++ fpE1 ++ " + " ++ fpE2 ++ " - " ++ "|" ++ fpE1 ++ " - " ++ fpE2 ++ "|) / 2)"+ Max ->+ let+ fpE1 = expressionToFPTaylor e1+ fpE2 = expressionToFPTaylor e2+ in+ "((" ++ fpE1 ++ " + " ++ fpE2 ++ " + " ++ "|" ++ fpE1 ++ " - " ++ fpE2 ++ "|) / 2)"+ Pow -> error "FPTaylor does not support powers"+ -- case e2 of+ -- Lit rat -> + -- if denominator rat == 1+ -- then expressionToFPTaylor (PowI e1 (numerator rat)) + -- else error "FPTaylor does not support non-integer powers"+ -- _ -> error "FPTaylor does not support non-integer powers"+expressionToFPTaylor (EUnOp op e) =+ case op of+ Sqrt -> "sqrt(" ++ expressionToFPTaylor e ++ ")"+ Negate -> "(-1 * " ++ expressionToFPTaylor e ++ ")"+ Abs -> "|" ++ expressionToFPTaylor e ++ "|"+ Sin -> "sin(" ++ expressionToFPTaylor e ++ ")"+ Cos -> "cos(" ++ expressionToFPTaylor e ++ ")"+expressionToFPTaylor Pi = "(4 * atan(1))"+expressionToFPTaylor (PowI e i) = error "FPTaylor does not support powers" --TODO: Is it safe to change these to the equivalent with multiplications? A: Depends on SPARK power definition+expressionToFPTaylor (Lit r) = showFrac r+expressionToFPTaylor (Var v) = v+expressionToFPTaylor (Float32 mode e) = + case mode of+ RNE -> "rnd32(" ++ expressionToFPTaylor e ++ ")"+ RTP -> "rnd32_up(" ++ expressionToFPTaylor e ++ ")"+ RTN -> "rnd32_down(" ++ expressionToFPTaylor e ++ ")"+ RTZ -> "rnd32_0(" ++ expressionToFPTaylor e ++ ")"+ RNA -> "rnd32(" ++ expressionToFPTaylor e ++ ")" -- We can treat RNA like RNE. See Rounding section here: https://github.com/soarlab/FPTaylor/blob/develop/REFERENCE.md+expressionToFPTaylor (Float64 mode e) = + case mode of+ RNE -> "rnd64(" ++ expressionToFPTaylor e ++ ")"+ RTP -> "rnd64_up(" ++ expressionToFPTaylor e ++ ")"+ RTN -> "rnd64_down(" ++ expressionToFPTaylor e ++ ")"+ RTZ -> "rnd64_0(" ++ expressionToFPTaylor e ++ ")"+ RNA -> "rnd(" ++ expressionToFPTaylor e ++ ")" -- We can treat RNA like RNE. See Rounding section here: https://github.com/soarlab/FPTaylor/blob/develop/REFERENCE.md+expressionToFPTaylor e@(Float _ _) = error "Float type with no precision found when translating to FPTaylor: " ++ show e+expressionToFPTaylor (RoundToInteger mode e) = expressionToFPTaylor e -- FIXME: is this ok because we are calculating abs error?+ -- alternative solution: manually add rounding logic for each case. possible without Ifs?+ -- This is ok for now+-- expressionToFPTaylor (Float e s) = "rnd32(" ++ expressionToFPTaylor e ++ ")" --TODO: FPTaylor only supports 16,32,64,128 floats. Use these numbers in PP2?++variableBoundsToFPTaylor :: VarMap -> String+variableBoundsToFPTaylor [] = ""+variableBoundsToFPTaylor ((v, (l, r)) : vs) = "real " ++ show v ++ " in [" ++ showFrac l ++ ", " ++ showFrac r ++ "];\n" ++ variableBoundsToFPTaylor vs+ where++showFrac :: Rational -> [Char]+showFrac rat = if den == 1.0 then show num else show num ++ " / " ++ show den+ where+ num = numerator rat+ den = denominator rat++expressionWithVarMapToFPTaylor :: E -> VarMap -> String+expressionWithVarMapToFPTaylor e vm =+ "Variables\n" ++ variableBoundsToFPTaylor vm ++ "\nExpressions\n" ++ expressionToFPTaylor e ++ ";"++-- parseFPTaylorOutput :: String -> Rational+-- parseFPTaylorOutput output =+-- case elemIndex "(exact):" wordsOutput of+-- Just i -> wordsOutput !! (i + 1)+-- where+-- wordsOutput = words output ++-- "1.788139e-07"+-- "1788140 % 10^-13"++-- To parse the left side:+-- Store length of string+-- Find position of dot+-- remove dot+-- parse integer+-- Add one to compensate for missing digits+-- divide integer using position of dot and length of string to get the rational we want++parseFPTaylorRational :: String -> Maybe Rational+parseFPTaylorRational output = mr+ where+ mr = toRational . (read :: String -> Scientific) <$> findErrorBound outputList++ outputList = words output++ findErrorBound :: [String] -> Maybe String+ findErrorBound [] = Nothing+ findErrorBound ("Absolute" : "error" : "(exact):" : errorBound : _) = Just errorBound+ findErrorBound (_ : xs) = findErrorBound xs+ -- ePos = Data.List.elemIndex 'e' output+ -- (decimal, exponentWithE) = Data.List.splitAt (ePos) output+ -- exponent = tail exponentWithE+ -- exponentInt = read exponent --Could throw exception++testOutput :: String +testOutput = + "Loading configuration file: /home/junaid/Research/git/FPTaylor/default.cfg \+ \FPTaylor, version 0.9.2+dev \++ \Loading: heronInit1PlusXDiv1 copy.txt \+ \Processing: Expression 1 \++ \************************************* \+ \Taylor form for: rnd32((1 + rnd32((X / 1)))) \++ \Conservative bound: [1.500000, 3.000000] \++ \Simplified rounding: rnd[32,ne,1.00,-24,0]((1 + rnd32((X / 1)))) \+ \Building Taylor forms... \+ \Simplifying Taylor forms... \+ \success \+ \v0 = (1 + (X * (1 / 1))) \+ \-1 (9): exp = -24: (1/5070602400912917605986812821504) \+ \1 (3): exp = -24: floor_power2(((X * (1 / 1)) + 0)) \+ \2 (5): exp = -24: floor_power2(((1 + (X * (1 / 1))) + interval(-5.96046447753906382349e-08, 5.96046447753906382349e-08))) \++ \Corresponding original subexpressions: \+ \1: rnd32((X / 1)) \+ \2: rnd[32,ne,1.00,-24,0]((1 + rnd32((X / 1)))) \++ \bounds: [1.500000e+00, 3.000000e+00] \++ \Computing absolute errors \+ \-1: exp = -24: 1.972152e-31 (low = 1.972152e-31, subopt = 0.0%) \++ \Solving the exact optimization problem \+ \exact bound (exp = -24): 3.000000e+00 (low = 3.000000e+00, subopt = 0.0%) \+ \total2: 1.175494e-38 (low = 1.175494e-38, subopt = 0.0%) \+ \exact total: 1.788139e-07 (low = 1.788139e-07, subopt = 0.0%) \++ \Elapsed time: 0.36412 \+ \************************************* \++ \------------------------------------------------------------------------------- \+ \Problem: Expression 1 \++ \Optimization lower bounds for error models: \+ \The absolute error model (exact): 1.788139e-07 (suboptimality = 0.0%) \+ + \Bounds (without rounding): [1.500000e+00, 3.000000e+00] \+ \Bounds (floating-point): [1.49999982118606545178e+00, 3.00000017881393477026e+00] \+ + \Absolute error (exact): 1.788139e-07 \+ + \Elapsed time: 0.36 \+ + + + \"
+ src/PropaFP/Translators/MetiTarski.hs view
@@ -0,0 +1,131 @@+module PropaFP.Translators.MetiTarski where++import MixedTypesNumPrelude++import PropaFP.Expression++-- import Data.List+import Data.Ratio+import Data.Char (toUpper)+import PropaFP.VarMap+import Data.List (intercalate)++formulaToTPTP :: F -> Integer -> String+formulaToTPTP (FConn op f1 f2) numTabs = + case op of+ And -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ formulaToTPTP f1 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ "&" ++ formulaToTPTP f2 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Or -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ formulaToTPTP f1 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ "|" ++ formulaToTPTP f2 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Impl -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ formulaToTPTP f1 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ "=>" ++ formulaToTPTP f2 (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+formulaToTPTP (FComp op e1 e2) numTabs =+ case op of+ Ge -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e1 ++ "\n" ++ concat (replicate numTabs "\t") ++ ">=" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e2 ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Gt -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e1 ++ "\n" ++ concat (replicate numTabs "\t") ++ ">" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e2 ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Le -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e1 ++ "\n" ++ concat (replicate numTabs "\t") ++ "<=" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e2 ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Lt -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e1 ++ "\n" ++ concat (replicate numTabs "\t") ++ "<" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e2 ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+ Eq -> "\n" ++ concat (replicate numTabs "\t") ++ "(" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e1 ++ "\n" ++ concat (replicate numTabs "\t") ++ "=" ++ "\n" ++ concat (replicate (numTabs + 1) "\t") ++ expressionToTPTP e2 ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+formulaToTPTP (FNot f) numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "~(" ++ formulaToTPTP f (numTabs + 1) ++ "\n" ++ concat (replicate numTabs "\t") ++ ")"+formulaToTPTP FTrue numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "(0 = 0)"+formulaToTPTP FFalse numTabs = "\n" ++ concat (replicate numTabs "\t") ++ "(0 = 1)"++expressionToTPTP :: E -> String+expressionToTPTP (EBinOp op e1 e2) =+ case op of+ Add -> "(" ++ expressionToTPTP e1 ++ " + " ++ expressionToTPTP e2 ++ ")"+ Sub -> "(" ++ expressionToTPTP e1 ++ " - " ++ expressionToTPTP e2 ++ ")"+ Mul -> "(" ++ expressionToTPTP e1 ++ " * " ++ expressionToTPTP e2 ++ ")"+ Div -> "(" ++ expressionToTPTP e1 ++ " / " ++ expressionToTPTP e2 ++ ")"+ Min -> "(min(" ++ expressionToTPTP e1 ++ ", " ++ expressionToTPTP e2 ++ "))"+ Max -> "(max(" ++ expressionToTPTP e1 ++ ", " ++ expressionToTPTP e2 ++ "))"+ Pow -> "(" ++ expressionToTPTP e1 ++ " ^ " ++ expressionToTPTP e2 ++ ")"+ Mod -> error "Modulo is not supported in tptp"+expressionToTPTP (EUnOp op e) =+ case op of+ Sqrt -> "(sqrt(" ++ expressionToTPTP e ++ "))"+ Negate -> "(-1 * " ++ expressionToTPTP e ++ ")"+ Abs -> "(abs(" ++ expressionToTPTP e ++ "))"+ Sin -> "(sin(" ++ expressionToTPTP e ++ "))"+ Cos -> "(cos(" ++ expressionToTPTP e ++ "))"+expressionToTPTP (RoundToInteger m e) = + case m of+ RNE -> "round(" ++ expressionToTPTP e ++ ")"+ RTP -> error "Round Towards Ceiling not supported in TPTP" -- "ceiling(" ++ expressionToTPTP e ++ ")"+ RTN -> "floor(" ++ expressionToTPTP e ++ ")"+ RTZ -> error "Round Towards Zero not supported in TPTP"+ RNA -> error "Round Nearest Away not supported in TPTP"+expressionToTPTP (PowI e i) = "(" ++ expressionToTPTP e ++ " ^ " ++ show i ++ ")"+expressionToTPTP (Var e) = map toUpper e+expressionToTPTP (Lit e) = + case denominator e of+ 1 -> show (numerator e)+ _ ->+ "(" ++ show (numerator e) ++ " / " ++ show (denominator e) ++ ")"+expressionToTPTP Pi = "pi"+expressionToTPTP (Float _ _) = "MetiTarski translator does not support Floats"+expressionToTPTP (Float32 _ _) = "MetiTarski translator does not support Floats"+expressionToTPTP (Float64 _ _) = "MetiTarski translator does not support Floats"++formulaAndVarMapToMetiTarski :: F -> TypedVarMap -> String+formulaAndVarMapToMetiTarski f typedVarMap =+ "fof(vc,conjecture," ++ + case typedVarMap of+ [] -> "\n\t(" ++ formulaToTPTP f 2 ++ "\n\t)" ++ "\n)."+ _ -> "\n\t! [" ++ intercalate "," (map (\(TypedVar (v,_) _) -> map toUpper v) typedVarMap) ++ "] : (" +++ "\n\t(" ++ variablesAsString typedVarMap ++ "\n\t) =>" +++ "\n\t(" ++ formulaToTPTP f 2 ++ "\n\t))" ++ "\n)."+ where+ variablesAsString [] = ""+ variablesAsString ((TypedVar (varName, (leftBound, rightBound)) _) : typedVarIntervals) =+ let + varNameUpper = map toUpper varName+ leftBoundString = show (numerator leftBound) ++ " / " ++ show (denominator leftBound)+ rightBoundString = show (numerator rightBound) ++ " / " ++ show (denominator rightBound)+ in+ "\n\t\t" ++ leftBoundString ++ " <= " ++ varNameUpper ++ " & " ++ varNameUpper ++ " <= " ++ rightBoundString ++ (if null typedVarIntervals then "" else " &" ++ variablesAsString typedVarIntervals)++disjunctionExpressionsToSMT :: [E] -> String+disjunctionExpressionsToSMT [] = ""+disjunctionExpressionsToSMT [e] = expressionToTPTP e+disjunctionExpressionsToSMT (e : es) = "(max " ++ expressionToTPTP e ++ disjunctionExpressionsToSMT es ++ ")"++cnfExpressionsToSMT :: [[E]] -> String+cnfExpressionsToSMT [] = ""+cnfExpressionsToSMT [e] = disjunctionExpressionsToSMT e+cnfExpressionsToSMT (e : es) = "(min " ++ disjunctionExpressionsToSMT e ++ cnfExpressionsToSMT es ++ ")"++disjunctionExpressionsToTptp :: [ESafe] -> String+disjunctionExpressionsToTptp [] = ""+disjunctionExpressionsToTptp [eSafe] = + case eSafe of+ EStrict e -> "\n\t\t\t" ++ expressionToTPTP e ++ " > 0.0"+ ENonStrict e -> "\n\t\t\t" ++ expressionToTPTP e ++ " >= 0.0"+disjunctionExpressionsToTptp (e : es) = disjunctionExpressionsToTptp [e] ++ "\n\t\t\t|" ++ disjunctionExpressionsToTptp es++cnfExpressionsToTptp :: [[ESafe]] -> String+cnfExpressionsToTptp [] = ""+cnfExpressionsToTptp [e] = "\n\t\t(" ++ disjunctionExpressionsToTptp e ++ "\n\t\t)"+cnfExpressionsToTptp (e : es) = "\n\t\t(" ++ disjunctionExpressionsToTptp e ++ "\n\t\t)" ++ "\n\t\t&" ++ cnfExpressionsToTptp es++cnfExpressionAndDomainsToMetiTarski :: [[ESafe]] -> [(String, (Rational, Rational))] -> String+cnfExpressionAndDomainsToMetiTarski cnf realDomains =+ "fof(vc,conjecture, " +++ "\n\t! [" ++ intercalate "," (map (\(v,_) -> map toUpper v) realDomains) ++ "] : " +++ "\n\t(" +++ case realDomains of+ [] -> + cnfExpressionsToTptp cnf +++ "\n\t))."+ _ ->+ "\n\t(" ++ + intercalate "\n\t& " (map (\(x',(l,u)) -> let x = map toUpper x' in show (numerator l) ++ "/" ++ show (denominator l) ++ " <= " ++ x ++ " & " ++ x ++ " <= " ++ show (numerator u) ++ "/" ++ show (denominator u)) realDomains) +++ "\n\t) =>" +++ "\n\t(" ++ cnfExpressionsToTptp cnf +++ "\n\t)" +++ "\n\t))."++runMetiTarskiTranslatorCNFWithVarMap :: [[ESafe]] -> [(String, (Rational, Rational))] -> IO ()+runMetiTarskiTranslatorCNFWithVarMap cnf realVarMap =+ do+ putStrLn "Running Haskell to dReal translator for Expressions"+ putStr "Enter target file name: "+ fileName <- getLine+ writeFile fileName $ cnfExpressionAndDomainsToMetiTarski cnf realVarMap
+ src/PropaFP/VarMap.hs view
@@ -0,0 +1,387 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE LambdaCase #-}++module PropaFP.VarMap where++import MixedTypesNumPrelude+import Data.List as L+import AERN2.BoxFun.Optimisation+import AERN2.MP.Ball (MPBall, endpoints, fromEndpointsAsIntervals, mpBallP)+import AERN2.BoxFun.TestFunctions (fromListDomain)+import AERN2.BoxFun.Box (Box)+import qualified AERN2.Linear.Vector.Type as V+import Data.Tuple.Extra++import Debug.Trace as T+import Prelude (Ord)+import qualified Prelude as P+import qualified Data.Functor.Contravariant as P+import qualified Data.Functor.Contravariant as P+import AERN2.MP.Precision+import Data.Ratio+-- data VarType = Integer | Real + -- deriving (Show, P.Eq, P.Ord) ++-- TODO: Add VarType to VarMap, or make new VarMap type+-- | An assosciation list mapping variable names to rational interval domains+data VarType = Real | Integer+ deriving (Show, P.Eq, P.Ord)++type VarInterval = (String, (Rational, Rational))++data TypedVarInterval = TypedVar VarInterval VarType+ deriving (Show, P.Eq, P.Ord)++type VarMap = [VarInterval]++type TypedVarMap = [TypedVarInterval]+++-- instance P.Contravariant VarInterval where++-- | Get the width of the widest interval+-- Fixme: maxWidth+maxWidth :: VarMap -> Rational+maxWidth [] = 0.0+maxWidth vMap = L.maximum (map (\(_, ds) -> snd ds - fst ds) vMap)++typedMaxWidth :: TypedVarMap -> Rational+typedMaxWidth [] = 0.0+typedMaxWidth vMap = L.maximum (map (\(TypedVar (_, ds) _) -> snd ds - fst ds) vMap)++-- | Get the sum of the width of each interval+taxicabWidth :: VarMap -> Rational+taxicabWidth vMap = L.sum (map (\(_, ds) -> snd ds - fst ds) vMap)++-- | Increase the diameter of all variables in a varMap by the given rational+increaseDiameter :: VarMap -> Rational -> VarMap+increaseDiameter [] _ = []+increaseDiameter ((v, (l, r)) : vs) d = ((v, (l - d, r + d)) : vs)++-- | Increase the radius of all variables in a varMap by the given rational+increaseRadius :: VarMap -> Rational -> VarMap+increaseRadius vm r = increaseDiameter vm (r/2)++-- | Bisect all elements in a given VarMap+fullBisect :: VarMap -> [VarMap]+fullBisect vMap = case L.length vMap of+ 0 -> [vMap]+ l ->+ -- y is the dimension bisected in the current iteration+ -- x is a bisection of the previous dimension (tail recursion)+ concatMap (\x -> map (\y -> x ++ [y]) (bisectDimension (l-1))) (fullBisect (L.take (fromIntegral (l-1)) vMap))++ where+ bisectDimension n = [fst bn L.!! (int n), snd bn L.!! (int n)]+ where bn = bisectN n vMap++-- | Bisect the domain of the given interval, resulting in a pair+-- Vars+bisectInterval :: (String, (Rational, Rational)) -> ((String, (Rational, Rational)), (String, (Rational, Rational)))+bisectInterval (var, (lower, upper)) = bisectedVar+ where+ varCentre = (lower + upper) / 2+ bisectedVar = ((var, (lower, varCentre)), (var, (varCentre, upper)))++bisectTypedInterval :: (String, (Rational, Rational)) -> VarType -> ((String, (Rational, Rational)), (String, (Rational, Rational)))+bisectTypedInterval (var, (lower, upper)) Real = bisectedVar+ where+ varCentre = (lower + upper) / 2+ bisectedVar = ((var, (lower, varCentre)), (var, (varCentre, upper)))+bisectTypedInterval (var, (lower, upper)) Integer = bisectedVar+ where+ varCentre = (lower + upper) / 2+ bisectedVar = ((var, (lower, floor varCentre % 1)), (var, (ceiling varCentre % 1, upper)))++-- | Bisect the given dimension of the given VarMap,+-- resulting in a pair of VarMaps+bisectN :: Integer -> VarMap -> (VarMap, VarMap)+bisectN n vMap =+ (+ map (\v -> if fst v == fst fstBisect then fstBisect else v) vMap,+ map (\v -> if fst v == fst sndBisect then sndBisect else v) vMap+ )+ where+ (fstBisect, sndBisect) = bisectInterval (vMap L.!! (int n))++bisectVar :: VarMap -> String -> (VarMap, VarMap)+bisectVar [] _ = ([], [])+bisectVar (v@(currentVar, (_, _)) : vm) bisectionVar =+ if currentVar == bisectionVar+ then (leftBisection : vm, rightBisection : vm)+ else (v : leftList, v : rightList)+ where+ (leftBisection, rightBisection) = bisectInterval v+ (leftList, rightList) = bisectVar vm bisectionVar++bisectTypedVar :: TypedVarMap -> String -> (TypedVarMap, TypedVarMap)+bisectTypedVar [] _ = ([], [])+bisectTypedVar (v@((TypedVar i@(currentVar, (_, _)) Real)) : vm) bisectionVar =+ if currentVar == bisectionVar+ then (TypedVar leftBisection Real : vm, TypedVar rightBisection Real : vm)+ else (v : leftList, v : rightList)+ where+ (leftBisection, rightBisection) = bisectTypedInterval i Real+ (leftList, rightList) = bisectTypedVar vm bisectionVar+bisectTypedVar (v@((TypedVar i@(currentVar, (_, _)) Integer)) : vm) bisectionVar =+ if currentVar == bisectionVar+ then (TypedVar leftBisection Integer : vm, TypedVar rightBisection Integer : vm)+ else (v : leftList, v : rightList)+ where+ (leftBisection, rightBisection) = bisectTypedInterval i Integer+ (leftList, rightList) = bisectTypedVar vm bisectionVar+++-- | Check whether or not v1 contain v2.+contains :: VarMap -> VarMap -> Bool+contains v1 v2 =+ L.all (\((v1v, (v1l, v1r)), (v2v, (v2l, v2r))) -> v1v == v2v && v1l !<=! v2l && v2r !<=! v1r) (zip v1' v2')+ where+ v1' = sort v1+ v2' = sort v2++-- | Convert VarMap to SearchBox with the provided minimum+toSearchBox :: VarMap -> CN MPBall -> SearchBox+toSearchBox vMap = SearchBox (fromListDomain (map snd vMap))++centre :: VarMap -> VarMap+centre = map (\(x,(dL,dR)) -> (x, ((dR+dL)/2,(dR+dL)/2)))++varMapToBox :: VarMap -> Precision -> Box+varMapToBox vs p = V.fromList $ map (\(_,(l,r)) -> fromEndpointsAsIntervals (cn (mpBallP p l)) (cn (mpBallP p r))) vs++typedVarMapToBox :: TypedVarMap -> Precision -> Box+typedVarMapToBox vs p = V.fromList $ map+ (\case+ TypedVar (_,(l,r)) _ -> fromEndpointsAsIntervals (cn (mpBallP p l)) (cn (mpBallP p r)))+ vs++-- Precondition, box and varNames have same length+boxToVarMap :: Box -> [String] -> VarMap+boxToVarMap box varNames = zip varNames $ V.toList $ V.map (both (rational . unCN) . endpoints) box++unsafeBoxToTypedVarMap :: Box -> [(String, VarType)] -> TypedVarMap+unsafeBoxToTypedVarMap box varNamesWithTypes =+ zipWith+ (\(varName, varType) varBounds ->+ case varType of+ Real -> TypedVar (varName, varBounds) Real+ Integer -> TypedVar (varName, (\(l,r) -> (ceiling l % 1, floor r % 1)) varBounds) Integer -- FIXME: may result in inverted interval+ )+ varNamesWithTypes $ V.toList $ V.map (both (rational . unCN) . endpoints) box++safeBoxToTypedVarMap :: Box -> [(String, VarType)] -> Maybe TypedVarMap+safeBoxToTypedVarMap box varNamesWithTypes =+ if any (\(TypedVar (_,(l, r)) _) -> l > r) unsafeTypedVarMap then Nothing else Just unsafeTypedVarMap+ where+ unsafeTypedVarMap = unsafeBoxToTypedVarMap box varNamesWithTypes++typedVarMapToVarMap :: TypedVarMap -> VarMap+typedVarMapToVarMap =+ map+ (\case TypedVar vm _ -> vm)++unsafeVarMapToTypedVarMap :: VarMap -> [(String, VarType)] -> TypedVarMap+unsafeVarMapToTypedVarMap [] _ = []+unsafeVarMapToTypedVarMap ((v, (l, r)) : vs) varTypes =+ case lookup v varTypes of+ Just Real -> TypedVar (v, (l, r)) Real : unsafeVarMapToTypedVarMap vs varTypes+ Just Integer -> TypedVar (v, (ceiling l % 1, floor r % 1)) Integer : unsafeVarMapToTypedVarMap vs varTypes+ Nothing -> TypedVar (v, (l, r)) Real : unsafeVarMapToTypedVarMap vs varTypes++safeVarMapToTypedVarMap :: VarMap -> [(String, VarType)] -> Maybe TypedVarMap+safeVarMapToTypedVarMap [] _ = Just []+safeVarMapToTypedVarMap ((v, (l, r)) : vs) varTypes =+ case lookup v varTypes of+ Just Real ->+ case safeVarMapToTypedVarMap vs varTypes of+ Just rs -> Just $ TypedVar (v, (l, r)) Real : rs+ Nothing -> Nothing+ Just Integer ->+ if ceiling l > floor r+ then Nothing+ else+ case safeVarMapToTypedVarMap vs varTypes of+ Just rs -> Just $ TypedVar (v, (ceiling l % 1, floor r % 1)) Integer : rs+ Nothing -> Nothing+ Nothing ->+ case safeVarMapToTypedVarMap vs varTypes of+ Just rs -> Just $ TypedVar (v, (l, r)) Real : rs+ Nothing -> Nothing++safeIntersectVarMap :: TypedVarMap -> TypedVarMap -> Maybe TypedVarMap+safeIntersectVarMap vm1 vm2 = + if isTypedVarMapInverted intersectedVm then Nothing else Just intersectedVm+ where+ -- Sort varMaps by varNames+ sortedVm1 = sortBy (\(TypedVar (v1, _) _ ) (TypedVar (v2, _) _ ) -> P.compare v1 v2) vm1+ sortedVm2 = sortBy (\(TypedVar (v1, _) _ ) (TypedVar (v2, _) _ ) -> P.compare v1 v2) vm1+ intersectedVm = unsafeIntersectVarMap sortedVm1 sortedVm2++-- |Assumes varMaps have vars appearing in the same order+unsafeIntersectVarMap :: TypedVarMap -> TypedVarMap -> TypedVarMap+unsafeIntersectVarMap [] [] = []+unsafeIntersectVarMap [] _ = undefined+unsafeIntersectVarMap _ [] = undefined+unsafeIntersectVarMap ((TypedVar (v1, (l1, r1)) t1) : vm1) ((TypedVar (v2, (l2, r2)) t2) : vm2) =+ if v1 P./= v2 || t1 P./= t2+ then error $ + "unsafeIntersectVarMap : varMaps have a different variable/variable type in the same position; vm1: " + ++ show v1 ++ ":: " ++ show t1 ++ ", vm2: " ++ show v2 ++ ":: " ++ show t2+ else TypedVar (v1, (newL, newR)) t1 : unsafeIntersectVarMap vm1 vm2+ where+ newL = max l1 l2+ newR = min r1 r2++isVarMapInverted :: VarMap -> Bool+isVarMapInverted [] = False+isVarMapInverted ((_, (l, r)) : vs) = l > r || isVarMapInverted vs++isTypedVarMapInverted :: TypedVarMap -> Bool+isTypedVarMapInverted [] = False+isTypedVarMapInverted ((TypedVar (_, (l, r)) _) : vs) = l > r || isTypedVarMapInverted vs++getVarNamesWithTypes :: TypedVarMap -> [(String, VarType)]+getVarNamesWithTypes = map+ (\case+ TypedVar (v, (_,_)) t -> (v,t)+ )++getCorners :: VarMap -> [VarMap]+getCorners vm =+ nub . map sort $ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') rights) lefts+ ++ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') lefts) lefts+ ++ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') rights) rights+ ++ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') lefts) rights+ where+ lefts = map (\(v,(l,_)) -> (v,(l,l))) vm+ rights = map (\(v,(_,r)) -> (v,(r,r))) vm++-- Order for two dimension VarMap, left bottom right top+getEdges :: VarMap -> [VarMap]+getEdges vm =+ nub . map sort $ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') vm) lefts+ ++ map (\vm'@(v,_) -> vm' : filter (\(v',_) -> v /= v') vm) rights+ where+ lefts = map (\(v,(l,_)) -> (v,(l,l))) vm+ rights = map (\(v,(_,r)) -> (v,(r,r))) vm++upperbound :: VarMap -> VarMap+upperbound = map (\(v,(_,r)) -> (v, (r, r)))++lowerbound :: VarMap -> VarMap+lowerbound = map (\(v,(l,_)) -> (v, (l, l)))+++-- |Intersect two varMaps+-- This assumes that both VarMaps have the same variables in the same order+intersectVarMap :: VarMap -> VarMap -> VarMap+intersectVarMap =+ zipWith+ (\(v, (l1, r1)) (_, (l2, r2)) ->+ (v,+ (+ max l1 l2,+ min r1 r2+ )+ )+ )++-- | Returns the widest interval in the given VarMap+widestInterval :: VarMap -> (String, (Rational, Rational)) -> (String, (Rational, Rational))+widestInterval [] widest = widest+widestInterval (current@(_, (cL, cR)) : vm) widest@(_, (wL, wR)) =+ if widestDist >= currentDist then widestInterval vm widest else widestInterval vm current+ where+ widestDist = abs(wR - wL)+ currentDist = abs(cR - cL)++widestTypedInterval :: TypedVarMap -> (String, (Rational, Rational)) -> (String, (Rational, Rational))+widestTypedInterval [] widest = widest+widestTypedInterval (TypedVar current@(_, (cL,cR)) _ : vm) widest@(_, (wL, wR)) =+ if widestDist >= currentDist then widestTypedInterval vm widest else widestTypedInterval vm current+ where+ widestDist = abs(wR - wL)+ currentDist = abs(cR - cL)++typedVarIntervalToVarInterval :: TypedVarInterval -> VarInterval+typedVarIntervalToVarInterval (TypedVar vi _) = vi++prettyShowVarMap :: VarMap -> String+prettyShowVarMap [] = []+prettyShowVarMap ((v, (l, r)) : vs) = show v ++ ": \n\t" ++ "[" ++ show (double l) ++ ", " ++ show (double r) ++ "]" ++ "\n" ++ prettyShowVarMap vs++prettyShowTypedVarMap :: TypedVarMap -> String+prettyShowTypedVarMap [] = []+prettyShowTypedVarMap (TypedVar (v, (l, r)) t : vs) = show v ++ " (" ++ show t ++ "): \n\t" ++ "[" ++ show (double l) ++ ", " ++ show (double r) ++ "]" ++ "\n" ++ prettyShowTypedVarMap vs+-- | Get all the possible edges of a given VarMap as a list of VarMaps+-- Examples:+-- edges [("x", (0.5, 2.0))] = +-- [[("x",(1 % 2,1 % 2))],[("x",(2 % 1,2 % 1))]]+-- edges [("x", (0.5, 2.0)), ("y", (0.8, 1.8))] = +-- [[("x",(1 % 2,1 % 2)),("y",(4 % 5,4 % 5))],+-- [("x",(1 % 2,1 % 2)),("y",(9 % 5,9 % 5))],+-- [("x",(2 % 1,2 % 1)),("y",(4 % 5,4 % 5))],+-- [("x",(2 % 1,2 % 1)),("y",(9 % 5,9 % 5))]]++-- [("x", (0.5, 2.0)), ("y" (0.8, 0.8))]+-- [("x", (0.5, 2.0)), ("y" (1.8, 1.8))]+-- [("x", (0.5, 0.5)), ("y" (0.8, 1.8))]+-- [("x", (2.0, 2.0)), ("y" (0.8, 1.8))]+-- edges :: VarMap -> [VarMap]+-- edges vs = (map (\(v, d) -> (filter (\(v', _) -> v /= v') vs)) vs)+-- where+-- points = []+-- points ([(v, (l, r))] : vs = [(v ((l, l), (r, r)))] ++ points vs++-- edges :: VarMap -> [VarMap]+-- edges vs = +-- case L.length vs of+-- 0 -> [[]]+-- 1 -> concatTuple (endpoints (head vs)) []+-- _ -> +-- -- concatMap ((\eps@((v, _), _) -> concatTuple eps (filter (\(v',_) -> v /= v') vs)) . endpoints) vs+-- -- trace (show (map endpoints vs)) $+-- -- map (\(l@(v,_), r) -> (filterOutVar v vsEdges)) vsEdges+-- -- map (\(l@, r)) vsEndpoints+-- -- joinEdges . sortAllEdges $ map endpoints vs+-- -- trace (show vsEndpoints) $+-- [l : leftEndpoints] ++ [r : leftEndpoints] ++ [l : rightEndpoints] ++ [r : rightEndpoints]++-- where+-- leftEndpoints = map fst (tail vsEndpoints)+-- rightEndpoints = map snd (tail vsEndpoints)+-- vsEndpoints = map endpoints vs+-- (l, r) = head vsEndpoints++-- -- fun [] = []+-- -- fun xs@(l',r') = case L.length xs of+-- -- 0 -> []+-- -- 1 -> [l, r]+++-- -- vsEdges = (map (\v -> [endpoints v]) vs)+-- filterOutVar x xs = filter (\(x',_) -> x /= x') xs++-- -- joinVM vm (l, r) = (l : vm)++-- endpoints (v, (l, r)) = ((v, (l, l)), (v, (r, r)))++-- concatTuple (l, r) xs = [l : xs, r : xs]++-- joinEdges [] = []+-- joinEdges ((v, d) : es) = +-- case filterOutSameVars of+-- [] -> []+-- es' ->+-- (map (\vd -> (v, d) : [vd])) es' ++ joinEdges es+-- where+-- filterOutSameVars = (filter (\(v',_) -> v /= v') es)++-- sortAllEdges es = sort . concat $ ls : [rs]+-- where+-- ls = map fst es+-- rs = map snd es++-- [0.5, 0.8, 3.0]+-- [2.0, 1.8]
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"