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