sbv 0.9.2 → 0.9.3
raw patch · 51 files changed
+567/−141 lines, 51 filessetup-changed
Files
- Data/SBV.hs +4/−0
- Data/SBV/BitVectors/Bit.hs +2/−2
- Data/SBV/BitVectors/Data.hs +53/−19
- Data/SBV/BitVectors/Model.hs +166/−7
- Data/SBV/BitVectors/Polynomial.hs +4/−4
- Data/SBV/BitVectors/PrettyNum.hs +6/−6
- Data/SBV/BitVectors/Splittable.hs +2/−2
- Data/SBV/Examples/Basics/UnsafeFunctionEquality.hs +2/−1
- Data/SBV/Examples/BitPrecise/Legato.hs +2/−1
- Data/SBV/Examples/CRC/CCITT_Unidir.hs +0/−1
- Data/SBV/Examples/Puzzles/MagicSquare.hs +2/−1
- Data/SBV/Examples/Puzzles/Sudoku.hs +3/−2
- Data/SBV/Examples/Puzzles/U2Bridge.hs +3/−2
- Data/SBV/Examples/Uninterpreted/AUF.hs +54/−0
- Data/SBV/Examples/Uninterpreted/Uninterpreted.hs +30/−0
- Data/SBV/Internals.hs +1/−1
- Data/SBV/Provers/Prover.hs +6/−6
- Data/SBV/Provers/SExpr.hs +3/−3
- Data/SBV/Provers/Yices.hs +5/−4
- Data/SBV/SMT/SMT.hs +10/−9
- Data/SBV/SMT/SMTLib.hs +37/−25
- Data/SBV/TestSuite/Uninterpreted/AUF.hs +25/−0
- Data/SBV/TestSuite/Uninterpreted/Uninterpreted.hs +25/−0
- Data/SBV/Utils/SBVTest.hs +2/−2
- Data/SBV/Utils/TDiff.hs +3/−3
- README +5/−4
- SBVUnitTest/GoldFiles/auf-1.gold +29/−0
- SBVUnitTest/GoldFiles/basic-2_1.gold +1/−0
- SBVUnitTest/GoldFiles/basic-2_2.gold +1/−0
- SBVUnitTest/GoldFiles/basic-2_3.gold +1/−0
- SBVUnitTest/GoldFiles/basic-2_4.gold +1/−0
- SBVUnitTest/GoldFiles/basic-3_1.gold +1/−0
- SBVUnitTest/GoldFiles/basic-3_2.gold +1/−0
- SBVUnitTest/GoldFiles/basic-3_3.gold +1/−0
- SBVUnitTest/GoldFiles/basic-3_4.gold +1/−0
- SBVUnitTest/GoldFiles/basic-3_5.gold +1/−0
- SBVUnitTest/GoldFiles/basic-4_1.gold +1/−0
- SBVUnitTest/GoldFiles/basic-4_2.gold +1/−0
- SBVUnitTest/GoldFiles/basic-4_3.gold +1/−0
- SBVUnitTest/GoldFiles/basic-4_4.gold +1/−0
- SBVUnitTest/GoldFiles/basic-4_5.gold +1/−0
- SBVUnitTest/GoldFiles/basic-5_1.gold +1/−0
- SBVUnitTest/GoldFiles/basic-5_2.gold +1/−0
- SBVUnitTest/GoldFiles/basic-5_3.gold +1/−0
- SBVUnitTest/GoldFiles/basic-5_4.gold +1/−0
- SBVUnitTest/GoldFiles/basic-5_5.gold +1/−0
- SBVUnitTest/GoldFiles/ccitt.gold +1/−0
- SBVUnitTest/GoldFiles/legato.gold +1/−0
- SBVUnitTest/SBVUnitTest.hs +42/−22
- Setup.hs +12/−11
- sbv.cabal +8/−3
Data/SBV.hs view
@@ -46,6 +46,8 @@ -- -- * Symbolic polynomials over GF(2^n), and polynomial arithmetic --+-- * Uninterpreted constants and functions over symbolic values+-- -- The user can construct ordinary Haskell programs using these types, which behave -- very similar to their concrete counterparts. In particular these types belong to the -- standard classes 'Num', 'Bits', custom versions of 'Eq' ('EqSymbolic') @@ -125,6 +127,8 @@ , bAnd, bOr, bAny, bAll -- ** Pretty-printing and reading numbers in Hex & Binary , PrettyNum(..), readBin+ -- * Uninterpreted constants and functions+ , Uninterpreted(..) -- * Proving properties -- $proveIntro
Data/SBV/BitVectors/Bit.hs view
@@ -12,8 +12,8 @@ module Data.SBV.BitVectors.Bit where -import Data.Bits-import Control.DeepSeq(NFData(..))+import Control.DeepSeq (NFData(..))+import Data.Bits (Bits(..)) data Bit = Zero | One deriving (Eq, Ord)
Data/SBV/BitVectors/Data.hs view
@@ -31,25 +31,27 @@ , SBVExpr(..), newExpr , cache, uncache, HasSignAndSize(..) , Op(..), NamedSymVar, getTableIndex, Pgm, Symbolic, runSymbolic, State, Size, output, Result(..)+ , SBVType(..), newUninterpreted ) where -import Control.Monad.Reader-import Control.DeepSeq(NFData(..))-import Data.Bits-import Data.Int-import Data.Word-import qualified Data.Foldable as F-import qualified Data.Sequence as S-import Data.SBV.BitVectors.Bit+import Control.DeepSeq (NFData(..))+import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)+import Control.Monad.Trans (MonadIO, liftIO)+import Data.Bits (Bits(..))+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.IORef-import Data.List(intercalate, sortBy)-import qualified Data.Map as Map-import qualified Data.IntMap as IMap+import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, insert)+import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup)+import qualified Data.Foldable as F (toList)+import qualified Data.Sequence as S (Seq, empty, (|>)) -import Test.QuickCheck hiding(Result, output)+import System.IO.Unsafe (unsafePerformIO) -- see the note at the bottom of the file+import Test.QuickCheck (Testable(..)) -import System.IO.Unsafe -- see the note at the bottom of the file+import Data.SBV.BitVectors.Bit -- | 'CW' represents a concrete word of a fixed size: -- The unsigned variants are: 'W1', 'W8', 'W16', 'W32', and 'W64'@@ -70,6 +72,15 @@ falseSW = SW (False, 1) $ NodeId (-2) trueSW = SW (False, 1) $ NodeId (-1) +newtype SBVType = SBVType [(Bool, Size)]+ deriving (Eq, Ord)++instance Show SBVType where+ show (SBVType []) = error "SBV: internal error, empty SBVType"+ show (SBVType xs) = intercalate " -> " $ map sh xs+ where sh (False, 1) = "SBool"+ sh (s, sz) = (if s then "SInt" else "SWord") ++ show sz+ data Op = Plus | Times | Minus | Quot | Rem -- quot and rem are unsigned only | Equal | NotEqual@@ -82,6 +93,7 @@ | LkUp (Int, Int, Int, Int) !SW !SW -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value | ArrEq Int Int | ArrRead Int+ | Uninterpreted String deriving (Eq, Ord) data SBVExpr = SBVApp {-# UNPACK #-} !Op {-# UNPACK #-} ![SW] deriving (Eq, Ord)@@ -178,6 +190,7 @@ where tinfo = "table" ++ show ti ++ "(" ++ show at ++ " -> " ++ show rt ++ ", " ++ show l ++ ")" show (ArrEq i j) = "array" ++ show i ++ " == array" ++ show j show (ArrRead i) = "select array" ++ show i+ show (Uninterpreted i) = "ui_" ++ i show op | Just s <- op `lookup` syms = s | True = error "impossible happened; can't find op!"@@ -218,14 +231,15 @@ [(SW, CW)] -- constants [((Int, Int, Int), [SW])] -- tables (automatically constructed) [(Int, ArrayInfo)] -- arrays (user specified)+ [(String, SBVType)] -- uninterpreted constants Pgm -- assignments [SW] -- outputs instance Show Result where- show (Result _ cs _ _ _ [r])+ show (Result _ cs _ _ [] _ [r]) | Just c <- r `lookup` cs = show c- show (Result is cs ts as xs os) = intercalate "\n" $+ show (Result is cs ts as uis xs os) = intercalate "\n" $ ["INPUTS"] ++ map shn is ++ ["CONSTANTS"]@@ -234,6 +248,8 @@ ++ map sht ts ++ ["ARRAYS"] ++ map sha as+ ++ ["UNINTERPRETED CONSTANTS"]+ ++ map shui uis ++ ["DEFINE"] ++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList xs) ++ ["OUTPUTS"]@@ -253,6 +269,7 @@ ni = "array" ++ show i alias | ni == nm = "" | True = ", aliasing " ++ show nm+ shui (nm, t) = " ui_" ++ nm ++ " :: " ++ show t data ArrayContext = ArrayFree | ArrayInit SW@@ -270,6 +287,7 @@ type TableMap = Map.Map [SW] (Int, Int, Int) type ArrayInfo = (String, ((Bool, Size), (Bool, Size)), ArrayContext) type ArrayMap = IMap.IntMap ArrayInfo+type UIMap = Map.Map String SBVType data State = State { rctr :: IORef Int , rinps :: IORef [NamedSymVar]@@ -279,6 +297,7 @@ , rconstMap :: IORef CnstMap , rexprMap :: IORef ExprMap , rArrayMap :: IORef ArrayMap+ , rUIMap :: IORef UIMap } -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic@@ -335,6 +354,17 @@ i `seq` writeIORef (rctr s) i return ctr +newUninterpreted :: State -> String -> SBVType -> IO ()+newUninterpreted st nm t = do+ uiMap <- readIORef (rUIMap st)+ case nm `Map.lookup` uiMap of+ Just t' -> if t /= t'+ then error $ "Uninterpreted constant " ++ nm ++ " used at incompatible types\n"+ ++ " Current type : " ++ show t ++ "\n"+ ++ " Previously used at: " ++ show t'+ else return ()+ Nothing -> modifyIORef (rUIMap st) (Map.insert nm t)+ -- Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW newConst st c = do@@ -429,6 +459,7 @@ outs <- newIORef [] tables <- newIORef Map.empty arrays <- newIORef IMap.empty+ uis <- newIORef Map.empty let st = State { rctr = ctr , rinps = inps , routs = outs@@ -437,6 +468,7 @@ , rconstMap = cmap , rArrayMap = arrays , rexprMap = emap+ , rUIMap = uis } _ <- newConst st $ W1 Zero -- s(-2) == falseSW _ <- newConst st $ W1 One -- s(-1) == trueSW@@ -449,7 +481,8 @@ cnsts <- (sortBy cmp . map swap . Map.toList) `fmap` readIORef (rconstMap st) tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables arrs <- IMap.toAscList `fmap` readIORef arrays- return $ Result (reverse inpsR) cnsts tbls arrs rpgm (reverse outsR)+ unint <- Map.toList `fmap` readIORef uis+ return $ Result (reverse inpsR) cnsts tbls arrs unint rpgm (reverse outsR) ------------------------------------------------------------------------------- -- * Symbolic Words@@ -614,13 +647,14 @@ rnf (I64 w) = rnf w `seq` () instance NFData Result where- rnf (Result inps consts tbls arrs pgm outs) = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf pgm `seq` rnf outs+ rnf (Result inps consts tbls arrs uis pgm outs) = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf pgm `seq` rnf outs instance NFData ArrayContext instance NFData Pgm instance NFData SW+instance NFData SBVType -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where property (SBV _ (Left (W1 b))) = property . bit2Bool $ b- property s = error $ "BV.Testable.SBool: impossible: quickcheck with non-constant bit: " ++ show s+ property s = error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show s ++ ")"
Data/SBV/BitVectors/Model.hs view
@@ -20,21 +20,22 @@ {-# LANGUAGE FunctionalDependencies #-} module Data.SBV.BitVectors.Model (- Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..)+ Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..) , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE , lsb, msb ) where -import Data.Array-import Data.Bits-import Data.Int-import Data.List(genericLength, genericIndex, genericSplitAt, unzip4, unzip5, unzip6, unzip7)-import Data.Word+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, genericSplitAt, unzip4, unzip5, unzip6, unzip7)+import Data.Word (Word8, Word16, Word32, Word64)+import Test.QuickCheck (Arbitrary(..))+ import Data.SBV.BitVectors.Bit import Data.SBV.BitVectors.Data import Data.SBV.Utils.Boolean-import Test.QuickCheck hiding((.&.), Result, (==>)) liftSym1 :: (State -> (Bool, Size) -> SW -> IO SW) -> (forall a. (Ord a, Bits a) => a -> a) -> SBV b -> SBV b liftSym1 _ opC (SBV sgnsz (Left a)) = SBV sgnsz $ Left $ mapCW opC a@@ -633,3 +634,161 @@ instance SymWord b => Mergeable (SFunArray a b) where symbolicMerge = mergeArrays++-- | Uninterpreted constants and functions. An uninterpreted constant is+-- a value that is indexed by its name. The only property the prover assumes+-- about these values are that they are equivalent to themselves; i.e., (for+-- functions) they return the same results when applied to same arguments.+-- We support uninterpreted-functions as a general means of black-box'ing+-- operations that are "irrelevant" for the purposes of the proof; i.e., when+-- the proofs can be performed without any knowledge about the function itself.+--+-- Minimal complete definition: 'uninterpret'. However, most instances in+-- practice are already provided by SBV, so end-users should not need to define their+-- own instances.+class Uninterpreted a where+ uninterpret :: String -> a++-- Plain constants+instance HasSignAndSize a => Uninterpreted (SBV a) where+ uninterpret nm = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ result st = do newUninterpreted st nm (SBVType [sgnsza])+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) []++-- Functions of one argument+instance (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) where+ uninterpret nm arg0 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ result st = do newUninterpreted st nm (SBVType [sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]++-- Functions of two arguments+instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ result st = do newUninterpreted st nm (SBVType [sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]++-- Functions of three arguments+instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 arg2 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ result st = do newUninterpreted st nm (SBVType [sgnszd, sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ sw2 <- sbvToSW st arg2+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]++-- Functions of four arguments+instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 arg2 arg3 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))+ result st = do newUninterpreted st nm (SBVType [sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ sw2 <- sbvToSW st arg2+ sw3 <- sbvToSW st arg3+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]++-- Functions of five arguments+instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 arg2 arg3 arg4 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))+ sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))+ result st = do newUninterpreted st nm (SBVType [sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ sw2 <- sbvToSW st arg2+ sw3 <- sbvToSW st arg3+ sw4 <- sbvToSW st arg4+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]++-- Functions of six arguments+instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))+ sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))+ sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))+ result st = do newUninterpreted st nm (SBVType [sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ sw2 <- sbvToSW st arg2+ sw3 <- sbvToSW st arg3+ sw4 <- sbvToSW st arg4+ sw5 <- sbvToSW st arg5+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]++-- Functions of seven arguments+instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) where+ uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 arg6 = SBV sgnsza $ Right $ cache result+ where sgnsza = (hasSign (undefined :: a), sizeOf (undefined :: a))+ sgnszb = (hasSign (undefined :: b), sizeOf (undefined :: b))+ sgnszc = (hasSign (undefined :: c), sizeOf (undefined :: c))+ sgnszd = (hasSign (undefined :: d), sizeOf (undefined :: d))+ sgnsze = (hasSign (undefined :: e), sizeOf (undefined :: e))+ sgnszf = (hasSign (undefined :: f), sizeOf (undefined :: f))+ sgnszg = (hasSign (undefined :: g), sizeOf (undefined :: g))+ sgnszh = (hasSign (undefined :: h), sizeOf (undefined :: h))+ result st = do newUninterpreted st nm (SBVType [sgnszh, sgnszg, sgnszf, sgnsze, sgnszd, sgnszc, sgnszb, sgnsza])+ sw0 <- sbvToSW st arg0+ sw1 <- sbvToSW st arg1+ sw2 <- sbvToSW st arg2+ sw3 <- sbvToSW st arg3+ sw4 <- sbvToSW st arg4+ sw5 <- sbvToSW st arg5+ sw6 <- sbvToSW st arg6+ newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]++-- Uncurried functions of two arguments+instance (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1) = uninterpret nm arg0 arg1++-- Uncurried functions of three arguments+instance (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1, arg2) = uninterpret nm arg0 arg1 arg2++-- Uncurried functions of four arguments+instance (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1, arg2, arg3) = uninterpret nm arg0 arg1 arg2 arg3++-- Uncurried functions of five arguments+instance (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1, arg2, arg3, arg4) = uninterpret nm arg0 arg1 arg2 arg3 arg4++-- Uncurried functions of six arguments+instance (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1, arg2, arg3, arg4, arg5) = uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5++-- Uncurried functions of seven arguments+instance (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a)+ => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) where+ uninterpret nm (arg0, arg1, arg2, arg3, arg4, arg5, arg6) = uninterpret nm arg0 arg1 arg2 arg3 arg4 arg5 arg6
Data/SBV/BitVectors/Polynomial.hs view
@@ -16,10 +16,10 @@ module Data.SBV.BitVectors.Polynomial (Polynomial(..)) where -import Data.Bits-import Data.List(genericTake)-import Data.Maybe(fromJust)-import Data.Word+import Data.Bits (Bits(..))+import Data.List (genericTake)+import Data.Maybe (fromJust)+import Data.Word (Word8, Word16, Word32, Word64) import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model
Data/SBV/BitVectors/PrettyNum.hs view
@@ -16,12 +16,12 @@ module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin) where -import Data.Maybe(fromJust)-import Data.Char(ord)-import Data.List(isPrefixOf)-import Data.Int-import Data.Word-import Numeric+import Data.Char (ord)+import Data.Int (Int8, Int16, Int32, Int64)+import Data.List (isPrefixOf)+import Data.Maybe (fromJust)+import Data.Word (Word8, Word16, Word32, Word64)+import Numeric (showIntAtBase, showHex, readInt) import Data.SBV.BitVectors.Bit import Data.SBV.BitVectors.Data
Data/SBV/BitVectors/Splittable.hs view
@@ -18,8 +18,8 @@ module Data.SBV.BitVectors.Splittable (Splittable(..), FromBits(..)) where -import Data.Bits-import Data.Word+import Data.Bits (Bits(..))+import Data.Word (Word8, Word16, Word32, Word64) import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model
Data/SBV/Examples/Basics/UnsafeFunctionEquality.hs view
@@ -19,7 +19,8 @@ module Data.SBV.Examples.Basics.UnsafeFunctionEquality where -import System.IO.Unsafe+import System.IO.Unsafe (unsafePerformIO)+ import Data.SBV instance Equality (a -> b) => Eq (a -> b) where
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -40,7 +40,8 @@ module Data.SBV.Examples.BitPrecise.Legato where -import Data.Array+import Data.Array (Array, Ix(..), (!), (//), array)+ import Data.SBV ------------------------------------------------------------------
Data/SBV/Examples/CRC/CCITT_Unidir.hs view
@@ -13,7 +13,6 @@ module Data.SBV.Examples.CRC.CCITT_Unidir where - import Data.SBV -- We don't have native support for 48 bits in Data.SBV
Data/SBV/Examples/Puzzles/MagicSquare.hs view
@@ -14,7 +14,8 @@ module Data.SBV.Examples.Puzzles.MagicSquare where -import Data.List+import Data.List (genericLength, transpose)+ import Data.SBV -- | Use 32-bit words for elements.
Data/SBV/Examples/Puzzles/Sudoku.hs view
@@ -12,8 +12,9 @@ module Data.SBV.Examples.Puzzles.Sudoku where -import Data.List-import Data.Maybe(fromJust)+import Data.List (transpose)+import Data.Maybe (fromJust)+ import Data.SBV -------------------------------------------------------------------
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -16,8 +16,9 @@ module Data.SBV.Examples.Puzzles.U2Bridge where -import Data.Maybe(fromJust)-import Control.Monad.State+import Control.Monad.State (State, runState, put, get, modify, evalState)+import Data.Maybe (fromJust)+ import Data.SBV -------------------------------------------------------------
+ Data/SBV/Examples/Uninterpreted/AUF.hs view
@@ -0,0 +1,54 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Uninterpreted.AUF+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Formalizes and proves the following theorem, about arithmetic,+-- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf>+-- slide number 24):+--+-- @+-- x + 2 = y implies f (read (write (a, x, 3), y - 2)) = f (y - x + 1)+-- @+--+-- We interpret the types as follows (other interpretations certainly possible):+--+-- [/x/] 'SWord32' (32-bit unsigned address)+--+-- [/y/] 'SWord32' (32-bit unsigned address)+--+-- [/a/] An array, indexed by 32-bit addresses, returning 32-bit unsigned integers+--+-- [/f/] An uninterpreted function of type @'SWord32' -> 'SWord64'@+--+-- The function @read@ and @write@ are usual array operations.+-----------------------------------------------------------------------------++module Data.SBV.Examples.Uninterpreted.AUF where++import Data.SBV++-- | The array type, takes symbolic 32-bit unsigned indexes+-- and stores 32-bit unsigned symbolic values+type A = SFunArray Word32 Word32++-- | Uninterpreted function in the theorem+f :: SWord32 -> SWord64+f = uninterpret "f"++-- | Correctness theorem. We state it for all values of @x@, @y@, and +-- the array @a@. We also take an arbitrary initializer for the array.+thm :: SWord32 -> SWord32 -> A -> SWord32 -> SBool+thm x y a initVal = lhs ==> rhs+ where a' = resetArray a initVal -- initialize array+ lhs = x + 2 .== y+ rhs = f (readArray (writeArray a' x 3) (y - 2))+ .== f (y - x + 1)++-- | Prints Q.E.D. when run, as expected+proveThm :: IO ()+proveThm = print =<< prove thm
+ Data/SBV/Examples/Uninterpreted/Uninterpreted.hs view
@@ -0,0 +1,30 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Uninterpreted.Uninterpreted+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Testing uninterpreted functions+-----------------------------------------------------------------------------++module Data.SBV.Examples.Uninterpreted.Uninterpreted where++import Data.SBV++f :: SInt8 -> SWord32+f = uninterpret "f"++g :: SInt8 -> SWord16 -> SWord32+g = uninterpret "g"++p0 :: SInt8 -> SInt8 -> SBool+p0 x y = x .== y ==> f x .== f y -- OK++p1 :: SInt8 -> SWord16 -> SWord16 -> SBool+p1 x y z = y .== z ==> g x y .== g x z -- OK++p2 :: SInt8 -> SWord16 -> SWord16 -> SBool+p2 x y z = y .== z ==> g x y .== f x -- Not true
Data/SBV/Internals.hs view
@@ -20,7 +20,7 @@ , module Data.SBV.Utils.SBVTest ) where -import Data.SBV.BitVectors.Data(Result, runSymbolic, SBV(..))+import Data.SBV.BitVectors.Data (Result, runSymbolic, SBV(..)) import Data.SBV.Utils.SBVTest {- $testFramework
Data/SBV/Provers/Prover.hs view
@@ -33,10 +33,10 @@ ) where -import Control.Monad(when)-import Control.Concurrent(forkIO)-import Control.Concurrent.Chan.Strict-import Data.Maybe(fromJust, isJust)+import Control.Monad (when)+import Control.Concurrent (forkIO)+import Control.Concurrent.Chan.Strict (newChan, writeChan, getChanContents)+import Data.Maybe (fromJust, isJust) import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model@@ -282,8 +282,8 @@ msg $ "Generated symbolic trace:\n" ++ show res msg "Translating to SMT-Lib.." case res of- Result is consts tbls arrs pgm [o@(SW{})] -> timeIf isTiming "translation" $ return (is, toSMTLib isSat is consts tbls arrs pgm o)- _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res+ Result is consts tbls arrs uis pgm [o@(SW{})] -> timeIf isTiming "translation" $ return (is, toSMTLib isSat is consts tbls arrs uis pgm o)+ _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res -- | Equality as a proof method. Allows for -- very concise construction of equivalence proofs, which is very typical in
Data/SBV/Provers/SExpr.hs view
@@ -12,9 +12,9 @@ module Data.SBV.Provers.SExpr where -import Control.Monad.Error() -- for Monad (Either String) instance-import Data.Char (isDigit, ord)-import Numeric+import Control.Monad.Error () -- for Monad (Either String) instance+import Data.Char (isDigit, ord)+import Numeric (readInt, readDec) data SExpr = S_Con String | S_Num Integer
Data/SBV/Provers/Yices.hs view
@@ -14,12 +14,13 @@ module Data.SBV.Provers.Yices(yices, timeout) where -import Data.Char(isDigit)-import Data.List(sortBy, isPrefixOf)+import Data.Char (isDigit)+import Data.List (sortBy, isPrefixOf)+import System.Environment (getEnv)+ import Data.SBV.BitVectors.Data-import Data.SBV.SMT.SMT import Data.SBV.Provers.SExpr-import System.Environment+import Data.SBV.SMT.SMT -- | The description of the Yices SMT solver -- The default executable is @\"yices\"@, which must be in your path. You can use the @SBV_YICES@ environment variable to point to the executable on your system.
Data/SBV/SMT/SMT.hs view
@@ -14,19 +14,20 @@ module Data.SBV.SMT.SMT where -import Control.Monad(when, zipWithM)-import Control.DeepSeq(NFData(..))-import Data.Char(isSpace)-import Data.List(intercalate)-import Data.Word-import Data.Int+import Control.DeepSeq (NFData(..))+import Control.Monad (when, zipWithM)+import Data.Char (isSpace)+import Data.Int (Int8, Int16, Int32, Int64)+import Data.List (intercalate)+import Data.Word (Word8, Word16, Word32, Word64)+import System.Directory (findExecutable)+import System.Process (readProcessWithExitCode)+import System.Exit (ExitCode(..))+ import Data.SBV.BitVectors.Bit import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff-import System.Directory(findExecutable)-import System.Process(readProcessWithExitCode)-import System.Exit -- | Solver configuration data SMTConfig = SMTConfig {
Data/SBV/SMT/SMTLib.hs view
@@ -13,9 +13,9 @@ module Data.SBV.SMT.SMTLib(SMTLibPgm, toSMTLib, addNonEqConstraints) where -import Control.DeepSeq(NFData(..))-import qualified Data.Foldable as F-import Data.List (intercalate)+import Control.DeepSeq (NFData(..))+import qualified Data.Foldable as F (toList)+import Data.List (intercalate) import Data.SBV.BitVectors.Bit import Data.SBV.BitVectors.Data@@ -33,11 +33,11 @@ | Just sw <- s `lookup` aliasTable = (show sw, c) | True = (s, c) -toSMTLib :: Bool -> [(SW, String)] -> [(SW, CW)] -> [((Int, Int, Int), [SW])] -> [(Int, ArrayInfo)] -> Pgm -> SW -> SMTLibPgm-toSMTLib isSat inps consts tbls arrs asgnsSeq out = SMTLibPgm (aliasTable, pre, post)+toSMTLib :: Bool -> [(SW, String)] -> [(SW, CW)] -> [((Int, Int, Int), [SW])] -> [(Int, ArrayInfo)] -> [(String, SBVType)] -> Pgm -> SW -> SMTLibPgm+toSMTLib isSat inps consts tbls arrs uis asgnsSeq out = SMTLibPgm (aliasTable, pre, post) where logic- | null tbls && null arrs = "QF_BV"- | True = "QF_AUFBV"+ | null tbls && null arrs && null uis = "QF_BV"+ | True = "QF_AUFBV" pre = [ "; Automatically generated by SBV. Do not edit." , "(benchmark sbv" , " :logic " ++ logic@@ -54,6 +54,8 @@ ++ concatMap mkTable tbls ++ [ " ; --- arrays ---" ] ++ concatMap declArray arrs+ ++ [ " ; --- uninterpreted constants ---" ]+ ++ concatMap declUI uis ++ [ " ; --- assignments ---" ] ++ map cvtAsgn asgns post = [ " ; --- formula ---" ]@@ -80,6 +82,9 @@ ArrayMutate j a b -> [" :assumption (= " ++ nm ++ " (store array" ++ show j ++ " " ++ show a ++ " " ++ show b ++ "))"] ArrayMerge t j k -> [" :assumption (= " ++ nm ++ " (ite (= bv1[1] " ++ show t ++ ") array" ++ show j ++ " array" ++ show k ++ "))"] +declUI :: (String, SBVType) -> [String]+declUI (i, t) = [" :extrafuns ((uninterpreted_" ++ i ++ " " ++ cvtType t ++ "))"]+ mkFormula :: Bool -> SW -> String mkFormula isSat s | isSat = " :formula (= " ++ show s ++ " bv1[1])"@@ -162,11 +167,13 @@ cvtExp (SBVApp (Extract i j) [a]) = "(extract[" ++ show i ++ ":" ++ show j ++ "] " ++ show a ++ ")" cvtExp (SBVApp (ArrEq i j) []) = "(ite (= array" ++ show i ++ " array" ++ show j ++") bv1[1] bv0[1])" cvtExp (SBVApp (ArrRead i) [a]) = "(select array" ++ show i ++ " " ++ show a ++ ")"+cvtExp (SBVApp (Uninterpreted nm) []) = "uninterpreted_" ++ nm+cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ intercalate " " (map show args) ++ ")" cvtExp inp@(SBVApp op args) | Just f <- lookup op smtOpTable = f (any hasSign args) (map show args) | True- = error $ "SBV2SMTLib.cvtExp: impossible happened; can't translate: " ++ show inp+ = error $ "SBV.SMT.SMTLib.cvtExp: impossible happened; can't translate: " ++ show inp where lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib.cvtExp.lift2: Unexpected arguments: " ++ show (o, sbvs) lift2B oU oS sgn sbvs@@ -176,21 +183,26 @@ = "(ite " ++ lift2 oU sgn sbvs ++ " bv1[1] bv0[1])" lift2N o sgn sbvs = "(bvnot " ++ lift2 o sgn sbvs ++ ")" lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")"- lift1 o _ sbvs = error $ "SBV.SMTLib.cvtExp.lift1: Unexpected arguments: " ++ show (o, sbvs)- smtOpTable = [ (Plus, lift2 "bvadd")- , (Minus, lift2 "bvsub")- , (Times, lift2 "bvmul")- , (Quot, lift2 "bvudiv")- , (Rem, lift2 "bvurem")- , (Equal, lift2 "bvcomp")- , (NotEqual, lift2N "bvcomp")- , (LessThan, lift2B "bvult" "bvslt")- , (GreaterThan, lift2B "bvugt" "bvsgt")- , (LessEq, lift2B "bvule" "bvsle")- , (GreaterEq, lift2B "bvuge" "bvsge")- , (And, lift2 "bvand")- , (Or, lift2 "bvor")- , (XOr, lift2 "bvxor")- , (Not, lift1 "bvnot")- , (Join, lift2 "concat")+ lift1 o _ sbvs = error $ "SBV.SMT.SMTLib.cvtExp.lift1: Unexpected arguments: " ++ show (o, sbvs)+ smtOpTable = [ (Plus, lift2 "bvadd")+ , (Minus, lift2 "bvsub")+ , (Times, lift2 "bvmul")+ , (Quot, lift2 "bvudiv")+ , (Rem, lift2 "bvurem")+ , (Equal, lift2 "bvcomp")+ , (NotEqual, lift2N "bvcomp")+ , (LessThan, lift2B "bvult" "bvslt")+ , (GreaterThan, lift2B "bvugt" "bvsgt")+ , (LessEq, lift2B "bvule" "bvsle")+ , (GreaterEq, lift2B "bvuge" "bvsge")+ , (And, lift2 "bvand")+ , (Or, lift2 "bvor")+ , (XOr, lift2 "bvxor")+ , (Not, lift1 "bvnot")+ , (Join, lift2 "concat") ]++cvtType :: SBVType -> String+cvtType (SBVType []) = error "SBV.SMT.SMTLib.cvtType: internal: received an empty type!"+cvtType (SBVType xs) = intercalate " " $ map sh xs+ where sh (_, s) = "BitVec[" ++ show s ++ "]"
+ Data/SBV/TestSuite/Uninterpreted/AUF.hs view
@@ -0,0 +1,25 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.TestSuite.Uninterpreted.AUF+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Test suite for Data.SBV.Examples.Uninterpreted.AUF+-----------------------------------------------------------------------------++module Data.SBV.TestSuite.Uninterpreted.AUF where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.Uninterpreted.AUF++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \goldCheck -> test [+ "auf-0" ~: assert =<< isTheorem thm+ , "auf-1" ~: pgm `goldCheck` "auf-1.gold"+ ]+ where pgm = runSymbolic $ forAll ["x", "y", "a", "initVal"] thm
+ Data/SBV/TestSuite/Uninterpreted/Uninterpreted.hs view
@@ -0,0 +1,25 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.TestSuite.Uninterpreted+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+-- Portability : portable+--+-- Test suite for Data.SBV.Examples.Uninterpreted.Uninterpreted+-----------------------------------------------------------------------------++module Data.SBV.TestSuite.Uninterpreted.Uninterpreted where++import Data.SBV+import Data.SBV.Internals+import Data.SBV.Examples.Uninterpreted.Uninterpreted++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \_ -> test [+ "uninterpreted-0" ~: assert =<< isTheorem p0+ , "uninterpreted-1" ~: assert =<< isTheorem p1+ , "uninterpreted-2" ~: assert . not =<< isTheorem p2+ ]
Data/SBV/Utils/SBVTest.hs view
@@ -13,8 +13,8 @@ {-# LANGUAGE RankNTypes #-} module Data.SBV.Utils.SBVTest(generateGoldCheck, showsAs, ioShowsAs, mkTestSuite, SBVTestSuite(..), module Test.HUnit) where -import System.FilePath((</>))-import Test.HUnit hiding(State)+import System.FilePath ((</>))+import Test.HUnit (Test(..), Assertion, assert, (~:), test) -- | A Test-suite, parameterized by the gold-check generator/checker data SBVTestSuite = SBVTestSuite ((forall a. Show a => (IO a -> FilePath -> IO ())) -> Test)
Data/SBV/Utils/TDiff.hs view
@@ -12,9 +12,9 @@ module Data.SBV.Utils.TDiff(timeIf) where -import Control.DeepSeq-import System.Time-import Numeric+import Control.DeepSeq (rnf, NFData(..))+import System.Time (TimeDiff(..), normalizeTimeDiff, diffClockTimes, getClockTime)+import Numeric (showFFloat) showTDiff :: TimeDiff -> String showTDiff itd = et
README view
@@ -41,6 +41,7 @@ - `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed) - Arrays of symbolic values - Symbolic polynomials over GF(2^n ), and polynomial arithmetic+ - Uninterpreted constants and functions over symbolic values The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the@@ -76,10 +77,10 @@ Prerequisites =============-You **should** download and install Yices on your machine, and make sure the-"yices" executable is in your path before using the sbv library, as it is the-current default solver. Alternatively, you can specify the location of yices-executable in the environment variable `SBV_YICES` and the options to yices+You **should** download and install Yices (version 2.X) on your machine, and+make sure the "yices" executable is in your path before using the sbv library,+as it is the current default solver. Alternatively, you can specify the location+of yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`. (The default for the latter is `"-m -f"`.) Examples
+ SBVUnitTest/GoldFiles/auf-1.gold view
@@ -0,0 +1,29 @@+INPUTS+ s0 :: SWord32, aliasing "x"+ s1 :: SWord32, aliasing "y"+ s2 :: SWord32, aliasing "initVal"+CONSTANTS+ s_2 = False+ s_1 = True+ s3 = 2 :: SWord32+ s9 = 3 :: SWord32+ s13 = 1 :: SWord32+TABLES+ARRAYS+UNINTERPRETED CONSTANTS+ ui_f :: SWord32 -> SWord64+DEFINE+ s4 :: SWord32 = s0 + s3+ s5 :: SBool = s1 == s4+ s6 :: SBool = ~ s5+ s7 :: SWord32 = s1 - s3+ s8 :: SBool = s0 == s7+ s10 :: SWord32 = if s8 then s9 else s2+ s11 :: SWord64 = ui_f s10+ s12 :: SWord32 = s1 - s0+ s14 :: SWord32 = s12 + s13+ s15 :: SWord64 = ui_f s14+ s16 :: SBool = s11 == s15+ s17 :: SBool = s6 | s16+OUTPUTS+ s17
SBVUnitTest/GoldFiles/basic-2_1.gold view
@@ -6,6 +6,7 @@ s1 = 3 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s1 - s0
SBVUnitTest/GoldFiles/basic-2_2.gold view
@@ -6,6 +6,7 @@ s1 = 9 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s1 - s2
SBVUnitTest/GoldFiles/basic-2_3.gold view
@@ -6,6 +6,7 @@ s1 = 3 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-2_4.gold view
@@ -6,6 +6,7 @@ s1 = 3 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_1.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s0 - s1
SBVUnitTest/GoldFiles/basic-3_2.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-3_3.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_4.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_5.gold view
@@ -7,6 +7,7 @@ s2 = 1 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s3 :: SWord8 = s0 + s2 OUTPUTS
SBVUnitTest/GoldFiles/basic-4_1.gold view
@@ -5,6 +5,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s0 - s0
SBVUnitTest/GoldFiles/basic-4_2.gold view
@@ -5,6 +5,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s1 :: SWord8 = s0 * s0 s2 :: SWord8 = s1 - s1
SBVUnitTest/GoldFiles/basic-4_3.gold view
@@ -5,6 +5,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-4_4.gold view
@@ -5,6 +5,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-4_5.gold view
@@ -6,6 +6,7 @@ s1 = 1 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s1 OUTPUTS
SBVUnitTest/GoldFiles/basic-5_1.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s0 - s0
SBVUnitTest/GoldFiles/basic-5_2.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s2 - s2
SBVUnitTest/GoldFiles/basic-5_3.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-5_4.gold view
@@ -6,6 +6,7 @@ s_1 = True TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-5_5.gold view
@@ -7,6 +7,7 @@ s2 = 1 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s3 :: SWord8 = s0 + s2 OUTPUTS
SBVUnitTest/GoldFiles/ccitt.gold view
@@ -77,6 +77,7 @@ s6250 = 1 :: SWord64 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s4 :: SBool = s0 == s2 s5 :: SBool = s1 == s3
SBVUnitTest/GoldFiles/legato.gold view
@@ -18,6 +18,7 @@ s35 = 128 :: SWord8 TABLES ARRAYS+UNINTERPRETED CONSTANTS DEFINE s10 :: SBool = s0 /= s2 s11 :: SBool = s0 /= s4
SBVUnitTest/SBVUnitTest.hs view
@@ -12,16 +12,17 @@ module Main(main, createGolds) where -import Control.Monad(when)-import System.Directory(doesDirectoryExist, findExecutable)-import System.Environment(getArgs)-import System.Exit-import System.FilePath((</>))-import Test.HUnit+import Control.Monad (when)+import System.Directory (doesDirectoryExist, findExecutable)+import System.Environment (getArgs, getEnv)+import System.Exit (exitWith, ExitCode(..))+import System.FilePath ((</>))+import System.Process (readProcessWithExitCode)+import Test.HUnit (Test(..), Counts(..), runTestTT) -import Data.SBV-import Data.SBV.Utils.SBVTest-import Paths_sbv(getDataDir)+import Data.SBV (yices, SMTSolver(..))+import Data.SBV.Utils.SBVTest (SBVTestSuite(..), generateGoldCheck)+import Paths_sbv (getDataDir) -- To add a new collection of tests, import below and add to testCollection variable import qualified Data.SBV.TestSuite.Arrays.Memory as T01(testSuite)@@ -46,6 +47,8 @@ import qualified Data.SBV.TestSuite.Puzzles.Sudoku as T20(testSuite) import qualified Data.SBV.TestSuite.Puzzles.Temperature as T21(testSuite) import qualified Data.SBV.TestSuite.Puzzles.U2Bridge as T22(testSuite)+import qualified Data.SBV.TestSuite.Uninterpreted.AUF as T23(testSuite)+import qualified Data.SBV.TestSuite.Uninterpreted.Uninterpreted as T24(testSuite) testCollection :: [SBVTestSuite] testCollection = [@@ -54,7 +57,7 @@ , T09.testSuite, T10.testSuite, T11.testSuite, T12.testSuite , T13.testSuite, T14.testSuite, T15.testSuite, T16.testSuite , T17.testSuite, T18.testSuite, T19.testSuite, T20.testSuite- , T21.testSuite, T22.testSuite+ , T21.testSuite, T22.testSuite, T23.testSuite, T24.testSuite ] -- No user serviceable parts below.. @@ -72,23 +75,40 @@ putStrLn $ "*** Cannot run test cases, exiting." exitWith $ ExitFailure 1 -checkDefaultSolver :: IO ()-checkDefaultSolver = do mbP <- findExecutable ex- case mbP of- Nothing -> do putStrLn $ "*** Cannot find default SMT solver executable for " ++ nm- putStrLn $ "*** Please make sure the executable " ++ show ex- putStrLn $ "*** is installed and is in your path."- putStrLn $ "*** Cannot run test cases, exiting."- exitWith $ ExitFailure 1- Just p -> putStrLn $ "*** Using solver : " ++ nm ++ " (" ++ show p ++ ")"- where ex = executable $ solver $ defaultSMTCfg- nm = name $ solver $ defaultSMTCfg+checkYices :: IO ()+checkYices = do ex <- getEnv "SBV_YICES" `catch` (\_ -> return (executable yices))+ mbP <- findExecutable ex+ case mbP of+ Nothing -> do putStrLn $ "*** Cannot find default SMT solver executable for " ++ nm+ putStrLn $ "*** Please make sure the executable " ++ show ex+ putStrLn $ "*** is installed and is in your path."+ putStrLn $ "*** Cannot run test cases, exiting."+ exitWith $ ExitFailure 1+ Just p -> do putStrLn $ "*** Using solver : " ++ nm ++ " (" ++ show p ++ ")"+ checkYicesVersion p+ where nm = name yices +checkYicesVersion :: FilePath -> IO ()+checkYicesVersion p =+ do (ec, yOut, _yErr) <- readProcessWithExitCode p ["-V"] ""+ case ec of+ ExitFailure _ -> do putStrLn $ "*** Cannot determine Yices version. Please install Yices version 2.X first."+ exitWith $ ExitFailure 1+ ExitSuccess -> do let isYices1 = take 2 yOut == "1." -- crude test; might fail..+ when isYices1 $ putStrLn $ "*** Yices version 1.X is detected. Version 2.X is strongly recommended!"+ opts <- getEnv "SBV_YICES_OPTIONS" `catch` (\_ -> return (unwords (options yices)))+ when (isYices1 && opts /= "-tc -smt -e") $ do+ putStrLn $ "*** Either install Yices 2.X, or set the environment variable:"+ putStrLn $ "*** SBV_YICES_OPTIONS=\"-tc -smt -e\""+ putStrLn $ "*** To use Yices 1.X with SBV."+ putStrLn $ "*** However, upgrading to Yices 2.X is highly recommended!"+ exitWith $ ExitFailure 1+ run :: Bool -> [String] -> IO () run shouldCreate [gd] = do putStrLn $ "*** Starting SBV unit tests..\n*** Gold files at: " ++ show gd checkGoldDir gd- checkDefaultSolver+ checkYices let mkTst (SBVTestSuite f) = f $ generateGoldCheck gd shouldCreate cts <- runTestTT $ TestList $ map mkTst testCollection decide cts
Setup.hs view
@@ -13,21 +13,22 @@ {-# OPTIONS_GHC -Wall #-} module Main(main) where -import Control.Monad(when)-import Distribution.PackageDescription-import Distribution.Simple-import Distribution.Simple.LocalBuildInfo(LocalBuildInfo(..))-import Distribution.Text(display)-import System.Directory(findExecutable)-import System.Process(system)-import System.Exit-import Data.SBV.Provers.Prover(SMTSolver(..), SMTConfig(..), defaultSMTCfg)+import Control.Monad (when)+import Distribution.PackageDescription (executables, modulePath, package, maintainer, customFieldsBI, homepage, exeName, buildInfo)+import Distribution.Simple (defaultMainWithHooks, simpleUserHooks, runTests, postInst)+import Distribution.Simple.LocalBuildInfo (LocalBuildInfo(..))+import Distribution.Text (display)+import System.Directory (findExecutable)+import System.Exit (exitWith, ExitCode(..))+import System.Process (system) +import Data.SBV.Provers.Prover (SMTSolver(..), yices)+ main :: IO () main = defaultMainWithHooks simpleUserHooks{ runTests = unittest True, postInst = unittest False} where checkDefSolver = do- let ex = executable $ solver $ defaultSMTCfg- nm = name $ solver $ defaultSMTCfg+ let ex = executable yices+ nm = name yices mbP <- findExecutable ex case mbP of Nothing -> do putStrLn $ "*** The sbv library requires the default solver " ++ nm ++ " to be installed."
sbv.cabal view
@@ -1,11 +1,12 @@ Name: sbv-Version: 0.9.2+Version: 0.9.3 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Adds support for symbolic bit vectors, allowing formal models of bit-precise programs to be created. Supports symbolic arrays and polynomials over GF(2^n).- Aims to provide seamless integration with SMT solvers to produce formal- property proofs of theoremhood and satisfiability, with counter-examples.+ Supports uninterpreted constants and functions. Aims to provide seamless integration+ with SMT solvers to produce formal property proofs of theoremhood and+ satisfiability, with counter-examples. Copyright: Levent Erkok, 2011 License: BSD3 License-file: LICENSE@@ -46,6 +47,7 @@ , Data.SBV.Examples.Puzzles.NQueens , Data.SBV.Examples.Puzzles.Sudoku , Data.SBV.Examples.Puzzles.U2Bridge+ , Data.SBV.Examples.Uninterpreted.AUF Other-modules : Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Bit , Data.SBV.BitVectors.Model@@ -75,6 +77,7 @@ , Data.SBV.Examples.PrefixSum.PrefixSum , Data.SBV.Examples.Puzzles.PowerSet , Data.SBV.Examples.Puzzles.Temperature+ , Data.SBV.Examples.Uninterpreted.Uninterpreted , Data.SBV.TestSuite.Arrays.Memory , Data.SBV.TestSuite.Basics.BasicTests , Data.SBV.TestSuite.Basics.Higher@@ -97,6 +100,8 @@ , Data.SBV.TestSuite.Puzzles.Sudoku , Data.SBV.TestSuite.Puzzles.U2Bridge , Data.SBV.TestSuite.Puzzles.Temperature+ , Data.SBV.TestSuite.Uninterpreted.AUF+ , Data.SBV.TestSuite.Uninterpreted.Uninterpreted Executable SBVUnitTests main-is : SBVUnitTest/SBVUnitTest.hs