diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,24 @@ * Hackage: * GitHub: -* Latest Hackage released version: 3.4 +* Latest Hackage released version: 3.5 +### Version 3.5, 2015-01-15 + +This release is mainly adding support for enumerated types in Haskell being +translated to their symbolic counterparts; instead of going completely +uninterpreted. + + * Keep track of data-type details for uninterpreted sorts. + * Rework the U2Bridge example to use enumerated types. + * The "Uninterpreted" name no longer makes sense with this change, so + rework the relevant names to ensure proper internal naming. + * Add Data/SBV/Examples/Misc/Enumerate.hs as an example for demonstrating + how enumerations are translated. + * Fix a long-standing bug in the implementation of select when + translated as SMT-Lib tables. (Github issue #103.) Thanks to + Brian Huffman for reporting. + ### Version 3.4, 2014-12-21 * This release is mainly addressing floating-point changes in SMT-Lib. @@ -236,14 +252,14 @@ - sbvShiftLeft - sbvShiftRight which can accommodate unsigned symbolic shift amounts. Note that - one cannot use Haskell's shiftL/shiftR from the Bits class since + one cannot use the Haskell shiftL/shiftR functions from the Bits class since they are hard-wired to take 'Int' values as the shift amounts only. - Add a new function 'sbvArithShiftRight', which is the same as a shift-right, except it uses the MSB of the input as the bit to fill in (instead of always filling in with 0 bits). Note that this is the same as shiftRight for signed values, but differs from a shiftRight when the input is unsigned. (There is no Haskell analogue of this - function, as Haskell's shiftR is always arithmetic for signed + function, as Haskell shiftR is always arithmetic for signed types and logical for unsigned ones.) This variant is designed for use cases when one uses the underlying unsigned SMT-Lib representation to implement custom signed operations, for instance. @@ -252,7 +268,7 @@ ### Version 2.7, 2012-10-21 - Add missing QuickCheck instance for SReal - - When dealing with concrete SReal's, make sure to operate + - When dealing with concrete SReals, make sure to operate only on exact algebraic reals on the Haskell side, leaving true algebraic reals (i.e., those that are roots of polynomials that cannot be expressed as a rational) symbolic. This avoids @@ -331,7 +347,7 @@ rationals as well. You *should* use Z3 v4.0 when working with real numbers. While the interface will - work with older versions of Z3 (or other SMT solvers in general), it uses Z3's + work with older versions of Z3 (or other SMT solvers in general), it uses Z3 root-obj construct to retrieve and query algebraic reals. While SReal values have infinite precision, printing such values is not trivial since @@ -350,7 +366,7 @@ * Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e., sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the right kind. Strictly speaking these are just synonyms for 'free' - and 'mapM free' (plural versions), so they aren't adding any additional + and 'mapM free' (plural versions), so they are not adding any additional power. Except, they are specialized at their respective types, and might be easier to remember. * Add function solve, which is merely a synonym for (return . bAnd), but @@ -394,10 +410,10 @@ detalied below: http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks As a consequence, mixed Integer/BV problems can cause soundness issues in Z3 - and does in SBV. Unfortunately, it's too severe for SBV to add the woraround - option, as it slows down the solver as a side effect as well. Thus, we're + and does in SBV. Unfortunately, it is too severe for SBV to add the woraround + option, as it slows down the solver as a side effect as well. Thus, we are making this optionally available if/when needed. (Note that the work-around - should not be necessary with Z3 v3.3; which isn't released yet.) + should not be necessary with Z3 v3.3; which is not released yet.) * Other minor clean-up ### Version 1.1, 2012-02-14 @@ -450,7 +466,7 @@ been better, but it's already taken.) This is not as useful as one might think as forAll and forSome do not nest, as an inner application of one pushes its argument to a Predicate, making - the outer one useless, but it's nonetheless useful by itself. + the outer one useless, but it is nonetheless useful by itself. * Add a "Modelable" class, which simplifies model extraction. * Add support for quick-check at the "Symbolic SBool" level. Previously SBV only allowed functions returning SBool to be quick-checked, which @@ -504,7 +520,7 @@ * Add support for SInteger, the type of signed unbounded integer values. SBV can now prove theorems about unbounded numbers, - following the semantics of Haskell's Integer type. (Requires z3 to + following the semantics of Haskell Integer type. (Requires z3 to be used as the backend solver.) * Add functions 'optimize', 'maximize', and 'minimize' that can be used to find optimal solutions to given constraints with @@ -522,7 +538,7 @@ actually returned "unknown" for the problem and the model might therefore be bogus. Note that we did not need this before since we only supported bounded bit-vectors, which has a decidable - theory. With the addition of unbounded Integer's and quantifiers, the + theory. With the addition of unbounded Integers and quantifiers, the solvers can now return unknown. This should still be rare in practice, but can happen with the use of non-linear constructs. (i.e., multiplication of two variables.) @@ -535,7 +551,7 @@ marks free-variables appropriately using forall/exists functions, and the solver translates them accordingly. Note that this is a non-backwards compatible change in sat calls, as the semantics of formulas is essentially - changing. While this is unfortunate, it's more uniform and simpler to understand + changing. While this is unfortunate, it is more uniform and simpler to understand in general. This release also adds support for the Z3 solver, which is the main @@ -563,7 +579,7 @@ on/off driver program generation. Default is to generate a driver. (Issue "cgGenerateDriver False" to skip the driver.) For a library, a driver will be generated if any of the - constituent parts has a driver. Otherwise it'll be skipped. + constituent parts has a driver. Otherwise it will be skipped. * Fix a bug in C code generation where "Not" over booleans were incorrectly getting translated due to need for masking. * Add support for compilation with uninterpreted functions. Users @@ -654,7 +670,7 @@ it relied on the Integer instance, which does the wrong thing after normalization. * Fix conversion of signed numbers from bits, - previous version did not handle two's + previous version did not handle twos complement layout correctly Testing: @@ -695,7 +711,7 @@ Bug fixes: * Output naming bug, reported by Josef Svenningsson - * Specification bug in Legato's multipler example + * Specification bug in Legatos multipler example ### Version 0.9.11, 2011-02-16 @@ -703,7 +719,7 @@ ### Version 0.9.10, 2011-02-15 - * Integrate commits from Iavor: Generalize SBV's to keep + * Integrate commits from Iavor: Generalize SBVs to keep track the integer directly without resorting to different leaf types * Remove the unnecessary CLC instruction from the Legato example @@ -718,7 +734,7 @@ ### Version 0.9.8, 2011-01-22 * Better support for uninterpreted-functions - * Support counter-examples with SArray's + * Support counter-examples with SArrays * Ladner-Fischer scheme example * Documentation updates diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,4 +1,4 @@ -Copyright (c) 2010-2014, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -177,6 +177,9 @@ -- $uninterpreted , Uninterpreted(..), addAxiom + -- * Enumerations + -- $enumerations + -- * Properties, proofs, and satisfiability -- $proveIntro @@ -752,9 +755,10 @@ following example demonstrates: @ - data B = B deriving (Eq, Ord, Data, Typeable) + data B = B () deriving (Eq, Ord, Data, Typeable, Read, Show) instance SymWord B instance HasKind B + instance SatModel B -- required only if 'getModel' etc. is used. @ (Note that you'll also need to use the language pragma @DeriveDataTypeable@, and import @Data.Generics@ for the above to work.) @@ -762,14 +766,57 @@ Once GHC implements derivable user classes (), we will be able to simplify this to: @ - data B = B deriving (Eq, Ord, Data, Typeable, SymWord, HasKind) + data B = B () deriving (Eq, Ord, Data, Typeable, Read, Show, SymWord, HasKind) @ This is all it takes to introduce 'B' as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type -of symbolic values that ranges over 'B' values. +of symbolic values that ranges over 'B' values. Note that the @()@ argument is important to distinguish it from enumerations. Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by the 'Uninterpreted' class. +-} + +{- $enumerations +If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually +translate that as just such a data-type to SMT-Lib, and will use the constructors as the inhabitants of the said sort. A simple example is: + + @ + data X = A | B | C deriving (Eq, Ord, Data, Typeable, Read, Show) + instance SymWord X + instance HasKind X + instance SatModel X + @ + +Now, the user can define + + @ + type SX = SBV X + @ + +and treat @SX@ as a regular symbolic type ranging over the values @A@, @B@, and @C@. Such values can be compared for equality, and with the usual +other comparison operators, such as @.==@, @./=@, @.>@, @.>=@, @<@, and @<=@. + +Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple +query would look like: + + @ + allSat $ \x -> x .== (x :: SX) + @ + +which would list all three elements of this domain as satisfying solutions. + + @ + Solution #1: + s0 = A :: X + Solution #2: + s0 = B :: X + Solution #3: + s0 = C :: X + Found 3 different solutions. + @ + +Note that the result is properly typed as @X@ elements; these are not mere strings. So, in a 'getModel' scenario, the user can recover actual +elements of the domain and program further with those values as usual. -} {-# ANN module "HLint: ignore Use import/export shortcut" #-} 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 @@ -9,15 +9,17 @@ -- Internal data-structures for the sbv library ----------------------------------------------------------------------------- -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64 @@ -50,18 +52,18 @@ import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT) import Control.Monad.Trans (MonadIO, liftIO) import Data.Char (isAlpha, isAlphaNum) -import Data.Generics (Data(..), dataTypeName, dataTypeOf, tyconUQname) import Data.Int (Int8, Int16, Int32, Int64) import Data.Word (Word8, Word16, Word32, Word64) import Data.IORef (IORef, newIORef, modifyIORef, readIORef, writeIORef) import Data.List (intercalate, sortBy) import Data.Maybe (isJust, fromJust) -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) -import qualified Data.Foldable as F (toList) -import qualified Data.Sequence as S (Seq, empty, (|>)) +import qualified Data.Generics as G (Data(..), DataType, dataTypeName, dataTypeOf, tyconUQname, dataTypeConstrs, constrFields) +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) +import qualified Data.Foldable as F (toList) +import qualified Data.Sequence as S (Seq, empty, (|>)) import System.Exit (ExitCode(..)) import System.Mem.StableName @@ -71,53 +73,53 @@ import Data.SBV.Utils.Lib -- | A constant value -data CWVal = CWAlgReal AlgReal -- ^ algebraic real - | CWInteger Integer -- ^ bit-vector/unbounded integer - | CWFloat Float -- ^ float - | CWDouble Double -- ^ double - | CWUninterpreted String -- ^ value of an uninterpreted kind +data CWVal = CWAlgReal AlgReal -- ^ algebraic real + | CWInteger Integer -- ^ bit-vector/unbounded integer + | CWFloat Float -- ^ float + | CWDouble Double -- ^ double + | CWUserSort (Maybe Int, String) -- ^ value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations -- We cannot simply derive Eq/Ord for CWVal, since CWAlgReal doesn't have proper -- instances for these when values are infinitely precise reals. However, we do -- need a structural eq/ord for Map indexes; so define custom ones here: instance Eq CWVal where - CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b - CWInteger a == CWInteger b = a == b - CWUninterpreted a == CWUninterpreted b = a == b - CWFloat a == CWFloat b = a == b - CWDouble a == CWDouble b = a == b - _ == _ = False + CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b + CWInteger a == CWInteger b = a == b + CWUserSort a == CWUserSort b = a == b + CWFloat a == CWFloat b = a == b + CWDouble a == CWDouble b = a == b + _ == _ = False instance Ord CWVal where - CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b - CWAlgReal _ `compare` CWInteger _ = LT - CWAlgReal _ `compare` CWFloat _ = LT - CWAlgReal _ `compare` CWDouble _ = LT - CWAlgReal _ `compare` CWUninterpreted _ = LT + CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b + CWAlgReal _ `compare` CWInteger _ = LT + CWAlgReal _ `compare` CWFloat _ = LT + CWAlgReal _ `compare` CWDouble _ = LT + CWAlgReal _ `compare` CWUserSort _ = LT - CWInteger _ `compare` CWAlgReal _ = GT - CWInteger a `compare` CWInteger b = a `compare` b - CWInteger _ `compare` CWFloat _ = LT - CWInteger _ `compare` CWDouble _ = LT - CWInteger _ `compare` CWUninterpreted _ = LT + CWInteger _ `compare` CWAlgReal _ = GT + CWInteger a `compare` CWInteger b = a `compare` b + CWInteger _ `compare` CWFloat _ = LT + CWInteger _ `compare` CWDouble _ = LT + CWInteger _ `compare` CWUserSort _ = LT - CWFloat _ `compare` CWAlgReal _ = GT - CWFloat _ `compare` CWInteger _ = GT - CWFloat a `compare` CWFloat b = a `compare` b - CWFloat _ `compare` CWDouble _ = LT - CWFloat _ `compare` CWUninterpreted _ = LT + CWFloat _ `compare` CWAlgReal _ = GT + CWFloat _ `compare` CWInteger _ = GT + CWFloat a `compare` CWFloat b = a `compare` b + CWFloat _ `compare` CWDouble _ = LT + CWFloat _ `compare` CWUserSort _ = LT - CWDouble _ `compare` CWAlgReal _ = GT - CWDouble _ `compare` CWInteger _ = GT - CWDouble _ `compare` CWFloat _ = GT - CWDouble a `compare` CWDouble b = a `compare` b - CWDouble _ `compare` CWUninterpreted _ = LT + CWDouble _ `compare` CWAlgReal _ = GT + CWDouble _ `compare` CWInteger _ = GT + CWDouble _ `compare` CWFloat _ = GT + CWDouble a `compare` CWDouble b = a `compare` b + CWDouble _ `compare` CWUserSort _ = LT - CWUninterpreted _ `compare` CWAlgReal _ = GT - CWUninterpreted _ `compare` CWInteger _ = GT - CWUninterpreted _ `compare` CWFloat _ = GT - CWUninterpreted _ `compare` CWDouble _ = GT - CWUninterpreted a `compare` CWUninterpreted b = a `compare` b + CWUserSort _ `compare` CWAlgReal _ = GT + CWUserSort _ `compare` CWInteger _ = GT + CWUserSort _ `compare` CWFloat _ = GT + CWUserSort _ `compare` CWDouble _ = GT + CWUserSort a `compare` CWUserSort b = a `compare` b -- | 'CW' represents a concrete word of a fixed size: -- Endianness is mostly irrelevant (see the 'FromBits' class). @@ -155,12 +157,18 @@ | True = v `mod` (2 ^ sz) normCW c = c +instance Eq G.DataType where + a == b = G.tyconUQname (G.dataTypeName a) == G.tyconUQname (G.dataTypeName b) + +instance Ord G.DataType where + a `compare` b = G.tyconUQname (G.dataTypeName a) `compare` G.tyconUQname (G.dataTypeName b) + -- | Kind of symbolic value data Kind = KBool | KBounded Bool Int | KUnbounded | KReal - | KUninterpreted String + | KUserSort String (Either String [String], G.DataType) | KFloat | KDouble deriving (Eq, Ord) @@ -171,7 +179,7 @@ show (KBounded True n) = "SInt" ++ show n show KUnbounded = "SInteger" show KReal = "SReal" - show (KUninterpreted s) = s + show (KUserSort s _) = s show KFloat = "SFloat" show KDouble = "SDouble" @@ -276,40 +284,40 @@ showType :: a -> String -- defaults hasSign x = case kindOf x of - KBool -> False - KBounded b _ -> b - KUnbounded -> True - KReal -> True - KFloat -> True - KDouble -> True - KUninterpreted{} -> False + KBool -> False + KBounded b _ -> b + KUnbounded -> True + KReal -> True + KFloat -> True + KDouble -> True + KUserSort{} -> False 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)" - KUninterpreted 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 | KUninterpreted{} <- kindOf x = True - | True = False + 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 kinds - default kindOf :: Data a => a -> Kind - kindOf = KUninterpreted . tyconUQname . dataTypeName . dataTypeOf + -- 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 @@ -326,41 +334,41 @@ instance HasKind Double where kindOf _ = KDouble -- | Lift a unary function thruough a CW -liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> (String -> b) -> CW -> b -liftCW f _ _ _ _ (CW _ (CWAlgReal v)) = f v -liftCW _ f _ _ _ (CW _ (CWInteger v)) = f v -liftCW _ _ f _ _ (CW _ (CWFloat v)) = f v -liftCW _ _ _ f _ (CW _ (CWDouble v)) = f v -liftCW _ _ _ _ f (CW _ (CWUninterpreted v)) = f v +liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> ((Maybe Int, String) -> b) -> CW -> b +liftCW f _ _ _ _ (CW _ (CWAlgReal v)) = f v +liftCW _ f _ _ _ (CW _ (CWInteger v)) = f v +liftCW _ _ f _ _ (CW _ (CWFloat v)) = f v +liftCW _ _ _ f _ (CW _ (CWDouble v)) = f v +liftCW _ _ _ _ f (CW _ (CWUserSort v)) = f v -- | Lift a binary function through a CW -liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (String -> String -> b) -> CW -> CW -> b +liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b liftCW2 r i f d u x y = case (cwVal x, cwVal y) of - (CWAlgReal a, CWAlgReal b) -> r a b - (CWInteger a, CWInteger b) -> i a b - (CWFloat a, CWFloat b) -> f a b - (CWDouble a, CWDouble b) -> d a b - (CWUninterpreted a, CWUninterpreted b) -> u a b - _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) + (CWAlgReal a, CWAlgReal b) -> r a b + (CWInteger a, CWInteger b) -> i a b + (CWFloat a, CWFloat b) -> f a b + (CWDouble a, CWDouble b) -> d a b + (CWUserSort a, CWUserSort b) -> u a b + _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) -- | Map a unary function through a CW -mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (String -> String) -> CW -> 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 - CWAlgReal a -> CWAlgReal (r a) - CWInteger a -> CWInteger (i a) - CWFloat a -> CWFloat (f a) - CWDouble a -> CWDouble (d a) - CWUninterpreted a -> CWUninterpreted (u a) + CWAlgReal a -> CWAlgReal (r a) + CWInteger a -> CWInteger (i a) + CWFloat a -> CWFloat (f a) + CWDouble a -> CWDouble (d a) + CWUserSort a -> CWUserSort (u a) -- | Map a binary function through a CW -mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (String -> String -> String) -> CW -> CW -> 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, CWUninterpreted a, CWUninterpreted b) -> normCW $ CW (cwKind x) (CWUninterpreted (u a b)) - _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) + (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)) + _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) instance HasKind CW where kindOf = cwKind @@ -370,7 +378,7 @@ instance Show CW where show w | cwIsBit w = show (cwToBool w) - show w = liftCW show show show show id w ++ " :: " ++ showType w + show w = liftCW show show show show snd w ++ " :: " ++ showType w instance Show SW where show (SW _ (NodeId n)) @@ -479,7 +487,7 @@ ++ map ((" " ++) . show) cstrs ++ ["OUTPUTS"] ++ map ((" " ++) . show) os - where usorts = [s | KUninterpreted s <- Set.toList kinds] + where usorts = [s | KUserSort s _ <- Set.toList kinds] 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 @@ -742,7 +750,7 @@ registerKind :: State -> Kind -> IO () registerKind st k - | KUninterpreted sortName <- k, sortName `elem` reserved + | KUserSort sortName _ <- k, sortName `elem` reserved = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." | True = modifyIORef (rUsedKinds st) (Set.insert k) @@ -772,13 +780,13 @@ -- | Create a constant word from an integral mkConstCW :: Integral a => Kind -> a -> CW -mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) -mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a)) -mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) -mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) -mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a))) -mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a))) -mkConstCW (KUninterpreted s) a = error $ "Unexpected call to mkConstCW with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a) +mkConstCW KBool a = normCW $ CW KBool (CWInteger (toInteger a)) +mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a)) +mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) +mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) +mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a))) +mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a))) +mkConstCW (KUserSort s _) a = error $ "Unexpected call to mkConstCW with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a) -- | Create a new expression; hash-cons as necessary newExpr :: State -> Kind -> SBVExpr -> IO SW @@ -965,6 +973,25 @@ extraCstrs <- reverse `fmap` readIORef cstrs return $ Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO +-- | 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) + where dataType = G.dataTypeOf a + sortName = G.tyconUQname . G.dataTypeName $ dataType + constrs = G.dataTypeConstrs dataType + isEnumeration = not (null constrs) && all (null . G.constrFields) constrs + mbEnumFields + | isEnumeration = check constrs [] + | True = Left $ sortName ++ "is not a finite non-empty enumeration" + check [] sofar = Right $ reverse sofar + check (c:cs) sofar = case checkConstr c of + Nothing -> check cs (show c : sofar) + Just s -> Left $ sortName ++ "." ++ show c ++ ": " ++ s + checkConstr c = case (reads (show c) :: [(a, String)]) of + ((_, "") : _) -> Nothing + _ -> Just $ "not a nullary constructor" + ------------------------------------------------------------------------------- -- * Symbolic Words ------------------------------------------------------------------------------- @@ -1013,8 +1040,8 @@ -- | One stop allocator mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) - -- minimal complete definition, Nothing. - -- Giving no instances is ok when defining an uninterpreted sort, but otherwise you really + -- minimal complete definition:: Nothing. + -- Giving no instances is ok when defining an uninterpreted/enumerated sort, but otherwise you really -- want to define: mbMaxBound, mbMinBound, literal, fromCW, mkSymWord forall = mkSymWord (Just ALL) . Just forall_ = mkSymWord (Just ALL) Nothing @@ -1035,17 +1062,26 @@ isConcretely s p | Just i <- unliteral s = p i | True = False - -- Followings, you really want to define them unless the instance is for an uninterpreted sort + -- Followings, you really want to define them unless the instance is for an uninterpreted/enumerated sort mbMaxBound = Nothing mbMinBound = Nothing - literal x = error $ "Cannot create symbolic literals for kind: " ++ show (kindOf x) - fromCW cw = error $ "Cannot convert CW " ++ show cw ++ " to kind " ++ show (kindOf (undefined :: a)) - default mkSymWord :: Data a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) + default literal :: Show a => a -> SBV a + literal x = let k@(KUserSort _ (conts, _)) = kindOf x + sx = show x + mbIdx = case conts of + Right xs -> sx `lookup` zip xs [0..] + _ -> Nothing + in SBV k (Left (CW k (CWUserSort (mbIdx, sx)))) + + default fromCW :: Read a => CW -> a + fromCW (CW _ (CWUserSort (_, s))) = read s + fromCW cw = error $ "Cannot convert CW " ++ show cw ++ " to kind " ++ show (kindOf (undefined :: a)) + + default mkSymWord :: (Read a, G.Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) mkSymWord mbQ mbNm = do - let sortName = tyconUQname . dataTypeName . dataTypeOf $ (undefined :: a) st <- ask - let k = KUninterpreted sortName + let k@(KUserSort sortName _) = constructUKind (undefined :: a) liftIO $ registerKind st k let q = case (mbQ, runMode st) of (Just x, _) -> x @@ -1101,7 +1137,7 @@ -- -- * Maps directly to SMT-lib arrays -- --- * Reading from an unintialized value is OK and yields an uninterpreted result +-- * Reading from an unintialized value is OK and yields an unspecified result -- -- * Can check for equality of these arrays -- 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 @@ -37,7 +37,7 @@ import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits (Bits(..)) import Data.Int (Int8, Int16, Int32, Int64) -import Data.List (genericLength, genericIndex, unzip4, unzip5, unzip6, unzip7, intercalate) +import Data.List (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate) import Data.Maybe (fromMaybe) import Data.Word (Word8, Word16, Word32, Word64) @@ -67,11 +67,11 @@ ghcBitSize = bitSize #endif -noUnint :: String -> a -noUnint x = error $ "Unexpected operation called on uninterpreted value: " ++ show x +noUnint :: (Maybe Int, String) -> a +noUnint x = error $ "Unexpected operation called on uninterpreted/enumerated value: " ++ show x -noUnint2 :: String -> String -> a -noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted values: " ++ show (x, y) +noUnint2 :: (Maybe Int, String) -> (Maybe Int, String) -> a +noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted/enumerated values: " ++ show (x, y) liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SBV b -> SBV b liftSym1 _ opCR opCI opCF opCD (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI opCF opCD noUnint a @@ -89,9 +89,9 @@ liftSym2 _ okCW opCR opCI opCF opCD (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI opCF opCD noUnint2 a b liftSym2 opS _ _ _ _ _ a@(SBV k _) b = SBV k $ Right $ liftSW2 opS k a b -liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool -liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b) -liftSym2B opS _ _ _ _ _ a b = SBV KBool $ Right $ liftSW2 opS KBool a b +liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> ((Maybe Int, String) -> (Maybe Int, String) -> Bool) -> SBV b -> SBV b -> SBool +liftSym2B _ okCW opCR opCI opCF opCD opUI (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD opUI a b) +liftSym2B opS _ _ _ _ _ _ a b = SBV KBool $ Right $ liftSW2 opS KBool a b liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a @@ -406,8 +406,8 @@ -} instance EqSymbolic (SBV a) where - (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) rationalCheck (==) (==) (==) (==) - (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=) + (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) rationalCheck (==) (==) (==) (==) (==) + (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=) (/=) -- | eqOpt says the references are to the same SW, thus we can optimize. Note that -- we explicitly disallow KFloat/KDouble here. Why? Because it's *NOT* true that @@ -419,23 +419,28 @@ KDouble -> Nothing _ -> if x == y then Just w else Nothing +-- For uninterpreted/enumerated values, we carefully lift through the constructor index for comparisons: +uiLift :: String -> (Int -> Int -> Bool) -> (Maybe Int, String) -> (Maybe Int, String) -> Bool +uiLift _ cmp (Just i, _) (Just j, _) = i `cmp` j +uiLift w _ a b = error $ "Data.SBV.BitVectors.Model: Impossible happened while trying to lift " ++ w ++ " over " ++ show (a, b) + instance SymWord a => OrdSymbolic (SBV a) where x .< y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false | Just mb <- mbMinBound, y `isConcretely` (== mb) = false - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) (uiLift "<" (<)) x y x .<= y | Just mb <- mbMinBound, x `isConcretely` (== mb) = true | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) (uiLift "<=" (<=)) x y x .> y | Just mb <- mbMinBound, x `isConcretely` (== mb) = false | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) (uiLift ">" (>)) x y x .>= y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true | Just mb <- mbMinBound, y `isConcretely` (== mb) = true - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) (uiLift ">=" (>=)) x y -- Bool instance EqSymbolic Bool where @@ -1175,8 +1180,11 @@ -- list is really humongous, which is not very common in general. (Also, -- for the case when the list is bit-vectors, we use SMT tables anyhow.) select xs err ind - | isReal ind = error "SBV.select: unsupported real valued select/index expression" - | True = walk xs ind err + | isReal ind = error "SBV.select: unsupported real valued select/index expression" + | isFloat ind = error "SBV.select: unsupported float valued select/index expression" + | isDouble ind = error "SBV.select: unsupported double valued select/index expression" + | hasSign ind = ite (ind .< 0) err (walk xs ind err) + | True = walk xs ind err where walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) @@ -1329,18 +1337,26 @@ CWInteger i -> if i < 0 || i >= genericLength xs then err else xs `genericIndex` i - _ -> error "SBV.select: unsupported real valued select/index expression" - select xs err ind = SBV kElt $ Right $ cache r - where kInd = kindOf ind - kElt = kindOf err - r st = do sws <- mapM (sbvToSW st) xs - swe <- sbvToSW st err - if all (== swe) sws -- off-chance that all elts are the same - then return swe - else do idx <- getTableIndex st kInd kElt sws - swi <- sbvToSW st ind - let len = length xs - newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) + _ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression" + select xsOrig err ind = xs `seq` SBV kElt (Right (cache r)) + where 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 of.. + xs = case kindOf ind of + KBounded False i -> genericTake ((2::Integer) ^ (fromIntegral i :: Integer)) xsOrig + KBounded True i -> genericTake ((2::Integer) ^ (fromIntegral (i-1) :: Integer)) xsOrig + KUnbounded -> xsOrig + _ -> error $ "SBV.select: unsupported " ++ show (kindOf ind) ++ " valued select/index expression" + r st = do sws <- mapM (sbvToSW st) xs + swe <- sbvToSW st err + if all (== swe) sws -- off-chance that all elts are the same + then return swe + else do idx <- getTableIndex st kInd kElt sws + swi <- sbvToSW st ind + let len = length xs + -- NB. No need to worry here that the index might be < 0; as the SMTLib translation takes care of that automatically + newExpr st kElt (SBVApp (LkUp (idx, kInd, kElt, len) swi swe) []) -- Unit instance Mergeable () where diff --git a/Data/SBV/BitVectors/SignCast.hs b/Data/SBV/BitVectors/SignCast.hs --- a/Data/SBV/BitVectors/SignCast.hs +++ b/Data/SBV/BitVectors/SignCast.hs @@ -88,7 +88,7 @@ KReal -> error "Data.SBV.SignCast.genericSign: Called on real value" KFloat -> error "Data.SBV.SignCast.genericSign: Called on float value" KDouble -> error "Data.SBV.SignCast.genericSign: Called on double value" - KUninterpreted s -> error $ "Data.SBV.SignCast.genericSign: Called on unintepreted sort " ++ s + KUserSort s _ -> error $ "Data.SBV.SignCast.genericSign: Called on unintepreted sort " ++ s y st = do xsw <- sbvToSW st x newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) @@ -105,7 +105,7 @@ KReal -> error "Data.SBV.SignCast.genericUnSign: Called on real value" KFloat -> error "Data.SBV.SignCast.genericUnSign: Called on float value" KDouble -> error "Data.SBV.SignCast.genericUnSign: Called on double value" - KUninterpreted s -> error $ "Data.SBV.SignCast.genericUnSign: Called on unintepreted sort " ++ s + KUserSort s _ -> error $ "Data.SBV.SignCast.genericUnSign: Called on unintepreted sort " ++ s y st = do xsw <- sbvToSW st x newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -161,13 +161,13 @@ -- | The printf specifier for the type specifier :: CgConfig -> SW -> Doc specifier cfg sw = case kindOf sw of - KBool -> spec (False, 1) - KBounded b i -> spec (b, i) - KUnbounded -> spec (True, fromJust (cgInteger cfg)) - KReal -> specF (fromJust (cgReal cfg)) - KFloat -> specF CgFloat - KDouble -> specF CgDouble - KUninterpreted s -> die $ "uninterpreted sort: " ++ s + KBool -> spec (False, 1) + KBounded b i -> spec (b, i) + KUnbounded -> spec (True, fromJust (cgInteger cfg)) + KReal -> specF (fromJust (cgReal cfg)) + KFloat -> specF CgFloat + KDouble -> specF CgDouble + KUserSort s _ -> die $ "uninterpreted sort: " ++ s where spec :: (Bool, Int) -> Doc spec (False, 1) = text "%d" spec (False, 8) = text "%\"PRIu8\"" @@ -411,7 +411,7 @@ = error "SBV->C: Cannot compile functions with existentially quantified variables." | True = [pre, header, post] - where usorts = [s | KUninterpreted s <- Set.toList kindInfo] + where usorts = [s | KUserSort s _ <- Set.toList kindInfo] pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */" $$ text "" $$ text "#include " @@ -439,14 +439,14 @@ $$ vcat (map text ls) $$ text "" typeWidth = getMax 0 [len (kindOf s) | (s, _) <- assignments] - where len (KReal{}) = 5 - len (KFloat{}) = 6 -- SFloat - len (KDouble{}) = 7 -- SDouble - len (KUnbounded{}) = 8 - len KBool = 5 -- SBool - len (KBounded False n) = 5 + length (show n) -- SWordN - len (KBounded True n) = 4 + length (show n) -- SIntN - len (KUninterpreted s) = die $ "Uninterpreted sort: " ++ s + where len (KReal{}) = 5 + len (KFloat{}) = 6 -- SFloat + len (KDouble{}) = 7 -- SDouble + len (KUnbounded{}) = 8 + len KBool = 5 -- SBool + len (KBounded False n) = 5 + length (show n) -- SWordN + len (KBounded True n) = 4 + length (show n) -- SIntN + len (KUserSort s _) = die $ "Uninterpreted sort: " ++ s getMax 8 _ = 8 -- 8 is the max we can get with SInteger, so don't bother looking any further getMax m [] = m getMax m (x:xs) = getMax (m `max` x) xs @@ -528,15 +528,15 @@ canOverflow True sz = (2::Integer)^(sz-1)-1 >= fromIntegral len canOverflow False sz = (2::Integer)^sz -1 >= fromIntegral len (needsCheckL, needsCheckR) = case k of - KBool -> (False, canOverflow False (1::Int)) - KBounded sg sz -> (sg, canOverflow sg sz) - KReal -> die "array index with real value" - KFloat -> die "array index with float value" - KDouble -> die "array index with double value" - KUnbounded -> case cgInteger cfg of - Nothing -> (True, True) -- won't matter, it'll be rejected later - Just i -> (True, canOverflow True i) - KUninterpreted s -> die $ "Uninterpreted sort: " ++ s + KBool -> (False, canOverflow False (1::Int)) + KBounded sg sz -> (sg, canOverflow sg sz) + KReal -> die "array index with real value" + KFloat -> die "array index with float value" + KDouble -> die "array index with double value" + KUnbounded -> case cgInteger cfg of + Nothing -> (True, True) -- won't matter, it'll be rejected later + Just i -> (True, canOverflow True i) + KUserSort s _ -> die $ "Uninterpreted sort: " ++ s -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior. -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ. diff --git a/Data/SBV/Examples/Misc/Enumerate.hs b/Data/SBV/Examples/Misc/Enumerate.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Misc/Enumerate.hs @@ -0,0 +1,91 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.Enumerate +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates how enumerations can be translated to their SMT-Lib +-- counterparts, without losing any information content. Also see +-- "Data.SBV.Examples.Puzzles.U2Bridge" for a more detailed +-- example involving enumerations. +----------------------------------------------------------------------------- + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.SBV.Examples.Misc.Enumerate where + +import Data.SBV +import Data.Generics + +-- | A simple enumerated type, that we'd like to translate to SMT-Lib intact; +-- i.e., this type will not be uninterpreted but rather preserved and will +-- be just like any other symbolic type SBV provides. Note the automatically +-- derived slew of classes we need: 'Eq', 'Ord', 'Data', 'Typeable', 'Read', +-- and 'Show'. For symbolic enumerated types, you should +-- always let GHC derive these instances. Aside from these, we also need +-- instances for 'SymWord', 'HasKind' and 'SatModel'. Again, the default definitions suffice +-- so the actual declarations are straightforward. +-- +-- Also note that we need to @import Data.Generics@ and have the @LANGUAGE@ +-- option @DeriveDataTypeable@ set. +data E = A | B | C + deriving (Eq, Ord, Data, Typeable, Read, Show) + +-- | The 'SymWord' instance for 'E'. In GHC 7.10 and forward, we'll be able to add these to the @deriving@ clause as well. +instance SymWord E + +-- | The 'HasKind' instance for 'E'. In GHC 7.10 and forward, we'll be able to add these to the @deriving@ clause as well. +instance HasKind E + +-- | The 'SatModel' instance for 'E'. In GHC 7.10 and forward, we'll be able to add these to the @deriving@ clause as well. +-- Note that the 'SatModel' instance is only needed if you use 'getModel' and its friends; but it does not hurt to always +-- derive the default definitions. +instance SatModel E + +-- | Give a name to the symbolic variants of 'E', for convenience +type SE = SBV E + +-- | Have the SMT solver enumerate the elements of the domain. We have: +-- +-- >>> elts +-- Solution #1: +-- s0 = A :: E +-- Solution #2: +-- s0 = B :: E +-- Solution #3: +-- s0 = C :: E +-- Found 3 different solutions. +elts :: IO AllSatResult +elts = allSat $ \(x::SE) -> x .== x + +-- | Shows that if we require 4 distinct elements of the type 'E', we shall fail; as +-- the domain only has three elements. We have: +-- +-- >>> four +-- Unsatisfiable +four :: IO SatResult +four = sat $ \a b c (d::SE) -> allDifferent [a, b, c, d] + +-- | Enumerations are automatically ordered, so we can ask for the maximum +-- element. Note the use of quantification. We have: +-- +-- >>> maxE +-- Satisfiable. Model: +-- maxE = C :: E +maxE :: IO SatResult +maxE = sat $ do mx <- exists "maxE" + e <- forall "e" + return $ mx .>= (e::SE) + +-- | Similarly, we get the minumum element. We have: +-- +-- >>> minE +-- Satisfiable. Model: +-- minE = A :: E +minE :: IO SatResult +minE = sat $ do mx <- exists "minE" + e <- forall "e" + return $ mx .<= (e::SE) diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -11,74 +11,88 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE DeriveDataTypeable #-} module Data.SBV.Examples.Puzzles.U2Bridge where import Control.Monad (unless) import Control.Monad.State (State, runState, put, get, modify, evalState) -import Data.Maybe (fromJust) +import Data.Generics import Data.SBV ------------------------------------------------------------- -- * Modeling the puzzle ------------------------------------------------------------- --- | U2 band members +-- | U2 band members. We want to translate this to SMT-Lib +-- as a data-type, and hence the deriving mechanism. data U2Member = Bono | Edge | Adam | Larry - deriving (Show, Enum) + deriving (Data, Typeable, Ord, Eq, Read, Show) --- | Model time using 32 bits -type Time = SWord32 +-- | Make 'U2Member' a valid symbolic element. In GHC 7.10; we'll be able to derive this automatically. +instance SymWord U2Member --- | Each member gets an 8-bit id -type SU2Member = SWord8 +-- | Make 'U2Member' have a default kind. In GHC 7.10; we'll be able to derive this automatically. +instance HasKind U2Member --- | Bono's ID -bono :: SU2Member -bono = fromIntegral . fromEnum $ Bono +-- | Make 'U2Member' part of model-generation facilities. In GHC 7.10; we'll be able to derive this automatically. +instance SatModel U2Member --- | Edge's ID -edge :: SU2Member -edge = fromIntegral . fromEnum $ Edge +-- | Symbolic shorthand for a 'U2Member' +type SU2Member = SBV U2Member --- | Adam's ID -adam :: SU2Member -adam = fromIntegral . fromEnum $ Adam +-- | Shorthands for symbolic versions of the members +bono, edge, adam, larry :: SU2Member +[bono, edge, adam, larry] = map literal [Bono, Edge, Adam, Larry] --- | Larry's ID -larry :: SU2Member -larry = fromIntegral . fromEnum $ Larry +-- | Model time using 32 bits +type Time = Word32 --- | Is this a valid person? -isU2Member :: SU2Member -> SBool -isU2Member = (.<= larry) -- 8 bits can represent 256 people; trim it down! +-- | Symbolic variant for time +type STime = SBV Time -- | Crossing times for each member of the band -crossTime :: SU2Member -> Time -crossTime = select [ 1 {- Bono -} - , 2 {- Edge -} - , 5 {- Adam -} - ] 10 {- Larry -} +crossTime :: U2Member -> Time +crossTime Bono = 1 +crossTime Edge = 2 +crossTime Adam = 5 +crossTime Larry = 10 +-- | The symbolic variant.. The duplication is unfortunate. +sCrossTime :: SU2Member -> STime +sCrossTime m = ite (m .== bono) (literal (crossTime Bono)) + $ ite (m .== edge) (literal (crossTime Edge)) + $ ite (m .== adam) (literal (crossTime Adam)) + (literal (crossTime Larry)) -- Must be Larry + -- | Location of the flash -type Location = SBool +data Location = Here | There + deriving (Data, Typeable, Ord, Eq, Read, Show) --- | We represent this side of the bridge as 'here', and arbitrarily as 'false' -here :: Location -here = false +-- | Make 'Location' a valid symbolic element. In GHC 7.10; we'll be able to derive this automatically. +instance SymWord Location --- | We represent other side of the bridge as 'there', and arbitrarily as 'true' -there :: Location -there = bnot here +-- | Make 'Location' have a default kind. In GHC 7.10; we'll be able to derive this automatically. +instance HasKind Location +-- | Make 'Location' part of model-generation facilities. In GHC 7.10; we'll be able to derive this automatically. +instance SatModel Location + +-- | Symbolic variant of 'Location' +type SLocation = SBV Location + +-- | Shorthands for symbolic versions of locations +here, there :: SLocation +[here, there] = map literal [Here, There] + -- | The status of the puzzle after each move -data Status = Status { time :: Time -- ^ elapsed time - , flash :: Location -- ^ location of the flash - , lBono :: Location -- ^ location of Bono - , lEdge :: Location -- ^ location of Edge - , lAdam :: Location -- ^ location of Adam - , lLarry :: Location -- ^ location of Larry +data Status = Status { time :: STime -- ^ elapsed time + , flash :: SLocation -- ^ location of the flash + , lBono :: SLocation -- ^ location of Bono + , lEdge :: SLocation -- ^ location of Edge + , lAdam :: SLocation -- ^ location of Adam + , lLarry :: SLocation -- ^ location of Larry } -- | Start configuration, time elapsed is 0 and everybody is 'here' @@ -121,30 +135,33 @@ return (f s) -- | Given an arbitrary member, return his location -whereIs :: SU2Member -> Move SBool -whereIs p = do [lb, le, la, ll] <- mapM peek [lBono, lEdge, lAdam, lLarry] - return $ select [lb, le, la] ll p +whereIs :: SU2Member -> Move SLocation +whereIs p = ite (p .== bono) (peek lBono) + $ ite (p .== edge) (peek lEdge) + $ ite (p .== adam) (peek lAdam) + (peek lLarry) -- | Transferring the flash to the other side xferFlash :: Move () -xferFlash = modify $ \s -> s{flash = bnot (flash s)} +xferFlash = modify $ \s -> s{flash = ite (flash s .== here) there here} -- | Transferring a person to the other side xferPerson :: SU2Member -> Move () xferPerson p = do [lb, le, la, ll] <- mapM peek [lBono, lEdge, lAdam, lLarry] - let lb' = ite (p .== bono) (bnot lb) lb - le' = ite (p .== edge) (bnot le) le - la' = ite (p .== adam) (bnot la) la - ll' = ite (p .== larry) (bnot ll) ll + let move l = ite (l .== here) there here + lb' = ite (p .== bono) (move lb) lb + le' = ite (p .== edge) (move le) le + la' = ite (p .== adam) (move la) la + ll' = ite (p .== larry) (move ll) ll modify $ \s -> s{lBono = lb', lEdge = le', lAdam = la', lLarry = ll'} -- | Increment the time, when only one person crosses bumpTime1 :: SU2Member -> Move () -bumpTime1 p = modify $ \s -> s{time = time s + crossTime p} +bumpTime1 p = modify $ \s -> s{time = time s + sCrossTime p} -- | Increment the time, when two people cross together bumpTime2 :: SU2Member -> SU2Member -> Move () -bumpTime2 p1 p2 = modify $ \s -> s{time = time s + crossTime p1 `smax` crossTime p2} +bumpTime2 p1 p2 = modify $ \s -> s{time = time s + sCrossTime p1 `smax` sCrossTime p2} -- | Symbolic version of 'when' whenS :: SBool -> Move () -> Move () @@ -192,22 +209,12 @@ -- | Check if a given sequence of actions is valid, i.e., they must all -- cross the bridge according to the rules and in less than 17 seconds isValid :: Actions -> SBool -isValid as = time end .<= 17 &&& bAll check as &&& zigZag there (map flash states) &&& bAll (.== there) [lBono end, lEdge end, lAdam end, lLarry end] - where check (s, p1, p2) = isU2Member p1 &&& isU2Member p2 - -- the following two conditions ensure we find distinct solutions - &&& (bnot s ==> p1 .> p2) -- for two person moves, ensure first person is "larger" - &&& (s ==> p2 .== bono) -- for one person moves, ensure second person is always "bono" +isValid as = time end .<= 17 &&& bAll check as &&& zigZag (cycle [there, here]) (map flash states) &&& bAll (.== there) [lBono end, lEdge end, lAdam end, lLarry end] + where check (s, p1, p2) = (bnot s ==> p1 .> p2) -- for two person moves, ensure first person is "larger" + &&& (s ==> p2 .== bono) -- for one person moves, ensure second person is always "bono" states = evalState (run as) start end = last states - zigZag _ [] = true - zigZag w (f:rest) = w .== f &&& zigZag (bnot w) rest - --- | The SatModel instance makes it easy to build models, mapping words to U2 members --- in the way we designated. -instance SatModel U2Member where - parseCWs as = cvtModel cvtCW $ parseCWs as - where cvtCW :: Word8 -> Maybe U2Member - cvtCW i = lookup i (zip [0..] [Bono, Edge, Adam, Larry]) + zigZag reqs locs = bAnd $ zipWith (.==) locs reqs ------------------------------------------------------------- -- * Solving the puzzle @@ -234,11 +241,10 @@ return () where lss = length ss go _ t [] = putStrLn $ "Total time: " ++ show t - go l t ((True, a, _):rest) = do putStrLn $ sh2 t ++ shL l ++ show a - go (not l) (t + ctime a) rest + go l t ((True, a, _):rest) = do putStrLn $ sh2 t ++ shL l ++ show a + go (not l) (t + crossTime a) rest go l t ((False, a, b):rest) = do putStrLn $ sh2 t ++ shL l ++ show a ++ ", " ++ show b - go (not l) (t + ctime a `max` ctime b) rest - ctime = fromJust . unliteral . crossTime . fromIntegral . fromEnum + go (not l) (t + crossTime a `max` crossTime b) rest sh2 t = let s = show t in if length s < 2 then ' ' : s else s shL False = " --> " shL True = " <-- " @@ -254,16 +260,16 @@ -- Checking for solutions with 5 moves. -- Solution #1: -- 0 --> Edge, Bono --- 2 <-- Edge --- 4 --> Larry, Adam --- 14 <-- Bono +-- 2 <-- Bono +-- 3 --> Larry, Adam +-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Solution #2: -- 0 --> Edge, Bono --- 2 <-- Bono --- 3 --> Larry, Adam --- 13 <-- Edge +-- 2 <-- Edge +-- 4 --> Larry, Adam +-- 14 <-- Bono -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves. diff --git a/Data/SBV/Examples/Uninterpreted/Deduce.hs b/Data/SBV/Examples/Uninterpreted/Deduce.hs --- a/Data/SBV/Examples/Uninterpreted/Deduce.hs +++ b/Data/SBV/Examples/Uninterpreted/Deduce.hs @@ -27,7 +27,9 @@ ----------------------------------------------------------------------------- -- | The uninterpreted sort 'B', corresponding to the carrier. -data B = B deriving (Eq, Ord, Data, Typeable) +-- To prevent SBV from translating it to an enumerated type, we simply attach an unused field +data B = B () + deriving (Eq, Ord, Data, Typeable, Read, Show) -- | Default instance declaration for 'SymWord' instance SymWord B diff --git a/Data/SBV/Examples/Uninterpreted/Sort.hs b/Data/SBV/Examples/Uninterpreted/Sort.hs --- a/Data/SBV/Examples/Uninterpreted/Sort.hs +++ b/Data/SBV/Examples/Uninterpreted/Sort.hs @@ -18,8 +18,9 @@ -- | A new data-type that we expect to use in an uninterpreted fashion -- in the backend SMT solver. Note the custom @deriving@ clause, which --- takes care of most of the boilerplate. -data Q = Q deriving (Eq, Ord, Data, Typeable) +-- takes care of most of the boilerplate. The () field is needed so +-- SBV will not translate it to an enumerated data-type +data Q = Q () deriving (Eq, Ord, Data, Typeable, Read, Show) -- | We need 'SymWord' and 'HasKind' instances, but default definitions -- are always sufficient for uninterpreted sorts, so all we do is to diff --git a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs --- a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs +++ b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -24,7 +24,7 @@ -- constructors. data L = Nil | Cons Int L - deriving (Eq, Ord, Data, Typeable) + deriving (Eq, Ord, Data, Typeable, Read, Show) -- | Declare instances to make 'L' a usable uninterpreted sort. First we need the -- 'SymWord' instance, with the default definition sufficing. diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -57,13 +57,15 @@ } } 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" - zero (KUninterpreted s) = error $ "SBV.CVC4.zero: Unexpected uninterpreted sort: " ++ s + 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) ++ "))\")" extract (Right (s, [])) = "(get-value (" ++ show s ++ "))" diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -56,13 +56,15 @@ } } 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" - zero (KUninterpreted s) = error $ "SBV.MathSAT.zero: Unexpected uninterpreted sort: " ++ s + 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 -- In the skolemMap: -- * Left's are universals: i.e., the model should be true for 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 @@ -371,7 +371,7 @@ 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 | KUninterpreted s <- Set.toList ki] + let usorts = [s | KUserSort s _ <- Set.toList ki] 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/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -72,13 +72,15 @@ 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 - zero _ (KUninterpreted s) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s + 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 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 @@ -11,6 +11,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DefaultSignatures #-} module Data.SBV.SMT.SMT where @@ -119,6 +120,10 @@ cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW]) cvtModel f x = x >>= \(a, r) -> f a >>= \b -> return (b, r) + default parseCWs :: Read a => [CW] -> Maybe (a, [CW]) + parseCWs (CW _ (CWUserSort (_, s)) : r) = Just (read s, r) + parseCWs _ = Nothing + -- | Parse a signed/sized value from a sequence of CWs genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r) @@ -249,7 +254,7 @@ -- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`. getModelUninterpretedValue :: String -> a -> Maybe String getModelUninterpretedValue v r = case v `M.lookup` getModelDictionary r of - Just (CW _ (CWUninterpreted s)) -> Just s + Just (CW _ (CWUserSort (_, s))) -> Just s _ -> Nothing -- | A simpler variant of 'getModel' to get a model out without the fuss. 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 @@ -60,7 +60,7 @@ = unsupported "uninterpreted sorts" | True = SMTLibPgm v (aliasTable, pre, post) - where sorts = [s | KUninterpreted s <- Set.toList kindInfo] + where sorts = [s | KUserSort s _ <- Set.toList kindInfo] unsupported w = error $ "SBV: Given problem needs " ++ w ++ ", which is not supported by SBV for the chosen solver: " ++ capSolverName solverCaps aliasTable = map (\(_, (x, y)) -> (y, x)) qinps converter = if v == SMTLib1 then SMT1.cvt else SMT2.cvt @@ -107,9 +107,11 @@ 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 extract (EApp [EApp [v, ENum i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) 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 = [(n, (nm, CW (kindOf s) (CWUninterpreted 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)))] extract (EApp [EApp [v, EFloat i]]) | Just (n, s, nm) <- getInput v, isFloat s = [(n, (nm, CW KFloat (CWFloat i)))] -- weird lambda app that CVC4 seems to throw out.. logic below derived from what I saw CVC4 print, hopefully sufficient @@ -118,3 +120,5 @@ ++ "\n\tInput: " ++ show line ++ "\n\tParse: " ++ show r extract _ = [] + +{-# ANN interpretSolverModelLine "HLint: ignore Use elemIndex" #-} diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -286,10 +286,10 @@ cvtType (SBVType xs) = unwords $ map kindType xs kindType :: Kind -> String -kindType KBool = "Bool" -kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]" -kindType KUnbounded = die "unbounded Integer" -kindType KReal = die "real value" -kindType KFloat = die "float value" -kindType KDouble = die "double value" -kindType (KUninterpreted s) = die $ "uninterpreted sort: " ++ s +kindType KBool = "Bool" +kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]" +kindType KUnbounded = die "unbounded Integer" +kindType KReal = die "real value" +kindType KFloat = die "float value" +kindType KDouble = die "double value" +kindType (KUserSort s _) = die $ "user sort: " ++ s 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 @@ -50,7 +50,9 @@ nonEqs :: RoundingMode -> [(String, CW)] -> [String] nonEqs rm scs = format $ interp ps ++ disallow (map eqClass uninterpClasses) - where (ups, ps) = partition (isUninterpreted . snd) scs + where isFree (KUserSort _ (Left _, _)) = True + isFree _ = False + (ups, ps) = partition (isFree . kindOf . snd) scs format [] = [] format [m] = ["(assert " ++ m ++ ")"] format (m:ms) = ["(assert (or " ++ m] @@ -58,7 +60,7 @@ ++ [" ))"] -- Regular (or interpreted) sorts simply get a constraint that we disallow the current assignment interp = map $ nonEq rm - -- Determine the equivalnce classes of uninterpreted sorts: + -- Determine the equivalence classes of uninterpreted sorts: uninterpClasses = filter (\l -> length l > 1) -- Only need this class if it has at least two members . map (map fst) -- throw away sorts, we only need the names . groupBy ((==) `on` snd) -- make sure they belong to the same sort and have the same value @@ -102,7 +104,7 @@ hasFloat = KFloat `Set.member` kindInfo hasDouble = KDouble `Set.member` kindInfo hasBVs = not $ null [() | KBounded{} <- Set.toList kindInfo] - sorts = [s | KUninterpreted s <- Set.toList kindInfo] + usorts = [(s, dt) | KUserSort s dt <- Set.toList kindInfo] logic | Just l <- smtLogic = ["(set-logic " ++ show l ++ ") ; NB. User specified."] @@ -110,9 +112,9 @@ = if hasBVs then ["(set-logic QF_FPABV)"] else ["(set-logic QF_FPA)"] - | hasInteger || hasReal || not (null sorts) + | hasInteger || hasReal || not (null usorts) = case mbDefaultLogic solverCaps of - Nothing -> ["; Has unbounded values (Int/Real) or sorts; no logic specified."] -- combination, let the solver pick + Nothing -> ["; Has unbounded values (Int/Real) or uninterpreted sorts; no logic specified."] -- combination, let the solver pick Just l -> ["(set-logic " ++ l ++ ")"] | True = ["(set-logic " ++ qs ++ as ++ ufs ++ "BV)"] @@ -130,7 +132,7 @@ ++ getModels ++ logic ++ [ "; --- uninterpreted sorts ---" ] - ++ map declSort sorts + ++ concatMap declSort usorts ++ [ "; --- literal constants ---" ] ++ concatMap (declConst (supportsMacros solverCaps)) consts ++ [ "; --- skolem constants ---" ] @@ -187,10 +189,16 @@ , "(assert (= " ++ show s ++ " " ++ cvtCW rm c ++ "))" ] where varT = show s ++ " " ++ swFunType [] s - declSort s = "(declare-sort " ++ s ++ " 0)" userName s = case s `lookup` map snd inputs of Just u | show s /= u -> " ; tracks user variable " ++ show u _ -> "" + 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) ++ ")" declUI :: (String, SBVType) -> [String] declUI (i, t) = ["(declare-fun " ++ i ++ " " ++ cvtType t ++ ")"] @@ -265,13 +273,13 @@ swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s smtType :: Kind -> String -smtType KBool = "Bool" -smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" -smtType KUnbounded = "Int" -smtType KReal = "Real" -smtType KFloat = "(_ FloatingPoint 8 24)" -smtType KDouble = "(_ FloatingPoint 11 53)" -smtType (KUninterpreted s) = s +smtType KBool = "Bool" +smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" +smtType KUnbounded = "Int" +smtType KReal = "Real" +smtType KFloat = "(_ FloatingPoint 8 24)" +smtType KDouble = "(_ FloatingPoint 11 53)" +smtType (KUserSort s _) = s cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!" @@ -301,17 +309,17 @@ cvtCW :: RoundingMode -> CW -> String cvtCW rm x - | isBoolean x, CWInteger w <- cwVal x = if w == 0 then "false" else "true" - | isUninterpreted x, CWUninterpreted 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 + | 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) + | 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) @@ -333,12 +341,12 @@ cvtExp :: RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr where ssw = cvtSW skolemMap - bvOp = all isBounded arguments - intOp = any isInteger arguments - realOp = any isReal arguments - doubleOp = any isDouble arguments - floatOp = any isFloat arguments - boolOp = all isBoolean arguments + bvOp = all isBounded arguments + intOp = any isInteger arguments + realOp = any isReal arguments + doubleOp = any isDouble arguments + floatOp = any isFloat arguments + boolOp = all isBoolean arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr ensureBVOrBool = bvOp || boolOp || bad @@ -381,6 +389,10 @@ lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn lift2Cmp o fo | doubleOp || floatOp = lift2 fo | True = lift2 o + unintComp o [a, b] + | 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 ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) sh (SBVApp Ite [a, b, c]) = "(ite " ++ ssw a ++ " " ++ ssw b ++ " " ++ ssw c ++ ")" @@ -388,25 +400,25 @@ | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")" | True = lkUp where needsCheck = case aKnd of - KBool -> (2::Integer) > fromIntegral l - KBounded _ n -> (2::Integer)^n > fromIntegral l - KUnbounded -> True - KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" - KFloat -> error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index" - KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" - KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s + KBool -> (2::Integer) > fromIntegral l + KBounded _ n -> (2::Integer)^n > fromIntegral l + KUnbounded -> True + KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" + KFloat -> error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index" + KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" + KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")" cond | hasSign i = "(or " ++ le0 ++ " " ++ gtl ++ ") " | True = gtl ++ " " (less, leq) = case aKnd of - KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index" - KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") - KUnbounded -> ("<", "<=") - KReal -> ("<", "<=") - KFloat -> ("fp.lt", "fp.leq") - KDouble -> ("fp.lt", "fp.geq") - KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s + KBool -> error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index" + KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") + KUnbounded -> ("<", "<=") + KReal -> ("<", "<=") + KFloat -> ("fp.lt", "fp.leq") + KDouble -> ("fp.lt", "fp.geq") + KUserSort s _ -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s mkCnst = cvtCW rm . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")" @@ -514,9 +526,13 @@ , (LessEq, lift2Cmp "<=" "fp.leq") , (GreaterEq, lift2Cmp ">=" "fp.geq") ] - -- equality is the only thing that works on uninterpreted sorts - uninterpretedTable = [ (Equal, lift2S "=" "=" True) - , (NotEqual, lift2S "distinct" "distinct" True) + -- equality and comparisons are the only thing that works on uninterpreted sorts + uninterpretedTable = [ (Equal, lift2S "=" "=" True) + , (NotEqual, lift2S "distinct" "distinct" True) + , (LessThan, unintComp "<") + , (GreaterThan, unintComp ">") + , (LessEq, unintComp "<=") + , (GreaterEq, unintComp ">=") ] rot :: (SW -> String) -> String -> Int -> SW -> String 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 @@ -124,7 +124,7 @@ KFloat -> "Float" KDouble -> "Double" KReal -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw - KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us + KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw s cw = case cwKind cw of KBool -> take 5 (show (cwToBool cw) ++ repeat ' ') @@ -133,7 +133,7 @@ KFloat -> let CWFloat w = cwVal cw in showHFloat w KDouble -> let CWDouble w = cwVal cw in showHDouble w KReal -> let CWAlgReal w = cwVal cw in algRealToHaskell w - KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us + KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us c :: String -> [([CW], [CW])] -> String c n vs = intercalate "\n" $ @@ -211,17 +211,17 @@ KDouble -> "SDouble" KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases." KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." - KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us + 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 - 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 - KFloat -> let CWFloat w = cwVal cw in showCFloat w - KDouble -> let CWDouble w = cwVal cw in showCDouble w - KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us - KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." + 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 + KFloat -> let CWFloat w = cwVal cw in showCFloat w + KDouble -> let CWDouble w = cwVal cw in showCDouble w + KUserSort us _ -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us + KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." outLine | null vs = "printf(\"\");" | True = "printf(\"%*d. " ++ fmtString ++ "\\n\", " ++ show (length (show (length vs - 1))) ++ ", i" @@ -281,11 +281,11 @@ KReal -> error "SBV.renderTest: Real values are not supported when generating Forte test-cases." KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating Forte test-cases." _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw - xlt s (CWInteger v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]] - xlt _ (CWFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r - xlt _ (CWDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r - xlt _ (CWAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r - xlt _ (CWUninterpreted r) = error $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " ++ show r + xlt s (CWInteger v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]] + xlt _ (CWFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r + xlt _ (CWDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r + xlt _ (CWAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r + xlt _ (CWUserSort r) = error $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " ++ show r mkLine (i, o) = "(" ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")" mkTuple [] = "()" mkTuple [x] = x diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2014, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without 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 = 1 :: SWord8 - s2 = 0 :: SWord8 + s1 = Edge :: U2Member + s2 = Bono :: U2Member s3 = True - s4 = 1 :: SWord8 - s5 = 0 :: SWord8 + s4 = Bono :: U2Member + s5 = Bono :: U2Member s6 = False - s7 = 3 :: SWord8 - s8 = 2 :: SWord8 + s7 = Larry :: U2Member + s8 = Adam :: U2Member s9 = True - s10 = 0 :: SWord8 - s11 = 0 :: SWord8 + s10 = Edge :: U2Member + s11 = Bono :: U2Member s12 = False - s13 = 1 :: SWord8 - s14 = 0 :: SWord8 + s13 = Edge :: U2Member + s14 = Bono :: U2Member 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 = "Sun Dec 21 15:07:02 PST 2014" +buildTime = "Thu Jan 15 19:08:18 PST 2015" diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs b/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs @@ -23,7 +23,7 @@ ] -- Example provided by Thomas DuBuisson: -data Bitstring = Bitstring deriving (Eq, Ord, Data, Typeable) +data Bitstring = Bitstring () deriving (Eq, Ord, Data, Typeable, Read, Show) instance SymWord Bitstring instance HasKind Bitstring type SBitstring = SBV Bitstring diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs b/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs @@ -23,7 +23,7 @@ "unint-sort" ~: assert . (==4) . length . (extractModels :: AllSatResult -> [L]) =<< allSat p0 ] -data L = Nil | Cons Int L deriving (Eq, Ord, Data, Typeable) +data L = Nil | Cons Int L deriving (Eq, Ord, Data, Typeable, Read, Show) instance SymWord L instance HasKind L instance SatModel L where diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 3.4 +Version: 3.5 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 @@ -9,7 +9,7 @@ . Release notes: -Copyright: Levent Erkok, 2010-2014 +Copyright: Levent Erkok, 2010-2015 License: BSD3 License-file: LICENSE Stability: Experimental @@ -70,6 +70,7 @@ , Data.SBV.Examples.Crypto.RC4 , Data.SBV.Examples.Existentials.CRCPolynomial , Data.SBV.Examples.Existentials.Diophantine + , Data.SBV.Examples.Misc.Enumerate , Data.SBV.Examples.Misc.Floating , Data.SBV.Examples.Misc.SBranch , Data.SBV.Examples.Misc.ModelExtract