sbv 1.1 → 1.2
raw patch · 14 files changed
+87/−77 lines, 14 files
Files
- Data/SBV.hs +3/−12
- Data/SBV/BitVectors/Model.hs +6/−2
- Data/SBV/Examples/Existentials/CRCPolynomial.hs +1/−1
- Data/SBV/Examples/Puzzles/U2Bridge.hs +6/−6
- Data/SBV/Provers/Prover.hs +4/−4
- Data/SBV/Provers/Yices.hs +10/−10
- Data/SBV/Provers/Z3.hs +10/−13
- Data/SBV/SMT/SMT.hs +15/−14
- Data/SBV/SMT/SMTLib2.hs +5/−4
- Data/SBV/Tools/Optimize.hs +5/−5
- RELEASENOTES +17/−1
- SBVUnitTest/GoldFiles/U2Bridge.gold +2/−2
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +2/−2
Data/SBV.hs view
@@ -75,18 +75,9 @@ -- <http://goedel.cs.uiowa.edu/smtlib/>. -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver.--- Currently, we support the Yices SMT solver from SRI: <http://yices.csl.sri.com/>,--- and the Z3 SMT solver from Microsoft: <http://research.microsoft.com/en-us/um/redmond/projects/z3/>.------ You /should/ download and install Yices on your machine, and make sure the--- @yices@ executable is in your path before using the sbv library, as it is the--- current default solver. Alternatively, you can specify the location of yices--- executable in the environment variable @SBV_YICES@ and the options to yices--- in @SBV_YICES_OPTIONS@.------ Use of quantified variables require an installation of z3. Again,--- z3 must be in your path. Or, you can use the @SBV_Z3@ and @SBV_Z3_OPTIONS@--- environment variables to set the executable and the options.+-- Currently, we support the Z3 SMT solver from Microsoft: <http://research.microsoft.com/en-us/um/redmond/projects/z3/>+-- and the Yices SMT solver from SRI: <http://yices.csl.sri.com/>, out-of-the-box. Support for other solvers+-- can be added with relative ease. --------------------------------------------------------------------------------- module Data.SBV (
Data/SBV/BitVectors/Model.hs view
@@ -388,7 +388,11 @@ false = literal False bnot b | b `isConcretely` (== False) = true | b `isConcretely` (== True) = false- | True = liftSym1Bool (mkSymOp1 Not) not b+ | True = liftSym1Bool (mkSymOp1SC opt Not) not b+ where opt x+ | x == falseSW = Just trueSW+ | x == trueSW = Just falseSW+ | True = Nothing a &&& b | a `isConcretely` (== False) || b `isConcretely` (== False) = false | a `isConcretely` (== True) = b | b `isConcretely` (== True) = a@@ -768,7 +772,7 @@ case () of () | swa == swb -> return swa () | swa == trueSW && swb == falseSW -> return swt- () | swa == falseSW && swa == trueSW -> newExpr st sgnsz (SBVApp Not [swt])+ () | swa == falseSW && swb == trueSW -> newExpr st sgnsz (SBVApp Not [swt]) () -> newExpr st sgnsz (SBVApp Ite [swt, swa, swb]) -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind
Data/SBV/Examples/Existentials/CRCPolynomial.hs view
@@ -56,7 +56,7 @@ -- | Generate good CRC polynomials for 48-bit words, given the hamming distance @hd@. genPoly :: SWord8 -> IO ()-genPoly hd = do res <- allSatWith z3 $ do+genPoly hd = do res <- allSat $ do -- the polynomial is existentially specified p <- exists "polynomial" -- sent word, universal
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -249,16 +249,16 @@ -- Checking for solutions with 5 moves. -- Solution #1: -- 0 --> Edge, Bono--- 2 <-- Bono--- 3 --> Larry, Adam--- 13 <-- Edge+-- 2 <-- Edge+-- 4 --> Larry, Adam+-- 14 <-- Bono -- 15 --> Edge, Bono -- Total time: 17 -- Solution #2: -- 0 --> Edge, Bono--- 2 <-- Edge--- 4 --> Larry, Adam--- 14 <-- Bono+-- 2 <-- Bono+-- 3 --> Larry, Adam+-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves.
Data/SBV/Provers/Prover.hs view
@@ -51,16 +51,16 @@ import qualified Data.SBV.Provers.Z3 as Z3 import Data.SBV.Utils.TDiff -mkConfig :: SMTSolver -> Bool -> SMTConfig-mkConfig s isSMTLib2 = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = s, useSMTLib2 = isSMTLib2}+mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig+mkConfig s isSMTLib2 tweaks = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, smtFile = Nothing, solver = s, solverTweaks = tweaks, useSMTLib2 = isSMTLib2} -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig-yices = mkConfig Yices.yices False+yices = mkConfig Yices.yices False [] -- | Default configuration for the Z3 SMT solver z3 :: SMTConfig-z3 = mkConfig Z3.z3 True+z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantification"] -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig
Data/SBV/Provers/Yices.hs view
@@ -32,16 +32,16 @@ -- The default options are @\"-m -f\"@, which is valid for Yices 2 series. You can use the @SBV_YICES_OPTIONS@ environment variable to override the options. yices :: SMTSolver yices = SMTSolver {- name = "Yices"- , executable = "yices"- -- , 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)))- let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }- script = SMTScript { scriptBody = pgm, scriptModel = Nothing }- standardSolver cfg' script id (ProofError cfg) (interpretSolverOutput cfg (extractMap (map snd qinps) modelMap))+ name = "Yices"+ , executable = "yices"+ -- , 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)))+ 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)) } where addTimeOut Nothing o = o addTimeOut (Just i) o
Data/SBV/Provers/Z3.hs view
@@ -39,20 +39,17 @@ -- The default options are @\"\/in \/smt2\"@, which is valid for Z3 3.2. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver {- name = "z3"- , 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)))- let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }- script = SMTScript {scriptBody = "(set-option :mbqi true)\n" ++ pgm, scriptModel = Just (cont skolemMap)}- standardSolver cfg' script cleanErrs (ProofError cfg) (interpretSolverOutput cfg (extractMap isSat qinps modelMap . zipWith match skolemMap))+ name = "z3"+ , 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)))+ let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }+ script = SMTScript {scriptBody = unlines (solverTweaks cfg') ++ pgm, scriptModel = Just (cont skolemMap)}+ standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap . zipWith match skolemMap)) }- where -- This is quite crude and failure prone.. But is necessary to get z3 working through Wine on Mac- -- TODO: get rid of this once there's a native Z3 release- cleanErrs = intercalate "\n" . filter (not . junk) . lines- junk "fixme:heap:HeapSetInformation 0x0 1 0x0 0" = True+ where cleanErrs = intercalate "\n" . filter (not . junk) . lines junk s | "WARNING:" `isPrefixOf` s = True junk _ = False zero :: Size -> String
Data/SBV/SMT/SMT.hs view
@@ -35,23 +35,24 @@ -- | Solver configuration data SMTConfig = SMTConfig {- verbose :: Bool -- ^ Debug mode- , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)- , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)- , printBase :: Int -- ^ Print literals in this base- , solver :: SMTSolver -- ^ The actual SMT solver- , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)- , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1+ verbose :: Bool -- ^ Debug mode+ , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.)+ , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds)+ , printBase :: Int -- ^ Print literals in this base+ , solver :: SMTSolver -- ^ The actual SMT solver+ , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)+ , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)+ , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 } type SMTEngine = SMTConfig -> Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [Either SW (SW, [SW])] -> String -> IO SMTResult -- | An SMT solver data SMTSolver = SMTSolver {- name :: String -- ^ Printable name of the solver- , executable :: String -- ^ The path to its executable- , options :: [String] -- ^ Options to provide to the solver- , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output+ name :: String -- ^ Printable name of the solver+ , executable :: String -- ^ The path to its executable+ , options :: [String] -- ^ Options to provide to the solver+ , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output } -- | A model, as returned by a solver@@ -154,8 +155,8 @@ cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW]) cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r) -genParse :: Integral a => (Bool,Size) -> [CW] -> Maybe (a,[CW])-genParse (signed,size) (x:r)+genParse :: Integral a => (Bool, Size) -> [CW] -> Maybe (a, [CW])+genParse (signed, size) (x:r) | hasSign x == signed && sizeOf x == size = Just (fromIntegral (cwVal x),r) genParse _ _ = Nothing @@ -164,7 +165,7 @@ parseCWs xs = return ((), xs) instance SatModel Bool where- parseCWs xs = do (x,r) <- genParse (False, Size (Just 1)) xs+ parseCWs xs = do (x, r) <- genParse (False, Size (Just 1)) xs return ((x :: Integer) /= 0, r) instance SatModel Word8 where
Data/SBV/SMT/SMTLib2.hs view
@@ -150,9 +150,10 @@ wrap s = "(assert " ++ s ++ ")" skolemTable :: String -> (((Int, (Bool, Size), (Bool, Size)), [SW]), [String]) -> String-skolemTable qs (((i, (_, atSz), (_, rtSz)), _elts), _) = decl- where t = "table" ++ show i- decl = "(declare-fun " ++ t ++ " (" ++ qs ++ " " ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")"+skolemTable qsIn (((i, (_, atSz), (_, rtSz)), _elts), _) = decl+ where qs = if null qsIn then "" else qsIn ++ " "+ t = "table" ++ show i+ decl = "(declare-fun " ++ t ++ " (" ++ qs ++ smtType atSz ++ ") " ++ smtType rtSz ++ ")" -- Left if all constants, Right if otherwise genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, (Bool, Size), (Bool, Size)), [SW]) -> Either [String] [String]@@ -234,7 +235,7 @@ where pad n s = replicate (n - length s) '0' ++ s cvtCW :: CW -> String-cvtCW x | isInfPrec x = if w > 0 then show w else "(- " ++ show (abs w) ++ ")"+cvtCW x | isInfPrec x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")" where w = cwVal x cvtCW x | not (hasSign x) = hex (intSizeOf x) (cwVal x) -- signed numbers (with 2's complement representation) is problematic
Data/SBV/Tools/Optimize.hs view
@@ -19,7 +19,7 @@ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model (OrdSymbolic(..), EqSymbolic(..))-import Data.SBV.Provers.Prover (satWith, z3)+import Data.SBV.Provers.Prover (satWith, defaultSMTCfg) import Data.SBV.SMT.SMT (SatModel, getModel, SMTConfig(..)) import Data.SBV.Utils.Boolean @@ -42,9 +42,9 @@ optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg optimizeWith cfg Quantified = quantOptimize cfg --- | Variant of 'optimizeWith' using z3+-- | Variant of 'optimizeWith' using the default solver optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-optimize = optimizeWith z3+optimize = optimizeWith defaultSMTCfg -- | Variant of 'maximize' allowing the use of a user specified solver. maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])@@ -55,7 +55,7 @@ -- >>> maximize Quantified sum 3 (bAll (.< (10 :: SInteger))) -- Just [9,9,9] maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-maximize = maximizeWith z3+maximize = maximizeWith defaultSMTCfg -- | Variant of 'minimize' allowing the use of a user specified solver. minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])@@ -66,7 +66,7 @@ -- >>> minimize Quantified sum 3 (bAll (.> (10 :: SInteger))) -- Just [11,11,11] minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])-minimize = minimizeWith z3+minimize = minimizeWith defaultSMTCfg -- | Optimization using quantifiers quantOptimize :: (SatModel a, SymWord a) => SMTConfig -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])
RELEASENOTES view
@@ -1,7 +1,23 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 1.1+Latest Hackage released version: 1.2++======================================================================+Version 1.2, 2012-02-25++ Library:+ * Add a hook so users can add custom script segments for SMT solvers. The new+ "solverTweaks" field in the SMTConfig data-type can be used for this purpose.+ The need for this came about due to the need to workaround a Z3 v3.2 issue+ detalied below:+ http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks+ As a consequence, mixed Integer/BV problems can cause soundness issues in Z3+ and does in SBV. Unfortunately, it's too severe for SBV to add the woraround+ option, as it slows down the solver as a side effect as well. Thus, we're+ making this optionally available if/when needed. (Note that the work-around+ should not be necessary with Z3 v3.3; which isn't released yet.)+ * Other minor clean-up ====================================================================== Version 1.1, 2012-02-14
SBVUnitTest/GoldFiles/U2Bridge.gold view
@@ -3,13 +3,13 @@ s1 = 1 :: SWord8 s2 = 0 :: SWord8 s3 = True- s4 = 0 :: SWord8+ s4 = 1 :: SWord8 s5 = 0 :: SWord8 s6 = False s7 = 3 :: SWord8 s8 = 2 :: SWord8 s9 = True- s10 = 1 :: SWord8+ s10 = 0 :: SWord8 s11 = 0 :: SWord8 s12 = False s13 = 1 :: SWord8
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Tue Feb 14 19:29:22 PST 2012"+buildTime = "Sat Feb 25 12:23:39 PST 2012"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 1.1+Version: 1.2 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation. Description: Express properties about bit-precise Haskell programs and automatically prove@@ -69,7 +69,7 @@ . Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>. -Copyright: Levent Erkok, 2010-2011+Copyright: Levent Erkok, 2010-2012 License: BSD3 License-file: LICENSE Stability: Experimental