sbv 4.0 → 4.1
raw patch · 29 files changed
+622/−171 lines, 29 filesdep ~deepseq
Dependency ranges changed: deepseq
Files
- CHANGES.md +33/−1
- Data/SBV.hs +4/−2
- Data/SBV/BitVectors/Data.hs +40/−19
- Data/SBV/BitVectors/PrettyNum.hs +45/−3
- Data/SBV/BitVectors/Rounding.hs +75/−0
- Data/SBV/Bridge/ABC.hs +113/−0
- Data/SBV/Bridge/Boolector.hs +2/−0
- Data/SBV/Bridge/CVC4.hs +2/−0
- Data/SBV/Bridge/MathSAT.hs +2/−0
- Data/SBV/Bridge/Yices.hs +2/−0
- Data/SBV/Bridge/Z3.hs +2/−0
- Data/SBV/Compilers/C.hs +1/−0
- Data/SBV/Examples/Misc/Floating.hs +69/−2
- Data/SBV/Internals.hs +5/−1
- Data/SBV/Provers/ABC.hs +79/−0
- Data/SBV/Provers/Boolector.hs +12/−17
- Data/SBV/Provers/CVC4.hs +5/−14
- Data/SBV/Provers/MathSAT.hs +5/−14
- Data/SBV/Provers/Prover.hs +9/−2
- Data/SBV/Provers/SExpr.hs +76/−27
- Data/SBV/Provers/Yices.hs +7/−7
- Data/SBV/Provers/Z3.hs +2/−12
- Data/SBV/SMT/SMT.hs +3/−0
- Data/SBV/SMT/SMTLib.hs +1/−1
- Data/SBV/SMT/SMTLib1.hs +1/−0
- Data/SBV/SMT/SMTLib2.hs +15/−45
- Data/SBV/Tools/Polynomial.hs +7/−2
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +4/−1
CHANGES.md view
@@ -1,7 +1,39 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 3.5+* Latest Hackage released version: 4.1, 2015-03-06++### Version 4.1, 2015-03-06++ * Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer+ for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/+ And Alan Mishchenko for adding infrastructure to ABC to work with SBV.++ * Upgrade the Boolector connection to use a SMT-Lib2 based interaction. NB. You+ need at least Boolector 2.0.6 installed!++ * Tracking changes in the SMT-Lib floating-point theory. If you are+ using symbolic floating-point types (i.e., SFloat and SDouble), then+ you should upgrade to this version and also get a very latest (unstable)+ Z3 release. See http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2+ for details.++ * Introduce a new class, 'RoundingFloat', which supports floating-point+ operations with arbitrary rounding-modes. Note that Haskell only allows+ RoundNearestTiesToAway, but with SBV, we get all 5 IEEE754 rounding-modes+ and all the basic operations ('fpAdd', 'fpMul', 'fpDiv', etc.) with these+ modes.+ + * Allow Floating-Point RoundingMode to be symbolic as well++ * Improve the example "Data/SBV/Examples/Misc/Floating.hs" to include+ rounding-mode based addition example.+ + * Changes required to make SBV compile with GHC 7.10; mostly around instance+ NFData declarations. Thanks to Iavor Diatchki for the patch.++ * Export a few extra symbols from the Internals module (mainly for+ Cryptol usage.) ### Version 4.0, 2015-01-22
Data/SBV.hs view
@@ -123,7 +123,7 @@ , SInteger -- *** IEEE-floating point numbers -- $floatingPoints- , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isSNaN, isFPPoint+ , SFloat, SDouble, RoundingFloat(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity, fusedMA, isSNaN, isFPPoint -- *** Signed algebraic reals -- $algReals , SReal, AlgReal, toSReal@@ -228,7 +228,7 @@ , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers- , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers+ , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers -- * Symbolic computations , Symbolic, output, SymWord(..)@@ -282,6 +282,7 @@ import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model import Data.SBV.BitVectors.PrettyNum+import Data.SBV.BitVectors.Rounding import Data.SBV.BitVectors.SignCast import Data.SBV.BitVectors.Splittable import Data.SBV.BitVectors.STree@@ -345,6 +346,7 @@ defaultSolverConfig Boolector = boolector defaultSolverConfig CVC4 = cvc4 defaultSolverConfig MathSAT = mathSAT+defaultSolverConfig ABC = abc -- | Return the known available solver configs, installed on your machine. sbvAvailableSolvers :: IO [SMTConfig]
Data/SBV/BitVectors/Data.hs view
@@ -19,12 +19,13 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64 , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble- , nan, infinity, sNaN, sInfinity, RoundingMode(..), smtLibSquareRoot, smtLibFusedMA+ , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode, smtLibSquareRoot, smtLibFusedMA , SymWord(..) , CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool , mkConstCW ,liftCW2, mapCW, mapCW2@@ -59,6 +60,7 @@ import Data.Maybe (isJust, fromJust) import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields)+import qualified Data.Typeable as T (Typeable) import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) import qualified Data.Set as Set (Set, empty, toList, insert)@@ -247,11 +249,13 @@ | ArrEq Int Int | ArrRead Int | Uninterpreted String+ -- Floating point uops with custom rounding-modes+ | FPRound String deriving (Eq, Ord) -- | SMT-Lib's square-root over floats/doubles. We piggy back on to the uninterpreted function mechanism -- to implement these; which is not a terrible idea; although the use of the constructor 'Uninterpreted'--- might be confusing. This function will *not* be uninterpreted in reality, as QF_FPA will define it. It's+-- might be confusing. This function will *not* be uninterpreted in reality, as QF_FP will define it. It's -- a bit of a shame, but much easier to implement it this way. smtLibSquareRoot :: Op smtLibSquareRoot = Uninterpreted "fp.sqrt"@@ -397,6 +401,7 @@ show (ArrEq i j) = "array_" ++ show i ++ " == array_" ++ show j show (ArrRead i) = "select array_" ++ show i show (Uninterpreted i) = "[uninterpreted] " ++ i+ show (FPRound w) = w show op | Just s <- op `lookup` syms = s | True = error "impossible happened; can't find op!"@@ -487,7 +492,9 @@ ++ map ((" " ++) . show) cstrs ++ ["OUTPUTS"] ++ map ((" " ++) . show) os- where usorts = [s | KUserSort s _ <- Set.toList kinds]+ where usorts = [sh s t | KUserSort s t <- Set.toList kinds]+ where sh s (Left _, _) = s+ sh s (Right es, _) = s ++ " (" ++ intercalate ", " es ++ ")" shs sw = show sw ++ " :: " ++ showType sw sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw@@ -692,7 +699,17 @@ | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.)+ deriving (Eq, Ord, G.Data, T.Typeable, Read, Show, Bounded, Enum) +-- | 'RoundingMode' can be used symbolically+instance SymWord RoundingMode++-- | 'RoundingMode' kind+instance HasKind RoundingMode++-- | The symbolic variant of 'RoundingMode'+type SRoundingMode = SBV RoundingMode+ -- Not particularly "desirable", but will do if needed instance Show (SBV a) where show (SBV _ (Left c)) = show c@@ -754,7 +771,8 @@ = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." | True = modifyIORef (rUsedKinds st) (Set.insert k)- where reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP", "FloatingPoint"] -- Reserved by SMT-Lib+ where -- TODO: this list is not comprehensive!+ reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP", "FloatingPoint", "fp"] -- Reserved by SMT-Lib -- | Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW@@ -1300,8 +1318,8 @@ data SMTLibPgm = SMTLibPgm SMTLibVersion ( [(String, SW)] -- alias table , [String] -- pre: declarations. , [String]) -- post: formula-instance NFData SMTLibVersion-instance NFData SMTLibPgm+instance NFData SMTLibVersion where rnf a = seq a ()+instance NFData SMTLibPgm where rnf a = seq a () instance Show SMTLibPgm where show (SMTLibPgm _ (_, pre, post)) = intercalate "\n" $ pre ++ post@@ -1316,19 +1334,20 @@ `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf cstr `seq` rnf outs-instance NFData Kind-instance NFData ArrayContext-instance NFData SW-instance NFData SBVExpr-instance NFData Quantifier-instance NFData SBVType-instance NFData UnintKind+instance NFData Kind where rnf a = seq a ()+instance NFData ArrayContext where rnf a = seq a ()+instance NFData SW where rnf a = seq a ()+instance NFData SBVExpr where rnf a = seq a ()+instance NFData Quantifier where rnf a = seq a ()+instance NFData SBVType where rnf a = seq a ()+instance NFData UnintKind where rnf a = seq a () instance NFData a => NFData (Cached a) where rnf (Cached f) = f `seq` () instance NFData a => NFData (SBV a) where rnf (SBV x y) = rnf x `seq` rnf y `seq` ()-instance NFData SBVPgm+instance NFData SBVPgm where rnf a = seq a () + instance NFData SMTResult where rnf (Unsatisfiable _) = () rnf (Satisfiable _ xs) = rnf xs `seq` ()@@ -1344,14 +1363,13 @@ -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the -- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if--- one is experimenting with custom logics that might be supported on new solvers.+-- one is experimenting with custom logics that might be supported on new solvers. See <http://smtlib.cs.uiowa.edu/logics.shtml>+-- for the official list. data SMTLibLogic = AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value | AUFNIRA -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value | LRA -- ^ Linear formulas in linear real arithmetic- | UFLRA -- ^ Linear real arithmetic with uninterpreted sort and function symbols. - | UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols. | QF_ABV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays | QF_AUFBV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols | QF_AUFLIA -- ^ Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols@@ -1369,8 +1387,10 @@ | QF_UFLIA -- ^ Unquantified linear integer arithmetic with uninterpreted sort and function symbols. | QF_UFLRA -- ^ Unquantified linear real arithmetic with uninterpreted sort and function symbols. | QF_UFNRA -- ^ Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. - | QF_FPABV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors- | QF_FPA -- ^ Quantifier-free formulas over the theory of floating point numbers+ | UFLRA -- ^ Linear real arithmetic with uninterpreted sort and function symbols. + | UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols. + | QF_FPBV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors+ | QF_FP -- ^ Quantifier-free formulas over the theory of floating point numbers deriving Show -- | Chosen logic for the solver@@ -1461,6 +1481,7 @@ | Boolector | CVC4 | MathSAT+ | ABC deriving (Show, Enum, Bounded) -- | An SMT solver
Data/SBV/BitVectors/PrettyNum.hs view
@@ -15,18 +15,19 @@ module Data.SBV.BitVectors.PrettyNum ( PrettyNum(..), readBin, shex, shexI, sbin, sbinI , showCFloat, showCDouble, showHFloat, showHDouble- , showSMTFloat, showSMTDouble, smtRoundingMode+ , showSMTFloat, showSMTDouble, smtRoundingMode, cwToSMTLib, mkSkolemZero ) where -import Data.Char (ord)+import Data.Char (ord, intToDigit) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf)-import Data.Maybe (fromJust)+import Data.Maybe (fromJust, fromMaybe, listToMaybe) import Data.Ratio (numerator, denominator) import Data.Word (Word8, Word16, Word32, Word64) import Numeric (showIntAtBase, showHex, readInt) import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.AlgReals (algRealToSMTLib2) -- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers. --@@ -240,3 +241,44 @@ smtRoundingMode RoundTowardPositive = "roundTowardPositive" smtRoundingMode RoundTowardNegative = "roundTowardNegative" smtRoundingMode RoundTowardZero = "roundTowardZero"++-- | Convert a CW to an SMTLib2 compliant value+cwToSMTLib :: RoundingMode -> CW -> String+cwToSMTLib rm x+ | isBoolean x, CWInteger w <- cwVal x = if w == 0 then "false" else "true"+ | isUninterpreted x, CWUserSort (_, s) <- cwVal x = roundModeConvert s+ | isReal x, CWAlgReal r <- cwVal x = algRealToSMTLib2 r+ | isFloat x, CWFloat f <- cwVal x = showSMTFloat rm f+ | isDouble x, CWDouble d <- cwVal x = showSMTDouble rm d+ | not (isBounded x), CWInteger w <- cwVal x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")"+ | not (hasSign x) , CWInteger w <- cwVal x = smtLibHex (intSizeOf x) w+ -- signed numbers (with 2's complement representation) is problematic+ -- since there's no way to put a bvneg over a positive number to get minBound..+ -- Hence, we punt and use binary notation in that particular case+ | hasSign x , CWInteger w <- cwVal x = if w == negate (2 ^ intSizeOf x)+ then mkMinBound (intSizeOf x)+ else negIf (w < 0) $ smtLibHex (intSizeOf x) (abs w)+ | True = error $ "SBV.cvtCW: Impossible happened: Kind/Value disagreement on: " ++ show (kindOf x, x)+ where roundModeConvert s = fromMaybe s (listToMaybe [smtRoundingMode m | m <- [minBound .. maxBound] :: [RoundingMode], show m == s])+ -- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time+ -- being, SBV only supports sizes that are multiples of 4, but the below code is more robust+ -- in case of future extensions to support arbitrary sizes.+ smtLibHex :: Int -> Integer -> String+ smtLibHex 1 v = "#b" ++ show v+ smtLibHex sz v+ | sz `mod` 4 == 0 = "#x" ++ pad (sz `div` 4) (showHex v "")+ | True = "#b" ++ pad sz (showBin v "")+ where showBin = showIntAtBase 2 intToDigit+ negIf :: Bool -> String -> String+ negIf True a = "(bvneg " ++ a ++ ")"+ negIf False a = a+ -- anamoly at the 2's complement min value! Have to use binary notation here+ -- as there is no positive value we can provide to make the bvneg work.. (see above)+ mkMinBound :: Int -> String+ mkMinBound i = "#b1" ++ replicate (i-1) '0'++-- | Create a skolem 0 for the kind+mkSkolemZero :: RoundingMode -> Kind -> String+mkSkolemZero _ (KUserSort _ (Right (f:_), _)) = f+mkSkolemZero _ (KUserSort s _) = error $ "SBV.mkSkolemZero: Unexpected uninterpreted sort: " ++ s+mkSkolemZero rm k = cwToSMTLib rm (mkConstCW k (0::Integer))
+ Data/SBV/BitVectors/Rounding.hs view
@@ -0,0 +1,75 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.BitVectors.Rounding+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Implementation of floating-point operations that know about rounding-modes+-----------------------------------------------------------------------------++module Data.SBV.BitVectors.Rounding (RoundingFloat(..)) where++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.Model () -- instances only++-- | A class of floating-point (IEEE754) operations that behave+-- differently based on rounding modes. Note that we will never+-- concretely evaluate these, but rather pass down to the SMT solver+-- even when we have a concrete rounding mode supported by Haskell.+-- (i.e., round-to-nearest even.) The extra complexity is just not+-- worth it to support constant folding in that rare case; and if+-- the rounding mode is already round-to-nearest-even then end-users simply+-- use the usual Num instances. (Except for FMA obviously, which has no+-- Haskell equivalent.)+class (SymWord a, Floating a) => RoundingFloat a where+ fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a+ fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a+ fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a+ fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a+ fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a+ fpSqrt :: SRoundingMode -> SBV a -> SBV a++ -- Default definitions simply piggy back onto FPRound+ fpAdd = lift2Rm "fp.add"+ fpSub = lift2Rm "fp.sub"+ fpMul = lift2Rm "fp.mul"+ fpDiv = lift2Rm "fp.div"+ fpFMA = lift3Rm "fp.fma"+ fpSqrt = lift1Rm "fp.sqrt"++-- | Lift a 1 arg floating point UOP+lift1Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a+lift1Rm w m a = SBV k $ Right $ cache r+ where k = kindOf a+ r st = do swm <- sbvToSW st m+ swa <- sbvToSW st a+ newExpr st k (SBVApp (FPRound w) [swm, swa])++-- | Lift a 2 arg floating point UOP+lift2Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a -> SBV a+lift2Rm w m a b = SBV k $ Right $ cache r+ where k = kindOf a+ r st = do swm <- sbvToSW st m+ swa <- sbvToSW st a+ swb <- sbvToSW st b+ newExpr st k (SBVApp (FPRound w) [swm, swa, swb])++-- | Lift a 3 arg floating point UOP+lift3Rm :: (SymWord a, Floating a) => String -> SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a+lift3Rm w m a b c = SBV k $ Right $ cache r+ where k = kindOf a+ r st = do swm <- sbvToSW st m+ swa <- sbvToSW st a+ swb <- sbvToSW st b+ swc <- sbvToSW st c+ newExpr st k (SBVApp (FPRound w) [swm, swa, swb, swc])++-- | SFloat instance+instance RoundingFloat Float++-- | SDouble instance+instance RoundingFloat Double++{-# ANN module "HLint: ignore Reduce duplication" #-}
+ Data/SBV/Bridge/ABC.hs view
@@ -0,0 +1,113 @@+---------------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Bridge.ABC+-- Copyright : (c) Adam Foltzer+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Interface to the ABC verification and synthesis tool. Import this+-- module if you want to use ABC as your backend solver. Also see:+--+-- - "Data.SBV.Bridge.Yices"+--+-- - "Data.SBV.Bridge.Z3"+--+-- - "Data.SBV.Bridge.Boolector"+--+-- - "Data.SBV.Bridge.MathSAT"+--+-- - "Data.SBV.Bridge.CVC4"+---------------------------------------------------------------------------------++module Data.SBV.Bridge.ABC (+ -- * ABC specific interface+ sbvCurrentSolver+ -- ** Proving, checking satisfiability, and safety+ , prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable+ -- ** Optimization routines+ , optimize, minimize, maximize+ , module Data.SBV+ ) where++import Data.SBV hiding (prove, sat, safe, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)++-- | Current solver instance, pointing to abc.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = abc++-- | Prove theorems, using ABC+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 ABC+sat :: Provable a+ => a -- ^ Property to check+ -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found+sat = satWith sbvCurrentSolver++-- | Check safety, i.e., prove that all 'sAssert' conditions are statically true in all paths+safe :: SExecutable a+ => a -- ^ Program to check the safety of+ -> IO SafeResult -- ^ Response of the SMT solver, containing the unsafe model if found+safe = safeWith sbvCurrentSolver++-- | Find all satisfying solutions, using ABC+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 ABC+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 ABC+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 ABC+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 ABC+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 ABC+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 ABC+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+ => OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)+ -> ([SBV a] -> SBV c) -- ^ Cost function to maximize+ -> Int -- ^ Number of inputs+ -> ([SBV a] -> SBool) -- ^ Validity function+ -> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+maximize = maximizeWith sbvCurrentSolver++{- $moduleExportIntro+The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.+-}
Data/SBV/Bridge/Boolector.hs view
@@ -16,6 +16,8 @@ -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.MathSAT"+--+-- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Boolector (
Data/SBV/Bridge/CVC4.hs view
@@ -16,6 +16,8 @@ -- - "Data.SBV.Bridge.Boolector" -- -- - "Data.SBV.Bridge.MathSAT"+--+-- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.CVC4 (
Data/SBV/Bridge/MathSAT.hs view
@@ -16,6 +16,8 @@ -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.Boolector"+--+-- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.MathSAT (
Data/SBV/Bridge/Yices.hs view
@@ -16,6 +16,8 @@ -- - "Data.SBV.Bridge.Z3" -- -- - "Data.SBV.Bridge.MathSAT"+--+-- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Yices (
Data/SBV/Bridge/Z3.hs view
@@ -16,6 +16,8 @@ -- - "Data.SBV.Bridge.Yices" -- -- - "Data.SBV.Bridge.MathSAT"+--+-- - "Data.SBV.Bridge.ABC" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Z3 (
Data/SBV/Compilers/C.hs view
@@ -501,6 +501,7 @@ uninterpret s as = text "/* Uninterpreted function */" <+> text s <> parens (fsep (punctuate comma as)) p (ArrRead _) _ = tbd "User specified arrays (ArrRead)" p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)"+ p (FPRound w) _ = tbd $ "Floating point operations with custom rounding modes (" ++ w ++ ")" p (Uninterpreted s) as = uninterpret s as p (Extract i j) [a] = extract i j (head opArgs) a p Join [a, b] = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b))
Data/SBV/Examples/Misc/Floating.hs view
@@ -14,6 +14,8 @@ -- the presence of @NaN@ is always something to look out for. ----------------------------------------------------------------------------- +{-# LANGUAGE ScopedTypeVariables #-}+ module Data.SBV.Examples.Misc.Floating where import Data.SBV@@ -109,7 +111,7 @@ -- * FP multiplicative inverses may not exist ----------------------------------------------------------------------------- --- | The last example illustrates that @a * (1/a)@ does not necessarily equal @1@. Again,+-- | This example illustrates that @a * (1/a)@ does not necessarily equal @1@. Again, -- we protect against division by @0@ and @NaN@/@Infinity@. -- -- We have:@@ -120,7 +122,7 @@ -- -- Indeed, we have: ----- >>> let a = 1.2354518252390238e308 :: Double+-- >>> let a = 1.2354518252390238e308 :: Double -- >>> a * (1/a) -- 0.9999999999999998 multInverse :: IO ThmResult@@ -128,3 +130,68 @@ constrain $ isFPPoint a constrain $ isFPPoint (1/a) return $ a * (1/a) .== 1++-----------------------------------------------------------------------------+-- * Effect of rounding modes+-----------------------------------------------------------------------------++-- | One interesting aspect of floating-point is that the chosen rounding-mode+-- can effect the results of a computation if the exact result cannot be precisely+-- represented. SBV exports the functions 'fpAdd', 'fpSub', 'fpMul', 'fpDiv', 'fpFMA'+-- and 'fpSqrt' which allows users to specify the IEEE supported 'RoundingMode' for+-- the operation. (Also see the class 'RoundingFloat'.) This example illustrates how SBV+-- can be used to find rounding-modes where, for instance, addition can produce different+-- results. We have:+--+-- >>> roundingAdd+-- Satisfiable. Model:+-- rm = RoundTowardPositive :: RoundingMode+-- x = 1.7014118e38 :: SFloat+-- y = 1.1754942e-38 :: SFloat+--+-- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports+-- 'RoundNearestTiesToEven'. We have:+--+-- >>> (1.7014118e38 + 1.1754942e-38) :: Float+-- 1.7014118e38+--+-- Note that result is identical to the first argument. But with a 'RoundTowardPositive', we would+-- get the result @1.701412e38@. While we cannot directly see this from within Haskell, we can+-- use SBV to provide us with that result thusly:+--+-- >>> sat $ \x -> x .== fpAdd (literal RoundTowardPositive) (1.7014118e38::SFloat) (1.1754942e-38::SFloat)+-- Satisfiable. Model:+-- s0 = 1.701412e38 :: SFloat+--+-- We can see why these two resuls are different if we treat these values as arbitrary+-- precision reals, as represented by the 'SReal' type:+--+-- >>> let x = 1.7014118e38 :: SReal+-- >>> let y = 1.1754942e-38 :: SReal+-- >>> x+-- 170141180000000000000000000000000000000.0 :: SReal+-- >>> y+-- 0.000000000000000000000000000000000000011754942 :: SReal+-- >>> x + y+-- 170141180000000000000000000000000000000.000000000000000000000000000000000000011754942 :: SReal+--+-- When we do 'RoundNearestTiesToEven', the entire suffix falls off, as it happens that the infinitely+-- precise result is closer to the value of @x@. But when we use 'RoundTowardPositive', we reach+-- for the next representable number, which happens to be @1.701412e38@. You might wonder why not+-- @1.7014119e38@? Because that number is not precisely representable as a 'Float':+--+-- >>> 1.7014119e38:: Float+-- 1.7014118e38+--+-- But @1.701412e38@ is:+--+-- >>> 1.701412e38 :: Float+-- 1.701412e38+--+-- Floating point representation and semantics is indeed a thorny subject, <https://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> happens to be an excellent guide, however.+roundingAdd :: IO SatResult+roundingAdd = sat $ do m :: SRoundingMode <- free "rm"+ x <- sFloat "x"+ y <- sFloat "y"+ constrain $ m ./= literal RoundNearestTiesToEven+ return $ fpAdd m x y ./= x + y
Data/SBV/Internals.hs view
@@ -18,16 +18,20 @@ , SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW, genVar, genVar_ , liftQRem, liftDMod, symbolicMergeWithKind , cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), mkSymSBVWithRandom+ , SBVType(..), newUninterpreted, forceSWArg -- * Operations useful for instantiating SBV type classes , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse+ -- * Polynomial operations that operate on bit-vectors+ , ites, mdp, addPoly -- * Compilation to C , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..) ) where import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW)-import Data.SBV.BitVectors.Data (cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), mkSymSBVWithRandom)+import Data.SBV.BitVectors.Data (cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), mkSymSBVWithRandom, SBVType(..), newUninterpreted, forceSWArg) import Data.SBV.BitVectors.Model (genVar, genVar_, slet, liftQRem, liftDMod, symbolicMergeWithKind, genLiteral, genFromCW, genMkSymVar) import Data.SBV.BitVectors.Splittable (checkAndConvert) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) import Data.SBV.SMT.SMT (genParse)+import Data.SBV.Tools.Polynomial (ites, mdp, addPoly)
+ Data/SBV/Provers/ABC.hs view
@@ -0,0 +1,79 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Provers.ABC+-- Copyright : (c) Adam Foltzer+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- The connection to the ABC verification and synthesis tool+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module Data.SBV.Provers.ABC(abc) where++import qualified Control.Exception as C++import Data.Function (on)+import Data.List (intercalate, sortBy)+import System.Environment (getEnv)++import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.PrettyNum (mkSkolemZero)+import Data.SBV.SMT.SMT+import Data.SBV.SMT.SMTLib++-- | The description of abc. The default executable is @\"abc\"@,+-- which must be in your path. You can use the @SBV_ABC@ environment+-- variable to point to the executable on your system. There are no+-- default options. You can use the @SBV_ABC_OPTIONS@ environment+-- variable to override the options.+abc :: SMTSolver+abc = SMTSolver {+ name = ABC+ , executable = "abc"+ , options = ["-S", "%blast; &put; dsat -s"]+ , engine = \cfg isSat qinps modelMap skolemMap pgm -> do+ execName <- getEnv "SBV_ABC" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (words `fmap` getEnv "SBV_ABC_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ let cfg' = cfg { solver = (solver cfg) {executable = execName, options = 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 (roundingMode cfg) skolemMap)}+ standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap))+ , xformExitCode = id+ , capabilities = SolverCapabilities {+ capSolverName = "ABC"+ , mbDefaultLogic = Nothing+ , supportsMacros = True+ , supportsProduceModels = True+ , supportsQuantifiers = False+ , supportsUninterpretedSorts = False+ , supportsUnboundedInts = False+ , supportsReals = False+ , supportsFloats = False+ , supportsDoubles = False+ }+ }+ where cont rm skolemMap = intercalate "\n" $ map extract skolemMap+ where extract (Left s) = "(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"+ extract (Right (s, [])) = "(get-value (" ++ show s ++ "))"+ extract (Right (s, ss)) = "(get-value (" ++ show s ++ concat [' ' : mkSkolemZero rm (kindOf a) | a <- ss] ++ "))"++extractMap :: Bool -> [(Quantifier, NamedSymVar)] -> [(String, UnintKind)] -> [String] -> SMTModel+extractMap isSat qinps _modelMap solverLines =+ SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps) 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 = map snd $ if all (== ALL) (map fst qinps)+ then qinps+ else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps+ -- for "proof", just display the prefix universals+ | True = map snd $ takeWhile ((== ALL) . fst) qinps
Data/SBV/Provers/Boolector.hs view
@@ -16,11 +16,12 @@ import qualified Control.Exception as C import Data.Function (on)-import Data.List (sortBy)+import Data.List (sortBy, intercalate) import System.Environment (getEnv) import System.Exit (ExitCode(..)) import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -31,25 +32,22 @@ boolector = SMTSolver { name = Boolector , executable = "boolector"- , options = ["-m", "--smt2"]- , engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do+ , options = ["--smt2", "--smt2-model"]+ , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do execName <- getEnv "SBV_BOOLECTOR" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg))) execOpts <- (words `fmap` getEnv "SBV_BOOLECTOR_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))- let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts}- , satCmd = satCmd cfg ++ "\n(exit)" -- boolector requires a final exit line- }+ 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 ---"]- -- boolector complains if we don't have "exit" at the end- script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Nothing}+ script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont (roundingMode cfg) skolemMap)} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap)) , xformExitCode = boolectorExitCode , capabilities = SolverCapabilities { capSolverName = "Boolector" , mbDefaultLogic = Nothing , supportsMacros = False- , supportsProduceModels = False+ , supportsProduceModels = True , supportsQuantifiers = False , supportsUninterpretedSorts = False , supportsUnboundedInts = False@@ -62,6 +60,10 @@ addTimeOut (Just i) o | i < 0 = error $ "Boolector: Timeout value must be non-negative, received: " ++ show i | True = o ++ ["-t=" ++ show i]+ cont rm skolemMap = intercalate "\n" $ map extract skolemMap+ where extract (Left s) = "(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"+ extract (Right (s, [])) = "(get-value (" ++ show s ++ "))"+ extract (Right (s, ss)) = "(get-value (" ++ show s ++ concat [' ' : mkSkolemZero rm (kindOf a) | a <- ss] ++ "))" -- | Similar to CVC4, Boolector uses different exit codes to indicate its status. boolectorExitCode :: ExitCode -> ExitCode@@ -70,16 +72,9 @@ extractMap :: [NamedSymVar] -> [(String, UnintKind)] -> [String] -> SMTModel extractMap inps _modelMap solverLines =- SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps . cvt) solverLines+ SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps) solverLines , modelUninterps = [] , modelArrays = [] } where sortByNodeId :: [(Int, a)] -> [(Int, a)] sortByNodeId = sortBy (compare `on` fst)- -- Boolector outputs in a non-parenthesized way; and also puts x's for don't care bits:- cvt :: String -> String- cvt s = case words s of- [_, val, var] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"- _ -> s -- good-luck..- where tr 'x' = '0'- tr x = x
Data/SBV/Provers/CVC4.hs view
@@ -22,6 +22,7 @@ import System.Exit (ExitCode(..)) import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -40,7 +41,7 @@ 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)}+ script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont (roundingMode cfg) skolemMap)} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap)) , xformExitCode = cvc4ExitCode , capabilities = SolverCapabilities {@@ -56,20 +57,10 @@ , supportsDoubles = False } }- where zero :: Kind -> String- zero KBool = "false"- zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'- zero KUnbounded = "0"- zero KReal = "0.0"- zero KFloat = error "SBV.CVC4.zero: Unexpected float value"- zero KDouble = error "SBV.CVC4.zero: Unexpected double value"- -- For uninterpreted sorts, we use the first element of the enumerations if available; otherwise bail out..- zero (KUserSort _ (Right (f:_), _)) = f- zero (KUserSort 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) ++ "))\")"+ where cont rm skolemMap = intercalate "\n" $ map extract skolemMap+ where extract (Left s) = "(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")" extract (Right (s, [])) = "(get-value (" ++ show s ++ "))"- extract (Right (s, ss)) = "(get-value (" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ "))"+ extract (Right (s, ss)) = "(get-value (" ++ show s ++ concat [' ' : mkSkolemZero rm (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
Data/SBV/Provers/MathSAT.hs view
@@ -20,6 +20,7 @@ import System.Environment (getEnv) import Data.SBV.BitVectors.Data+import Data.SBV.BitVectors.PrettyNum (mkSkolemZero) import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -39,7 +40,7 @@ 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)}+ script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont (roundingMode cfg) skolemMap)} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap)) , xformExitCode = id , capabilities = SolverCapabilities {@@ -55,26 +56,16 @@ , supportsDoubles = False } }- where zero :: Kind -> String- zero KBool = "false"- zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'- zero KUnbounded = "0"- zero KReal = "0.0"- zero KFloat = error "SBV.MathSAT.zero: Unexpected sort SFloat"- zero KDouble = error "SBV.MathSAT.zero: Unexpected sort SDouble"- -- For uninterpreted sorts, we use the first element of the enumerations if available; otherwise bail out..- zero (KUserSort _ (Right (f:_), _)) = f- zero (KUserSort s _) = error $ "SBV.MathSAT.zero: Unexpected uninterpreted sort: " ++ s- cont skolemMap = intercalate "\n" $ concatMap extract skolemMap+ where cont rm skolemMap = intercalate "\n" $ concatMap extract skolemMap 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 (Left s) = ["(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"] extract (Right (s, [])) = ["(get-value (" ++ show s ++ "))"]- extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in [g]+ extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : mkSkolemZero rm (kindOf a) | a <- ss] ++ ")))" in [g] addTimeOut Nothing o = o addTimeOut (Just _) _ = error "MathSAT: Timeout values are not supported by MathSat"
Data/SBV/Provers/Prover.hs view
@@ -26,7 +26,7 @@ , isVacuous, isVacuousWith , SatModel(..), Modelable(..), displayModels, extractModels , getModelDictionaries, getModelValues, getModelUninterpretedValues- , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg+ , boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks , isSBranchFeasibleInState , isConditionSatisfiable@@ -52,6 +52,7 @@ import qualified Data.SBV.Provers.Yices as Yices import qualified Data.SBV.Provers.Z3 as Z3 import qualified Data.SBV.Provers.MathSAT as MathSAT+import qualified Data.SBV.Provers.ABC as ABC import Data.SBV.Utils.TDiff mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig@@ -90,6 +91,10 @@ mathSAT :: SMTConfig mathSAT = mkConfig MathSAT.mathSAT True [] +-- | Default configuration for the ABC synthesis and verification tool.+abc :: SMTConfig+abc = mkConfig ABC.abc True []+ -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig defaultSMTCfg = z3@@ -371,7 +376,9 @@ let converter = if useSMTLib2 config then toSMTLib2 else toSMTLib1 msg "Checking Satisfiability, all solutions.." sbvPgm@(qinps, _, _, ki, _) <- simulate converter config True [] p- let usorts = [s | KUserSort s _ <- Set.toList ki]+ let usorts = [s | us@(KUserSort s _) <- Set.toList ki, isFree us]+ where isFree (KUserSort _ (Left _, _)) = True+ isFree _ = False unless (null usorts) $ msg $ "SBV.allSat: Uninterpreted sorts present: " ++ unwords usorts ++ "\n SBV will use equivalence classes to generate all-satisfying instances." results <- unsafeInterleaveIO $ go sbvPgm (1::Int) []
Data/SBV/Provers/SExpr.hs view
@@ -11,16 +11,23 @@ module Data.SBV.Provers.SExpr where +import Data.Bits (setBit, testBit)+import Data.Word (Word32, Word64) import Data.Char (isDigit, ord) import Data.List (isPrefixOf)+import Data.Maybe (fromMaybe, listToMaybe) import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.BitVectors.AlgReals-import Data.SBV.BitVectors.Data (nan, infinity)+import Data.SBV.BitVectors.Data (nan, infinity, RoundingMode(..)) +-- Needed for conversion from SMTLib triple-IEEE formats to float/double+import qualified Foreign as F+import qualified System.IO.Unsafe as U (unsafePerformIO) -- Only used safely!+ -- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib data SExpr = ECon String- | ENum Integer+ | ENum (Integer, Maybe Int) -- Second argument is how wide the field was in bits, if known. Useful in FP parsing. | EReal AlgReal | EFloat Float | EDouble Double@@ -55,44 +62,57 @@ parseApp r (f : sofar) parseApp (tok:toks) sofar = do t <- pTok tok parseApp toks (t : sofar)- pTok "false" = return $ ENum 0- pTok "true" = return $ ENum 1- pTok ('0':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r- pTok ('b':'v':r) = mkNum $ readDec (takeWhile (/= '[') r)- pTok ('#':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r- pTok ('#':'x':r) = mkNum $ readHex r+ pTok "false" = return $ ENum (0, Nothing)+ pTok "true" = return $ ENum (1, Nothing)+ pTok ('0':'b':r) = mkNum (Just (length r)) $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+ pTok ('b':'v':r) = mkNum Nothing $ readDec (takeWhile (/= '[') r)+ pTok ('#':'b':r) = mkNum (Just (length r)) $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+ pTok ('#':'x':r) = mkNum (Just (4 * length r)) $ readHex r pTok n | not (null n) && isDigit (head n) = if '.' `elem` n then getReal n- else mkNum $ readDec n- pTok n = return $ ECon n- mkNum [(n, "")] = return $ ENum n- mkNum _ = die "cannot read number"+ else mkNum Nothing $ readDec n+ pTok n = return $ ECon (constantMap n)+ mkNum l [(n, "")] = return $ ENum (n, l)+ mkNum _ _ = die "cannot read number" getReal n = return $ EReal $ mkPolyReal (Left (exact, n')) where exact = not ("?" `isPrefixOf` reverse n) n' | exact = n | True = init n -- simplify numbers and root-obj values cvt (EApp [ECon "/", EReal a, EReal b]) = return $ EReal (a / b)- cvt (EApp [ECon "/", EReal a, ENum b]) = return $ EReal (a / fromInteger b)- cvt (EApp [ECon "/", ENum a, EReal b]) = return $ EReal (fromInteger a / b)- cvt (EApp [ECon "/", ENum a, ENum b]) = return $ EReal (fromInteger a / fromInteger b)+ cvt (EApp [ECon "/", EReal a, ENum b]) = return $ EReal (a / fromInteger (fst b))+ cvt (EApp [ECon "/", ENum a, EReal b]) = return $ EReal (fromInteger (fst a) / b )+ cvt (EApp [ECon "/", ENum a, ENum b]) = return $ EReal (fromInteger (fst a) / fromInteger (fst b)) cvt (EApp [ECon "-", EReal a]) = return $ EReal (-a)- cvt (EApp [ECon "-", ENum a]) = return $ ENum (-a)+ cvt (EApp [ECon "-", ENum a]) = return $ ENum (-(fst a), snd a) -- bit-vector value as CVC4 prints: (_ bv0 16) for instance cvt (EApp [ECon "_", ENum a, ENum _b]) = return $ ENum a cvt (EApp [ECon "root-obj", EApp (ECon "+":trms), ENum k]) = do ts <- mapM getCoeff trms- return $ EReal $ mkPolyReal (Right (k, ts))- cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum 11, ENum 53]]) = getDouble n- cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum 8, ENum 24]]) = getFloat n- cvt (EApp [ECon "as", n, ECon "Float64"]) = getDouble n- cvt (EApp [ECon "as", n, ECon "Float32"]) = getFloat n- cvt x = return x- getCoeff (EApp [ECon "*", ENum k, EApp [ECon "^", ECon "x", ENum p]]) = return (k, p) -- kx^p- getCoeff (EApp [ECon "*", ENum k, ECon "x" ] ) = return (k, 1) -- kx- getCoeff ( EApp [ECon "^", ECon "x", ENum p] ) = return (1, p) -- x^p- getCoeff ( ECon "x" ) = return (1, 1) -- x- getCoeff ( ENum k ) = return (k, 0) -- k+ return $ EReal $ mkPolyReal (Right (fst k, ts))+ cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum (11, _), ENum (53, _)]]) = getDouble n+ cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FloatingPoint", ENum ( 8, _), ENum (24, _)]]) = getFloat n+ cvt (EApp [ECon "as", n, ECon "Float64"]) = getDouble n+ cvt (EApp [ECon "as", n, ECon "Float32"]) = getFloat n+ -- NB. Note the lengths on the mantissa for the following two are 23/52; not 24/53!+ cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 8), ENum (m, Just 23)]) = return $ EFloat $ getTripleFloat s e m+ cvt (EApp [ECon "fp", ENum (s, Just 1), ENum ( e, Just 11), ENum (m, Just 52)]) = return $ EDouble $ getTripleDouble s e m+ cvt (EApp [ECon "_", ECon "NaN", ENum ( 8, _), ENum (24, _)]) = return $ EFloat nan+ cvt (EApp [ECon "_", ECon "NaN", ENum (11, _), ENum (53, _)]) = return $ EDouble nan+ cvt (EApp [ECon "_", ECon "+oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat infinity+ cvt (EApp [ECon "_", ECon "+oo", ENum (11, _), ENum (53, _)]) = return $ EDouble infinity+ cvt (EApp [ECon "_", ECon "-oo", ENum ( 8, _), ENum (24, _)]) = return $ EFloat (-infinity)+ cvt (EApp [ECon "_", ECon "-oo", ENum (11, _), ENum (53, _)]) = return $ EDouble (-infinity)+ cvt (EApp [ECon "_", ECon "+zero", ENum ( 8, _), ENum (24, _)]) = return $ EFloat 0+ cvt (EApp [ECon "_", ECon "+zero", ENum (11, _), ENum (53, _)]) = return $ EDouble 0+ cvt (EApp [ECon "_", ECon "-zero", ENum ( 8, _), ENum (24, _)]) = return $ EFloat (-0)+ cvt (EApp [ECon "_", ECon "-zero", ENum (11, _), ENum (53, _)]) = return $ EDouble (-0)+ cvt x = return x+ getCoeff (EApp [ECon "*", ENum k, EApp [ECon "^", ECon "x", ENum p]]) = return (fst k, fst p) -- kx^p+ getCoeff (EApp [ECon "*", ENum k, ECon "x" ] ) = return (fst k, 1) -- kx+ getCoeff ( EApp [ECon "^", ECon "x", ENum p] ) = return ( 1, fst p) -- x^p+ getCoeff ( ECon "x" ) = return ( 1, 1) -- x+ getCoeff ( ENum k ) = return (fst k, 0) -- k getCoeff x = die $ "Cannot parse a root-obj,\nProcessing term: " ++ show x getDouble (ECon s) = case (s, rdFP (dropWhile (== '+') s)) of ("plusInfinity", _ ) -> return $ EDouble infinity@@ -131,3 +151,32 @@ where rd v = case reads v of [(n, "")] -> Just n _ -> Nothing++-- | Convert an (s, e, m) triple to a float value+getTripleFloat :: Integer -> Integer -> Integer -> Float+getTripleFloat s e m = U.unsafePerformIO $ F.alloca $ \buf -> do {F.poke (F.castPtr buf) w32; F.peek buf}+ where sign = [s == 1]+ expt = [e `testBit` i | i <- [ 7, 6 .. 0]]+ mantissa = [m `testBit` i | i <- [22, 21 .. 0]]+ positions = [i | (i, b) <- zip [31, 30 .. 0] (sign ++ expt ++ mantissa), b]+ w32 = foldr (flip setBit) (0::Word32) positions++-- | Convert an (s, e, m) triple to a float value+getTripleDouble :: Integer -> Integer -> Integer -> Double+getTripleDouble s e m = U.unsafePerformIO $ F.alloca $ \buf -> do {F.poke (F.castPtr buf) w64; F.peek buf}+ where sign = [s == 1]+ expt = [e `testBit` i | i <- [10, 9 .. 0]]+ mantissa = [m `testBit` i | i <- [51, 50 .. 0]]+ positions = [i | (i, b) <- zip [63, 62 .. 0] (sign ++ expt ++ mantissa), b]+ w64 = foldr (flip setBit) (0::Word64) positions++-- | Special constants of SMTLib2 and their internal translation. Mainly+-- rounding modes for now.+constantMap :: String -> String+constantMap n = fromMaybe n (listToMaybe [to | (from, to) <- special, n `elem` from])+ where special = [ (["RNE", "roundNearestTiesToEven"], show RoundNearestTiesToEven)+ , (["RNA", "roundNearestTiesToAway"], show RoundNearestTiesToAway)+ , (["RTP", "roundTowardPositive"], show RoundTowardPositive)+ , (["RTN", "roundTowardNegative"], show RoundTowardNegative)+ , (["RTZ", "roundTowardZero"], show RoundTowardZero)+ ]
Data/SBV/Provers/Yices.hs view
@@ -92,8 +92,8 @@ matches -> error $ "SBV.Yices: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing- extract (EApp [ECon "=", ECon v, ENum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]- extract (EApp [ECon "=", ENum i, ECon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))]+ extract (EApp [ECon "=", ECon v, ENum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) (fst i)))]+ extract (EApp [ECon "=", ENum i, ECon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) (fst i)))] extract _ = [] extractUnints :: [(String, UnintKind)] -> [String] -> [(UnintKind, [String])]@@ -124,20 +124,20 @@ = getDefaultVal knd (dropWhile (/= ' ') s) | True = case parseSExpr s of- Right (EApp [ECon "=", EApp (ECon _ : args), ENum i]) -> getCallVal knd args i- Right (EApp [ECon "=", ECon _, ENum i]) -> getCallVal knd [] i+ Right (EApp [ECon "=", EApp (ECon _ : args), ENum i]) -> getCallVal knd args (fst i)+ Right (EApp [ECon "=", ECon _, ENum i]) -> getCallVal knd [] (fst i) _ -> Nothing getDefaultVal :: UnintKind -> String -> Maybe (String, [String], String) getDefaultVal knd n = case parseSExpr n of- Right (ENum i) -> Just $ showDefault knd (show i)- _ -> Nothing+ Right (ENum i) -> Just $ showDefault knd (show (fst i))+ _ -> Nothing getCallVal :: UnintKind -> [SExpr] -> Integer -> Maybe (String, [String], String) getCallVal knd args res = mapM getArg args >>= \as -> return (showCall knd as (show res)) getArg :: SExpr -> Maybe String-getArg (ENum i) = Just (show i)+getArg (ENum i) = Just (show (fst i)) getArg _ = Nothing showDefault :: UnintKind -> String -> (String, [String], String)
Data/SBV/Provers/Z3.hs view
@@ -71,16 +71,6 @@ } where cleanErrs = intercalate "\n" . filter (not . junk) . lines junk = ("WARNING:" `isPrefixOf`)- zero :: RoundingMode -> Kind -> String- zero _ KBool = "false"- zero _ (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0'- zero _ KUnbounded = "0"- zero _ KReal = "0.0"- zero rm KFloat = showSMTFloat rm 0- zero rm KDouble = showSMTDouble rm 0- -- For uninterpreted sorts, we use the first element of the enumerations if available; otherwise bail out..- zero _ (KUserSort _ (Right (f:_), _)) = f- zero _ (KUserSort s _) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s cont rm skolemMap = intercalate "\n" $ concatMap extract skolemMap where -- In the skolemMap: -- * Left's are universals: i.e., the model should be true for@@ -88,9 +78,9 @@ -- * 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 rm (kindOf s) ++ "))\")"]+ extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ mkSkolemZero rm (kindOf s) ++ "))\")"] extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g- extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero rm (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g+ extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : mkSkolemZero rm (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] addTimeOut Nothing o = o
Data/SBV/SMT/SMT.hs view
@@ -194,6 +194,9 @@ parseCWs (cw : r) = Just (cw, r) parseCWs [] = Nothing +-- | A rounding mode, extracted from a model. (Default definition suffices)+instance SatModel RoundingMode+ -- | A list of values as extracted from a model. When reading a list, we -- go as long as we can (maximal-munch). Note that this never fails, as -- we can always return the empty list!
Data/SBV/SMT/SMTLib.hs view
@@ -109,7 +109,7 @@ isInput _ = Nothing getUIIndex (KUserSort _ (Right xs, _)) i = i `lookup` zip xs [0..] getUIIndex _ _ = Nothing- extract (EApp [EApp [v, ENum i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) i))]+ extract (EApp [EApp [v, ENum i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) (fst i)))] extract (EApp [EApp [v, EReal i]]) | Just (n, s, nm) <- getInput v, isReal s = [(n, (nm, CW KReal (CWAlgReal i)))] extract (EApp [EApp [v, ECon i]]) | Just (n, s, nm) <- getInput v, isUninterpreted s = let k = kindOf s in [(n, (nm, CW k (CWUserSort (getUIIndex k i, i))))] extract (EApp [EApp [v, EDouble i]]) | Just (n, s, nm) <- getInput v, isDouble s = [(n, (nm, CW KDouble (CWDouble i)))]
Data/SBV/SMT/SMTLib1.hs view
@@ -189,6 +189,7 @@ cvtExp (SBVApp (Ror i) [a]) = rot "rotate_right" i a cvtExp (SBVApp (Shl i) [a]) = shft "bvshl" "bvshl" i a cvtExp (SBVApp (Shr i) [a]) = shft "bvlshr" "bvashr" i a+cvtExp (SBVApp (FPRound w) _) = die $ "cvtExp: SMTLib1 backend does not support floating point operations with rounding modes: (" ++ w ++ ")" cvtExp (SBVApp (LkUp (t, ak, _, l) i e) []) | needsCheck = "(ite " ++ cond ++ show e ++ " " ++ lkUp ++ ")" | True = lkUp
Data/SBV/SMT/SMTLib2.hs view
@@ -13,19 +13,17 @@ module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where import Data.Bits (bit)-import Data.Char (intToDigit) import Data.Function (on) import Data.Ord (comparing)+import Data.List (intercalate, partition, groupBy, sortBy)+ import qualified Data.Foldable as F (toList) import qualified Data.Map as M import qualified Data.IntMap as IM import qualified Data.Set as Set-import Data.List (intercalate, partition, groupBy, sortBy)-import Numeric (showIntAtBase, showHex) -import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data-import Data.SBV.BitVectors.PrettyNum (showSMTFloat, showSMTDouble, smtRoundingMode)+import Data.SBV.BitVectors.PrettyNum (smtRoundingMode, cwToSMTLib) -- | Add constraints to generate /new/ models. This function is used to query the SMT-solver, while -- disallowing a previous model.@@ -51,7 +49,7 @@ nonEqs :: RoundingMode -> [(String, CW)] -> [String] nonEqs rm scs = format $ interp ps ++ disallow (map eqClass uninterpClasses) where isFree (KUserSort _ (Left _, _)) = True- isFree _ = False+ isFree _ = False (ups, ps) = partition (isFree . kindOf . snd) scs format [] = [] format [m] = ["(assert " ++ m ++ ")"]@@ -80,7 +78,7 @@ tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e -- | Translate a problem into an SMTLib2 script-cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic+cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic -> Maybe Logic -- ^ SMT-Lib logic, if requested by the user -> SolverCapabilities -- ^ capabilities of the current solver -> Set.Set Kind -- ^ kinds used@@ -110,8 +108,8 @@ = ["(set-logic " ++ show l ++ ") ; NB. User specified."] | hasDouble || hasFloat -- NB. We don't check for quantifiers here, we probably should.. = if hasBVs- then ["(set-logic QF_FPABV)"]- else ["(set-logic QF_FPA)"]+ then ["(set-logic QF_FPBV)"]+ else ["(set-logic QF_FP)"] | hasInteger || hasReal || not (null usorts) = case mbDefaultLogic solverCaps of Nothing -> ["; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified."] -- combination, let the solver pick@@ -192,6 +190,10 @@ userName s = case s `lookup` map snd inputs of Just u | show s /= u -> " ; tracks user variable " ++ show u _ -> ""+ -- following sorts are built-in; do not translate them:+ builtInSort = (`elem` ["RoundingMode"])+ declSort (s, _)+ | builtInSort s = [] declSort (s, (Left r, _)) = ["(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted: " ++ r] declSort (s, (Right fs, _)) = [ "(declare-datatypes () ((" ++ s ++ " " ++ unwords (map (\c -> "(" ++ c ++ ")") fs) ++ ")))" , "(define-fun " ++ s ++ "_constrIndex ((x " ++ s ++ ")) Int"@@ -296,42 +298,8 @@ | True = show s --- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time--- being, SBV only supports sizes that are multiples of 4, but the below code is more robust--- in case of future extensions to support arbitrary sizes.-hex :: Int -> Integer -> String-hex 1 v = "#b" ++ show v-hex sz v- | sz `mod` 4 == 0 = "#x" ++ pad (sz `div` 4) (showHex v "")- | True = "#b" ++ pad sz (showBin v "")- where pad n s = replicate (n - length s) '0' ++ s- showBin = showIntAtBase 2 intToDigit- cvtCW :: RoundingMode -> CW -> String-cvtCW rm x- | isBoolean x, CWInteger w <- cwVal x = if w == 0 then "false" else "true"- | isUninterpreted x, CWUserSort (_, s) <- cwVal x = s- | isReal x, CWAlgReal r <- cwVal x = algRealToSMTLib2 r- | isFloat x, CWFloat f <- cwVal x = showSMTFloat rm f- | isDouble x, CWDouble d <- cwVal x = showSMTDouble rm d- | not (isBounded x), CWInteger w <- cwVal x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")"- | not (hasSign x) , CWInteger w <- cwVal x = hex (intSizeOf x) w- -- signed numbers (with 2's complement representation) is problematic- -- since there's no way to put a bvneg over a positive number to get minBound..- -- Hence, we punt and use binary notation in that particular case- | hasSign x , CWInteger w <- cwVal x = if w == negate (2 ^ intSizeOf x)- then mkMinBound (intSizeOf x)- else negIf (w < 0) $ hex (intSizeOf x) (abs w)- | True = error $ "SBV.cvtCW: Impossible happened: Kind/Value disagreement on: " ++ show (kindOf x, x)--negIf :: Bool -> String -> String-negIf True a = "(bvneg " ++ a ++ ")"-negIf False a = a---- anamoly at the 2's complement min value! Have to use binary notation here--- as there is no positive value we can provide to make the bvneg work.. (see above)-mkMinBound :: Int -> String-mkMinBound i = "#b1" ++ replicate (i-1) '0'+cvtCW = cwToSMTLib getTable :: TableMap -> Int -> String getTable m i@@ -427,7 +395,7 @@ sh (SBVApp (Uninterpreted nm) []) = nm sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm' ++ " " ++ unwords (map ssw args) ++ ")" where -- slight hack needed here to take advantage of custom floating-point functions.. sigh.- fpSpecials = ["fp.sqrt", "fusedMA"]+ fpSpecials = ["fp.sqrt", "fp.fma"] nm' | (floatOp || doubleOp) && (nm `elem` fpSpecials) = addRM nm | True = nm sh (SBVApp (Extract 0 0) [a]) -- special SInteger -> SReal conversion@@ -464,6 +432,8 @@ , (Not, lift1B "not" "bvnot") , (Join, lift2 "concat") ]+ sh (SBVApp (FPRound w) args)+ = "(" ++ w ++ " " ++ unwords (map ssw args) ++ ")" sh inp@(SBVApp op args) | intOp, Just f <- lookup op smtOpIntTable = f True (map ssw args)
Data/SBV/Tools/Polynomial.hs view
@@ -15,7 +15,7 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeSynonymInstances #-} -module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV) where+module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV, ites, mdp, addPoly) where import Data.Bits (Bits(..)) import Data.List (genericTake)@@ -118,13 +118,17 @@ addPoly [] ys = ys addPoly (x:xs) (y:ys) = x <+> y : addPoly xs ys +-- | Run down a boolean condition over two lists. Note that this is+-- different than zipWith as shorter list is assumed to be filled with+-- false at the end (i.e., zero-bits); which nicely pads it when+-- considered as an unsigned number in little-endian form. ites :: SBool -> [SBool] -> [SBool] -> [SBool] ites s xs ys | Just t <- unliteral s = if t then xs else ys | True = go xs ys- where go [] [] = []+ where go [] [] = [] go [] (b:bs) = ite s false b : go [] bs go (a:as) [] = ite s a false : go as [] go (a:as) (b:bs) = ite s a b : go as bs@@ -168,6 +172,7 @@ | True = n -- over-estimate +-- | Compute modulus/remainder of polynomials on bit-vectors. mdp :: [SBool] -> [SBool] -> ([SBool], [SBool]) mdp xs ys = go (length ys - 1) (reverse ys) where degTop = degree xs
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Thu Jan 22 19:53:39 PST 2015"+buildTime = "Fri Mar 6 17:06:57 PST 2015"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 4.0+Version: 4.1 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@@ -55,6 +55,7 @@ , Data.SBV.Bridge.MathSAT , Data.SBV.Bridge.Yices , Data.SBV.Bridge.Z3+ , Data.SBV.Bridge.ABC , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks , Data.SBV.Examples.BitPrecise.Legato@@ -94,6 +95,7 @@ , Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Model , Data.SBV.BitVectors.PrettyNum+ , Data.SBV.BitVectors.Rounding , Data.SBV.BitVectors.SignCast , Data.SBV.BitVectors.Splittable , Data.SBV.BitVectors.STree@@ -110,6 +112,7 @@ , Data.SBV.Provers.Yices , Data.SBV.Provers.Z3 , Data.SBV.Provers.MathSAT+ , Data.SBV.Provers.ABC , Data.SBV.Tools.ExpectedValue , Data.SBV.Tools.GenTest , Data.SBV.Tools.Optimize