diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,25 @@ * Hackage: * GitHub: -* Latest Hackage released version: 5.5, 2015-11-10 +* Latest Hackage released version: 5.6, 2015-12-06 + +### Version 5.6, 2015-12-06 + + * Minor changes to how we print models: + * Align by the type + * Always print the type (previously we were skipping for Bool) + + * Rework how SBV properties are quick-checked; much more usable and robust + + * Provide a function sbvQuickCheck, which is essentially the same as + quickCheck, except it also returns a boolean. Useful for the + programmable API. (The dynamic version is called svQuickCheck) + + * Several changes/additions in support of the sbvPlugin development: + * Data.SBV.Dynamic: Define/export svFloat/svDouble/sReal/sNumerator/sDenominator + * Data.SBV.Internals: Export constructors of Result, SMTModel, + and the function showModel + * Simplify how Uninterpreted-types are internally represented. ### Version 5.5, 2015-11-10 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -213,6 +213,8 @@ , constrain, pConstrain -- ** Checking constraint vacuity , isVacuous, isVacuousWith + -- ** Quick-checking + , sbvQuickCheck -- * Proving properties using multiple solvers -- $multiIntro diff --git a/Data/SBV/BitVectors/Concrete.hs b/Data/SBV/BitVectors/Concrete.hs --- a/Data/SBV/BitVectors/Concrete.hs +++ b/Data/SBV/BitVectors/Concrete.hs @@ -72,20 +72,18 @@ -- | 'CW' represents a concrete word of a fixed size: -- Endianness is mostly irrelevant (see the 'FromBits' class). -- For signed words, the most significant digit is considered to be the sign. -data CW = CW { cwKind :: !Kind +data CW = CW { _cwKind :: !Kind , cwVal :: !CWVal } deriving (Eq, Ord) +-- | 'Kind' instance for CW +instance HasKind CW where + kindOf (CW k _) = k + -- | Are two CW's of the same type? cwSameType :: CW -> CW -> Bool -cwSameType x y = cwKind x == cwKind y - --- | Is this a bit? -cwIsBit :: CW -> Bool -cwIsBit x = case cwKind x of - KBool -> True - _ -> False +cwSameType x y = kindOf x == kindOf y -- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded) cwToBool :: CW -> Bool @@ -134,7 +132,7 @@ -- | Map a unary function through a CW. mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -mapCW r i f d u x = normCW $ CW (cwKind x) $ case cwVal x of +mapCW r i f d u x = normCW $ CW (kindOf x) $ case cwVal x of CWAlgReal a -> CWAlgReal (r a) CWInteger a -> CWInteger (i a) CWFloat a -> CWFloat (f a) @@ -144,23 +142,22 @@ -- | Map a binary function through a CW. mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW mapCW2 r i f d u x y = case (cwSameType x y, cwVal x, cwVal y) of - (True, CWAlgReal a, CWAlgReal b) -> normCW $ CW (cwKind x) (CWAlgReal (r a b)) - (True, CWInteger a, CWInteger b) -> normCW $ CW (cwKind x) (CWInteger (i a b)) - (True, CWFloat a, CWFloat b) -> normCW $ CW (cwKind x) (CWFloat (f a b)) - (True, CWDouble a, CWDouble b) -> normCW $ CW (cwKind x) (CWDouble (d a b)) - (True, CWUserSort a, CWUserSort b) -> normCW $ CW (cwKind x) (CWUserSort (u a b)) + (True, CWAlgReal a, CWAlgReal b) -> normCW $ CW (kindOf x) (CWAlgReal (r a b)) + (True, CWInteger a, CWInteger b) -> normCW $ CW (kindOf x) (CWInteger (i a b)) + (True, CWFloat a, CWFloat b) -> normCW $ CW (kindOf x) (CWFloat (f a b)) + (True, CWDouble a, CWDouble b) -> normCW $ CW (kindOf x) (CWDouble (d a b)) + (True, CWUserSort a, CWUserSort b) -> normCW $ CW (kindOf x) (CWUserSort (u a b)) _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) -- | Show instance for 'CW'. instance Show CW where show = showCW True --- | Show a CW, with kind info if bool is True. Note that bits never get their type printed --- as it is more or less useless. (i.e., No need to say SBool for True and False) +-- | Show a CW, with kind info if bool is True showCW :: Bool -> CW -> String -showCW _ w | cwIsBit w = show (cwToBool w) -showCW shk w = liftCW show show show show snd w ++ kInfo - where kInfo | shk = " :: " ++ shKind (cwKind w) +showCW shk w | isBoolean w = show (cwToBool w) ++ (if shk then " :: Bool" else "") +showCW shk w = liftCW show show show show snd w ++ kInfo + where kInfo | shk = " :: " ++ shKind (kindOf w) | True = "" shKind k@(KUserSort {}) = show k shKind k | ('S':sk) <- show k = sk diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -25,7 +25,7 @@ , sRoundNearestTiesToEven, sRoundNearestTiesToAway, sRoundTowardPositive, sRoundTowardNegative, sRoundTowardZero , sRNE, sRNA, sRTP, sRTN, sRTZ , SymWord(..) - , CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool + , CW(..), CWVal(..), AlgReal(..), cwSameType, cwToBool , mkConstCW ,liftCW2, mapCW, mapCW2 , SW(..), trueSW, falseSW, trueCW, falseCW, normCW , SVal(..) @@ -41,7 +41,7 @@ , addConstraint, internalVariable, internalConstraint, isCodeGenMode , SBVType(..), newUninterpreted, addAxiom , Quantifier(..), needsExistentials - , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension + , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension, smtLibReservedNames , SolverCapabilities(..) , extractSymbolicSimulationState , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), getSBranchRunConfig @@ -66,79 +66,11 @@ import Data.SBV.BitVectors.Kind import Data.SBV.BitVectors.Concrete import Data.SBV.BitVectors.Symbolic +import Data.SBV.SMT.SMTLibNames import Prelude () import Prelude.Compat --- | A class for capturing values that have a sign and a size (finite or infinite) --- minimal complete definition: kindOf. This class can be automatically derived --- for data-types that have a 'Data' instance; this is useful for creating uninterpreted --- sorts. -class HasKind a where - kindOf :: a -> Kind - hasSign :: a -> Bool - intSizeOf :: a -> Int - isBoolean :: a -> Bool - isBounded :: a -> Bool -- NB. This really means word/int; i.e., Real/Float will test False - isReal :: a -> Bool - isFloat :: a -> Bool - isDouble :: a -> Bool - isInteger :: a -> Bool - isUninterpreted :: a -> Bool - showType :: a -> String - -- defaults - hasSign x = kindHasSign (kindOf x) - intSizeOf x = case kindOf x of - KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" - KBounded _ s -> s - KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" - KReal -> error "SBV.HasKind.intSizeOf((S)Real)" - KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" - KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" - KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s - isBoolean x | KBool{} <- kindOf x = True - | True = False - isBounded x | KBounded{} <- kindOf x = True - | True = False - isReal x | KReal{} <- kindOf x = True - | True = False - isFloat x | KFloat{} <- kindOf x = True - | True = False - isDouble x | KDouble{} <- kindOf x = True - | True = False - isInteger x | KUnbounded{} <- kindOf x = True - | True = False - isUninterpreted x | KUserSort{} <- kindOf x = True - | True = False - showType = show . kindOf - - -- default signature for uninterpreted/enumerated kinds - default kindOf :: (Read a, G.Data a) => a -> Kind - kindOf = constructUKind - -instance HasKind Bool where kindOf _ = KBool -instance HasKind Int8 where kindOf _ = KBounded True 8 -instance HasKind Word8 where kindOf _ = KBounded False 8 -instance HasKind Int16 where kindOf _ = KBounded True 16 -instance HasKind Word16 where kindOf _ = KBounded False 16 -instance HasKind Int32 where kindOf _ = KBounded True 32 -instance HasKind Word32 where kindOf _ = KBounded False 32 -instance HasKind Int64 where kindOf _ = KBounded True 64 -instance HasKind Word64 where kindOf _ = KBounded False 64 -instance HasKind Integer where kindOf _ = KUnbounded -instance HasKind AlgReal where kindOf _ = KReal -instance HasKind Float where kindOf _ = KFloat -instance HasKind Double where kindOf _ = KDouble - -instance HasKind Kind where - kindOf = id - -instance HasKind CW where - kindOf = cwKind - -instance HasKind SW where - kindOf (SW k _) = k - -- | Get the current path condition getPathCondition :: State -> SBool getPathCondition st = SBV (getSValPathCondition st) @@ -213,9 +145,6 @@ -- | 'RoundingMode' can be used symbolically instance SymWord RoundingMode --- | 'RoundingMode' kind -instance HasKind RoundingMode - -- | The symbolic variant of 'RoundingMode' type SRoundingMode = SBV RoundingMode @@ -397,8 +326,8 @@ | True = False default literal :: Show a => a -> SBV a - literal x = let k@(KUserSort _ (conts, _)) = kindOf x - sx = show x + literal x = let k@(KUserSort _ conts) = kindOf x + sx = show x mbIdx = case conts of Right xs -> sx `elemIndex` xs _ -> Nothing diff --git a/Data/SBV/BitVectors/Kind.hs b/Data/SBV/BitVectors/Kind.hs --- a/Data/SBV/BitVectors/Kind.hs +++ b/Data/SBV/BitVectors/Kind.hs @@ -9,29 +9,45 @@ -- Internal data-structures for the sbv library ----------------------------------------------------------------------------- +{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.SBV.BitVectors.Kind - ( Kind(..) - , kindHasSign - , constructUKind - ) where +module Data.SBV.BitVectors.Kind (Kind(..), HasKind(..), constructUKind) where import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields) -import Data.SBV.BitVectors.AlgReals () -- instances only +import Data.Int +import Data.Word +import Data.SBV.BitVectors.AlgReals -- | Kind of symbolic value data Kind = KBool | KBounded Bool Int | KUnbounded | KReal - | KUserSort String (Either String [String], G.DataType) + | KUserSort String (Either String [String]) | KFloat | KDouble - deriving (Eq, Ord) +-- | Helper for Eq/Ord instances below +kindRank :: Kind -> Either Int (Either (Bool, Int) String) +kindRank KBool = Left 0 +kindRank (KBounded b i) = Right (Left (b, i)) +kindRank KUnbounded = Left 1 +kindRank KReal = Left 2 +kindRank (KUserSort s _) = Right (Right s) +kindRank KFloat = Left 3 +kindRank KDouble = Left 4 + +-- | We want to equate user-sorts only by name +instance Eq Kind where + k1 == k2 = kindRank k1 == kindRank k2 + +-- | We want to order user-sorts only by name +instance Ord Kind where + k1 `compare` k2 = kindRank k1 `compare` kindRank k2 + instance Show Kind where show KBool = "SBool" show (KBounded False n) = "SWord" ++ show n @@ -63,7 +79,7 @@ -- | Construct an uninterpreted/enumerated kind from a piece of data; we distinguish simple enumerations as those -- are mapped to proper SMT-Lib2 data-types; while others go completely uninterpreted constructUKind :: forall a. (Read a, G.Data a) => a -> Kind -constructUKind a = KUserSort sortName (mbEnumFields, dataType) +constructUKind a = KUserSort sortName mbEnumFields where dataType = G.dataTypeOf a sortName = G.tyconUQname . G.dataTypeName $ dataType constrs = G.dataTypeConstrs dataType @@ -78,3 +94,66 @@ checkConstr c = case (reads (show c) :: [(a, String)]) of ((_, "") : _) -> Nothing _ -> Just "not a nullary constructor" + +-- | A class for capturing values that have a sign and a size (finite or infinite) +-- minimal complete definition: kindOf. This class can be automatically derived +-- for data-types that have a 'Data' instance; this is useful for creating uninterpreted +-- sorts. +class HasKind a where + kindOf :: a -> Kind + hasSign :: a -> Bool + intSizeOf :: a -> Int + isBoolean :: a -> Bool + isBounded :: a -> Bool -- NB. This really means word/int; i.e., Real/Float will test False + isReal :: a -> Bool + isFloat :: a -> Bool + isDouble :: a -> Bool + isInteger :: a -> Bool + isUninterpreted :: a -> Bool + showType :: a -> String + -- defaults + hasSign x = kindHasSign (kindOf x) + intSizeOf x = case kindOf x of + KBool -> error "SBV.HasKind.intSizeOf((S)Bool)" + KBounded _ s -> s + KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" + KReal -> error "SBV.HasKind.intSizeOf((S)Real)" + KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" + KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" + KUserSort s _ -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s + isBoolean x | KBool{} <- kindOf x = True + | True = False + isBounded x | KBounded{} <- kindOf x = True + | True = False + isReal x | KReal{} <- kindOf x = True + | True = False + isFloat x | KFloat{} <- kindOf x = True + | True = False + isDouble x | KDouble{} <- kindOf x = True + | True = False + isInteger x | KUnbounded{} <- kindOf x = True + | True = False + isUninterpreted x | KUserSort{} <- kindOf x = True + | True = False + showType = show . kindOf + + -- default signature for uninterpreted/enumerated kinds + default kindOf :: (Read a, G.Data a) => a -> Kind + kindOf = constructUKind + +instance HasKind Bool where kindOf _ = KBool +instance HasKind Int8 where kindOf _ = KBounded True 8 +instance HasKind Word8 where kindOf _ = KBounded False 8 +instance HasKind Int16 where kindOf _ = KBounded True 16 +instance HasKind Word16 where kindOf _ = KBounded False 16 +instance HasKind Int32 where kindOf _ = KBounded True 32 +instance HasKind Word32 where kindOf _ = KBounded False 32 +instance HasKind Int64 where kindOf _ = KBounded True 64 +instance HasKind Word64 where kindOf _ = KBounded False 64 +instance HasKind Integer where kindOf _ = KUnbounded +instance HasKind AlgReal where kindOf _ = KReal +instance HasKind Float where kindOf _ = KFloat +instance HasKind Double where kindOf _ = KDouble + +instance HasKind Kind where + kindOf = id 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 @@ -33,10 +33,11 @@ , liftQRem, liftDMod, symbolicMergeWithKind , genLiteral, genFromCW, genMkSymVar , isSatisfiableInCurrentPath + , sbvQuickCheck ) where -import Control.Monad (when, liftM) +import Control.Monad (when, unless, liftM) import Control.Monad.Reader (ask) import Control.Monad.Trans (liftIO) @@ -49,9 +50,10 @@ import Data.Maybe (fromMaybe) import Data.Word (Word8, Word16, Word32, Word64) -import Test.QuickCheck (Testable(..), Arbitrary(..)) -import qualified Test.QuickCheck as QC (whenFail) -import qualified Test.QuickCheck.Monadic as QC (monadicIO, run) +import Test.QuickCheck (Testable(..), Arbitrary(..)) +import qualified Test.QuickCheck.Test as QC (isSuccess) +import qualified Test.QuickCheck as QC (quickCheckResult, counterexample) +import qualified Test.QuickCheck.Monadic as QC (monadicIO, run, assert, pre, monitor) import System.Random import Data.SBV.BitVectors.AlgReals @@ -59,7 +61,7 @@ import Data.SBV.Utils.Boolean import Data.SBV.Provers.Prover (isVacuous, prove, defaultSMTCfg, internalSATCheck) -import Data.SBV.SMT.SMT (ThmResult, SatResult(..)) +import Data.SBV.SMT.SMT (ThmResult, SatResult(..), showModel) import Data.SBV.BitVectors.Symbolic import Data.SBV.BitVectors.Operations @@ -1553,31 +1555,31 @@ property s = error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show s ++ ")" instance Testable (Symbolic SBool) where - property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test - where runOnce g = do (r, Result{resTraces=tvals, resConsts=cs, resConstraints=cstrs}) <- runSymbolic' (Concrete g) m - let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs) - cond = all (cwToBool . cval) cstrs - when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")" - if cond then if r `isConcretely` id - then return False - else do putStrLn $ complain tvals - return True - else runOnce g -- cstrs failed, go again - test = do die <- QC.run $ newStdGen >>= runOnce - when die $ fail "Falsifiable" - msg = "*** SBV: See the custom counter example reported above." - complain [] = "*** SBV Counter Example: Predicate contains no universally quantified variables." - complain qcInfo = intercalate "\n" $ "*** SBV Counter Example:" : map ((" " ++) . info) qcInfo - where maxLen = maximum (0:[length s | (s, _) <- qcInfo]) - shN s = s ++ replicate (maxLen - length s) ' ' - info (n, cw) = shN n ++ " = " ++ show cw + property prop = QC.monadicIO $ do (cond, r, tvals) <- QC.run (newStdGen >>= test) + QC.pre cond + unless (r || null tvals) $ QC.monitor (QC.counterexample (complain tvals)) + QC.assert r + where test g = do (r, Result{resTraces=tvals, resConsts=cs, resConstraints=cstrs, resUIConsts=unints}) <- runSymbolic' (Concrete g) prop + let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs) + cond = all (cwToBool . cval) cstrs + case map fst unints of + [] -> case unliteral r of + Nothing -> noQC [show r] + Just b -> return (cond, b, tvals) + us -> noQC us + complain qcInfo = showModel defaultSMTCfg (SMTModel qcInfo) + noQC us = error $ "Cannot quick-check in the presence of uninterpreted constants: " ++ intercalate ", " us +-- | Quick check an SBV property. Note that a regular 'quickCheck' call will work just as +-- well. Use this variant if you want to receive the boolean result. +sbvQuickCheck :: Symbolic SBool -> IO Bool +sbvQuickCheck prop = QC.isSuccess `fmap` QC.quickCheckResult prop + -- Quickcheck interface on dynamically-typed values. A run-time check -- ensures that the value has boolean type. instance Testable (Symbolic SVal) where property m = property $ do s <- m - when (svKind s /= KBool) $ - error "Cannot quickcheck non-boolean value" + when (kindOf s /= KBool) $ error "Cannot quickcheck non-boolean value" return (SBV s :: SBool) -- | Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms diff --git a/Data/SBV/BitVectors/Operations.hs b/Data/SBV/BitVectors/Operations.hs --- a/Data/SBV/BitVectors/Operations.hs +++ b/Data/SBV/BitVectors/Operations.hs @@ -13,9 +13,9 @@ ( -- ** Basic constructors svTrue, svFalse, svBool - , svInteger + , svInteger, svFloat, svDouble, svReal -- ** Basic destructors - , svAsBool, svAsInteger + , svAsBool, svAsInteger, svNumerator, svDenominator -- ** Basic operations , svPlus, svTimes, svMinus, svUNeg, svAbs , svDivide, svQuot, svRem @@ -43,6 +43,8 @@ import Data.SBV.BitVectors.Concrete import Data.SBV.BitVectors.Symbolic +import Data.Ratio + -------------------------------------------------------------------------------- -- Basic constructors @@ -62,8 +64,19 @@ svInteger :: Kind -> Integer -> SVal svInteger k n = SVal k (Left (mkConstCW k n)) --- TODO: svFloat, svDouble, svReal +-- | Convert from a Float +svFloat :: Float -> SVal +svFloat f = SVal KFloat (Left (CW KFloat (CWFloat f))) +-- | Convert from a Float +svDouble :: Double -> SVal +svDouble d = SVal KDouble (Left (CW KDouble (CWDouble d))) + +-- | Convert from a Rational +svReal :: Rational -> SVal +svReal d = SVal KReal (Left (CW KReal (CWAlgReal (fromRational d)))) + + -------------------------------------------------------------------------------- -- Basic destructors @@ -77,6 +90,16 @@ svAsInteger (SVal _ (Left (CW _ (CWInteger n)))) = Just n svAsInteger _ = Nothing +-- | Grab the numerator of an SReal, if available +svNumerator :: SVal -> Maybe Integer +svNumerator (SVal KReal (Left (CW KReal (CWAlgReal (AlgRational True r))))) = Just $ numerator r +svNumerator _ = Nothing + +-- | Grab the denominator of an SReal, if available +svDenominator :: SVal -> Maybe Integer +svDenominator (SVal KReal (Left (CW KReal (CWAlgReal (AlgRational True r))))) = Just $ denominator r +svDenominator _ = Nothing + -------------------------------------------------------------------------------- -- Basic operations @@ -129,7 +152,7 @@ | True = liftSym2 (mkSymOp Quot) nonzeroCheck (noReal "quot") quot' (noFloat "quot") (noDouble "quot") x y where - quot' a b | svKind x == KUnbounded = div a (abs b) * signum b + quot' a b | kindOf x == KUnbounded = div a (abs b) * signum b | otherwise = quot a b -- | Remainder: Overloaded operation whose meaning depends on the kind at which @@ -141,11 +164,11 @@ svRem :: SVal -> SVal -> SVal svRem x y | isConcreteZero x = x - | isConcreteOne y = svInteger (svKind x) 0 + | isConcreteOne y = svInteger (kindOf x) 0 | True = liftSym2 (mkSymOp Rem) nonzeroCheck (noReal "rem") rem' (noFloat "rem") (noDouble "rem") x y where - rem' a b | svKind x == KUnbounded = mod a (abs b) + rem' a b | kindOf x == KUnbounded = mod a (abs b) | otherwise = rem a b -- | Optimize away x == true and x /= false to x; otherwise just do eqOpt @@ -274,7 +297,7 @@ svRol x i | i < 0 = svRor x (-i) | i == 0 = x - | True = case svKind x of + | True = case kindOf x of KBounded _ sz -> liftSym1 (mkSymOp1 (Rol (i `mod` sz))) (noRealUnary "rotateL") (rot True sz i) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x @@ -285,7 +308,7 @@ svRor x i | i < 0 = svRol x (-i) | i == 0 = x - | True = case svKind x of + | True = case kindOf x of KBounded _ sz -> liftSym1 (mkSymOp1 (Ror (i `mod` sz))) (noRealUnary "rotateR") (rot False sz i) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x @@ -340,7 +363,7 @@ -- the proofs can be performed without any knowledge about the function itself. svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal svUninterpreted k nm code args = SVal k $ Right $ cache result - where result st = do let ty = SBVType (map svKind args ++ [k]) + where result st = do let ty = SBVType (map kindOf args ++ [k]) newUninterpreted st nm ty code sws <- mapM (svToSW st) args mapM_ forceSWArg sws @@ -348,7 +371,7 @@ -- | If-then-else. This one will force branches. svIte :: SVal -> SVal -> SVal -> SVal -svIte t a b = svSymbolicMerge (svKind a) True t a b +svIte t a b = svSymbolicMerge (kindOf a) True t a b -- | Lazy If-then-else. This one will delay forcing the branches unless it's really necessary. svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal @@ -443,11 +466,11 @@ CWInteger i -> if i < 0 || i >= genericLength xs then err else xs `genericIndex` i - _ -> error $ "SBV.select: unsupported " ++ show (svKind ind) ++ " valued select/index expression" + _ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression" svSelect xsOrig err ind = xs `seq` SVal kElt (Right (cache r)) where - kInd = svKind ind - kElt = svKind err + kInd = kindOf ind + kElt = kindOf err -- Based on the index size, we need to limit the elements. For -- instance if the index is 8 bits, but there are 257 elements, -- that last element will never be used and we can chop it off. @@ -473,9 +496,9 @@ | Just n <- svAsInteger x = svInteger k n | True = SVal k (Right (cache y)) where - k = KBounded s (svBitSize x) + k = KBounded s (intSizeOf x) y st = do xsw <- svToSW st x - newExpr st k (SBVApp (Extract (svBitSize x - 1) 0) [xsw]) + newExpr st k (SBVApp (Extract (intSizeOf x - 1) 0) [xsw]) -- | Convert a symbolic bitvector from unsigned to signed. svSign :: SVal -> SVal @@ -496,23 +519,23 @@ -- | Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool. svFromWord1 :: SVal -> SVal svFromWord1 x = svNotEqual x (svInteger k 0) - where k = svKind x + where k = kindOf x -- | Test the value of a bit. Note that we do an extract here -- as opposed to masking and checking against zero, as we found -- extraction to be much faster with large bit-vectors. svTestBit :: SVal -> Int -> SVal svTestBit x i - | i < svBitSize x = svFromWord1 (svExtract i i x) + | i < intSizeOf x = svFromWord1 (svExtract i i x) | True = svFalse -- | Generalization of 'svShl', where the shift-amount is symbolic. -- The shift amount must be an unsigned quantity. svShiftLeft :: SVal -> SVal -> SVal svShiftLeft x i - | svSigned i = error "sShiftLeft: shift amount should be unsigned" - | True = svSelect [svShl x k | k <- [0 .. svBitSize x - 1]] z i - where z = svInteger (svKind x) 0 + | hasSign i = error "sShiftLeft: shift amount should be unsigned" + | True = svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z i + where z = svInteger (kindOf x) 0 -- | Generalization of 'svShr', where the shift-amount is symbolic. -- The shift amount must be an unsigned quantity. @@ -521,33 +544,33 @@ -- otherwise it's logical. svShiftRight :: SVal -> SVal -> SVal svShiftRight x i - | svSigned i = error "sShiftRight: shift amount should be unsigned" - | True = svSelect [svShr x k | k <- [0 .. svBitSize x - 1]] z i - where z = svInteger (svKind x) 0 + | hasSign i = error "sShiftRight: shift amount should be unsigned" + | True = svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z i + where z = svInteger (kindOf x) 0 -- | Generalization of 'svRol', where the rotation amount is symbolic. -- The rotation amount must be an unsigned quantity. svRotateLeft :: SVal -> SVal -> SVal svRotateLeft x i - | svSigned i = error "sRotateLeft: rotation amount should be unsigned" + | hasSign i = error "sRotateLeft: rotation amount should be unsigned" | bit si <= toInteger sx = svSelect [x `svRol` k | k <- [0 .. bit si - 1]] z i -- wrap-around not possible | True = svSelect [x `svRol` k | k <- [0 .. sx - 1]] z (i `svRem` n) - where sx = svBitSize x - si = svBitSize i - z = svInteger (svKind x) 0 - n = svInteger (svKind i) (toInteger sx) + where sx = intSizeOf x + si = intSizeOf i + z = svInteger (kindOf x) 0 + n = svInteger (kindOf i) (toInteger sx) -- | Generalization of 'svRor', where the rotation amount is symbolic. -- The rotation amount must be an unsigned quantity. svRotateRight :: SVal -> SVal -> SVal svRotateRight x i - | svSigned i = error "sRotateRight: rotation amount should be unsigned" + | hasSign i = error "sRotateRight: rotation amount should be unsigned" | bit si <= toInteger sx = svSelect [x `svRor` k | k <- [0 .. bit si - 1]] z i -- wrap-around not possible | True = svSelect [x `svRor` k | k <- [0 .. sx - 1]] z (i `svRem` n) - where sx = svBitSize x - si = svBitSize i - z = svInteger (svKind x) 0 - n = svInteger (svKind i) (toInteger sx) + where sx = intSizeOf x + si = intSizeOf i + z = svInteger (kindOf x) 0 + n = svInteger (kindOf i) (toInteger sx) -------------------------------------------------------------------------------- diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs --- a/Data/SBV/BitVectors/PrettyNum.hs +++ b/Data/SBV/BitVectors/PrettyNum.hs @@ -67,16 +67,16 @@ {hexS = shexI True True; binS = sbinI True True; hex = shexI False False; bin = sbinI False False;} instance PrettyNum CW where - hexS cw | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) - | cwIsBit cw = hexS (cwToBool cw) + hexS cw | isUninterpreted cw = show cw ++ " :: " ++ show (kindOf cw) + | isBoolean cw = hexS (cwToBool cw) ++ " :: Bool" | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" | not (isBounded cw) = let CWInteger w = cwVal cw in shexI True True w | True = let CWInteger w = cwVal cw in shex True True (hasSign cw, intSizeOf cw) w - binS cw | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) - | cwIsBit cw = binS (cwToBool cw) + binS cw | isUninterpreted cw = show cw ++ " :: " ++ show (kindOf cw) + | isBoolean cw = binS (cwToBool cw) ++ " :: Bool" | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" @@ -84,7 +84,7 @@ | True = let CWInteger w = cwVal cw in sbin True True (hasSign cw, intSizeOf cw) w hex cw | isUninterpreted cw = show cw - | cwIsBit cw = hexS (cwToBool cw) + | isBoolean cw = hexS (cwToBool cw) ++ " :: Bool" | isFloat cw = let CWFloat f = cwVal cw in show f | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w @@ -92,7 +92,7 @@ | True = let CWInteger w = cwVal cw in shex False False (hasSign cw, intSizeOf cw) w bin cw | isUninterpreted cw = show cw - | cwIsBit cw = binS (cwToBool cw) + | isBoolean cw = binS (cwToBool cw) ++ " :: Bool" | isFloat cw = let CWFloat f = cwVal cw in show f | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w @@ -220,7 +220,8 @@ | isNaN f = as "NaN" | isInfinite f, f < 0 = as "-oo" | isInfinite f = as "+oo" - | isNegativeZero f = "(fp.neg ((_ to_fp 8 24) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | isNegativeZero f = as "-zero" + | f == 0 = as "+zero" | True = "((_ to_fp 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")" where as s = "(_ " ++ s ++ " 8 24)" @@ -230,7 +231,8 @@ | isNaN d = as "NaN" | isInfinite d, d < 0 = as "-oo" | isInfinite d = as "+oo" - | isNegativeZero d = "(fp.neg ((_ to_fp 11 53) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | isNegativeZero d = as "-zero" + | d == 0 = as "+zero" | True = "((_ to_fp 11 53) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational d) ++ ")" where as s = "(_ " ++ s ++ " 11 53)" @@ -289,6 +291,6 @@ -- | 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)) +mkSkolemZero _ (KUserSort _ (Right (f:_))) = f +mkSkolemZero _ (KUserSort s _) = error $ "SBV.mkSkolemZero: Unexpected uninterpreted sort: " ++ s +mkSkolemZero rm k = cwToSMTLib rm (mkConstCW k (0::Integer)) diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -28,8 +28,7 @@ , Quantifier(..), needsExistentials , RoundingMode(..) , SBVType(..), newUninterpreted, addAxiom - , SVal(..), svKind - , svBitSize, svSigned + , SVal(..) , svMkSymVar , ArrayContext(..), ArrayInfo , svToSW, svToSymSW, forceSWArg @@ -76,6 +75,7 @@ import Data.SBV.BitVectors.Kind import Data.SBV.BitVectors.Concrete +import Data.SBV.SMT.SMTLibNames import Prelude () import Prelude.Compat @@ -86,6 +86,9 @@ -- | A symbolic word, tracking it's signedness and size. data SW = SW Kind NodeId deriving (Eq, Ord) +instance HasKind SW where + kindOf (SW k _) = k + instance Show SW where show (SW _ (NodeId n)) | n < 0 = "s_" ++ show (abs n) @@ -222,7 +225,7 @@ , (Quot, "quot") , (Rem, "rem") , (Equal, "=="), (NotEqual, "/=") - , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<"), (GreaterEq, ">") + , (LessThan, "<"), (GreaterThan, ">"), (LessEq, "<="), (GreaterEq, ">=") , (Ite, "if_then_else") , (And, "&"), (Or, "|"), (XOr, "^"), (Not, "~") , (Join, "#") @@ -283,7 +286,7 @@ , resConsts :: [(SW, CW)] -- ^ constants , resTables :: [((Int, Kind, Kind), [SW])] -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts , resArrays :: [(Int, ArrayInfo)] -- ^ arrays (user specified) - , resUOConsts :: [(String, SBVType)] -- ^ uninterpreted constants + , resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants , resAxioms :: [(String, [String])] -- ^ axioms , resAsgns :: SBVPgm -- ^ assignments , resConstraints :: [SW] -- ^ additional constraints (boolean) @@ -321,8 +324,8 @@ ++ ["OUTPUTS"] ++ map ((" " ++) . show) os where usorts = [sh s t | KUserSort s t <- Set.toList kinds] - where sh s (Left _, _) = s - sh s (Right es, _) = s ++ " (" ++ intercalate ", " es ++ ")" + where sh s (Left _) = s + sh s (Right es) = s ++ " (" ++ intercalate ", " es ++ ")" shs sw = show sw ++ " :: " ++ show (swKind sw) sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw @@ -450,21 +453,8 @@ -- sure sharing is preserved. data SVal = SVal !Kind !(Either CW (Cached SW)) --- | Extract the 'Kind'. -svKind :: SVal -> Kind -svKind (SVal k _) = k - --- | Extract the but-size from the kind. Assumption: Only called --- on kinds that have an associated size. (i.e., no 'SFloat'/'SDouble' etc.) -svBitSize :: SVal -> Int -svBitSize x = - case svKind x of - KBounded _ s -> s - _ -> error $ "svBitSize: invalid kind " ++ show (svKind x) - --- | Is the value signed? -svSigned :: SVal -> Bool -svSigned x = kindHasSign (svKind x) +instance HasKind SVal where + kindOf (SVal k _) = k -- | Show instance for 'SVal'. Not particularly "desirable", but will do if needed -- NB. We do not show the type info on constant KBool values, since there's no @@ -500,7 +490,7 @@ -- | Create a new uninterpreted symbol, possibly with user given code newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () newUninterpreted st nm t mbCode - | null nm || not (isAlpha (head nm)) || not (all validChar (tail nm)) + | null nm || not enclosed && (not (isAlpha (head nm)) || not (all validChar (tail nm))) = error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier." | True = do uiMap <- readIORef (rUIMap st) @@ -511,6 +501,7 @@ Nothing -> do modifyIORef (rUIMap st) (Map.insert nm t) when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode)) where validChar x = isAlphaNum x || x `elem` "_" + enclosed = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` "|\\") (tail (init nm))) -- | Add a new sAssert based constraint addAssertion :: State -> Maybe CallStack -> String -> SW -> IO () @@ -536,16 +527,13 @@ return (sw, 's' : show ctr) {-# INLINE newSW #-} --- | Register a new kind with the system, used for uninterpreted sorts. We try to avoid names that --- might be conflicting with SMTLib; but this list is not comprehensive.. Beware! +-- | Register a new kind with the system, used for uninterpreted sorts registerKind :: State -> Kind -> IO () registerKind st k - | KUserSort sortName _ <- k, sortName `elem` reserved + | KUserSort sortName _ <- k, sortName `elem` smtLibReservedNames = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." | True = modifyIORef (rUsedKinds st) (Set.insert k) - 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 -- NB. For each constant, we also store weather it's negative-0 or not, @@ -558,7 +546,7 @@ let key = (isNeg0 (cwVal c), c) case key `Map.lookup` constMap of Just sw -> return sw - Nothing -> do let k = cwKind c + Nothing -> do let k = kindOf c (sw, _) <- newSW st k modifyIORef (rconstMap st) (Map.insert key sw) return sw @@ -1034,6 +1022,9 @@ | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.) deriving (Eq, Ord, Show, Read, T.Typeable, G.Data, Bounded, Enum) + +-- | 'RoundingMode' kind +instance HasKind RoundingMode -- | Solver configuration. See also 'z3', 'yices', 'cvc4', 'boolector', 'mathSAT', etc. 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}@.) diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -19,7 +19,6 @@ -- *** Abstract symbolic value type SVal , Kind(..), CW(..), CWVal(..), cwToBool - , svKind, svBitSize, svSigned -- *** Arrays of symbolic values , SArr , readSArr, resetSArr, writeSArr, mergeSArr, newSArr, eqSArr @@ -33,6 +32,10 @@ , svTrue, svFalse, svBool, svAsBool -- *** Integer literals , svInteger, svAsInteger + -- *** Float literals + , svFloat, svDouble + -- ** Algrebraic reals (only from rationals) + , svReal, svNumerator, svDenominator -- *** Symbolic equality , svEqual, svNotEqual -- *** Symbolic ordering @@ -67,6 +70,9 @@ , safeWith -- * Proving properties using multiple solvers , proveWithAll, proveWithAny, satWithAll, satWithAny + -- * Quick-check + , svQuickCheck + -- * Model extraction -- ** Inspecting proof results @@ -131,13 +137,17 @@ import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny) import qualified Data.SBV.BitVectors.Data as SBV (SBV(..)) -import qualified Data.SBV.BitVectors.Model as SBV (isSatisfiableInCurrentPath) +import qualified Data.SBV.BitVectors.Model as SBV (isSatisfiableInCurrentPath, sbvQuickCheck) import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, safeWith, allSatWith, compileToSMTLib, generateSMTBenchmarks) import qualified Data.SBV.SMT.SMT as SBV (Modelable(getModel, getModelDictionary)) -- | Reduce a condition (i.e., try to concretize it) under the given path svIsSatisfiableInCurrentPath :: SVal -> Symbolic Bool svIsSatisfiableInCurrentPath = SBV.isSatisfiableInCurrentPath . toSBool + +-- | Dynamic variant of quick-check +svQuickCheck :: Symbolic SVal -> IO Bool +svQuickCheck = SBV.sbvQuickCheck . fmap toSBool toSBool :: SVal -> SBV.SBool toSBool = SBV.SBV 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 @@ -110,8 +110,8 @@ -- s6 :: SWord8 -- s7 :: SWord8 -- CONSTANTS --- s_2 = False --- s_1 = True +-- s_2 = False :: Bool +-- s_1 = True :: Bool -- TABLES -- ARRAYS -- UNINTERPRETED CONSTANTS @@ -159,8 +159,8 @@ -- s6 :: SWord8 -- s7 :: SWord8 -- CONSTANTS --- s_2 = False --- s_1 = True +-- s_2 = False :: Bool +-- s_1 = True :: Bool -- TABLES -- ARRAYS -- UNINTERPRETED CONSTANTS diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs --- a/Data/SBV/Examples/Misc/Floating.hs +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -57,8 +57,8 @@ -- >>> assocPlusRegular -- Falsifiable. Counter-example: -- x = -1.5991211e-2 :: Float --- y = 131071.99 :: Float --- z = -131069.99 :: Float +-- y = 131071.99 :: Float +-- z = -131069.99 :: Float -- -- Indeed, we have: -- @@ -87,7 +87,7 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = 5.1705105e-26 :: Float +-- a = 5.1705105e-26 :: Float -- b = -3.8518597e-34 :: Float -- -- Indeed, we have: @@ -146,8 +146,8 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundTowardZero :: RoundingMode --- x = 7.984373 :: Float --- y = -2.1684042e-19 :: Float +-- x = 7.984373 :: Float +-- y = -2.1684042e-19 :: Float -- -- (Note that depending on your version of Z3, you might get a different result.) -- Unfortunately we can't directly validate this result at the Haskell level, as Haskell only supports diff --git a/Data/SBV/Examples/Puzzles/Birthday.hs b/Data/SBV/Examples/Puzzles/Birthday.hs --- a/Data/SBV/Examples/Puzzles/Birthday.hs +++ b/Data/SBV/Examples/Puzzles/Birthday.hs @@ -139,7 +139,7 @@ -- >>> cheryl -- Solution #1: -- birthDay = 16 :: Word8 --- birthMonth = 7 :: Word8 +-- birthMonth = 7 :: Word8 -- This is the only solution. cheryl :: IO () cheryl = print =<< allSat puzzle diff --git a/Data/SBV/Examples/Puzzles/DogCatMouse.hs b/Data/SBV/Examples/Puzzles/DogCatMouse.hs --- a/Data/SBV/Examples/Puzzles/DogCatMouse.hs +++ b/Data/SBV/Examples/Puzzles/DogCatMouse.hs @@ -21,7 +21,7 @@ -- -- >>> puzzle -- Solution #1: --- dog = 3 :: Integer +-- dog = 3 :: Integer -- cat = 41 :: Integer -- mouse = 56 :: Integer -- This is the only solution. diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -13,14 +13,14 @@ module Data.SBV.Internals ( -- * Running symbolic programs /manually/ - Result, SBVRunMode(..), Symbolic, runSymbolic, runSymbolic' + Result(..), SBVRunMode(..), Symbolic, runSymbolic, runSymbolic' -- * Other internal structures useful for low-level programming - , SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW, genVar, genVar_ + , SBV(..), slet, CW(..), Kind(..), HasKind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW, genVar, genVar_ , liftQRem, liftDMod, symbolicMergeWithKind , cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..) , SBVType(..), newUninterpreted, forceSWArg -- * Operations useful for instantiating SBV type classes - , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse + , genLiteral, genFromCW, genMkSymVar, checkAndConvert, genParse, showModel, SMTModel(..), smtLibReservedNames -- * Polynomial operations that operate on bit-vectors , ites, mdp, addPoly -- * Compilation to C @@ -29,12 +29,14 @@ , module Data.SBV.Utils.Numeric ) where -import Data.SBV.BitVectors.Data (Result, Symbolic, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), Quantifier(..), mkConstCW) -import Data.SBV.BitVectors.Data (cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), SBVType(..), newUninterpreted, forceSWArg) +import Data.SBV.BitVectors.Data ( Result(..), Symbolic, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), HasKind(..), CWVal(..) + , AlgReal(..), Quantifier(..), mkConstCW, cache, sbvToSW, newExpr, normCW, SBVExpr(..), Op(..), SBVType(..) + , newUninterpreted, forceSWArg, SMTModel(..)) 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.SMT.SMT (genParse, showModel) +import Data.SBV.SMT.SMTLibNames (smtLibReservedNames) import Data.SBV.Tools.Polynomial (ites, mdp, addPoly) import Data.SBV.Utils.Numeric 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 @@ -397,8 +397,8 @@ msg "Checking Satisfiability, all solutions.." sbvPgm@(qinps, _, ki, _, _) <- simulate converter config True [] p let usorts = [s | us@(KUserSort s _) <- Set.toList ki, isFree us] - where isFree (KUserSort _ (Left _, _)) = True - isFree _ = False + 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) [] 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 @@ -347,12 +347,18 @@ -- | Show a model in human readable form. Ignore bindings to those variables that start -- with "__internal_sbv_"; as these are only for internal purposes showModel :: SMTConfig -> SMTModel -> String -showModel cfg m = intercalate "\n" $ map shM interesting - where interesting = filter (not . ignore) $ modelAssocs m - ignore (s, _) = "__internal_sbv_" `isPrefixOf` s - width = maximum (0 : map (length . fst) interesting) - shM (s, v) = " " ++ align s ++ " = " ++ shCW cfg v - align s = s ++ replicate (width - length s) ' ' +showModel cfg = intercalate "\n" . display . map shM . filter (not . ignore) . modelAssocs + where ignore (s, _) = "__internal_sbv_" `isPrefixOf` s + shM (s, v) = let vs = shCW cfg v in ((length s, s), (vlength vs, vs)) + display svs = map line svs + where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - length (takeWhile (not . isSpace) v)) v + nameWidth = maximum $ 0 : [l | ((l, _), _) <- svs] + valWidth = maximum $ 0 : [l | (_, (l, _)) <- svs] + right p s = s ++ replicate p ' ' + left p s = replicate p ' ' ++ s + vlength s = case dropWhile (/= ':') (reverse s) of + (':':':':r) -> length (dropWhile isSpace r) + _ -> length s -- conservative -- | Show a constant value, in the user-specified base shCW :: SMTConfig -> CW -> String 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 @@ -102,8 +102,8 @@ matches -> error $ "SBV.SMTLib2: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing - getUIIndex (KUserSort _ (Right xs, _)) i = i `lookup` zip xs [0..] - getUIIndex _ _ = 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) (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))))] 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 @@ -48,8 +48,8 @@ nonEqs :: RoundingMode -> [(String, CW)] -> [String] nonEqs rm scs = format $ interp ps ++ disallow (map eqClass uninterpClasses) - where isFree (KUserSort _ (Left _, _)) = True - isFree _ = False + where isFree (KUserSort _ (Left _)) = True + isFree _ = False (ups, ps) = partition (isFree . kindOf . snd) scs format [] = [] format [m] = ["(assert " ++ m ++ ")"] @@ -201,10 +201,10 @@ 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" - ] ++ [" " ++ body fs (0::Int)] ++ [")"] + 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" + ] ++ [" " ++ body fs (0::Int)] ++ [")"] where body [] _ = "" body [_] i = show i body (c:cs) i = "(ite (= x " ++ c ++ ") " ++ show i ++ " " ++ body cs (i+1) ++ ")" @@ -363,7 +363,7 @@ lift2Cmp o fo | doubleOp || floatOp = lift2 fo | True = lift2 o unintComp o [a, b] - | KUserSort s (Right _, _) <- kindOf (head arguments) + | KUserSort s (Right _) <- kindOf (head arguments) = let idx v = "(" ++ s ++ "_constrIndex " ++ " " ++ v ++ ")" in "(" ++ o ++ " " ++ idx a ++ " " ++ idx b ++ ")" unintComp o sbvs = error $ "SBV.SMT.SMTLib2.sh.unintComp: Unexpected arguments: " ++ show (o, sbvs) lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" diff --git a/Data/SBV/SMT/SMTLibNames.hs b/Data/SBV/SMT/SMTLibNames.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/SMT/SMTLibNames.hs @@ -0,0 +1,22 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.SMT.SMTLibNames +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- SMTLib Reserved names +----------------------------------------------------------------------------- + +module Data.SBV.SMT.SMTLibNames where + +-- | Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course +-- there's no guarantee it'll stay that way. +smtLibReservedNames :: [String] +smtLibReservedNames = [ "Int", "Real", "List", "Array", "Bool", "FP", "FloatingPoint", "fp" + , "!", "_", "as", "BINARY", "DECIMAL", "exists", "HEXADECIMAL", "forall", "let", "NUMERAL", "par", "STRING" + , "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-fun", "declare-sort", "define-fun", "define-fun-rec" + , "define-sort", "echo", "exit", "get-assertions", "get-assignment", "get-info", "get-model", "get-option", "get-proof", "get-unsat-assumptions" + , "get-unsat-core", "get-value", "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option" + ] diff --git a/Data/SBV/Tools/ExpectedValue.hs b/Data/SBV/Tools/ExpectedValue.hs --- a/Data/SBV/Tools/ExpectedValue.hs +++ b/Data/SBV/Tools/ExpectedValue.hs @@ -41,7 +41,7 @@ runOnce g = do (_, Result _ _ _ _ cs _ _ _ _ _ cstrs _ os) <- runSymbolic' (Concrete g) (m >>= output) let cval o = case o `lookup` cs of Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!" - Just cw -> case (cwKind cw, cwVal cw) of + Just cw -> case (kindOf cw, cwVal cw) of (KBool, _) -> if cwToBool cw then 1 else 0 (KBounded{}, CWInteger v) -> v (KUnbounded, CWInteger v) -> v diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -126,7 +126,7 @@ KReal -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw - s cw = case cwKind cw of + s cw = case kindOf cw of KBool -> take 5 (show (cwToBool cw) ++ repeat ' ') KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w @@ -198,7 +198,7 @@ , "}" ] where mkField p cw i = " " ++ t ++ " " ++ p ++ show i ++ ";" - where t = case cwKind cw of + where t = case kindOf cw of KBool -> "SBool" KBounded False 8 -> "SWord8" KBounded False 16 -> "SWord16" @@ -215,7 +215,7 @@ KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}" - v cw = case cwKind cw of + v cw = case kindOf cw of KBool -> if cwToBool cw then "true " else "false" KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w @@ -231,11 +231,11 @@ where (is, os) = head vs inp cw i = mkBool cw (n ++ "[i].input.i" ++ show i) out cw i = mkBool cw (n ++ "[i].output.o" ++ show i) - mkBool cw s = case cwKind cw of + mkBool cw s = case kindOf cw of KBool -> "(" ++ s ++ " == true) ? \"true \" : \"false\"" _ -> s fmtString = unwords (map fmt is) ++ " -> " ++ unwords (map fmt os) - fmt cw = case cwKind cw of + fmt cw = case kindOf cw of KBool -> "%s" KBounded False 8 -> "0x%02\"PRIx8\"" KBounded False 16 -> "0x%04\"PRIx16\"U" @@ -267,7 +267,7 @@ | True = "rev (map (\\s. s == \"1\") (explode (string_tl r)))" toF True = '1' toF False = '0' - blast cw = case cwKind cw of + blast cw = case kindOf cw of KBool -> [toF (cwToBool cw)] KBounded False 8 -> xlt 8 (cwVal cw) KBounded False 16 -> xlt 16 (cwVal cw) diff --git a/INSTALL b/INSTALL --- a/INSTALL +++ b/INSTALL @@ -12,7 +12,7 @@ highly recommended that you run this program to ensure everything is working correctly. In particular, you will first need to install Z3, the default SMT solver used by sbv, from Microsoft. (You can get it -from http://research.microsoft.com/en-us/um/redmond/projects/z3/.) +from http://github.com/Z3Prover/z3.) Please make sure that the "z3" executable is in your path. Once you have installed sbv, you can use it in your Haskell programs diff --git a/SBVUnitTest/GoldFiles/U2Bridge.gold b/SBVUnitTest/GoldFiles/U2Bridge.gold --- a/SBVUnitTest/GoldFiles/U2Bridge.gold +++ b/SBVUnitTest/GoldFiles/U2Bridge.gold @@ -1,16 +1,16 @@ Satisfiable. Model: - s0 = False - s1 = Edge :: U2Member - s2 = Bono :: U2Member - s3 = True - s4 = Bono :: U2Member - s5 = Bono :: U2Member - s6 = False + s0 = False :: Bool + s1 = Edge :: U2Member + s2 = Bono :: U2Member + s3 = True :: Bool + s4 = Bono :: U2Member + s5 = Bono :: U2Member + s6 = False :: Bool s7 = Larry :: U2Member - s8 = Adam :: U2Member - s9 = True - s10 = Edge :: U2Member - s11 = Bono :: U2Member - s12 = False - s13 = Edge :: U2Member - s14 = Bono :: U2Member + s8 = Adam :: U2Member + s9 = True :: Bool + s10 = Edge :: U2Member + s11 = Bono :: U2Member + s12 = False :: Bool + s13 = Edge :: U2Member + s14 = Bono :: U2Member diff --git a/SBVUnitTest/GoldFiles/auf-1.gold b/SBVUnitTest/GoldFiles/auf-1.gold --- a/SBVUnitTest/GoldFiles/auf-1.gold +++ b/SBVUnitTest/GoldFiles/auf-1.gold @@ -3,8 +3,8 @@ s1 :: SWord32, existential, aliasing "y" s2 :: SWord32, existential, aliasing "initVal" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s3 = 2 :: Word32 s9 = 3 :: Word32 s13 = 1 :: Word32 diff --git a/SBVUnitTest/GoldFiles/basic-2_1.gold b/SBVUnitTest/GoldFiles/basic-2_1.gold --- a/SBVUnitTest/GoldFiles/basic-2_1.gold +++ b/SBVUnitTest/GoldFiles/basic-2_1.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 3 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-2_2.gold b/SBVUnitTest/GoldFiles/basic-2_2.gold --- a/SBVUnitTest/GoldFiles/basic-2_2.gold +++ b/SBVUnitTest/GoldFiles/basic-2_2.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 9 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-2_3.gold b/SBVUnitTest/GoldFiles/basic-2_3.gold --- a/SBVUnitTest/GoldFiles/basic-2_3.gold +++ b/SBVUnitTest/GoldFiles/basic-2_3.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 3 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-2_4.gold b/SBVUnitTest/GoldFiles/basic-2_4.gold --- a/SBVUnitTest/GoldFiles/basic-2_4.gold +++ b/SBVUnitTest/GoldFiles/basic-2_4.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 3 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-3_1.gold b/SBVUnitTest/GoldFiles/basic-3_1.gold --- a/SBVUnitTest/GoldFiles/basic-3_1.gold +++ b/SBVUnitTest/GoldFiles/basic-3_1.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-3_2.gold b/SBVUnitTest/GoldFiles/basic-3_2.gold --- a/SBVUnitTest/GoldFiles/basic-3_2.gold +++ b/SBVUnitTest/GoldFiles/basic-3_2.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-3_3.gold b/SBVUnitTest/GoldFiles/basic-3_3.gold --- a/SBVUnitTest/GoldFiles/basic-3_3.gold +++ b/SBVUnitTest/GoldFiles/basic-3_3.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-3_4.gold b/SBVUnitTest/GoldFiles/basic-3_4.gold --- a/SBVUnitTest/GoldFiles/basic-3_4.gold +++ b/SBVUnitTest/GoldFiles/basic-3_4.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-3_5.gold b/SBVUnitTest/GoldFiles/basic-3_5.gold --- a/SBVUnitTest/GoldFiles/basic-3_5.gold +++ b/SBVUnitTest/GoldFiles/basic-3_5.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "y" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s2 = 1 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-4_1.gold b/SBVUnitTest/GoldFiles/basic-4_1.gold --- a/SBVUnitTest/GoldFiles/basic-4_1.gold +++ b/SBVUnitTest/GoldFiles/basic-4_1.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-4_2.gold b/SBVUnitTest/GoldFiles/basic-4_2.gold --- a/SBVUnitTest/GoldFiles/basic-4_2.gold +++ b/SBVUnitTest/GoldFiles/basic-4_2.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-4_3.gold b/SBVUnitTest/GoldFiles/basic-4_3.gold --- a/SBVUnitTest/GoldFiles/basic-4_3.gold +++ b/SBVUnitTest/GoldFiles/basic-4_3.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-4_4.gold b/SBVUnitTest/GoldFiles/basic-4_4.gold --- a/SBVUnitTest/GoldFiles/basic-4_4.gold +++ b/SBVUnitTest/GoldFiles/basic-4_4.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-4_5.gold b/SBVUnitTest/GoldFiles/basic-4_5.gold --- a/SBVUnitTest/GoldFiles/basic-4_5.gold +++ b/SBVUnitTest/GoldFiles/basic-4_5.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 1 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/basic-5_1.gold b/SBVUnitTest/GoldFiles/basic-5_1.gold --- a/SBVUnitTest/GoldFiles/basic-5_1.gold +++ b/SBVUnitTest/GoldFiles/basic-5_1.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "q" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-5_2.gold b/SBVUnitTest/GoldFiles/basic-5_2.gold --- a/SBVUnitTest/GoldFiles/basic-5_2.gold +++ b/SBVUnitTest/GoldFiles/basic-5_2.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "q" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-5_3.gold b/SBVUnitTest/GoldFiles/basic-5_3.gold --- a/SBVUnitTest/GoldFiles/basic-5_3.gold +++ b/SBVUnitTest/GoldFiles/basic-5_3.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "q" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-5_4.gold b/SBVUnitTest/GoldFiles/basic-5_4.gold --- a/SBVUnitTest/GoldFiles/basic-5_4.gold +++ b/SBVUnitTest/GoldFiles/basic-5_4.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "q" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/basic-5_5.gold b/SBVUnitTest/GoldFiles/basic-5_5.gold --- a/SBVUnitTest/GoldFiles/basic-5_5.gold +++ b/SBVUnitTest/GoldFiles/basic-5_5.gold @@ -2,8 +2,8 @@ s0 :: SWord8, aliasing "x" s1 :: SWord8, aliasing "q" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s2 = 1 :: Word8 TABLES ARRAYS diff --git a/SBVUnitTest/GoldFiles/ccitt.gold b/SBVUnitTest/GoldFiles/ccitt.gold --- a/SBVUnitTest/GoldFiles/ccitt.gold +++ b/SBVUnitTest/GoldFiles/ccitt.gold @@ -4,8 +4,8 @@ s2 :: SWord32 s3 :: SWord16 CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s13 = 0 :: Word1 s1686 = 0 :: Word8 s1687 = 1 :: Word8 diff --git a/SBVUnitTest/GoldFiles/coins.gold b/SBVUnitTest/GoldFiles/coins.gold --- a/SBVUnitTest/GoldFiles/coins.gold +++ b/SBVUnitTest/GoldFiles/coins.gold @@ -6,8 +6,8 @@ s54 :: SWord16, existential, aliasing "c5" s66 :: SWord16, existential, aliasing "c6" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s1 = 1 :: Word16 s3 = 5 :: Word16 s5 = 10 :: Word16 @@ -551,11 +551,11 @@ s539 :: SBool = s3 /= s534 s540 :: SWord16 = s123 + s492 s541 :: SBool = s88 /= s540 - s542 :: SBool = s0 > s18 - s543 :: SBool = s18 > s30 - s544 :: SBool = s30 > s42 - s545 :: SBool = s42 > s54 - s546 :: SBool = s54 > s66 + s542 :: SBool = s0 >= s18 + s543 :: SBool = s18 >= s30 + s544 :: SBool = s30 >= s42 + s545 :: SBool = s42 >= s54 + s546 :: SBool = s54 >= s66 s547 :: SBool = s545 & s546 s548 :: SBool = s544 & s547 s549 :: SBool = s543 & s548 diff --git a/SBVUnitTest/GoldFiles/counts.gold b/SBVUnitTest/GoldFiles/counts.gold --- a/SBVUnitTest/GoldFiles/counts.gold +++ b/SBVUnitTest/GoldFiles/counts.gold @@ -10,8 +10,8 @@ s8 :: SWord8 s9 :: SWord8 CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s10 = 10 :: Word8 s12 = 0 :: Word8 s32 = 2 :: Word8 diff --git a/SBVUnitTest/GoldFiles/crcPolyExist.gold b/SBVUnitTest/GoldFiles/crcPolyExist.gold --- a/SBVUnitTest/GoldFiles/crcPolyExist.gold +++ b/SBVUnitTest/GoldFiles/crcPolyExist.gold @@ -5,8 +5,8 @@ s3 :: SWord32, aliasing "rh" s4 :: SWord16, aliasing "rl" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s6 = 0 :: Word1 s18 = 1 :: Word8 s3340 = 0 :: Word8 @@ -3477,7 +3477,7 @@ s3465 :: SWord8 = if s23 then s3464 else s3463 s3466 :: SWord8 = s18 + s3465 s3467 :: SWord8 = if s17 then s3466 else s3465 - s3469 :: SBool = s3467 > s3468 + s3469 :: SBool = s3467 >= s3468 s3470 :: SBool = s12 | s3469 s3471 :: SBool = s7 & s3470 CONSTRAINTS diff --git a/SBVUnitTest/GoldFiles/dogCatMouse.gold b/SBVUnitTest/GoldFiles/dogCatMouse.gold --- a/SBVUnitTest/GoldFiles/dogCatMouse.gold +++ b/SBVUnitTest/GoldFiles/dogCatMouse.gold @@ -1,5 +1,5 @@ Solution #1: - dog = 3 :: Integer + dog = 3 :: Integer cat = 41 :: Integer mouse = 56 :: Integer This is the only solution. diff --git a/SBVUnitTest/GoldFiles/iteTest1.gold b/SBVUnitTest/GoldFiles/iteTest1.gold --- a/SBVUnitTest/GoldFiles/iteTest1.gold +++ b/SBVUnitTest/GoldFiles/iteTest1.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/iteTest2.gold b/SBVUnitTest/GoldFiles/iteTest2.gold --- a/SBVUnitTest/GoldFiles/iteTest2.gold +++ b/SBVUnitTest/GoldFiles/iteTest2.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/iteTest3.gold b/SBVUnitTest/GoldFiles/iteTest3.gold --- a/SBVUnitTest/GoldFiles/iteTest3.gold +++ b/SBVUnitTest/GoldFiles/iteTest3.gold @@ -1,8 +1,8 @@ INPUTS s0 :: SWord8, aliasing "x" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool TABLES ARRAYS UNINTERPRETED CONSTANTS diff --git a/SBVUnitTest/GoldFiles/legato.gold b/SBVUnitTest/GoldFiles/legato.gold --- a/SBVUnitTest/GoldFiles/legato.gold +++ b/SBVUnitTest/GoldFiles/legato.gold @@ -10,8 +10,8 @@ s8 :: SBool, existential, aliasing "flagC" s9 :: SBool, existential, aliasing "flagZ" CONSTANTS - s_2 = False - s_1 = True + s_2 = False :: Bool + s_1 = True :: Bool s19 = 0 :: Word1 s17 = 0 :: Word8 s24 = 128 :: Word8 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 Nov 10 17:02:49 PST 2015" +buildTime = "Sun Dec 6 18:51:28 PST 2015" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 5.5 +Version: 5.6 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 @@ -115,6 +115,7 @@ , Data.SBV.SMT.SMT , Data.SBV.SMT.SMTLib , Data.SBV.SMT.SMTLib2 + , Data.SBV.SMT.SMTLibNames , Data.SBV.Provers.Prover , Data.SBV.Provers.SExpr , Data.SBV.Provers.Boolector