diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,3 @@ +# Changelog for PropaFP + +## Unreleased changes diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/PropaFP.cabal b/PropaFP.cabal new file mode 100644 --- /dev/null +++ b/PropaFP.cabal @@ -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 +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 diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. + +![SPARK + PropaFP](https://raw.githubusercontent.com/rasheedja/PropaFP/c7680a48c9524768ac113ab5ca0e179dc2f315c6/images/SPARK_Toolchain_PropaFP.png) + +[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) diff --git a/app/DRealRunner.hs b/app/DRealRunner.hs new file mode 100644 --- /dev/null +++ b/app/DRealRunner.hs @@ -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" ) diff --git a/app/DRealTranslator.hs b/app/DRealTranslator.hs new file mode 100644 --- /dev/null +++ b/app/DRealTranslator.hs @@ -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" ) diff --git a/app/LPPaverRunner.hs b/app/LPPaverRunner.hs new file mode 100644 --- /dev/null +++ b/app/LPPaverRunner.hs @@ -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" ) diff --git a/app/MetiTarskiRunner.hs b/app/MetiTarskiRunner.hs new file mode 100644 --- /dev/null +++ b/app/MetiTarskiRunner.hs @@ -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" ) diff --git a/app/MetiTarskiTranslator.hs b/app/MetiTarskiTranslator.hs new file mode 100644 --- /dev/null +++ b/app/MetiTarskiTranslator.hs @@ -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" ) diff --git a/app/PrettifySMT2.hs b/app/PrettifySMT2.hs new file mode 100644 --- /dev/null +++ b/app/PrettifySMT2.hs @@ -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" ) diff --git a/src/PropaFP/DeriveBounds.hs b/src/PropaFP/DeriveBounds.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/DeriveBounds.hs @@ -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 diff --git a/src/PropaFP/EliminateFloats.hs b/src/PropaFP/EliminateFloats.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/EliminateFloats.hs @@ -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] [] diff --git a/src/PropaFP/Eliminator.hs b/src/PropaFP/Eliminator.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Eliminator.hs @@ -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)]] diff --git a/src/PropaFP/Expression.hs b/src/PropaFP/Expression.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Expression.hs @@ -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 diff --git a/src/PropaFP/Parsers/DRealSmt.hs b/src/PropaFP/Parsers/DRealSmt.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Parsers/DRealSmt.hs @@ -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 diff --git a/src/PropaFP/Parsers/Lisp/DataTypes.hs b/src/PropaFP/Parsers/Lisp/DataTypes.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Parsers/Lisp/DataTypes.hs @@ -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 + diff --git a/src/PropaFP/Parsers/Lisp/Parser.hs b/src/PropaFP/Parsers/Lisp/Parser.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Parsers/Lisp/Parser.hs @@ -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 + diff --git a/src/PropaFP/Parsers/Smt.hs b/src/PropaFP/Parsers/Smt.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Parsers/Smt.hs @@ -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 diff --git a/src/PropaFP/Translators/BoxFun.hs b/src/PropaFP/Translators/BoxFun.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Translators/BoxFun.hs @@ -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) diff --git a/src/PropaFP/Translators/DReal.hs b/src/PropaFP/Translators/DReal.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Translators/DReal.hs @@ -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)) diff --git a/src/PropaFP/Translators/FPTaylor.hs b/src/PropaFP/Translators/FPTaylor.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Translators/FPTaylor.hs @@ -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 \ + + + + \" diff --git a/src/PropaFP/Translators/MetiTarski.hs b/src/PropaFP/Translators/MetiTarski.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/Translators/MetiTarski.hs @@ -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 diff --git a/src/PropaFP/VarMap.hs b/src/PropaFP/VarMap.hs new file mode 100644 --- /dev/null +++ b/src/PropaFP/VarMap.hs @@ -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] diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,2 @@ +main :: IO () +main = putStrLn "Test suite not yet implemented"