diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -76,9 +76,16 @@ -- . -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver. --- Currently, we support the Z3 SMT solver from Microsoft: --- and the Yices SMT solver from SRI: , 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: +-- +-- * Yices from SRI: +-- +-- * CVC4 from New York University and University of Iowa: +-- +-- 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 diff --git a/Data/SBV/Bridge/CVC4.hs b/Data/SBV/Bridge/CVC4.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Bridge/CVC4.hs @@ -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. +-} diff --git a/Data/SBV/Bridge/Yices.hs b/Data/SBV/Bridge/Yices.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Bridge/Yices.hs @@ -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. +-} diff --git a/Data/SBV/Bridge/Z3.hs b/Data/SBV/Bridge/Z3.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Bridge/Z3.hs @@ -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. +-} diff --git a/Data/SBV/Examples/BitPrecise/PrefixSum.hs b/Data/SBV/Examples/BitPrecise/PrefixSum.hs --- a/Data/SBV/Examples/BitPrecise/PrefixSum.hs +++ b/Data/SBV/Examples/BitPrecise/PrefixSum.hs @@ -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" } ---------------------------------------------------------------------- diff --git a/Data/SBV/Examples/Uninterpreted/Function.hs b/Data/SBV/Examples/Uninterpreted/Function.hs --- a/Data/SBV/Examples/Uninterpreted/Function.hs +++ b/Data/SBV/Examples/Uninterpreted/Function.hs @@ -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 diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Provers/CVC4.hs @@ -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 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' diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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 diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -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 diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -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 diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -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) diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -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 '=' diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -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 _ = [] diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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 ++ ")"] diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/README b/README --- a/README +++ b/README @@ -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/ diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,7 +1,37 @@ Hackage: -GitHub: +GitHub: -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 diff --git a/SBVUnitTest/Examples/Basics/Index.hs b/SBVUnitTest/Examples/Basics/Index.hs --- a/SBVUnitTest/Examples/Basics/Index.hs +++ b/SBVUnitTest/Examples/Basics/Index.hs @@ -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_ diff --git a/SBVUnitTest/Examples/CRC/GenPoly.hs b/SBVUnitTest/Examples/CRC/GenPoly.hs --- a/SBVUnitTest/Examples/CRC/GenPoly.hs +++ b/SBVUnitTest/Examples/CRC/GenPoly.hs @@ -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 diff --git a/SBVUnitTest/SBVTest.hs b/SBVUnitTest/SBVTest.hs --- a/SBVUnitTest/SBVTest.hs +++ b/SBVUnitTest/SBVTest.hs @@ -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -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" diff --git a/SBVUnitTest/TestSuite/Arrays/Memory.hs b/SBVUnitTest/TestSuite/Arrays/Memory.hs --- a/SBVUnitTest/TestSuite/Arrays/Memory.hs +++ b/SBVUnitTest/TestSuite/Arrays/Memory.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs @@ -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) diff --git a/SBVUnitTest/TestSuite/Basics/ProofTests.hs b/SBVUnitTest/TestSuite/Basics/ProofTests.hs --- a/SBVUnitTest/TestSuite/Basics/ProofTests.hs +++ b/SBVUnitTest/TestSuite/Basics/ProofTests.hs @@ -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_ diff --git a/SBVUnitTest/TestSuite/Basics/QRem.hs b/SBVUnitTest/TestSuite/Basics/QRem.hs --- a/SBVUnitTest/TestSuite/Basics/QRem.hs +++ b/SBVUnitTest/TestSuite/Basics/QRem.hs @@ -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) ] diff --git a/SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs b/SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs --- a/SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs +++ b/SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs b/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs --- a/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs +++ b/SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs @@ -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" ] diff --git a/SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs b/SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs --- a/SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs +++ b/SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs @@ -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) ] diff --git a/SBVUnitTest/TestSuite/CRC/GenPoly.hs b/SBVUnitTest/TestSuite/CRC/GenPoly.hs --- a/SBVUnitTest/TestSuite/CRC/GenPoly.hs +++ b/SBVUnitTest/TestSuite/CRC/GenPoly.hs @@ -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_ diff --git a/SBVUnitTest/TestSuite/CRC/Parity.hs b/SBVUnitTest/TestSuite/CRC/Parity.hs --- a/SBVUnitTest/TestSuite/CRC/Parity.hs +++ b/SBVUnitTest/TestSuite/CRC/Parity.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/CRC/USB5.hs b/SBVUnitTest/TestSuite/CRC/USB5.hs --- a/SBVUnitTest/TestSuite/CRC/USB5.hs +++ b/SBVUnitTest/TestSuite/CRC/USB5.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/Crypto/RC4.hs b/SBVUnitTest/TestSuite/Crypto/RC4.hs --- a/SBVUnitTest/TestSuite/Crypto/RC4.hs +++ b/SBVUnitTest/TestSuite/Crypto/RC4.hs @@ -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 diff --git a/SBVUnitTest/TestSuite/Polynomials/Polynomials.hs b/SBVUnitTest/TestSuite/Polynomials/Polynomials.hs --- a/SBVUnitTest/TestSuite/Polynomials/Polynomials.hs +++ b/SBVUnitTest/TestSuite/Polynomials/Polynomials.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs b/SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs --- a/SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs +++ b/SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs @@ -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) diff --git a/SBVUnitTest/TestSuite/Puzzles/Sudoku.hs b/SBVUnitTest/TestSuite/Puzzles/Sudoku.hs --- a/SBVUnitTest/TestSuite/Puzzles/Sudoku.hs +++ b/SBVUnitTest/TestSuite/Puzzles/Sudoku.hs @@ -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 diff --git a/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs b/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/AUF.hs @@ -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 diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Function.hs b/SBVUnitTest/TestSuite/Uninterpreted/Function.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/Function.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/Function.hs @@ -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 ] diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs b/SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs @@ -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 ] diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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 () as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (), 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 (). + . + [@import "Data.SBV.Bridge.Yices"@] + Picks Yices from SRI () + . + [@import "Data.SBV.Bridge.CVC4"@] + Picks CVC4 from New York University and the University of Iowa () + . SBV introduces the following types and concepts: . * 'SBool': Symbolic Booleans (bits) @@ -76,12 +89,12 @@ . Release notes can be seen at: . -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