PropaFP 0.1.0.0 → 0.1.1.0
raw patch · 8 files changed
+189/−15 lines, 8 filesdep ~basedep ~scientificPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, scientific
API changes (from Hackage documentation)
Files
- ChangeLog.md +16/−0
- PropaFP.cabal +10/−9
- README.md +4/−4
- src/PropaFP/DeriveBounds.hs +1/−0
- src/PropaFP/Expression.hs +1/−0
- src/PropaFP/Translators/FPTaylor.hs +1/−1
- test/Spec.hs +58/−1
- test/TestFiles.hs +98/−0
ChangeLog.md view
@@ -1,3 +1,19 @@ # Changelog for PropaFP ## Unreleased changes++## [v0.1.1.0](https://github.com/rasheedja/PropaFP/compare/v0.1.0.0...v0.1.1.0)++- Remove quotes from FPTaylor variables, allowing support for FPTaylor >=0.9.3+- Re-enable `PropaFP.Expression.normalizeBoolean` in `PropaFP.DeriveBounds`+ - Aggressive simplification rules applied in `normalizeBoolean` are sometimes required to successfully derive bounds for variables+- Add `eliminate_if` transformation to the PropaFP Why3 driver+ - This transformation performs simplifications that PropaFP cannot currently do, making some problems easier for provers+- Regenerate Why3 SMT files using new driver+- Add test suite+ - Tests dReal(/LPPaver) and MetiTarski translators+ - Checks that PropaFP generated files are the same as the processed files stored under the examples folder++## [v0.1.0.0](https://github.com/rasheedja/PropaFP/tree/v0.1.0.0)++- Initial release
PropaFP.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: PropaFP-version: 0.1.0.0+version: 0.1.1.0 synopsis: Auto-active verification of floating-point programs description: Please see the README on GitHub at <https://github.com/rasheedja/PropaFP#readme> category: Math, Maths, Mathematics, Formal methods, Theorem Provers@@ -71,7 +71,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -108,7 +108,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -145,7 +145,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -182,7 +182,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -219,7 +219,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -256,7 +256,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -293,7 +293,7 @@ , 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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010 @@ -301,6 +301,7 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules:+ TestFiles Paths_PropaFP hs-source-dirs: test@@ -333,6 +334,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+ , scientific >=0.3.7.0 && <0.4 , temporary ==1.3.* default-language: Haskell2010
README.md view
@@ -8,7 +8,7 @@ Below is a diagram summarising the integration with PropaFP and SPARK. -+ [1]: https://en.wikipedia.org/wiki/SPARK_(programming_language) [2]: https://en.wikipedia.org/wiki/Ada_(programming_language)@@ -43,7 +43,7 @@ ### PropaFP as a Standalone Program -To produce some input for PropaFP, see the [Reference](https://github.com/rasheedja/PropaFP/blob/c7680a48c9524768ac113ab5ca0e179dc2f315c6/REFERENCE.md).+To produce some input for PropaFP, see the [Reference](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/REFERENCE.md). #### Translator Executables @@ -70,8 +70,8 @@ ### 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)+For instructions to use with GNAT Studio 2022, see [sparkFiles/INSTRUCTIONS.md](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/sparkFiles/INSTRUCTIONS.md) ## Guided Example -[A guided example of using PropaFP with GNAT Studio.](https://github.com/rasheedja/PropaFP/blob/c7680a48c9524768ac113ab5ca0e179dc2f315c6/sparkFiles/EXAMPLE.md)+[A guided example of using PropaFP with GNAT Studio.](https://github.com/rasheedja/PropaFP/blob/v0.1.1.0/sparkFiles/EXAMPLE.md)
src/PropaFP/DeriveBounds.hs view
@@ -153,6 +153,7 @@ 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 + | normalizeBoolean cond1 P.== normalizeBoolean 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 -- =
src/PropaFP/Expression.hs view
@@ -1260,6 +1260,7 @@ -- 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 + -- Eliminate implications and distribute FNots -- 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))
src/PropaFP/Translators/FPTaylor.hs view
@@ -77,7 +77,7 @@ variableBoundsToFPTaylor :: VarMap -> String variableBoundsToFPTaylor [] = ""-variableBoundsToFPTaylor ((v, (l, r)) : vs) = "real " ++ show v ++ " in [" ++ showFrac l ++ ", " ++ showFrac r ++ "];\n" ++ variableBoundsToFPTaylor vs+variableBoundsToFPTaylor ((v, (l, r)) : vs) = "real " ++ v ++ " in [" ++ showFrac l ++ ", " ++ showFrac r ++ "];\n" ++ variableBoundsToFPTaylor vs where showFrac :: Rational -> [Char]
test/Spec.hs view
@@ -1,2 +1,59 @@+module Main where++import Prelude+import TestFiles+import System.Directory+import PropaFP.Expression+import PropaFP.VarMap+import PropaFP.Parsers.Smt+import PropaFP.Translators.DReal+import PropaFP.Translators.MetiTarski+import System.Exit+import MixedTypesNumPrelude (ifThenElse)+ main :: IO ()-main = putStrLn "Test suite not yet implemented"+main = do+ putStrLn "Testing dReal translator"+ testProverTranslator allTestFiles DReal []+ putStrLn "Testing MetiTarski translator"+ testProverTranslator allTestFiles MetiTarski unsupportedByMetiTarskiFiles+ exitSuccess++-- |Take a list of input files, a prover for which PropaFP provides a translator, and a list of files unsupported by the translator.+-- Test if PropaFP generates the same file as the one stored (currently under PropaFP/examples/testParent/proverFolderName/testName.proverExt)+testProverTranslator :: [(String, String)] -> SupportedProver -> [(String, String)] -> IO ()+testProverTranslator [] _ _ = putStrLn "All tests passed"+testProverTranslator (test@(testParent, testName) : tests) prover unsupportedTests = do+ mFptaylorPath <- findExecutable "fptaylor"+ currentDirectory <- getCurrentDirectory+ case mFptaylorPath of+ Nothing -> putStrLn "FPTaylor executable not found in PATH"+ Just fptaylorPath -> do+ let vcToProcess = currentDirectory ++ "/examples/" ++ testParent ++ "/why3smt/" ++ testName ++ ".smt2"+ let originalProcessedVCPath = currentDirectory ++ "/examples/" ++ testParent ++ "/" ++ getProverFolderName prover ++ "/" ++ testName ++ "." ++ getFileExtension prover+ if test `elem` unsupportedTests+ then do+ putStrLn ("Test skipped (unsupported): " ++ vcToProcess) + testProverTranslator tests prover unsupportedTests+ else do+ originalProcessedVC <- readFile originalProcessedVCPath+ mNewProcessedVC <- parseVCToSolver vcToProcess fptaylorPath (getTranslator prover) (getNegationStatus prover)+ case mNewProcessedVC of+ Just newProcessedVC -> + if newProcessedVC == originalProcessedVC+ then do+ putStrLn ("Test passed: " ++ vcToProcess)+ testProverTranslator tests prover unsupportedTests+ else do+ putStrLn $ "Processing the following file for dReal: " ++ vcToProcess+ putStrLn $ "Resulted in an output that differs from: " ++ originalProcessedVCPath+ putStrLn $ "The incorrect output is:\n"+ putStrLn newProcessedVC + putStrLn $ "The correct output is:\n"+ putStrLn originalProcessedVC+ putStrLn ("Test failed: " ++ vcToProcess)+ exitFailure+ Nothing -> do+ putStrLn $ "Issue generating input for dReal using file: " ++ vcToProcess + exitFailure+
+ test/TestFiles.hs view
@@ -0,0 +1,98 @@+module TestFiles where++import Prelude+import PropaFP.Expression+import PropaFP.VarMap+import PropaFP.Translators.DReal (formulaAndVarMapToDReal)+import PropaFP.Translators.MetiTarski (formulaAndVarMapToMetiTarski)++-- |Files which PropaFP can process within a few seconds+quickTestFiles :: [(String, String)]+quickTestFiles =+ [+ ("heron", "heron_init"),+ ("heron", "heron_pres"),+ ("hie_sine", "approx_cos_ge"),+ ("hie_sine", "approx_cos_ge_b1"),+ ("hie_sine", "approx_cos_ge_b2"),+ ("hie_sine", "approx_cos_ge_b3"),+ ("hie_sine", "approx_cos_le"),+ ("hie_sine", "approx_cos_le_b1"),+ ("hie_sine", "approx_cos_le_b2"),+ ("hie_sine", "approx_cos_le_b3"),+ ("hie_sine", "approx_sin_ge"),+ ("hie_sine", "approx_sin_ge_b1"),+ ("hie_sine", "approx_sin_ge_b2"),+ ("hie_sine", "approx_sin_ge_b3"),+ ("hie_sine", "approx_sin_le"),+ ("hie_sine", "approx_sin_le_b1"),+ ("hie_sine", "approx_sin_le_b2"),+ ("hie_sine", "approx_sin_le_b3"),+ ("hie_sine", "my_machine_rounding_ge"),+ ("hie_sine", "my_machine_rounding_le"),+ ("hie_sine", "reduce_half_pi_x_ge"),+ ("hie_sine", "reduce_half_pi_x_le"),+ ("hie_sine", "sin_ge"),+ ("hie_sine", "sin_le"),+ ("taylor_sine", "taylor_sin_double"),+ ("taylor_sine", "taylor_sin_p"),+ ("taylor_sine", "taylor_sin_plus"),+ ("taylor_sine", "taylor_sin_swap"),+ ("taylor_sine", "taylor_sin_tight"),+ ("taylor_sine", "taylor_sin"),+ ("taylor_sine", "sinsin"),+ ("taylor_sine", "sinsin_b1"),+ ("taylor_sine", "sinsin_b2"),+ ("taylor_sine", "sinsin_b3")+ ]++-- |Files which take at least a few seconds to process by PropaFP+slowTestFiles :: [(String, String)]+slowTestFiles = + [+ ("hie_sine", "reduce_half_pi_ge"),+ ("hie_sine", "reduce_half_pi_le")+ ]++-- |Files unsupported by the MetiTarski translator+unsupportedByMetiTarskiFiles :: [(String, String)]+unsupportedByMetiTarskiFiles =+ [+ ("hie_sine", "my_machine_rounding_ge"),+ ("hie_sine", "my_machine_rounding_le"),+ ("hie_sine", "sin_ge"),+ ("hie_sine", "sin_le"),+ ("taylor_sine", "taylor_sin_double"),+ ("taylor_sine", "taylor_sin_p"),+ ("taylor_sine", "taylor_sin_plus"),+ ("taylor_sine", "taylor_sin_swap"),+ ("taylor_sine", "taylor_sin_tight"),+ ("taylor_sine", "taylor_sin")+ ]++-- |Quick + slow test files+allTestFiles :: [(String, String)]+allTestFiles = quickTestFiles ++ slowTestFiles++-- |Provers for which PropaFP provides translators+data SupportedProver = MetiTarski | DReal++-- |Get the translator function for a chosen prover+getTranslator :: SupportedProver -> (F -> TypedVarMap -> String)+getTranslator MetiTarski = formulaAndVarMapToMetiTarski+getTranslator DReal = formulaAndVarMapToDReal++-- |Check if PropaFP should negate a VC before translating for one of these provers+getNegationStatus :: SupportedProver -> Bool+getNegationStatus MetiTarski = True+getNegationStatus DReal = False++-- |Get the file extension that the PropaFP translator writes to for a certain prover+getFileExtension :: SupportedProver -> String+getFileExtension MetiTarski = "tptp"+getFileExtension DReal = "smt2"++-- |Get the name of the folder under which the translated files are stored in the PropaFP repo+getProverFolderName :: SupportedProver -> String+getProverFolderName MetiTarski = "metit"+getProverFolderName DReal = "smt"