packages feed

sbv 2.8 → 2.9

raw patch · 41 files changed

+780/−402 lines, 41 files

Files

@@ -1,4 +1,4 @@-Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2013, Levent Erkok (erkokl@gmail.com) All rights reserved.  The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV.hs view
@@ -76,9 +76,16 @@ -- <http://goedel.cs.uiowa.edu/smtlib/>. -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver.--- 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.+-- 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/>+--+--   * CVC4 from New York University and University of Iowa: <http://cvc4.cs.nyu.edu/>+--+-- Support for other compliant solvers can be added relatively easily, please+-- get in touch if there is a solver you'd like to see included. ---------------------------------------------------------------------------------  module Data.SBV (@@ -151,11 +158,11 @@   -- ** Predicates   , Predicate, Provable(..), Equality(..)   -- ** Proving properties-  , prove, proveWith, isTheorem, isTheoremWithin+  , prove, proveWith, isTheorem, isTheoremWith   -- ** Checking satisfiability-  , sat, satWith, isSatisfiable, isSatisfiableWithin+  , sat, satWith, isSatisfiable, isSatisfiableWith   -- ** Finding all satisfying assignments-  , allSat, allSatWith, numberOfModels+  , allSat, allSatWith   -- ** Satisfying a sequence of boolean conditions   , solve   -- ** Adding constraints@@ -184,7 +191,7 @@   , SatModel(..), Modelable(..), displayModels, extractModels    -- * SMT Interface: Configurations and solvers-  , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, defaultSMTCfg, sbvCheckSolverInstallation+  , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, cvc4, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation    -- * Symbolic computations   , Symbolic, output, SymWord(..)@@ -249,6 +256,13 @@ import Data.Int import Data.Ratio import Data.Word++-- | The currently active solver, obtained by importing "Data.SBV".+-- To have other solvers /current/, import one of the bridge+-- modules "Data.SBV.Bridge.CVC4", "Data.SBV.Bridge.Yices", or+-- "Data.SBV.Bridge.Z3" directly.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = z3  -- Haddock section documentation {- $progIntro
+ Data/SBV/Bridge/CVC4.hs view
@@ -0,0 +1,103 @@+---------------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Bridge.CVC4+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- 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"+---------------------------------------------------------------------------------++module Data.SBV.Bridge.CVC4 (+  -- * CVC4 specific interface+  sbvCurrentSolver+  -- ** Proving and checking satisfiability+  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  -- ** Optimization routines+  , optimize, minimize, maximize+  -- * Non-CVC4 specific SBV interface+  -- $moduleExportIntro+  , module Data.SBV+  ) where++import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)++-- | Current solver instance, pointing to cvc4.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = cvc4++-- | Prove theorems, using the CVC4 SMT solver+prove :: Provable a+      => a              -- ^ Property to check+      -> IO ThmResult   -- ^ Response from the SMT solver, containing the counter-example if found+prove = proveWith sbvCurrentSolver++-- | Find satisfying solutions, using the CVC4 SMT solver+sat :: Provable a+    => a                -- ^ Property to check+    -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found+sat = satWith sbvCurrentSolver++-- | Find all satisfying solutions, using the CVC4 SMT solver+allSat :: Provable a+       => a                -- ^ Property to check+       -> IO AllSatResult  -- ^ List of all satisfying models+allSat = allSatWith sbvCurrentSolver++-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the CVC4 SMT solver+isVacuous :: Provable a+          => a             -- ^ Property to check+          -> IO Bool       -- ^ True if the constraints are unsatisifiable+isVacuous = isVacuousWith sbvCurrentSolver++-- | Check if the statement is a theorem, with an optional time-out in seconds, using the CVC4 SMT solver+isTheorem :: Provable a+          => Maybe Int          -- ^ Optional time-out, specify in seconds+          -> a                  -- ^ Property to check+          -> IO (Maybe Bool)    -- ^ Returns Nothing if time-out expires+isTheorem = isTheoremWith sbvCurrentSolver++-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the CVC4 SMT solver+isSatisfiable :: Provable a+              => Maybe Int       -- ^ Optional time-out, specify in seconds+              -> a               -- ^ Property to check+              -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers+isSatisfiable = isSatisfiableWith sbvCurrentSolver++-- | Optimize cost functions, using the CVC4 SMT solver+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> (SBV c -> SBV c -> SBool)   -- ^ Betterness check: This is the comparison predicate for optimization+         -> ([SBV a] -> SBV c)          -- ^ Cost function+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+optimize = optimizeWith sbvCurrentSolver++-- | Minimize cost functions, using the CVC4 SMT solver+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to minimize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+minimize = minimizeWith sbvCurrentSolver++-- | Maximize cost functions, using the CVC4 SMT solver+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to maximize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+maximize = maximizeWith sbvCurrentSolver++{- $moduleExportIntro+The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.+-}
+ Data/SBV/Bridge/Yices.hs view
@@ -0,0 +1,103 @@+---------------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Bridge.Yices+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- 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.CVC4"+--+--       - "Data.SBV.Bridge.Z3"+---------------------------------------------------------------------------------++module Data.SBV.Bridge.Yices (+  -- * Yices specific interface+  sbvCurrentSolver+  -- ** Proving and checking satisfiability+  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  -- ** Optimization routines+  , optimize, minimize, maximize+  -- * Non-Yices specific SBV interface+  -- $moduleExportIntro+  , module Data.SBV+  ) where++import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)++-- | Current solver instance, pointing to yices.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = yices++-- | Prove theorems, using the Yices SMT solver+prove :: Provable a+      => a              -- ^ Property to check+      -> IO ThmResult   -- ^ Response from the SMT solver, containing the counter-example if found+prove = proveWith sbvCurrentSolver++-- | Find satisfying solutions, using the Yices SMT solver+sat :: Provable a+    => a                -- ^ Property to check+    -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found+sat = satWith sbvCurrentSolver++-- | Find all satisfying solutions, using the Yices SMT solver+allSat :: Provable a+       => a                -- ^ Property to check+       -> IO AllSatResult  -- ^ List of all satisfying models+allSat = allSatWith sbvCurrentSolver++-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the Yices SMT solver+isVacuous :: Provable a+          => a             -- ^ Property to check+          -> IO Bool       -- ^ True if the constraints are unsatisifiable+isVacuous = isVacuousWith sbvCurrentSolver++-- | Check if the statement is a theorem, with an optional time-out in seconds, using the Yices SMT solver+isTheorem :: Provable a+          => Maybe Int          -- ^ Optional time-out, specify in seconds+          -> a                  -- ^ Property to check+          -> IO (Maybe Bool)    -- ^ Returns Nothing if time-out expires+isTheorem = isTheoremWith sbvCurrentSolver++-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the Yices SMT solver+isSatisfiable :: Provable a+              => Maybe Int       -- ^ Optional time-out, specify in seconds+              -> a               -- ^ Property to check+              -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers+isSatisfiable = isSatisfiableWith sbvCurrentSolver++-- | Optimize cost functions, using the Yices SMT solver+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> (SBV c -> SBV c -> SBool)   -- ^ Betterness check: This is the comparison predicate for optimization+         -> ([SBV a] -> SBV c)          -- ^ Cost function+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+optimize = optimizeWith sbvCurrentSolver++-- | Minimize cost functions, using the Yices SMT solver+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to minimize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+minimize = minimizeWith sbvCurrentSolver++-- | Maximize cost functions, using the Yices SMT solver+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to maximize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+maximize = maximizeWith sbvCurrentSolver++{- $moduleExportIntro+The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.+-}
+ Data/SBV/Bridge/Z3.hs view
@@ -0,0 +1,103 @@+---------------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Bridge.Z3+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- 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.CVC4"+--+--       - "Data.SBV.Bridge.Yices"+---------------------------------------------------------------------------------++module Data.SBV.Bridge.Z3 (+  -- * Z3 specific interface+  sbvCurrentSolver+  -- ** Proving and checking satisfiability+  , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+  -- ** Optimization routines+  , optimize, minimize, maximize+  -- * Non-Z3 specific SBV interface+  -- $moduleExportIntro+  , module Data.SBV+  ) where++import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)++-- | Current solver instance, pointing to z3.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = z3++-- | Prove theorems, using the Z3 SMT solver+prove :: Provable a+      => a              -- ^ Property to check+      -> IO ThmResult   -- ^ Response from the SMT solver, containing the counter-example if found+prove = proveWith sbvCurrentSolver++-- | Find satisfying solutions, using the Z3 SMT solver+sat :: Provable a+    => a                -- ^ Property to check+    -> IO SatResult     -- ^ Response of the SMT Solver, containing the model if found+sat = satWith sbvCurrentSolver++-- | Find all satisfying solutions, using the Z3 SMT solver+allSat :: Provable a+       => a                -- ^ Property to check+       -> IO AllSatResult  -- ^ List of all satisfying models+allSat = allSatWith sbvCurrentSolver++-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the Z3 SMT solver+isVacuous :: Provable a+          => a             -- ^ Property to check+          -> IO Bool       -- ^ True if the constraints are unsatisifiable+isVacuous = isVacuousWith sbvCurrentSolver++-- | Check if the statement is a theorem, with an optional time-out in seconds, using the Z3 SMT solver+isTheorem :: Provable a+          => Maybe Int          -- ^ Optional time-out, specify in seconds+          -> a                  -- ^ Property to check+          -> IO (Maybe Bool)    -- ^ Returns Nothing if time-out expires+isTheorem = isTheoremWith sbvCurrentSolver++-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the Z3 SMT solver+isSatisfiable :: Provable a+              => Maybe Int       -- ^ Optional time-out, specify in seconds+              -> a               -- ^ Property to check+              -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers+isSatisfiable = isSatisfiableWith sbvCurrentSolver++-- | Optimize cost functions, using the Z3 SMT solver+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> (SBV c -> SBV c -> SBool)   -- ^ Betterness check: This is the comparison predicate for optimization+         -> ([SBV a] -> SBV c)          -- ^ Cost function+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+optimize = optimizeWith sbvCurrentSolver++-- | Minimize cost functions, using the Z3 SMT solver+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to minimize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+minimize = minimizeWith sbvCurrentSolver++-- | Maximize cost functions, using the Z3 SMT solver+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+         => OptimizeOpts                -- ^ Parameters to optimization (Iterative, Quantified, etc.)+         -> ([SBV a] -> SBV c)          -- ^ Cost function to maximize+         -> Int                         -- ^ Number of inputs+         -> ([SBV a] -> SBool)          -- ^ Validity function+         -> IO (Maybe [a])              -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+maximize = maximizeWith sbvCurrentSolver++{- $moduleExportIntro+The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.+-}
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -129,8 +129,8 @@ -- (NB. We need to use yices for this proof as the uninterpreted function -- examples are only supported through the yices interface currently.) thm3 :: IO ThmResult-thm3 = proveWith yices $ do args :: PowerList SWord32 <- mkForallVars 8-                            return $ ps (u, op) args .== lf (u, op) args+thm3 = proveWith yicesSMT09 $ do args :: PowerList SWord32 <- mkForallVars 8+                                 return $ ps (u, op) args .== lf (u, op) args   where op :: SWord32 -> SWord32 -> SWord32         op = uninterpret "flOp"         u :: SWord32@@ -195,10 +195,20 @@   | i <= 1 || (i .&. (i-1)) /= 0   = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i   | True-  = proveWith cfg $ genPrefixSumInstance i-  where cfg = yices { solver = yices' }-        yices' = Yices.yices { options    = ["-tc", "-smt", "-e"]+  = proveWith yices1029 $ genPrefixSumInstance i++-- | Old version of Yices that supports quantified axioms in SMT-Lib1+yices1029 :: SMTConfig+yices1029 = yices {solver = yices'}+  where yices' = Yices.yices { options    = ["-tc", "-smt", "-e"]                              , executable = "yices-1.0.29"+                             }++-- | Another old version of yices, suitable for the non-axiom based problem+yicesSMT09 :: SMTConfig+yicesSMT09 = yices {solver = yices'}+  where yices' = Yices.yices { options    = ["-m"]+                             , executable = "yices-SMT09"                              }  ----------------------------------------------------------------------
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -12,6 +12,7 @@ module Data.SBV.Examples.Uninterpreted.Function where  import Data.SBV+import qualified Data.SBV.Provers.Yices as Yices  -- | An uninterpreted function f :: SWord8 -> SWord8 -> SWord16@@ -30,7 +31,7 @@ -- counterexamples are not yet supported by sbv.) We have: -- ----- >>> proveWith yices $ forAll ["x", "y"] thmBad+-- >>> proveWith yicesSMT09 $ forAll ["x", "y"] thmBad -- Falsifiable. Counter-example: --   x = 0 :: SWord8 --   y = 128 :: SWord8@@ -42,3 +43,16 @@ -- thus providing evidence that the asserted theorem is not valid. thmBad :: SWord8 -> SWord8 -> SBool thmBad x y = f x y .== f y x++-- | Old version of Yices, which supports nice output for uninterpreted functions.+yicesSMT09 :: SMTConfig+yicesSMT09 = yices {solver = yices'}+  where yices' = Yices.yices { options    = ["-m"]+                             , executable = "yices-SMT09"+                             }++----------------------------------------------------------------------+-- * Inspecting symbolic traces+----------------------------------------------------------------------++-- | A symbolic trace can help illustrate the action of Ladner-Fischer. This
+ Data/SBV/Provers/CVC4.hs view
@@ -0,0 +1,89 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.SBV.Provers.CVC4+-- Copyright   :  (c) Levent Erkok+-- License     :  BSD3+-- Maintainer  :  erkokl@gmail.com+-- Stability   :  experimental+--+-- The connection to the CVC4 SMT solver+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module Data.SBV.Provers.CVC4(cvc4) where++import qualified Control.Exception as C++import Data.Char          (isSpace)+import Data.Function      (on)+import Data.List          (sortBy, intercalate)+import System.Environment (getEnv)+import System.Exit        (ExitCode(..))++import Data.SBV.BitVectors.Data+import Data.SBV.SMT.SMT+import Data.SBV.SMT.SMTLib++-- | 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.+-- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.+cvc4 :: SMTSolver+cvc4 = SMTSolver {+           name           = "cvc4"+         , 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)))+                                    let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} }+                                        tweaks = case solverTweaks cfg' of+                                                   [] -> ""+                                                   ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]+                                        script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont skolemMap)}+                                    standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap))+         , xformExitCode  = cvc4ExitCode+         , defaultLogic   = Just "ALL_SUPPORTED"  -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary+         }+ where zero :: Kind -> String+       zero (KBounded False 1)  = "#b0"+       zero (KBounded _     sz) = "#x" ++ replicate (sz `div` 4) '0'+       zero KUnbounded          = "0"+       zero KReal               = "0.0"+       zero (KUninterpreted s)  = error $ "SBV.CVC4.zero: Unexpected uninterpreted sort: " ++ s+       cont skolemMap = intercalate "\n" $ map extract skolemMap+        where extract (Left s)        = "(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"+              extract (Right (s, [])) = "(get-value (" ++ show s ++ "))"+              extract (Right (s, ss)) = "(get-value (" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ "))"+       addTimeOut Nothing  o   = o+       addTimeOut (Just i) o+         | i < 0               = error $ "CVC4: Timeout value must be non-negative, received: " ++ show i+         | True                = o ++ ["--tlimit=" ++ show i ++ "000"]  -- SBV takes seconds, CVC4 wants milli-seconds++-- | CVC4 uses different exit codes to indicate its status, rather than the+-- standard 0 being success and non-0 being failure. Make it palatable to SBV.+-- See <http://cvc4.cs.nyu.edu/wiki/User_Manual#Exit_status> for details.+cvc4ExitCode :: ExitCode -> ExitCode+cvc4ExitCode (ExitFailure n) | n `elem` [10, 20, 0] = ExitSuccess+cvc4ExitCode ec                                     = ec++extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel+extractMap isSat qinps _modelMap solverLines =+   SMTModel { modelAssocs    = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps . unstring) solverLines+            , modelUninterps = []+            , modelArrays    = []+            }+  where sortByNodeId :: [(Int, a)] -> [(Int, a)]+        sortByNodeId = sortBy (compare `on` fst)+        inps -- for "sat", display the prefix existentials. For completeness, we will drop+             -- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls+             | isSat = if all (== ALL) (map fst qinps)+                       then map snd qinps+                       else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps+             -- for "proof", just display the prefix universals+             | True  = map snd $ takeWhile ((== ALL) . fst) qinps+        -- CVC4 puts quotes around echo's, go figure. strip them here+        unstring s' = case (s, head s, last s) of+                        (_:tl@(_:_), '"', '"') -> init tl+                        _                      -> s'+          where s = reverse . dropWhile isSpace . reverse . dropWhile isSpace $ s'
Data/SBV/Provers/Prover.hs view
@@ -17,9 +17,7 @@ module Data.SBV.Provers.Prover (          SMTSolver(..), SMTConfig(..), Predicate, Provable(..)        , ThmResult(..), SatResult(..), AllSatResult(..), SMTResult(..)-       , isSatisfiable, isTheorem-       , isSatisfiableWithin, isTheoremWithin-       , numberOfModels+       , isSatisfiable, isSatisfiableWith, isTheorem, isTheoremWith        , Equality(..)        , prove, proveWith        , sat, satWith@@ -27,7 +25,7 @@        , isVacuous, isVacuousWith        , solve        , SatModel(..), Modelable(..), displayModels, extractModels-       , yices, z3, defaultSMTCfg+       , yices, z3, cvc4, defaultSMTCfg        , compileToSMTLib, generateSMTBenchmarks        , sbvCheckSolverInstallation        ) where@@ -45,6 +43,7 @@ import Data.SBV.BitVectors.Model import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib+import qualified Data.SBV.Provers.CVC4  as CVC4 import qualified Data.SBV.Provers.Yices as Yices import qualified Data.SBV.Provers.Z3    as Z3 import Data.SBV.Utils.TDiff@@ -63,6 +62,9 @@                                         , satCmd        = "(check-sat)"                                         } +-- | Default configuration for the CVC4 SMT Solver.+cvc4 :: SMTConfig+cvc4 = mkConfig CVC4.cvc4 True [] -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig yices = mkConfig Yices.yices False []@@ -277,61 +279,55 @@ isVacuous = isVacuousWith defaultSMTCfg  -- Decision procedures (with optional timeout)-checkTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)-checkTheorem mbTo p = do r <- pr p-                         case r of-                           ThmResult (Unsatisfiable _) -> return $ Just True-                           ThmResult (Satisfiable _ _) -> return $ Just False-                           ThmResult (TimeOut _)       -> return Nothing-                           _                           -> error $ "SBV.isTheorem: Received:\n" ++ show r-   where pr = maybe prove (\i -> proveWith (defaultSMTCfg{timeOut = Just i})) mbTo -checkSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)-checkSatisfiable mbTo p = do r <- s p-                             case r of-                               SatResult (Satisfiable _ _) -> return $ Just True-                               SatResult (Unsatisfiable _) -> return $ Just False-                               SatResult (TimeOut _)       -> return Nothing-                               _                           -> error $ "SBV.isSatisfiable: Received: " ++ show r-   where s = maybe sat (\i -> satWith defaultSMTCfg{timeOut = Just i}) mbTo---- | Checks theoremhood within the given time limit of @i@ seconds.+-- | Check whether a given property is a theorem, with an optional time out and the given solver. -- Returns @Nothing@ if times out, or the result wrapped in a @Just@ otherwise.-isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)-isTheoremWithin i = checkTheorem (Just i)+isTheoremWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)+isTheoremWith cfg mbTo p = do r <- proveWith cfg{timeOut = mbTo} p+                              case r of+                                ThmResult (Unsatisfiable _) -> return $ Just True+                                ThmResult (Satisfiable _ _) -> return $ Just False+                                ThmResult (TimeOut _)       -> return Nothing+                                _                           -> error $ "SBV.isTheorem: Received:\n" ++ show r --- | Checks satisfiability within the given time limit of @i@ seconds.+-- | Check whether a given property is satisfiable, with an optional time out and the given solver. -- Returns @Nothing@ if times out, or the result wrapped in a @Just@ otherwise.-isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)-isSatisfiableWithin i = checkSatisfiable (Just i)---- | Checks theoremhood-isTheorem :: Provable a => a -> IO Bool-isTheorem p = fromJust `fmap` checkTheorem Nothing p+isSatisfiableWith :: Provable a => SMTConfig -> Maybe Int -> a -> IO (Maybe Bool)+isSatisfiableWith cfg mbTo p = do r <- satWith cfg{timeOut = mbTo} p+                                  case r of+                                    SatResult (Satisfiable _ _) -> return $ Just True+                                    SatResult (Unsatisfiable _) -> return $ Just False+                                    SatResult (TimeOut _)       -> return Nothing+                                    _                           -> error $ "SBV.isSatisfiable: Received: " ++ show r --- | Checks satisfiability-isSatisfiable :: Provable a => a -> IO Bool-isSatisfiable p = fromJust `fmap` checkSatisfiable Nothing p+-- | Checks theoremhood within the given optional time limit of @i@ seconds.+-- Returns @Nothing@ if times out, or the result wrapped in a @Just@ otherwise.+isTheorem :: Provable a => Maybe Int -> a -> IO (Maybe Bool)+isTheorem = isTheoremWith defaultSMTCfg --- | Returns the number of models that satisfy the predicate, as it would--- be returned by 'allSat'. Note that the number of models is always a--- finite number, and hence this will always return a result. Of course,--- computing it might take quite long, as it literally generates and counts--- the number of satisfying models.-numberOfModels :: Provable a => a -> IO Int-numberOfModels p = do AllSatResult (_, rs) <- allSat p-                      return $ length rs+-- | Checks satisfiability within the given optional time limit of @i@ seconds.+-- Returns @Nothing@ if times out, or the result wrapped in a @Just@ otherwise.+isSatisfiable :: Provable a => Maybe Int -> a -> IO (Maybe Bool)+isSatisfiable = isSatisfiableWith defaultSMTCfg  -- | Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving -- the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively--- supported out-of-the box by the SBV library. If 'smtLib2' parameter is False, then we will generate--- SMTLib1 output, otherwise we will generate SMTLib2 output-compileToSMTLib :: Provable a => Bool -> a -> IO String-compileToSMTLib smtLib2 a = do+-- supported out-of-the box by the SBV library. It takes two booleans:+--+--    * smtLib2: If 'True', will generate SMT-Lib2 output, otherwise SMT-Lib1 output+--+--    * isSat  : If 'True', will translate it as a SAT query, i.e., in the positive. If 'False', will+--               translate as a PROVE query, i.e., it will negate the result. (In this case, the check-sat+--               call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)+compileToSMTLib :: Provable a => Bool   -- ^ If True, output SMT-Lib2, otherwise SMT-Lib1+                              -> Bool   -- ^ If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.)+                              -> a+                              -> IO String+compileToSMTLib smtLib2 isSat a = do         t <- getClockTime         let comments = ["Created on " ++ show t]             cvt = if smtLib2 then toSMTLib2 else toSMTLib1-        (_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg False comments a+        (_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a         let out = show smtLibPgm         if smtLib2 -- append check-sat in case of smtLib2            then return $ out ++ "\n(check-sat)\n"@@ -339,12 +335,14 @@  -- | Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, -- SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with--- suffix ".smt2"-generateSMTBenchmarks :: Provable a => FilePath -> a -> IO ()-generateSMTBenchmarks f a = gen False smt1 >> gen True smt2+-- suffix ".smt2". The 'Bool' argument controls whether this is a SAT instance, i.e., translate the query+-- directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to+-- 'compileToSMTLib' for details.)+generateSMTBenchmarks :: Provable a => Bool -> FilePath -> a -> IO ()+generateSMTBenchmarks isSat f a = gen False smt1 >> gen True smt2   where smt1     = addExtension f "smt1"         smt2     = addExtension f "smt2"-        gen b fn = do s <- compileToSMTLib b a+        gen b fn = do s <- compileToSMTLib b isSat a                       writeFile fn s                       putStrLn $ "Generated SMT benchmark " ++ show fn ++ "." @@ -451,6 +449,7 @@ runProofOn :: SMTLibConverter -> SMTConfig -> Bool -> [String] -> Result -> IO SMTProblem runProofOn converter config isSat comments res =         let isTiming = timing config+            defLogic = defaultLogic (solver config)         in case res of              Result boundInfo usorts _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->                timeIf isTiming "translation" $ let uiMap     = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis@@ -462,7 +461,7 @@                                                                 where go []                   (_,  sofar) = reverse sofar                                                                       go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar)                                                                       go ((EX,  (v, _)):rest) (us, sofar) = go rest (us,   Right (v, reverse us) : sofar)-                                               in return (is, uiMap, skolemMap, usorts, converter boundInfo isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o)+                                               in return (is, uiMap, skolemMap, usorts, converter boundInfo defLogic isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o)              Result _boundInfo _us _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of                            0  -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res                            1  -> error $ "Impossible happened, non-boolean output in " ++ show os
Data/SBV/Provers/SExpr.hs view
@@ -75,6 +75,8 @@         cvt (SApp [SCon "/", SNum  a, SNum  b])                    = return $ SReal (fromInteger a / fromInteger b)         cvt (SApp [SCon "-", SReal a])                             = return $ SReal (-a)         cvt (SApp [SCon "-", SNum a])                              = return $ SNum  (-a)+        -- bit-vector value as CVC4 prints: (_ bv0 16) for instance+        cvt (SApp [SCon "_", SNum a, SNum _b])                     = return $ SNum a         cvt (SApp [SCon "root-obj", SApp (SCon "+":trms), SNum k]) = do ts <- mapM getCoeff trms                                                                         return $ SReal $ mkPolyReal (Right (k, ts))         cvt x                                                      = return x
Data/SBV/Provers/Yices.hs view
@@ -27,20 +27,22 @@ import Data.SBV.SMT.SMTLib  -- | The description of the Yices SMT solver--- The default executable is @\"yices\"@, which must be in your path. You can use the @SBV_YICES@ environment variable to point to the executable on your system.--- 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.+-- 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.+-- The default options are @\"-m -f\"@, which is valid for Yices 2.1 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 = unlines (solverTweaks cfg') ++ pgm, scriptModel = Nothing}-                                  standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap))+           name           = "Yices"+         , executable     = "yices-smt"+         -- , 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))+         , xformExitCode  = id+         , defaultLogic   = Nothing          }   where addTimeOut Nothing  o   = o         addTimeOut (Just i) o
Data/SBV/Provers/Z3.hs view
@@ -9,14 +9,13 @@ -- The connection to the Z3 SMT solver ----------------------------------------------------------------------------- -{-# LANGUAGE PatternGuards       #-} {-# LANGUAGE ScopedTypeVariables #-}  module Data.SBV.Provers.Z3(z3) where  import qualified Control.Exception as C -import Data.Char          (isDigit, toLower)+import Data.Char          (toLower) import Data.Function      (on) import Data.List          (sortBy, intercalate, isPrefixOf, groupBy) import System.Environment (getEnv)@@ -24,7 +23,6 @@  import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data-import Data.SBV.Provers.SExpr import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -37,25 +35,27 @@  -- | The description of the Z3 SMT solver -- The default executable is @\"z3\"@, which must be in your path. You can use the @SBV_Z3@ environment variable to point to the executable on your system.--- 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.+-- The default options are @\"-in -smt2\"@, which is valid for Z3 4.1. 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} }-                                    tweaks = case solverTweaks cfg' of-                                               [] -> ""-                                               ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]-                                    dlim = printRealPrec cfg'-                                    ppDecLim = "(set-option :pp-decimal-precision " ++ show dlim ++ ")\n"-                                    script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont skolemMap)}-                                if dlim < 1-                                   then error $ "SBV.Z3: printRealPrec value should be at least 1, invalid value received: " ++ show dlim-                                   else standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap . 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} }+                                        tweaks = case solverTweaks cfg' of+                                                   [] -> ""+                                                   ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]+                                        dlim = printRealPrec cfg'+                                        ppDecLim = "(set-option :pp-decimal-precision " ++ show dlim ++ ")\n"+                                        script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont skolemMap)}+                                    if dlim < 1+                                       then error $ "SBV.Z3: printRealPrec value should be at least 1, invalid value received: " ++ show dlim+                                       else standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap))+         , xformExitCode  = id+         , defaultLogic   = Nothing          }  where -- Get rid of the following when z3_4.0 is out        cleanErrs = intercalate "\n" . filter (not . junk) . lines@@ -67,17 +67,17 @@        zero KReal               = "0.0"        zero (KUninterpreted s)  = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s        cont skolemMap = intercalate "\n" $ concatMap extract skolemMap-        where extract (Left s)        = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]+        where -- In the skolemMap:+              --    * Left's are universals: i.e., the model should be true for+              --      any of these. So, we simply "echo 0" for these values.+              --    * Right's are existentials. If there are no dependencies (empty list), then we can+              --      simply use get-value to extract it's value. Otherwise, we have to apply it to+              --      an appropriate number of 0's to get the final value.+              extract (Left s)        = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"]               extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g-              extract (Right (s, ss)) = let g = "(eval (" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ "))" in getVal (kindOf s) g+              extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g               getVal KReal g = ["(set-option :pp-decimal false)", g, "(set-option :pp-decimal true)", g]               getVal _     g = [g]-       match skolemMap = zipWith annotate (concatMap dupRight skolemMap)-         where dupRight (Left s)  = [Left s]-               dupRight (Right x) = [Right x, Right x]-               annotate (Left _)        l = l-               annotate (Right (_, [])) l = l-               annotate (Right (s, _))  l = "((" ++ show s ++ " " ++ l ++ "))"        addTimeOut Nothing  o   = o        addTimeOut (Just i) o          | i < 0               = error $ "Z3: Timeout value must be non-negative, received: " ++ show i@@ -85,7 +85,7 @@  extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel extractMap isSat qinps _modelMap solverLines =-   SMTModel { modelAssocs    = map snd $ squashReals $ sortByNodeId $ concatMap (getCounterExample inps) solverLines+   SMTModel { modelAssocs    = map snd $ squashReals $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines             , modelUninterps = []             , modelArrays    = []             }@@ -103,26 +103,6 @@           where squash [(i, (n, cw1)), (_, (_, cw2))] = [(i, (n, mergeReals n cw1 cw2))]                 squash xs = xs                 mergeReals :: String -> CW -> CW -> CW-                mergeReals n (CW KReal (CWAlgReal a)) (CW KReal (CWAlgReal b)) = CW KReal (CWAlgReal (mergeAlgReals (error (bad n a b)) a b))-                mergeReals n a b = error $ bad n a b-                bad n a b = "SBV.Z3: Cannot merge reals for variable: " ++ n ++ " received: " ++ show (a, b)--getCounterExample :: [NamedSymVar] -> String -> [(Int, (String, CW))]-getCounterExample inps line = either err extract (parseSExpr line)-  where err r =  error $  "*** Failed to parse SMT-Lib2 model output from: "-                       ++ "*** " ++ show line ++ "\n"-                       ++ "*** Reason: " ++ r ++ "\n"-        isInput ('s':v)-          | all isDigit v = let inpId :: Int-                                inpId = read v-                            in case [(s, nm) | (s@(SW _ (NodeId n)), nm) <-  inps, n == inpId] of-                                 []        -> Nothing-                                 [(s, nm)] -> Just (inpId, s, nm)-                                 matches -> error $  "SBV.SMTLib2: Cannot uniquely identify value for "-                                                  ++ 's':v ++ " in "  ++ show matches-        isInput _       = Nothing-        extract (SApp [SApp [SCon v, SNum i]])  | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]-        extract (SApp [SApp [SCon v, SReal i]]) | Just (n, _, nm) <- isInput v = [(n, (nm, CW KReal      (CWAlgReal i)))]-        extract (SApp [SApp [SCon v, SCon i]])  | Just (n, s, nm) <- isInput v = [(n, (nm, CW (kindOf s) (CWUninterpreted i)))]-        extract (SApp [SApp (SCon v : r)])      | Just{}          <- isInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show v ++ ", received:\n\t" ++  show r-        extract _                                                              = []+                mergeReals n (CW KReal (CWAlgReal a)) (CW KReal (CWAlgReal b)) = CW KReal (CWAlgReal (mergeAlgReals (bad n a b) a b))+                mergeReals n a b = bad n a b+                bad n a b = error $ "SBV.Z3: Cannot merge reals for variable: " ++ n ++ " received: " ++ show (a, b)
Data/SBV/SMT/SMT.hs view
@@ -33,7 +33,7 @@ import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff --- | Solver configuration. See also 'z3' and 'yices', which are instantiations of this type for those solvers, with+-- | Solver configuration. See also 'z3', 'yices', and 'cvc4', which are instantiations of this type for those solvers, with -- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.) -- -- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does@@ -64,10 +64,12 @@  -- | 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+       , defaultLogic   :: Maybe String         -- ^ Default logic to set, if any+       , xformExitCode  :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.        }  -- | A model, as returned by a solver@@ -358,24 +360,26 @@                                    ++ "\nExecutable specified: " ++ show execName           Just execPath -> do (ec, contents, allErrors) <- runSolver cfg execPath opts script                               let errors = dropWhile isSpace (cleanErrs allErrors)-                              case ec of-                                ExitSuccess  ->  if null errors-                                                 then return $ Right $ map clean (filter (not . null) (lines contents))-                                                 else return $ Left errors-                                ExitFailure n -> let errors' = if null errors-                                                               then (if null (dropWhile isSpace contents)-                                                                     then "(No error message printed on stderr by the executable.)"-                                                                     else contents)-                                                               else errors-                                                 in return $ Left $  "Failed to complete the call to " ++ nm-                                                                  ++ "\nExecutable   : " ++ show execPath-                                                                  ++ "\nOptions      : " ++ unwords opts-                                                                  ++ "\nExit code    : " ++ show n-                                                                  ++ "\nSolver output: "-                                                                  ++ "\n" ++ line ++ "\n"-                                                                  ++ intercalate "\n" (filter (not . null) (lines errors'))-                                                                  ++ "\n" ++ line-                                                                  ++ "\nGiving up.."+                              case (null errors, xformExitCode (solver cfg) ec) of+                                (True, ExitSuccess)  -> return $ Right $ map clean (filter (not . null) (lines contents))+                                (_, ec')             -> let errors' = if null errors+                                                                      then (if null (dropWhile isSpace contents)+                                                                            then "(No error message printed on stderr by the executable.)"+                                                                            else contents)+                                                                      else errors+                                                            finalEC = case (ec', ec) of+                                                                        (ExitFailure n, _) -> n+                                                                        (_, ExitFailure n) -> n+                                                                        _                  -> 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+                                                                         ++ "\nExit code    : " ++ show finalEC+                                                                         ++ "\nSolver output: "+                                                                         ++ "\n" ++ line ++ "\n"+                                                                         ++ intercalate "\n" (filter (not . null) (lines errors'))+                                                                         ++ "\n" ++ line+                                                                         ++ "\nGiving up.."   where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace         line  = replicate 78 '='
Data/SBV/SMT/SMTLib.hs view
@@ -9,16 +9,20 @@ -- Conversion of symbolic programs to SMTLib format ----------------------------------------------------------------------------- -module Data.SBV.SMT.SMTLib(SMTLibPgm, SMTLibConverter, toSMTLib1, toSMTLib2, addNonEqConstraints, interpretSolverOutput) where+module Data.SBV.SMT.SMTLib(SMTLibPgm, SMTLibConverter, toSMTLib1, toSMTLib2, addNonEqConstraints, interpretSolverOutput, interpretSolverModelLine) where +import Data.Char (isDigit)+ import Data.SBV.BitVectors.Data import Data.SBV.SMT.SMT+import Data.SBV.Provers.SExpr import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2  -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for -- newer versions in the future.) type SMTLibConverter =  (Bool, Bool)                -- ^ has unbounded integers/reals+                     -> Maybe String                 -- ^ set-logic string to use in case not automatically determined (if any)                      -> Bool                        -- ^ is this a sat problem?                      -> [String]                    -- ^ extra comments to place on top                      -> [String]                    -- ^ uninterpreted sorts@@ -40,10 +44,10 @@ -- | Convert to SMTLib-2 format toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)-  where cvt v boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)+  where cvt v mbDefaultLogic boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)          where aliasTable  = map (\(_, (x, y)) -> (y, x)) qinps                converter   = if v == SMTLib1 then SMT1.cvt else SMT2.cvt-               (pre, post) = converter boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out+               (pre, post) = converter mbDefaultLogic boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out  -- | Add constraints generated from older models, used for querying new models addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String@@ -57,3 +61,35 @@ interpretSolverOutput cfg extractMap ("sat":rest)     = Satisfiable   cfg  $ extractMap rest interpretSolverOutput cfg _          ("timeout":_)    = TimeOut       cfg interpretSolverOutput cfg _          ls               = ProofError    cfg  ls++-- | Get a counter-example from an SMT-Lib2 like model output line+-- This routing is necessarily fragile as SMT solvers tend to print output+-- in whatever form they deem convenient for them.. Currently, it's tuned to+-- work with Z3 and CVC4; if new solvers are added, we might need to rework+-- the logic here.+interpretSolverModelLine :: [NamedSymVar] -> String -> [(Int, (String, CW))]+interpretSolverModelLine inps line = either err extract (parseSExpr line)+  where err r =  error $  "*** Failed to parse SMT-Lib2 model output from: "+                       ++ "*** " ++ show line ++ "\n"+                       ++ "*** Reason: " ++ r ++ "\n"+        getInput (SCon v)            = isInput v+        getInput (SApp (SCon v : _)) = isInput v+        getInput _                   = Nothing+        isInput ('s':v)+          | all isDigit v = let inpId :: Int+                                inpId = read v+                            in case [(s, nm) | (s@(SW _ (NodeId n)), nm) <-  inps, n == inpId] of+                                 []        -> Nothing+                                 [(s, nm)] -> Just (inpId, s, nm)+                                 matches -> error $  "SBV.SMTLib2: Cannot uniquely identify value for "+                                                  ++ 's':v ++ " in "  ++ show matches+        isInput _       = Nothing+        extract (SApp [SApp [v, SNum i]])  | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) i))]+        extract (SApp [SApp [v, SReal i]]) | Just (n, _, nm) <- getInput v = [(n, (nm, CW KReal      (CWAlgReal i)))]+        extract (SApp [SApp [v, SCon i]])  | Just (n, s, nm) <- getInput v = [(n, (nm, CW (kindOf s) (CWUninterpreted i)))]+        -- weird lambda app that CVC4 seems to throw out.. logic below derived from what I saw CVC4 print, hopefully sufficient+        extract (SApp (SApp (v : SApp (SCon "LAMBDA" : xs) : _) : _)) | Just{} <- getInput v, not (null xs) = extract (SApp [SApp [v, last xs]])+        extract (SApp [SApp (v : r)])      | Just (_, _, nm) <- getInput v = error $   "SBV.SMTLib2: Cannot extract value for " ++ show nm+                                                                                   ++ "\n\tInput: " ++ show line+                                                                                   ++ "\n\tParse: " ++  show r+        extract _                                                          = []
Data/SBV/SMT/SMTLib1.hs view
@@ -41,6 +41,7 @@  -- | Translate a problem into an SMTLib1 script cvt :: (Bool, Bool)                 -- ^ has infinite precision integers/reals+    -> Maybe String                 -- ^ Not used in the SMTLib1 converter     -> Bool                         -- ^ is this a sat problem?     -> [String]                     -- ^ extra comments to place on top     -> [String]                     -- ^ uninterpreted sorts@@ -55,15 +56,15 @@     -> [SW]                         -- ^ extra constraints     -> SW                           -- ^ output variable     -> ([String], [String])-cvt (hasIntegers, hasReals) isSat comments sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out+cvt (hasIntegers, hasReals) _mbDefaultLogic isSat comments sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out   | hasIntegers-  = error "SBV: Unbounded integers are not supported in the SMTLib1/yices interface. (Use z3 instead.)"+  = error "SBV: Unbounded integers are not supported in the SMTLib1/yices interface."   | hasReals-  = error "SBV: The real value domain is not supported in the SMTLib1/yices interface. (Use z3 instead.)"+  = error "SBV: The real value domain is not supported in the SMTLib1/yices interface."   | not ((isSat && allExistential) || (not isSat && allUniversal))-  = error "SBV: The chosen solver does not support quantified variables. (Use z3 instead.)"+  = error "SBV: The chosen solver does not support quantified variables."   | not (null sorts)-  = error "SBV: The chosen solver does not support unintepreted sorts. (Use z3 instead.)"+  = error "SBV: The chosen solver does not support unintepreted sorts."   | True   = (pre, post)   where quantifiers    = map fst qinps
Data/SBV/SMT/SMTLib2.hs view
@@ -58,6 +58,7 @@  -- | Translate a problem into an SMTLib2 script cvt :: (Bool, Bool)                 -- ^ has infinite precision values+    -> Maybe String                 -- ^ set-logic string to use in case not automatically determined (if any)     -> Bool                         -- ^ is this a sat problem?     -> [String]                     -- ^ extra comments to place on top     -> [String]                     -- ^ uninterpreted sorts@@ -72,11 +73,13 @@     -> [SW]                         -- ^ extra constraints     -> SW                           -- ^ output variable     -> ([String], [String])-cvt (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, [])+cvt (hasInteger, hasReal) mbDefaultLogic isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, [])   where -- the logic is an over-approaximation         logic            | hasInteger || hasReal || not (null sorts)-           = ["; Has unbounded values (Int/Real) or sorts; no logic specified."]   -- combination, let the solver pick+           = case mbDefaultLogic of+                Nothing -> ["; Has unbounded values (Int/Real) or sorts; no logic specified."]   -- combination, let the solver pick+                Just l  -> ["(set-logic " ++ l ++ ")"]            | True            = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"]           where qs  | null foralls && null axs = "QF_"  -- axioms are likely to contain quantifiers@@ -88,7 +91,6 @@         pre  =  ["; Automatically generated by SBV. Do not edit."]              ++ map ("; " ++) comments              ++ [ "(set-option :produce-models true)"-                , "(set-option :pp-decimal false)"                 ]              ++ logic              ++ [ "; --- uninterpreted sorts ---" ]@@ -144,7 +146,7 @@         asgns = F.toList asgnsSeq         mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap tableMap e ++ "))"         declConst (s, c) = "(define-fun " ++ show s ++ " " ++ swFunType [] s ++ " " ++ cvtCW c ++ ")"-        declSort s = "(declare-sort " ++ s ++ ")"+        declSort s = "(declare-sort " ++ s ++ " 0)"  declUI :: (String, SBVType) -> [String] declUI (i, t) = ["(declare-fun " ++ i ++ " " ++ cvtType t ++ ")"]
LICENSE view
@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2013, Levent Erkok (erkokl@gmail.com) All rights reserved.  Redistribution and use in source and binary forms, with or without
README view
@@ -1,138 +1,4 @@ SBV: SMT Based Verification in Haskell ====================================== -Express properties about Haskell programs and automatically prove them using SMT solvers.--```haskell-        $ ghci -XScopedTypeVariables-        Prelude> :m Data.SBV-        Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x-        Q.E.D.-        Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x-        Falsifiable. Counter-example:-          x = 128 :: SWord8-```--The function `prove` has the following type:-    -```haskell-        prove :: Provable a => a -> IO ThmResult-```--The class `Provable` comes with instances for n-ary predicates, for arbitrary n.-The predicates are just regular Haskell functions over symbolic signed and unsigned-bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided.-In addition, functions using the SBV library can be compiled to C automatically.--Build Status-============-SBV uses Travis-CI's automated build infrastructure, making a build for each commit. Current build status:-[![Build Status](https://secure.travis-ci.org/LeventErkok/sbv.png?branch=master)](http://travis-ci.org/LeventErkok/sbv)--Resources-=========-The SBV library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).--The hackage site-[http://hackage.haskell.org/package/sbv](http://hackage.haskell.org/package/sbv) is the best place-for details on the API and the example use cases.--Comments, bug reports, and patches are always welcome.--Overview-========-The Haskell SBV library provides support for dealing with Symbolic Bit Vectors-in Haskell. It introduces the types:--  - `SBool`: Symbolic Booleans (bits).-  - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned).-  - `SInt8`,  `SInt16`,  `SInt32`,  `SInt64`: Symbolic Ints (signed).-  - `SInteger`: Symbolic unbounded integers (signed).-  - `SReal`: Symbolic infinite precision algebraic reals (signed).-  - Arrays of symbolic values.-  - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs.-  - Uninterpreted constants and functions over symbolic values, with user defined axioms.-  - Uninterpreted sorts, and proofs over such sorts, potentially with axioms.--The user can construct ordinary Haskell programs using these types, which behave-very similar to their concrete counterparts. In particular these types belong to the-standard classes `Num`, `Bits`, (custom versions of) `Eq` and `Ord`, along with several-other custom classes for simplifying bit-precise programming with symbolic values. The-framework takes full advantage of Haskell's type inference to avoid many common mistakes.--Furthermore, functions built out of these types can also be:--  - proven correct via an external SMT solver (the `prove` function)-  - checked for satisfiability (the `sat`, and `allSat` functions)-  - used in synthesis (the `sat` function with existentials)-  - optimized with respect to cost functions (the `optimize`, `maximize`, and `minimize` functions)-  - quick-checked-  - used in concrete test case generation (the `genTest` function), rendered as values in various-    languages, including Haskell and C.--If a predicate is not valid, `prove` will return a counterexample: An -assignment to inputs such that the predicate fails. The `sat` function will-return a satisfying assignment, if there is one. The `allSat` function returns-all satisfying assignments, lazily.--The SBV library can also compile Haskell functions that manipulate symbolic-values directly to C, rendering them as straight-line C programs.--Use of SMT solvers-==================-The SBV library uses third-party SMT solvers via the standard SMT-Lib interface-[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/).--Currently, we fully support the-[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,-and the [Yices](http://yices.csl.sri.com) SMT solver from SRI. Both solvers are available-for Windows, Linux, and Mac OSX.--Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please-do get in touch if you plan to use SBV with any other solver.--Prerequisites-=============-You **should** have at least one of -Z3 [(download)](http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html), or-Yices [(download)](http://yices.csl.sri.com/download-yices2.shtml) (version 2.X) -installed on your machine, preferably both. Note that z3 is the default solver used by 'sat',-'allSat', 'prove', etc. commands. To use "yices", use the 'satWith', 'proveWith', 'allSatWith' variants.--Make sure the executables for the solvers are in your path. Alternatively, you can specify the location-of the yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`.-(The default for the latter is `"-m -f"`). Similarly the environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can-be used for choosing executable location and custom options for Z3.  (The default for the latter is-`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 4.1 or later.)--Examples-=========-Please see the files under the-[Examples](http://github.com/LeventErkok/sbv/tree/master/Data/SBV/Examples)-directory for a number of interesting applications and use cases. Amongst others,-it contains solvers for Sudoku and N-Queens puzzles as mandatory SMT solver examples in-the Puzzles directory.--Installation-============-The SBV library is cabalized. Assuming you have cabal/ghc installed, it should merely-be a matter of running -     -         cabal install sbv-	 -Please see [INSTALL](http://github.com/LeventErkok/sbv/tree/master/INSTALL) for installation details.--Once the installation is done, you can run the executable `SBVUnitTests` which will-execute the regression test suite for SBV on your machine to ensure all is well.--Copyright, License-==================-The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for-details. The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains-the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.--Thanks-======-The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:-Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson,-and Nis Wegmann.+Please see: http://leventerkok.github.com/sbv/
RELEASENOTES view
@@ -1,7 +1,37 @@ Hackage: <http://hackage.haskell.org/package/sbv>-GitHub:  <http://github.com/LeventErkok/sbv>+GitHub:  <http://leventerkok.github.com/sbv/> -Latest Hackage released version: 2.8+Latest Hackage released version: 2.9++======================================================================+Version 2.9, 2013-01-02++  - Add support for the CVC4 SMT solver from New York University and+    the University of Iowa. (http://cvc4.cs.nyu.edu/).+    NB. Z3 remains the default solver for SBV. To use CVC4, use the+    *With variants of the interface (i.e., proveWith, satWith, ..)+    by passing cvc4 as the solver argument. (Similarly, use 'yices'+    as the argument for the *With functions for invoking yices.)+  - Latest release of Yices calls the SMT-Lib based solver executable+    yices-smt. Updated the default value of the executable to have this+    name for ease of use.+  - Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks+    functions to control if the translation should keep the query as is+    (for SAT cases), or negate it (for PROVE cases). Previously, this value+    was hard-coded to do the PROVE case only.+  - Add bridge modules, to simplify use of different solvers. You can now say:++       import Data.SBV.Bridge.CVC4+       import Data.SBV.Bridge.Yices+       import Data.SBV.Bridge.Z3+   +    to pick the appropriate default solver. if you simply 'import Data.SBV', then+    you will get the default SMT solver, which is currently Z3. The value+    'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers+    to the chosen solver as determined by the imported module. (The latter is+    useful for modifying options to the SMT solver in an solver-agnostic way.)+  - Various improvements to Z3 model parsing routines.+  - New web page for SBV: http://leventerkok.github.com/sbv/ is now online.  ====================================================================== Version 2.8, 2012-11-29
SBVUnitTest/Examples/Basics/Index.hs view
@@ -12,10 +12,11 @@ module Examples.Basics.Index where  import Data.SBV+import SBVTest  -- prove that the "select" primitive is working correctly test1 :: Int -> IO Bool-test1 n = isTheorem $ do+test1 n = isThm $ do             elts <- mkForallVars n             err  <- forall_             ind  <- forall_@@ -30,7 +31,7 @@                go (x:xs) curInd = ite (curInd .== 0) x (go xs (curInd - 1))  test2 :: Int -> IO Bool-test2 n = isTheorem $ do+test2 n = isThm $ do             elts1 <- mkForallVars n             elts2 <- mkForallVars n             let elts = zip elts1 elts2@@ -49,7 +50,7 @@                go (x:xs) curInd = ite (curInd .== 0) x (go xs (curInd - 1))  test3 :: Int -> IO Bool-test3 n = isTheorem $ do+test3 n = isThm $ do             eltsI <- mkForallVars n             let elts = map Left eltsI             errI  <- forall_
SBVUnitTest/Examples/CRC/GenPoly.hs view
@@ -60,7 +60,7 @@         go poly skip acc          | poly == maxBound = return (skip, acc)          | True             = do putStr $ "Testing " ++ showPoly  (mkPoly poly) ++ "... "-                                 thm <- isTheoremWithin waitFor $ crcGood hd poly+                                 thm <- isTheorem (Just waitFor) $ crcGood hd poly                                  case thm of                                    Nothing    -> do putStrLn "Timeout, skipping.."                                                     go (poly+1) (poly:skip) acc
SBVUnitTest/SBVTest.hs view
@@ -10,8 +10,10 @@ -----------------------------------------------------------------------------  {-# LANGUAGE RankNTypes #-}-module SBVTest(generateGoldCheck, showsAs, ioShowsAs, mkTestSuite, SBVTestSuite(..), module Test.HUnit) where+module SBVTest(generateGoldCheck, showsAs, ioShowsAs, mkTestSuite, SBVTestSuite(..), module Test.HUnit, isThm, isSat, numberOfModels) where +import Data.SBV        (Provable(..), isTheorem, isSatisfiable, AllSatResult(..), allSat)+import Data.Maybe      (fromJust) import System.FilePath ((</>)) import Test.HUnit      (Test(..), Assertion, assert, (~:), test) @@ -42,3 +44,16 @@                       g <- readFile gf                       assert $ show v == g  where gf = goldDir </> goldFile++-- | Check if a property is a theorem, no timeout+isThm :: Provable a => a -> IO Bool+isThm p = fromJust `fmap` isTheorem Nothing p++-- | Check if a property is satisfiable, no timeout+isSat :: Provable a => a -> IO Bool+isSat p = fromJust `fmap` isSatisfiable Nothing p++-- | Count the number of models+numberOfModels :: Provable a => a -> IO Int+numberOfModels p = do AllSatResult (_, rs) <- allSat p+                      return $ length rs
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Wed Nov 28 19:14:22 PST 2012"+buildTime = "Tue Jan  1 22:35:55 PST 2013"
SBVUnitTest/TestSuite/Arrays/Memory.hs view
@@ -11,16 +11,14 @@  module TestSuite.Arrays.Memory(testSuite) where -import Data.SBV- import Examples.Arrays.Memory import SBVTest  -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-     "memory-raw"           ~: assert       =<< isTheorem raw-   , "memory-waw"           ~: assert       =<< isTheorem waw-   , "memory-wcommute-bad"  ~: assert . not =<< isTheorem wcommutesBad-   , "memory-wcommute-good" ~: assert       =<< isTheorem wcommutesGood+     "memory-raw"           ~: assert       =<< isThm raw+   , "memory-waw"           ~: assert       =<< isThm waw+   , "memory-wcommute-bad"  ~: assert . not =<< isThm wcommutesBad+   , "memory-wcommute-good" ~: assert       =<< isThm wcommutesGood    ]
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -67,10 +67,10 @@                                           ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]                                           ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]   where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t-        mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]-                                      constrain $ a .== literal x-                                      constrain $ b .== literal y-                                      return $ literal r .== a `op` b+        mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"]+                                  constrain $ a .== literal x+                                  constrain $ b .== literal y+                                  return $ literal r .== a `op` b  genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test] genBoolTest nm op opS = map mkTest $  [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- w8s ]@@ -83,10 +83,10 @@                                    ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]                                    ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs]   where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t-        mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]-                                      constrain $ a .== literal x-                                      constrain $ b .== literal y-                                      return $ literal r .== a `opS` b+        mkThm2 x y r = isThm $ do [a, b] <- mapM free ["x", "y"]+                                  constrain $ a .== literal x+                                  constrain $ b .== literal y+                                  return $ literal r .== a `opS` b  genUnTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [Test] genUnTest unboundedOK nm op = map mkTest $  [(show x, mkThm x (op x)) | x <- w8s ]@@ -99,9 +99,9 @@                                          ++ [(show x, mkThm x (op x)) | x <- i64s]                                          ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]   where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t-        mkThm x r = isTheorem $ do a <- free "x"-                                   constrain $ a .== literal x-                                   return $ literal r .== op a+        mkThm x r = isThm $ do a <- free "x"+                               constrain $ a .== literal x+                               return $ literal r .== op a  genIntTest :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTest nm op = map mkTest $  [("u8",  show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- is]@@ -115,9 +115,9 @@                               ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is]   where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t         is = [-10 .. 10]-        mkThm2 x y r = isTheorem $ do a <- free "x"-                                      constrain $ a .== literal x-                                      return $ literal r .== a `op` y+        mkThm2 x y r = isThm $ do a <- free "x"+                                  constrain $ a .== literal x+                                  return $ literal r .== a `op` y   genIntTestS :: Bool -> String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test]@@ -131,9 +131,9 @@                                            ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]]                                            ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]]   where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t-        mkThm2 x y r = isTheorem $ do a <- free "x"-                                      constrain $ a .== literal x-                                      return $ literal r .== a `op` y+        mkThm2 x y r = isThm $ do a <- free "x"+                                  constrain $ a .== literal x+                                  return $ literal r .== a `op` y  genBlasts :: [Test] genBlasts = map mkTest $  [(show x, mkThm fromBitsLE blastLE x) | x <- w8s ]@@ -153,9 +153,9 @@                        ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s]                        ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s]   where mkTest (x, t) = "blast-" ++ show x ~: assert t-        mkThm from to v = isTheorem $ do a <- free "x"-                                         constrain $ a .== literal v-                                         return $ a .== from (to a)+        mkThm from to v = isThm $ do a <- free "x"+                                     constrain $ a .== literal v+                                     return $ a .== from (to a)  genCasts :: [Test] genCasts = map mkTest $  [(show x, mkThm unsignCast signCast x) | x <- w8s ]@@ -177,12 +177,12 @@                       ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s]                       ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s]   where mkTest (x, t) = "cast-" ++ show x ~: assert t-        mkThm from to v = isTheorem $ do a <- free "x"-                                         constrain $ a .== literal v-                                         return $ a .== from (to a)-        mkFEq f g v = isTheorem $ do a <- free "x"+        mkThm from to v = isThm $ do a <- free "x"                                      constrain $ a .== literal v-                                     return $ f a .== g a+                                     return $ a .== from (to a)+        mkFEq f g v = isThm $ do a <- free "x"+                                 constrain $ a .== literal v+                                 return $ f a .== g a  genReals :: [Test] genReals = map mkTest $  [("+",  show x, show y, mkThm2 (+)   x y (x +  y)) | x <- rs, y <- rs        ]@@ -196,10 +196,10 @@                       ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs        ]                       ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs        ]   where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t-        mkThm2 op x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]-                                         constrain $ a .== literal x-                                         constrain $ b .== literal y-                                         return $ literal r .== a `op` b+        mkThm2 op x y r = isThm $ do [a, b] <- mapM free ["x", "y"]+                                     constrain $ a .== literal x+                                     constrain $ b .== literal y+                                     return $ literal r .== a `op` b  genQRems :: [Test] genQRems = map mkTest $  [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- w8s,  y <- w8s ]@@ -223,10 +223,10 @@   where divMod'  x y = if y == 0 then (0, x) else x `divMod`  y         quotRem' x y = if y == 0 then (0, x) else x `quotRem` y         mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t-        mkThm2 op x y (e1, e2) = isTheorem $ do [a, b] <- mapM free ["x", "y"]-                                                constrain $ a .== literal x-                                                constrain $ b .== literal y-                                                return $ (literal e1, literal e2) .== a `op` b+        mkThm2 op x y (e1, e2) = isThm $ do [a, b] <- mapM free ["x", "y"]+                                            constrain $ a .== literal x+                                            constrain $ b .== literal y+                                            return $ (literal e1, literal e2) .== a `op` b         -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for signed types; so avoid that case         noOverflow x y = not (x == minBound && y == -1)
SBVUnitTest/TestSuite/Basics/ProofTests.hs view
@@ -19,15 +19,15 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "proofs-1"  ~: assert       =<< isTheorem f1eqf2- , "proofs-2"  ~: assert . not =<< isTheorem f1eqf3- , "proofs-3"  ~: assert       =<< isTheorem f3eqf4- , "proofs-4"  ~: assert       =<< isTheorem f1Single- , "proofs-5"  ~: assert       =<< isSatisfiable (f1 `xyEq` f2)- , "proofs-6"  ~: assert       =<< isSatisfiable (f1 `xyEq` f3)- , "proofs-7"  ~: assert . not =<< isSatisfiable (exists "x" >>= \x -> return (x .== x + (1 :: SWord16)))- , "proofs-8"  ~: assert       =<< isSatisfiable (exists "x" >>= \x -> return (x :: SBool))- , "proofs-9"  ~: assert       =<< isSatisfiable (exists "x" >>= \x -> return x :: Predicate)+   "proofs-1"  ~: assert       =<< isThm f1eqf2+ , "proofs-2"  ~: assert . not =<< isThm f1eqf3+ , "proofs-3"  ~: assert       =<< isThm f3eqf4+ , "proofs-4"  ~: assert       =<< isThm f1Single+ , "proofs-5"  ~: assert       =<< isSat (f1 `xyEq` f2)+ , "proofs-6"  ~: assert       =<< isSat (f1 `xyEq` f3)+ , "proofs-7"  ~: assert . not =<< isSat (exists "x" >>= \x -> return (x .== x + (1 :: SWord16)))+ , "proofs-8"  ~: assert       =<< isSat (exists "x" >>= \x -> return (x :: SBool))+ , "proofs-9"  ~: assert       =<< isSat (exists "x" >>= \x -> return x :: Predicate)  ]  where func1 `xyEq` func2 = do x <- exists_                                y <- exists_
SBVUnitTest/TestSuite/Basics/QRem.hs view
@@ -19,7 +19,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "qremW8" ~: assert =<< isTheorem (qrem :: SWord8   -> SWord8   -> SBool)- , "qremI8" ~: assert =<< isTheorem (qrem :: SInt8    -> SInt8    -> SBool)- , "qremI"  ~: assert =<< isTheorem (qrem :: SInteger -> SInteger -> SBool)+   "qremW8" ~: assert =<< isThm (qrem :: SWord8   -> SWord8   -> SBool)+ , "qremI8" ~: assert =<< isThm (qrem :: SInt8    -> SInt8    -> SBool)+ , "qremI"  ~: assert =<< isThm (qrem :: SInteger -> SInteger -> SBool)  ]
SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs view
@@ -11,7 +11,6 @@  module TestSuite.BitPrecise.BitTricks(testSuite) where -import Data.SBV import Data.SBV.Examples.BitPrecise.BitTricks  import SBVTest@@ -19,9 +18,9 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "fast min"              ~: assert =<< isTheorem fastMinCorrect- , "fast max"              ~: assert =<< isTheorem fastMaxCorrect- , "opposite signs"        ~: assert =<< isTheorem oppositeSignsCorrect- , "conditional set clear" ~: assert =<< isTheorem conditionalSetClearCorrect- , "power of two"          ~: assert =<< isTheorem powerOfTwoCorrect+   "fast min"              ~: assert =<< isThm fastMinCorrect+ , "fast max"              ~: assert =<< isThm fastMaxCorrect+ , "opposite signs"        ~: assert =<< isThm oppositeSignsCorrect+ , "conditional set clear" ~: assert =<< isThm conditionalSetClearCorrect+ , "power of two"          ~: assert =<< isThm powerOfTwoCorrect  ]
SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs view
@@ -20,7 +20,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [-    "prefixSum1" ~: assert =<< isTheorem (flIsCorrect  8 (0, (+)))-  , "prefixSum2" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax))+    "prefixSum1" ~: assert =<< isThm (flIsCorrect  8 (0, (+)))+  , "prefixSum2" ~: assert =<< isThm (flIsCorrect 16 (0, smax))   , "prefixSum3" ~: runSymbolic True (genPrefixSumInstance 16 >>= output) `goldCheck` "prefixSum_16.gold"   ]
SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs view
@@ -11,14 +11,12 @@  module TestSuite.CRC.CCITT_Unidir(testSuite) where -import Data.SBV- import Examples.CRC.CCITT_Unidir import SBVTest  -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "ccitHDis3" ~: assert       =<< isTheorem (crcUniGood 3)- , "ccitHDis4" ~: assert . not =<< isTheorem (crcUniGood 4)+   "ccitHDis3" ~: assert       =<< isThm (crcUniGood 3)+ , "ccitHDis4" ~: assert . not =<< isThm (crcUniGood 4)  ]
SBVUnitTest/TestSuite/CRC/GenPoly.hs view
@@ -19,8 +19,8 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "crcGood" ~: assert       =<< isSatisfiable crcGoodE- , "crcGood" ~: assert . not =<< isTheorem (crcGood 3 12)+   "crcGood" ~: assert       =<< isSat crcGoodE+ , "crcGood" ~: assert . not =<< isThm (crcGood 3 12)  ]  where crcGoodE = do x1 <- exists_                      x2 <- exists_
SBVUnitTest/TestSuite/CRC/Parity.hs view
@@ -11,13 +11,11 @@  module TestSuite.CRC.Parity(testSuite) where -import Data.SBV- import Examples.CRC.Parity import SBVTest  -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "parity" ~: assert =<< isTheorem parityOK+   "parity" ~: assert =<< isThm parityOK  ]
SBVUnitTest/TestSuite/CRC/USB5.hs view
@@ -11,13 +11,11 @@  module TestSuite.CRC.USB5(testSuite) where -import Data.SBV- import Examples.CRC.USB5 import SBVTest  -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "usbGood" ~: assert =<< isTheorem usbGood+   "usbGood" ~: assert =<< isThm usbGood  ]
SBVUnitTest/TestSuite/Crypto/RC4.hs view
@@ -19,6 +19,6 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "rc4swap" ~: assert =<< isTheorem readWrite+   "rc4swap" ~: assert =<< isThm readWrite  ]  where readWrite i j = readSTree (writeSTree initS i j) i .== j
SBVUnitTest/TestSuite/Polynomials/Polynomials.hs view
@@ -11,7 +11,6 @@  module TestSuite.Polynomials.Polynomials(testSuite) where -import Data.SBV import Data.SBV.Examples.Polynomials.Polynomials  import SBVTest@@ -19,7 +18,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "polynomial-1" ~: assert =<< isTheorem multUnit- , "polynomial-2" ~: assert =<< isTheorem multComm- , "polynomial-3" ~: assert =<< isTheorem polyDivMod+   "polynomial-1" ~: assert =<< isThm multUnit+ , "polynomial-2" ~: assert =<< isThm multComm+ , "polynomial-3" ~: assert =<< isThm polyDivMod  ]
SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs view
@@ -19,7 +19,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "magic 2" ~: assert . not =<< isSatisfiable (mkMagic 2)- , "magic 3" ~: assert       =<< isSatisfiable (mkMagic 3)+   "magic 2" ~: assert . not =<< isSat (mkMagic 2)+ , "magic 3" ~: assert       =<< isSat (mkMagic 3)  ]  where mkMagic n = (isMagic . chunk n) `fmap` mkExistVars (n*n)
SBVUnitTest/TestSuite/Puzzles/Sudoku.hs view
@@ -22,4 +22,4 @@   "sudoku " ++ show n ~: assert (checkPuzzle s)      | (n, s) <- zip [(0::Int)..] [puzzle0, puzzle1, puzzle2, puzzle3, puzzle4, puzzle5, puzzle6]  ]- where checkPuzzle (i, f) = isSatisfiable $ (valid . f) `fmap` mkExistVars i+ where checkPuzzle (i, f) = isSat $ (valid . f) `fmap` mkExistVars i
SBVUnitTest/TestSuite/Uninterpreted/AUF.hs view
@@ -20,8 +20,8 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [-   "auf-0" ~: assert =<< isTheorem thm1- , "auf-1" ~: assert =<< isTheorem thm2+   "auf-0" ~: assert =<< isThm thm1+ , "auf-1" ~: assert =<< isThm thm2  , "auf-2" ~: pgm `goldCheck` "auf-1.gold"  ]  where pgm = runSymbolic True $ forAll ["x", "y", "a", "initVal"] thm1 >>= output
SBVUnitTest/TestSuite/Uninterpreted/Function.hs view
@@ -11,7 +11,6 @@  module TestSuite.Uninterpreted.Function where -import Data.SBV import Data.SBV.Examples.Uninterpreted.Function  import SBVTest@@ -19,6 +18,6 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "aufunc-0" ~: assert       =<< isTheorem thmGood- , "aufunc-1" ~: assert . not =<< isTheorem thmBad+   "aufunc-0" ~: assert       =<< isThm thmGood+ , "aufunc-1" ~: assert . not =<< isThm thmBad  ]
SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs view
@@ -11,15 +11,13 @@  module TestSuite.Uninterpreted.Uninterpreted where -import Data.SBV- import Examples.Uninterpreted.Uninterpreted import SBVTest  -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [-   "uninterpreted-0" ~: assert       =<< isTheorem p0- , "uninterpreted-1" ~: assert       =<< isTheorem p1- , "uninterpreted-2" ~: assert . not =<< isTheorem p2+   "uninterpreted-0" ~: assert       =<< isThm p0+ , "uninterpreted-1" ~: assert       =<< isThm p1+ , "uninterpreted-2" ~: assert . not =<< isThm p2  ]
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       2.8+Version:       2.9 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@@ -15,8 +15,21 @@                >   Falsifiable. Counter-example:                >     x = 128 :: SWord8                .-               The SBV library uses Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (<http://yices.csl.sri.com/download-yices2.shtml>), although the Z3 binding is much more richer.+               You can pick the SMT solver you want to use by importing the appropriate module. The SBV library currently+               works with the the following SMT solvers:                .+                  [@import "Data.SBV"@]+                  Picks the default solver, which is currently set to be Z3. (Might change in the future!)+               .+                  [@import "Data.SBV.Bridge.Z3"@]+                  Picks Z3 from Microsoft (<http://z3.codeplex.com/>).+               .+                  [@import "Data.SBV.Bridge.Yices"@]+                  Picks Yices from SRI (<http://yices.csl.sri.com/>) +               .+                  [@import "Data.SBV.Bridge.CVC4"@]+                  Picks CVC4 from New York University and the University of Iowa (<http://cvc4.cs.nyu.edu>) +               .                SBV introduces the following types and concepts:                .                  * 'SBool': Symbolic Booleans (bits)@@ -76,12 +89,12 @@                .                Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>. -Copyright:     Levent Erkok, 2010-2012+Copyright:     Levent Erkok, 2010-2013 License:       BSD3 License-file:  LICENSE Stability:     Experimental Author:        Levent Erkok-Homepage:      http://github.com/LeventErkok/sbv+Homepage:      http://leventerkok.github.com/sbv/ Bug-reports:   http://github.com/LeventErkok/sbv/issues Maintainer:    Levent Erkok (erkokl@gmail.com) Build-Type:    Simple@@ -119,6 +132,9 @@                   , array, containers, deepseq, directory, filepath, old-time                   , pretty, process, mtl, QuickCheck, random, syb   Exposed-modules : Data.SBV+                  , Data.SBV.Bridge.CVC4+                  , Data.SBV.Bridge.Yices+                  , Data.SBV.Bridge.Z3                   , Data.SBV.Internals                   , Data.SBV.Examples.BitPrecise.BitTricks                   , Data.SBV.Examples.BitPrecise.Legato@@ -162,6 +178,7 @@                   , Data.SBV.SMT.SMTLib2                   , Data.SBV.Provers.Prover                   , Data.SBV.Provers.SExpr+                  , Data.SBV.Provers.CVC4                   , Data.SBV.Provers.Yices                   , Data.SBV.Provers.Z3                   , Data.SBV.Tools.ExpectedValue