diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 diff --git a/PropaFP.cabal b/PropaFP.cabal --- a/PropaFP.cabal +++ b/PropaFP.cabal @@ -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 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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ 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) +![SPARK + PropaFP](https://github.com/rasheedja/PropaFP/raw/v0.1.1.0/images/SPARK_Toolchain_PropaFP.png) [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) diff --git a/src/PropaFP/DeriveBounds.hs b/src/PropaFP/DeriveBounds.hs --- a/src/PropaFP/DeriveBounds.hs +++ b/src/PropaFP/DeriveBounds.hs @@ -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 -- = diff --git a/src/PropaFP/Expression.hs b/src/PropaFP/Expression.hs --- a/src/PropaFP/Expression.hs +++ b/src/PropaFP/Expression.hs @@ -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)) diff --git a/src/PropaFP/Translators/FPTaylor.hs b/src/PropaFP/Translators/FPTaylor.hs --- a/src/PropaFP/Translators/FPTaylor.hs +++ b/src/PropaFP/Translators/FPTaylor.hs @@ -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] diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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 + diff --git a/test/TestFiles.hs b/test/TestFiles.hs new file mode 100644 --- /dev/null +++ b/test/TestFiles.hs @@ -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"