sbv 4.1 → 4.2
raw patch · 33 files changed
+175/−91 lines, 33 files
Files
- CHANGES.md +17/−1
- Data/SBV.hs +13/−9
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/BitVectors/Model.hs +12/−3
- Data/SBV/BitVectors/Rounding.hs +1/−1
- Data/SBV/Bridge/ABC.hs +7/−6
- Data/SBV/Bridge/Boolector.hs +7/−6
- Data/SBV/Bridge/CVC4.hs +7/−6
- Data/SBV/Bridge/MathSAT.hs +7/−6
- Data/SBV/Bridge/Yices.hs +6/−5
- Data/SBV/Bridge/Z3.hs +6/−5
- Data/SBV/Examples/BitPrecise/Legato.hs +2/−2
- Data/SBV/Examples/BitPrecise/MergeSort.hs +2/−2
- Data/SBV/Examples/BitPrecise/PrefixSum.hs +2/−10
- Data/SBV/Examples/Crypto/AES.hs +2/−2
- Data/SBV/Examples/Existentials/CRCPolynomial.hs +1/−1
- Data/SBV/Examples/Puzzles/Counts.hs +1/−1
- Data/SBV/Provers/ABC.hs +4/−3
- Data/SBV/Provers/Boolector.hs +3/−2
- Data/SBV/Provers/CVC4.hs +3/−2
- Data/SBV/Provers/MathSAT.hs +3/−2
- Data/SBV/Provers/Yices.hs +3/−2
- Data/SBV/Provers/Z3.hs +3/−2
- Data/SBV/SMT/SMT.hs +3/−2
- Data/SBV/SMT/SMTLib.hs +1/−1
- Data/SBV/Utils/Lib.hs +51/−1
- SBVUnitTest/Examples/CRC/CCITT.hs +1/−1
- SBVUnitTest/Examples/CRC/CCITT_Unidir.hs +1/−1
- SBVUnitTest/Examples/CRC/GenPoly.hs +1/−1
- SBVUnitTest/Examples/CRC/USB5.hs +1/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,23 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 4.1, 2015-03-06+* Latest Hackage released version: 4.2, 2015-03-17++### Version 4.2, 2015-03-17++ * Add exponentiation (.^). Thanks to Daniel Wagner for contributing the code!++ * Better handling of SBV_$SOLVER_OPTIONS, in particular keeping track of+ proper quoting in environment variables. Thanks to Adam Foltzer for+ the patch!++ * Silence some hlint/ghci warnings. Thanks to Trevor Elliott for the patch!++ * Haddock documentation fixes, improvements, etc.+ + * Change ABC default option string to %blast; "&sweep -C 5000; &syn4; &cec -s -m -C 2000"+ which seems to give good results. Use SBV_ABC_OPTIONS environment variable (or+ via abc.rc file and a combination of SBV_ABC_OPTIONS) to experiment. ### Version 4.1, 2015-03-06
Data/SBV.hs view
@@ -17,9 +17,9 @@ -- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8) -- Q.E.D. ----- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)+-- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8) -- Falsifiable. Counter-example:--- x = 51 :: SWord8+-- s0 = 32 :: SWord8 -- -- The function 'prove' has the following type: --@@ -81,14 +81,12 @@ -- all satisfying assignments, lazily. -- -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface:--- <http://goedel.cs.uiowa.edu/smtlib/>.+-- <http://smtlib.cs.uiowa.edu/> -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver. -- Currently, we support the following SMT-Solvers out-of-the box: ----- * Z3 from Microsoft: <http://research.microsoft.com/en-us/um/redmond/projects/z3/>------ * Yices from SRI: <http://yices.csl.sri.com/>+-- * ABC from University of Berkeley: <http://www.eecs.berkeley.edu/~alanmi/abc/> -- -- * CVC4 from New York University and University of Iowa: <http://cvc4.cs.nyu.edu/> --@@ -96,6 +94,10 @@ -- -- * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: <http://mathsat.fbk.eu/> --+-- * Yices from SRI: <http://yices.csl.sri.com/>+--+-- * Z3 from Microsoft: <http://z3.codeplex.com/>+-- -- SBV also allows calling these solvers in parallel, either getting results from multiple solvers -- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.) --@@ -146,6 +148,8 @@ , allEqual, allDifferent, inRange, sElem -- *** Addition and Multiplication with high-bits , fullAdder, fullMultiplier+ -- *** Exponentiation+ , (.^) -- *** Blasting/Unblasting , blastBE, blastLE, FromBits(..) -- *** Splitting, joining, and extending@@ -469,7 +473,7 @@ design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers.-To that end, we use the SMT-Lib standard (<http://goedel.cs.uiowa.edu/smtlib/>)+To that end, we use the SMT-Lib standard (<http://smtlib.cs.uiowa.edu/>) to communicate with arbitrary SMT solvers. -} @@ -650,7 +654,7 @@ others are not (such as pi and e). SBV can deal with real numbers just fine, since the theory of reals is decidable. (See-<http://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2>.) In addition, by leveraging backend+<http://smtlib.cs.uiowa.edu/theories/Reals.smt2>.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) -}@@ -821,4 +825,4 @@ elements of the domain and program further with those values as usual. -} -{-# ANN module "HLint: ignore Use import/export shortcut" #-}+{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}
Data/SBV/BitVectors/Data.hs view
@@ -1156,7 +1156,7 @@ -- Merging pushes the if-then-else choice down on to elements mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b --- | Arrays implemented in terms of SMT-arrays: <http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2>+-- | Arrays implemented in terms of SMT-arrays: <http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2> -- -- * Maps directly to SMT-lib arrays --
Data/SBV/BitVectors/Model.hs view
@@ -23,7 +23,7 @@ module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral , ite, iteLazy, sBranch, sAssert, sAssertCont, sbvTestBit, sbvPopCount, setBitTo- , sbvShiftLeft, sbvShiftRight, sbvRotateLeft, sbvRotateRight, sbvSignedShiftArithRight+ , sbvShiftLeft, sbvShiftRight, sbvRotateLeft, sbvRotateRight, sbvSignedShiftArithRight, (.^) , allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32@@ -662,6 +662,15 @@ -- just cannot rely on its default definition; which would be 0-0, which is not -0! negate = liftSym1 (mkSymOp1 UNeg) (\x -> -x) (\x -> -x) (\x -> -x) (\x -> -x) +-- | Symbolic exponentiation using bit blasting and repeated squaring.+--+-- N.B. The exponent must be unsigned. Signed exponents will be rejected.+(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b+b .^ e | isSigned e = error "(.^): exponentiation only works with unsigned exponents"+ | True = product $ zipWith (\use n -> ite use n 1)+ (blastLE e)+ (iterate (\x -> x*x) b)+ instance (SymWord a, Fractional a) => Fractional (SBV a) where fromRational = literal . fromRational x / y = liftSym2 (mkSymOp Quot) rationalCheck (/) die (/) (/) x y@@ -1883,5 +1892,5 @@ __unused :: a __unused = error "__unused" (isVacuous :: SBool -> IO Bool) (prove :: SBool -> IO ThmResult) -{-# ANN module "HLint: ignore Eta reduce" #-}-{-# ANN module "HLint: ignore Reduce duplication" #-}+{-# ANN module ("HLint: ignore Eta reduce" :: String) #-}+{-# ANN module ("HLint: ignore Reduce duplication" :: String)#-}
Data/SBV/BitVectors/Rounding.hs view
@@ -72,4 +72,4 @@ -- | SDouble instance instance RoundingFloat Double -{-# ANN module "HLint: ignore Reduce duplication" #-}+{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
Data/SBV/Bridge/ABC.hs view
@@ -9,15 +9,16 @@ -- Interface to the ABC verification and synthesis tool. Import this -- module if you want to use ABC as your backend solver. Also see: ----- - "Data.SBV.Bridge.Yices"------ - "Data.SBV.Bridge.Z3"--- -- - "Data.SBV.Bridge.Boolector"---+-- +-- - "Data.SBV.Bridge.CVC4"+-- -- - "Data.SBV.Bridge.MathSAT"+-- +-- - "Data.SBV.Bridge.Yices"+-- +-- - "Data.SBV.Bridge.Z3" ----- - "Data.SBV.Bridge.CVC4" --------------------------------------------------------------------------------- module Data.SBV.Bridge.ABC (
Data/SBV/Bridge/Boolector.hs view
@@ -9,15 +9,16 @@ -- Interface to the Boolector SMT solver. Import this module if you want to use the -- Boolector SMT prover as your backend solver. Also see: ----- - "Data.SBV.Bridge.Yices"------ - "Data.SBV.Bridge.Z3"---+-- - "Data.SBV.Bridge.ABC"+-- -- - "Data.SBV.Bridge.CVC4"---+-- -- - "Data.SBV.Bridge.MathSAT"+-- +-- - "Data.SBV.Bridge.Yices"+-- +-- - "Data.SBV.Bridge.Z3" ----- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Boolector (
Data/SBV/Bridge/CVC4.hs view
@@ -9,15 +9,16 @@ -- Interface to the CVC4 SMT solver. Import this module if you want to use the -- CVC4 SMT prover as your backend solver. Also see: ----- - "Data.SBV.Bridge.Yices"------ - "Data.SBV.Bridge.Z3"---+-- - "Data.SBV.Bridge.ABC"+-- -- - "Data.SBV.Bridge.Boolector"---+-- -- - "Data.SBV.Bridge.MathSAT"+-- +-- - "Data.SBV.Bridge.Yices"+-- +-- - "Data.SBV.Bridge.Z3" ----- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.CVC4 (
Data/SBV/Bridge/MathSAT.hs view
@@ -9,15 +9,16 @@ -- Interface to the MathSAT SMT solver. Import this module if you want to use the -- MathSAT SMT prover as your backend solver. Also see: --+-- - "Data.SBV.Bridge.ABC"+-- +-- - "Data.SBV.Bridge.Boolector"+-- +-- - "Data.SBV.Bridge.CVC4"+-- -- - "Data.SBV.Bridge.Yices"---+-- -- - "Data.SBV.Bridge.Z3" ----- - "Data.SBV.Bridge.CVC4"------ - "Data.SBV.Bridge.Boolector"------ - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.MathSAT (
Data/SBV/Bridge/Yices.hs view
@@ -9,15 +9,16 @@ -- Interface to the Yices SMT solver. Import this module if you want to use the -- Yices SMT prover as your backend solver. Also see: --+-- - "Data.SBV.Bridge.ABC"+-- -- - "Data.SBV.Bridge.Boolector"---+-- -- - "Data.SBV.Bridge.CVC4"------ - "Data.SBV.Bridge.Z3"---+-- -- - "Data.SBV.Bridge.MathSAT"+-- +-- - "Data.SBV.Bridge.Z3" ----- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Yices (
Data/SBV/Bridge/Z3.hs view
@@ -9,15 +9,16 @@ -- Interface to the Z3 SMT solver. Import this module if you want to use the -- Z3 SMT prover as your backend solver. Also see: --+-- - "Data.SBV.Bridge.ABC"+-- -- - "Data.SBV.Bridge.Boolector"---+-- -- - "Data.SBV.Bridge.CVC4"------ - "Data.SBV.Bridge.Yices"---+-- -- - "Data.SBV.Bridge.MathSAT"+-- +-- - "Data.SBV.Bridge.Yices" ----- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Z3 (
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -302,5 +302,5 @@ cgOutput "hi" hi cgOutput "lo" lo -{-# ANN legato "HLint: ignore Redundant $" #-}-{-# ANN module "HLint: ignore Reduce duplication" #-}+{-# ANN legato ("HLint: ignore Redundant $" :: String) #-}+{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
Data/SBV/Examples/BitPrecise/MergeSort.hs view
@@ -43,7 +43,7 @@ There are two main parts to proving that a sorting algorithm is correct: * Prove that the output is non-decreasing-+ * Prove that the output is a permutation of the input -} @@ -87,7 +87,7 @@ -- | Generate C code for merge-sorting an array of size 'n'. Again, we're restricted -- to fixed size inputs. While the output is not how one would code merge sort in C -- by hand, it's a faithful rendering of all the operations merge-sort would do as--- described by it's Haskell counterpart.+-- described by its Haskell counterpart. codeGen :: Int -> IO () codeGen n = compileToC (Just ("mergeSort" ++ show n)) "mergeSort" $ do xs <- cgInputArr n "xs"
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -171,15 +171,7 @@ ] -- | Prove the generic problem for powerlists of given sizes. Note that--- this will only work for Yices-1. This is due to the fact that Yices-2--- follows the SMT-Lib standard and does not accept bit-vector problems with--- quantified axioms in them, while Yices-1 did allow for that. The crux of--- the problem is that there are no SMT-Lib logics that combine BV's and--- quantifiers, see: <http://goedel.cs.uiowa.edu/smtlib/logics.html>. So we--- are stuck until new powerful logics are added to SMT-Lib.------ Here, we explicitly tell SBV to use Yices-1 that did not have that limitation.--- Tweak the executable location accordingly below for your platform..+-- this only works with Yices-1 currently. -- -- We have: --@@ -311,4 +303,4 @@ where gen = runSymbolic (True, Nothing) $ do args :: [SWord8] <- mkForallVars n mapM_ output $ ps (0, (+)) args -{-# ANN module "HLint: ignore Reduce duplication" #-}+{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
Data/SBV/Examples/Crypto/AES.hs view
@@ -577,5 +577,5 @@ cgAES128Library :: IO () cgAES128Library = compileToCLib Nothing "aes128Lib" aes128LibComponents -{-# ANN aesRound "HLint: ignore Use head" #-}-{-# ANN aesInvRound "HLint: ignore Use head" #-}+{-# ANN aesRound ("HLint: ignore Use head" :: String) #-}+{-# ANN aesInvRound ("HLint: ignore Use head" :: String) #-}
Data/SBV/Examples/Existentials/CRCPolynomial.hs view
@@ -97,4 +97,4 @@ findHD4Polynomials :: IO () findHD4Polynomials = genPoly 4 -{-# ANN crc_48_16 "HLint: ignore Use camelCase" #-}+{-# ANN crc_48_16 ("HLint: ignore Use camelCase" :: String) #-}
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -80,4 +80,4 @@ ++ ", of 8 is " ++ show (ns !! 8) ++ ", of 9 is " ++ show (ns !! 9) ++ "."-{-# ANN counts "HLint: ignore Use head" #-}+{-# ANN counts ("HLint: ignore Use head" :: String) #-}
Data/SBV/Provers/ABC.hs view
@@ -23,6 +23,7 @@ import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- | The description of abc. The default executable is @\"abc\"@, -- which must be in your path. You can use the @SBV_ABC@ environment@@ -33,10 +34,10 @@ abc = SMTSolver { name = ABC , executable = "abc"- , options = ["-S", "%blast; &put; dsat -s"]+ , options = ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_ABC" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_ABC_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_ABC" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_ABC_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg { solver = (solver cfg) {executable = execName, options = execOpts} } tweaks = case solverTweaks cfg' of [] -> ""
Data/SBV/Provers/Boolector.hs view
@@ -24,6 +24,7 @@ import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- | The description of the Boolector SMT solver -- The default executable is @\"boolector\"@, which must be in your path. You can use the @SBV_BOOLECTOR@ environment variable to point to the executable on your system.@@ -34,8 +35,8 @@ , executable = "boolector" , options = ["--smt2", "--smt2-model"] , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_BOOLECTOR" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_BOOLECTOR_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_BOOLECTOR" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_BOOLECTOR_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg {solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts}} tweaks = case solverTweaks cfg' of [] -> ""
Data/SBV/Provers/CVC4.hs view
@@ -25,6 +25,7 @@ import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- | The description of the CVC4 SMT solver -- The default executable is @\"cvc4\"@, which must be in your path. You can use the @SBV_CVC4@ environment variable to point to the executable on your system.@@ -35,8 +36,8 @@ , executable = "cvc4" , options = ["--lang", "smt"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_CVC4" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_CVC4_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_CVC4" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_CVC4_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} } tweaks = case solverTweaks cfg' of [] -> ""
Data/SBV/Provers/MathSAT.hs view
@@ -23,6 +23,7 @@ import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- | The description of the MathSAT SMT solver -- The default executable is @\"mathsat\"@, which must be in your path. You can use the @SBV_MATHSAT@ environment variable to point to the executable on your system.@@ -33,8 +34,8 @@ , executable = "mathsat" , options = ["-input=smt2"] , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_MATHSAT" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_MATHSAT_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_MATHSAT" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_MATHSAT_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} } tweaks = case solverTweaks cfg' of
Data/SBV/Provers/Yices.hs view
@@ -25,6 +25,7 @@ import Data.SBV.Provers.SExpr import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- | The description of the Yices SMT solver -- The default executable is @\"yices-smt\"@, which must be in your path. You can use the @SBV_YICES@ environment variable to point to the executable on your system.@@ -36,8 +37,8 @@ -- , options = ["-tc", "-smt", "-e"] -- For Yices1 , options = ["-m", "-f"] -- For Yices2 , engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do- execName <- getEnv "SBV_YICES" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_YICES_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_YICES" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_YICES_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg {solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts}} script = SMTScript {scriptBody = unlines (solverTweaks cfg') ++ pgm, scriptModel = Nothing} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap))
Data/SBV/Provers/Z3.hs view
@@ -26,6 +26,7 @@ import Data.SBV.BitVectors.PrettyNum import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import Data.SBV.Utils.Lib (splitArgs) -- Choose the correct prefix character for passing options -- TBD: Is there a more foolproof way of determining this?@@ -43,8 +44,8 @@ , executable = "z3" , options = map (optionPrefix:) ["in", "smt2"] , engine = \cfg isSat qinps modelMap skolemMap pgm -> do- execName <- getEnv "SBV_Z3" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))- execOpts <- (words `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ execName <- getEnv "SBV_Z3" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (splitArgs `fmap` getEnv "SBV_Z3_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} } tweaks = case solverTweaks cfg' of [] -> ""
Data/SBV/SMT/SMT.hs view
@@ -35,6 +35,7 @@ import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum+import Data.SBV.Utils.Lib (joinArgs) import Data.SBV.Utils.TDiff -- | Extract the final configuration from a result@@ -401,7 +402,7 @@ _ -> 0 -- can happen if ExitSuccess but there is output on stderr in return $ Left $ "Failed to complete the call to " ++ nm ++ "\nExecutable : " ++ show execPath- ++ "\nOptions : " ++ unwords opts+ ++ "\nOptions : " ++ joinArgs opts ++ "\nExit code : " ++ show finalEC ++ "\nSolver output: " ++ "\n" ++ line ++ "\n"@@ -421,7 +422,7 @@ opts = options smtSolver isTiming = timing config nmSolver = show (name smtSolver)- msg $ "Calling: " ++ show (unwords (exec:opts))+ msg $ "Calling: " ++ show (unwords (exec:[joinArgs opts])) case smtFile config of Nothing -> return () Just f -> do msg $ "Saving the generated script in file: " ++ show f
Data/SBV/SMT/SMTLib.hs view
@@ -121,4 +121,4 @@ ++ "\n\tParse: " ++ show r extract _ = [] -{-# ANN interpretSolverModelLine "HLint: ignore Use elemIndex" #-}+{-# ANN interpretSolverModelLine ("HLint: ignore Use elemIndex" :: String) #-}
Data/SBV/Utils/Lib.hs view
@@ -9,8 +9,11 @@ -- Misc helpers ----------------------------------------------------------------------------- -module Data.SBV.Utils.Lib where+module Data.SBV.Utils.Lib (mlift2, mlift3, mlift4, mlift5, mlift6, mlift7, mlift8, joinArgs, splitArgs) where +import Data.Char (isSpace)+import Data.Maybe (fromJust, isNothing)+ -- | Monadic lift over 2-tuples mlift2 :: Monad m => (a' -> b' -> r) -> (a -> m a') -> (b -> m b') -> (a, b) -> m r mlift2 k f g (a, b) = f a >>= \a' -> g b >>= \b' -> return $ k a' b'@@ -38,3 +41,50 @@ -- | Monadic lift over 8-tuples mlift8 :: Monad m => (a' -> b' -> c' -> d' -> e' -> f' -> g' -> h' -> r) -> (a -> m a') -> (b -> m b') -> (c -> m c') -> (d -> m d') -> (e -> m e') -> (f -> m f') -> (g -> m g') -> (h -> m h') -> (a, b, c, d, e, f, g, h) -> m r mlift8 k f g h i j l m n (a, b, c, d, e, y, z, w) = f a >>= \a' -> g b >>= \b' -> h c >>= \c' -> i d >>= \d' -> j e >>= \e' -> l y >>= \y' -> m z >>= \z' -> n w >>= \w' -> return $ k a' b' c' d' e' y' z' w'++-- Command line argument parsing code courtesy of Neil Mitchell's cmdargs package: see+-- <https://github.com/ndmitchell/cmdargs/blob/master/System/Console/CmdArgs/Explicit/SplitJoin.hs>++-- | Given a sequence of arguments, join them together in a manner that could be used on+-- the command line, giving preference to the Windows @cmd@ shell quoting conventions.+--+-- For an alternative version, intended for actual running the result in a shell, see "System.Process.showCommandForUser"+joinArgs :: [String] -> String+joinArgs = unwords . map f+ where f x = q ++ g x ++ q+ where hasSpace = any isSpace x+ q = ['\"' | hasSpace || null x]+ g ('\\':'\"':xs) = '\\':'\\':'\\':'\"': g xs+ g "\\" | hasSpace = "\\\\"+ g ('\"':xs) = '\\':'\"': g xs+ g (x':xs) = x' : g xs+ g [] = []++data State = Init -- either I just started, or just emitted something+ | Norm -- I'm seeing characters+ | Quot -- I've seen a quote++-- | Given a string, split into the available arguments. The inverse of 'joinArgs'.+-- Courtesy of the cmdargs package.+splitArgs :: String -> [String]+splitArgs = join . f Init+ where -- Nothing is start a new string+ -- Just x is accumulate onto the existing string+ join :: [Maybe Char] -> [String]+ join [] = []+ join xs = map fromJust a : join (drop 1 b)+ where (a,b) = break isNothing xs++ f Init (x:xs) | isSpace x = f Init xs+ f Init "\"\"" = [Nothing]+ f Init "\"" = [Nothing]+ f Init xs = f Norm xs+ f m ('\"':'\"':'\"':xs) = Just '\"' : f m xs+ f m ('\\':'\"':xs) = Just '\"' : f m xs+ f m ('\\':'\\':'\"':xs) = Just '\\' : f m ('\"':xs)+ f Norm ('\"':xs) = f Quot xs+ f Quot ('\"':'\"':xs) = Just '\"' : f Norm xs+ f Quot ('\"':xs) = f Norm xs+ f Norm (x:xs) | isSpace x = Nothing : f Init xs+ f m (x:xs) = Just x : f m xs+ f _ [] = []
SBVUnitTest/Examples/CRC/CCITT.hs view
@@ -59,4 +59,4 @@ putStrLn $ " Sent : " ++ binS (mkFrame (literal sh, literal sl)) putStrLn $ " Received: " ++ binS (mkFrame (literal rh, literal rl)) -{-# ANN crc_48_16 "HLint: ignore Use camelCase" #-}+{-# ANN crc_48_16 ("HLint: ignore Use camelCase" :: String) #-}
SBVUnitTest/Examples/CRC/CCITT_Unidir.hs view
@@ -57,4 +57,4 @@ ccitHDis4 :: IO () ccitHDis4 = print =<< prove (crcUniGood 4) -{-# ANN crc_48_16 "HLint: ignore Use camelCase" #-}+{-# ANN crc_48_16 ("HLint: ignore Use camelCase" :: String) #-}
SBVUnitTest/Examples/CRC/GenPoly.hs view
@@ -72,4 +72,4 @@ findHD3Polynomials :: IO () findHD3Polynomials = genPoly 3 -{-# ANN crc_48_16 "HLint: ignore Use camelCase" #-}+{-# ANN crc_48_16 ("HLint: ignore Use camelCase" :: String) #-}
SBVUnitTest/Examples/CRC/USB5.hs view
@@ -48,4 +48,4 @@ frameSent = mkFrame sent frameReceived = mkFrame received -{-# ANN crc_11_16 "HLint: ignore Use camelCase" #-}+{-# ANN crc_11_16 ("HLint: ignore Use camelCase" :: String) #-}
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Fri Mar 6 17:06:57 PST 2015"+buildTime = "Tue Mar 17 00:18:03 PDT 2015"
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -327,4 +327,4 @@ ds :: [Double] ds = nan : -infinity : infinity : 0 : -0 : [-5.0, -4.1 .. 5] ++ [5]-{-# ANN module "HLint: ignore Reduce duplication" #-}+{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 4.1+Version: 4.2 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT