sbv 0.9.8 → 0.9.9
raw patch · 38 files changed
+536/−159 lines, 38 files
Files
- Data/SBV.hs +10/−7
- Data/SBV/BitVectors/Data.hs +22/−5
- Data/SBV/BitVectors/Model.hs +130/−101
- Data/SBV/Examples/PrefixSum/PrefixSum.hs +137/−3
- Data/SBV/Examples/Puzzles/DogCatMouse.hs +8/−8
- Data/SBV/Examples/Puzzles/U2Bridge.hs +3/−4
- Data/SBV/Examples/Uninterpreted/AUF.hs +36/−5
- Data/SBV/Examples/Uninterpreted/Function.hs +2/−3
- Data/SBV/Provers/Prover.hs +2/−2
- Data/SBV/SMT/SMT.hs +20/−9
- Data/SBV/SMT/SMTLib.hs +16/−2
- Data/SBV/TestSuite/PrefixSum/PrefixSum.hs +5/−4
- Data/SBV/TestSuite/Uninterpreted/AUF.hs +4/−3
- SBVUnitTest/GoldFiles/auf-1.gold +1/−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/dogCatMouse.gold +1/−2
- SBVUnitTest/GoldFiles/legato.gold +1/−0
- SBVUnitTest/GoldFiles/prefixSum_16.gold +117/−0
- sbv.cabal +1/−1
Data/SBV.hs view
@@ -15,14 +15,13 @@ -- Express properties about bit-precise Haskell programs and automatically prove -- them using SMT solvers. ----- > $ ghci -XScopedTypeVariables--- > Prelude> :m Data.SBV--- > Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x--- > Q.E.D.--- > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x--- > Falsifiable. Counter-example:--- > x = 128 :: SWord8+-- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)+-- Q.E.D. --+-- >>> prove $ forAll ["x"] $ \x -> x `shiftL` 2 .== (x :: SWord8)+-- Falsifiable. Counter-example:+-- x = 128 :: SWord8+-- -- The function 'prove' has the following type: -- -- @@@ -129,6 +128,10 @@ , PrettyNum(..), readBin -- * Uninterpreted constants and functions , Uninterpreted(..)+ -- ** Accessing the handle+ , SBVUF, sbvUFName+ -- ** Adding axioms+ , addAxiom -- * Proving properties -- $proveIntro
Data/SBV/BitVectors/Data.hs view
@@ -31,7 +31,7 @@ , SBVExpr(..), newExpr , cache, uncache, HasSignAndSize(..) , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, State, Size, output, Result(..)- , SBVType(..), newUninterpreted, unintFnUIKind+ , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom ) where import Control.DeepSeq (NFData(..))@@ -243,14 +243,15 @@ [((Int, Int, Int), [SW])] -- tables (automatically constructed) [(Int, ArrayInfo)] -- arrays (user specified) [(String, SBVType)] -- uninterpreted constants+ [(String, [String])] -- axioms 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 uis xs os) = intercalate "\n" $+ show (Result is cs ts as uis axs xs os) = intercalate "\n" $ ["INPUTS"] ++ map shn is ++ ["CONSTANTS"]@@ -261,6 +262,8 @@ ++ map sha as ++ ["UNINTERPRETED CONSTANTS"] ++ map shui uis+ ++ ["AXIOMS"]+ ++ map shax axs ++ ["DEFINE"] ++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList xs) ++ ["OUTPUTS"]@@ -281,6 +284,7 @@ alias | ni == nm = "" | True = ", aliasing " ++ show nm shui (nm, t) = " uninterpreted_" ++ nm ++ " :: " ++ show t+ shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss data ArrayContext = ArrayFree (Maybe SW) | ArrayReset Int SW@@ -323,6 +327,7 @@ , rexprMap :: IORef ExprMap , rArrayMap :: IORef ArrayMap , rUIMap :: IORef UIMap+ , raxioms :: IORef [(String, [String])] } -- | The "Symbolic" value. Either a constant (@Left@) or a symbolic@@ -478,6 +483,14 @@ liftIO $ modifyIORef (routs st) (sw:) return i +-- | Add a user specified axiom to the generated SMT-Lib file. Note that the input is a+-- mere string; we perform no checking on the input that it's well-formed or is sensical.+-- A separate formalization of SMT-Lib would be very useful here.+addAxiom :: String -> [String] -> Symbolic ()+addAxiom nm ax = do+ st <- ask+ liftIO $ modifyIORef (raxioms st) ((nm, ax) :)+ -- | Run a symbolic computation and return a 'Result' runSymbolic :: Symbolic a -> IO Result runSymbolic (Symbolic c) = do@@ -490,6 +503,7 @@ tables <- newIORef Map.empty arrays <- newIORef IMap.empty uis <- newIORef Map.empty+ axioms <- newIORef [] let st = State { rctr = ctr , rinps = inps , routs = outs@@ -499,6 +513,7 @@ , rArrayMap = arrays , rexprMap = emap , rUIMap = uis+ , raxioms = axioms } _ <- newConst st $ W1 Zero -- s(-2) == falseSW _ <- newConst st $ W1 One -- s(-1) == trueSW@@ -512,7 +527,8 @@ tbls <- (sortBy (\((x, _, _), _) ((y, _, _), _) -> x `compare` y) . map swap . Map.toList) `fmap` readIORef tables arrs <- IMap.toAscList `fmap` readIORef arrays unint <- Map.toList `fmap` readIORef uis- return $ Result (reverse inpsR) cnsts tbls arrs unint rpgm (reverse outsR)+ axs <- reverse `fmap` readIORef axioms+ return $ Result (reverse inpsR) cnsts tbls arrs unint axs rpgm (reverse outsR) ------------------------------------------------------------------------------- -- * Symbolic Words@@ -704,7 +720,8 @@ rnf (I64 w) = rnf w `seq` () instance NFData Result where- 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+ rnf (Result inps consts tbls arrs uis axs pgm outs)+ = rnf inps `seq` rnf consts `seq` rnf tbls `seq` rnf arrs `seq` rnf uis `seq` rnf axs `seq` rnf pgm `seq` rnf outs instance NFData ArrayContext instance NFData Pgm
Data/SBV/BitVectors/Model.hs view
@@ -22,7 +22,7 @@ module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..) , bitValue, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE- , lsb, msb+ , lsb, msb, SBVUF, sbvUFName ) where @@ -635,23 +635,45 @@ instance SymWord b => Mergeable (SFunArray a b) where symbolicMerge = mergeArrays +-- | An uninterpreted function handle. This is the handle to be used for+-- adding axioms about uninterpreted constants/functions. Note that+-- we will leave this abstract for safety purposes+newtype SBVUF = SBVUF String++-- | Get the name associated with the uninterpreted-value; useful when+-- constructing axioms about this UI.+sbvUFName :: SBVUF -> String+sbvUFName (SBVUF s) = s++-- The name we use for translating the UF constants to SMT-Lib..+mkUFName :: String -> SBVUF+mkUFName nm = SBVUF $ "uninterpreted_" ++ nm+ -- | 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+-- 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+-- Minimal complete definition: 'uninterpretWithHandle'. 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 a value, receiving an object that can be used instead. Use this version+ -- when you do not need to add an axiom about this value. uninterpret :: String -> a+ -- | Uninterpret a value, but also get a handle to the resulting object. This handle+ -- can be used to add axioms for this object. (See 'addAxiom'.)+ uninterpretWithHandle :: String -> (SBVUF, a) + -- minimal complete definition: 'uninterpretWithHandle'+ uninterpret = snd . uninterpretWithHandle+ -- Plain constants instance HasSignAndSize a => Uninterpreted (SBV a) where- uninterpret nm = SBV sgnsza $ Right $ cache result+ uninterpretWithHandle nm = (mkUFName 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) []@@ -664,144 +686,151 @@ -- 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- mapM_ forceArg [sw0]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0]+ 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- mapM_ forceArg [sw0, sw1]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1]+ 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- mapM_ forceArg [sw0, sw1, sw2]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1, sw2]+ 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- mapM_ forceArg [sw0, sw1, sw2, sw3]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1, sw2, sw3]+ 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- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4]+ 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- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5]+ 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- mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]- newExpr st sgnsza $ SBVApp (Uninterpreted nm) [sw0, sw1, sw2, sw3, sw4, sw5, sw6]+ uninterpretWithHandle nm = (mkUFName nm, f)+ where f 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+ mapM_ forceArg [sw0, sw1, sw2, sw3, sw4, sw5, sw6]+ 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1) -> f 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2) -> f 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3) -> f 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4) -> f 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5) -> f 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+ uninterpretWithHandle nm = let (h, f) = uninterpretWithHandle nm in (h, \(arg0, arg1, arg2, arg3, arg4, arg5, arg6) -> f arg0 arg1 arg2 arg3 arg4 arg5 arg6)
Data/SBV/Examples/PrefixSum/PrefixSum.hs view
@@ -20,6 +20,10 @@ import Data.SBV +----------------------------------------------------------------------+-- * Formalizing power-lists+----------------------------------------------------------------------+ -- | A poor man's representation of powerlists and -- basic operations on them: <http://www.cs.utexas.edu/users/psp/powerlist.pdf>. -- We merely represent power-lists by ordinary lists.@@ -43,10 +47,18 @@ chunk2 (x:y:xs) = (x,y) : chunk2 xs chunk2 _ = error "unzipPL: malformed powerlist" +----------------------------------------------------------------------+-- * Reference prefix-sum implementation+----------------------------------------------------------------------+ -- | Reference prefix sum (@ps@) is simply Haskell's @scanl1@ function ps :: (a, a -> a -> a) -> PowerList a -> PowerList a ps (_, f) = scanl1 f +----------------------------------------------------------------------+-- * The Ladner-Fischer parallel version+----------------------------------------------------------------------+ -- | The Ladner-Fischer (@lf@) implementation of prefix-sum. See <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf> -- or pg. 16 of <http://www.cs.utexas.edu/users/psp/powerlist.pdf>. lf :: (a, a -> a -> a) -> PowerList a -> PowerList a@@ -58,18 +70,140 @@ flpq = lf (zero, f) pq rsh xs = zero : init xs --- | Correctness theorem, for a powerlist of given size, an associative operator, and its unit element++----------------------------------------------------------------------+-- * Sample proofs for concrete operators+----------------------------------------------------------------------++-- | Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool flIsCorrect n zf = do args :: PowerList SWord32 <- mapM (const free_) [1..n] output $ ps zf args .== lf zf args -- | Proves Ladner-Fischer is equivalent to reference specification for addition.--- @0@ is the unit element, and we use a power-list of size @8@.+-- @0@ is the left-unit element, and we use a power-list of size @8@. thm1 :: IO ThmResult thm1 = prove $ flIsCorrect 8 (0, (+)) -- | Proves Ladner-Fischer is equivalent to reference specification for the function @max@.--- @0@ is the unit element, and we use a power-list of size @16@.+-- @0@ is the left-unit element, and we use a power-list of size @16@. thm2 :: IO ThmResult thm2 = prove $ flIsCorrect 16 (0, smax)++----------------------------------------------------------------------+-- * Attempt at proving for arbitrary operators+----------------------------------------------------------------------+-- | Try proving correctness for an arbitrary operator. This proof will /not/ go through since the+-- SMT solver does not know that the operator associative and has the given left-unit element+--+-- >>> thm3+-- Falsifiable. Counter-example:+-- s0 = 0 :: SWord32+-- s1 = 0 :: SWord32+-- s2 = 0 :: SWord32+-- s3 = 0 :: SWord32+-- s4 = 0 :: SWord32+-- s5 = 0 :: SWord32+-- s6 = 0 :: SWord32+-- s7 = 3221225472 :: SWord32+-- -- uninterpreted: u+-- u = 0+-- -- uninterpreted: flOp+-- flOp 0 3221225472 = 2147483648+-- flOp 0 2147483648 = 3758096384+-- flOp _ _ = 0+--+-- You can verify that the above function for @flOp@ is not associative:+--+-- @+-- ghci> flOp 3221225472 (flOp 2147483648 3221225472)+-- 0+-- ghci> flOp (flOp 3221225472 2147483648) 3221225472+-- 2147483648+-- @+--+-- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the third+-- equation for @flOp@ will simply map many elements to @0@.+thm3 :: IO ThmResult+thm3 = prove $ do args :: PowerList SWord32 <- mapM (const free_) [(1::Int)..8]+ output $ ps (u, op) args .== lf (u, op) args+ where op :: SWord32 -> SWord32 -> SWord32+ op = uninterpret "flOp"+ u :: SWord32+ u = uninterpret "u"++----------------------------------------------------------------------+-- * Proving for arbitrary operators using axioms+----------------------------------------------------------------------+-- | Generate an instance of the prefix-sum problem for an arbitrary operator, by telling the SMT solver+-- the necessary axioms for associativity and left-unit. The first argument states how wide the power list should be.+genPrefixSumInstance :: Int -> Symbolic SBool+genPrefixSumInstance n = do+ args :: PowerList SWord32 <- mapM (const free_) [1..n]+ addAxiom "flOp is associative" $ assocAxiom (sbvUFName opH)+ addAxiom "u is left-unit for flOp" $ leftUnitAxiom (sbvUFName opH) (sbvUFName uH)+ output $ ps (u, op) args .== lf (u, op) args+ where op :: SWord32 -> SWord32 -> SWord32+ opH :: SBVUF+ (opH, op) = uninterpretWithHandle "flOp"+ u :: SWord32+ uH :: SBVUF+ (uH, u) = uninterpretWithHandle "u"+ -- this is the brittle part; but it'll have to do until we get a proper+ -- DSL for expressing SMT-axioms..+ mkCall :: String -> String -> String -> String+ mkCall o x y = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"+ assocAxiom :: String -> [String]+ assocAxiom o = [+ ":assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])"+ , " (= " ++ lhs+ , " " ++ rhs+ , " )"+ , " )"+ ]+ where lhs = mkCall o (mkCall o "?x" "?y") "?z"+ rhs = mkCall o "?x" (mkCall o "?y" "?z")+ leftUnitAxiom :: String -> String -> [String]+ leftUnitAxiom o ue = [+ ":assumption (forall (?x BitVec[32])"+ , " (= " ++ lhs+ , " " ++ rhs+ , " )"+ , " )"+ ]+ where lhs = "(" ++ o ++ " " ++ ue ++ " " ++ "?x" ++ ")"+ rhs = "?x"++-- | Prove the generic problem for powerlists of given sizes. Note that+-- this will only work for Yices-1. This is due to the fact that Yices-2+-- follows the SMT-Lib standard and does not accept bit-vector problems with+-- quantified axioms in them, while Yices-1 did allow for that. The crux of+-- the problem is that there are no SMT-Lib logics that combine BV's and+-- quantifiers, see: <http://goedel.cs.uiowa.edu/smtlib/logics.html>. So we+-- are stuck until new powerful logics are added to SMT-Lib.+--+-- Here, we explicitly tell SBV to use Yices-1 that did not have that limitation.+-- Tweak the executable location accordingly below for your platform..+--+-- We have:+--+-- >>> prefixSum 2+-- Q.E.D.+--+-- >>> prefixSum 4+-- Q.E.D.+--+-- Note that these proofs tend to run long. Also, Yices-1.0.28 ran out of memory+-- and crashed on my box when I tried for size @8@, after running for about 2.5 minutes..+prefixSum :: Int -> IO ThmResult+prefixSum i+ -- Fast way of checking whether a number is a power of two, see: <http://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2>+ | i <= 1 || (i .&. (i-1)) /= 0+ = error $ "prefixSum: input must be a power of 2 larger than 2, received: " ++ show i+ | True+ = proveWith cfg $ genPrefixSumInstance i+ where cfg = defaultSMTCfg { solver = yices' }+ yices' = yices { options = ["-tc", "-smt", "-e"]+ , executable = "/usr/local/yices-1.0.28/bin/yices"+ }
Data/SBV/Examples/Puzzles/DogCatMouse.hs view
@@ -30,12 +30,12 @@ &&& dog + cat + mouse .== 100 -- buy precisely 100 animals &&& 1500 * dog + 100 * cat + 25 * mouse .== 10000 -- spend exactly 100 dollars (use cents since we don't have fractions) --- | prints the only solution:+-- | Prints the only solution: ----- @--- dog = 3 :: SWord16--- cat = 41 :: SWord16--- mouse = 56 :: SWord16--- @-solve :: IO ()-solve = print =<< allSat (forAll ["dog", "cat", "mouse"] puzzle)+-- >>> solve+-- Only one solution found:+-- dog = 3 :: SWord16+-- cat = 41 :: SWord16+-- mouse = 56 :: SWord16+solve :: IO AllSatResult+solve = allSat $ forAll ["dog", "cat", "mouse"] puzzle
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -239,9 +239,9 @@ shL True = " <-- " -- | Solve the U2-bridge crossing puzzle, starting by testing solutions with--- increasing number of steps, until we find one. This call prints:+-- increasing number of steps, until we find one. We have: ----- @+-- >>> solveU2 -- Checking for solutions with 1 move. -- Checking for solutions with 2 moves. -- Checking for solutions with 3 moves.@@ -261,8 +261,7 @@ -- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17--- Found: 2 solutions with 5 moves--- @+-- Found: 2 solutions with 5 moves. -- -- Finding the all 2 possible solutions to the puzzle. solveU2 :: IO ()
Data/SBV/Examples/Uninterpreted/AUF.hs view
@@ -32,8 +32,14 @@ import Data.SBV +--------------------------------------------------------------+-- * Model using functional arrays+--------------------------------------------------------------+ -- | The array type, takes symbolic 32-bit unsigned indexes--- and stores 32-bit unsigned symbolic values+-- and stores 32-bit unsigned symbolic values. These are+-- functional arrays where reading before writing a cell+-- throws an exception. type A = SFunArray Word32 Word32 -- | Uninterpreted function in the theorem@@ -42,13 +48,38 @@ -- | 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+thm1 :: SWord32 -> SWord32 -> A -> SWord32 -> SBool+thm1 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+--+-- >>> proveThm1+-- Q.E.D.+proveThm1 :: IO ()+proveThm1 = print =<< prove thm1++--------------------------------------------------------------+-- * Model using SMT arrays+--------------------------------------------------------------++-- | This version directly uses SMT-arrays and hence does not need an initializer.+-- Reading an element before writing to it returns an arbitrary value.+type B = SArray Word32 Word32++-- | Same as 'thm1', except we don't need an initializer with the 'SArray' model.+thm2 :: SWord32 -> SWord32 -> B -> SBool+thm2 x y a = lhs ==> rhs+ where 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:+--+-- >>> proveThm2+-- Q.E.D.+proveThm2 :: IO ()+proveThm2 = print =<< prove thm2
Data/SBV/Examples/Uninterpreted/Function.hs view
@@ -26,15 +26,14 @@ -- Indeed, the SMT solver (Yices in this case) returns a counter-example -- function that is not commutative. We have: ----- @--- ghci> prove $ forAll ["x", "y"] thmBad+--+-- >>> prove $ forAll ["x", "y"] thmBad -- Falsifiable. Counter-example: -- x = 0 :: SWord8 -- y = 128 :: SWord8 -- -- uninterpreted: f -- f 128 0 = 32768 -- f _ _ = 0--- @ -- -- Note how the counterexample function @f@ returned by Yices violates commutativity; -- thus providing evidence that the asserted theorem is not valid.
Data/SBV/Provers/Prover.hs view
@@ -287,9 +287,9 @@ msg $ "Generated symbolic trace:\n" ++ show res msg "Translating to SMT-Lib.." case res of- Result is consts tbls arrs uis pgm [o@(SW{})] ->+ Result is consts tbls arrs uis axs pgm [o@(SW{})] -> timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis- in return (is, uiMap, toSMTLib isSat is consts tbls arrs uis pgm o)+ in return (is, uiMap, toSMTLib isSat is consts tbls arrs uis axs pgm o) _ -> error $ "SBVProver.callSolver: Impossible happened: " ++ show res -- | Equality as a proof method. Allows for
Data/SBV/SMT/SMT.hs view
@@ -106,13 +106,15 @@ instance Show AllSatResult where show (AllSatResult []) = "No solutions found"- show (AllSatResult [s]) = "One solution found\n" ++ show (SatResult s)- show (AllSatResult ss) = "Multiple solutions found:\n" -- shouldn't display how-many; would be too slow/leak-space to compute everything..+ show (AllSatResult [s]) = "Only one solution found:\n" ++ shUnique s+ where shUnique = showSMTResult "Unsatisfiable"+ ("Unknown (No assignment to variables returned)") "Unknown. Potential assignment:\n" "" ""+ show (AllSatResult ss) = "Multiple solutions found:\n" -- shouldn't display how-many; would be too slow/leak-space to compute everything.. ++ unlines (zipWith sh [(1::Int)..] ss) ++ "Done."- where sh i s = showSMTResult "Unsatisfiable"- ("Unknown #" ++ show i ++ "(No assignment to variables returned)") "Unknown. Potential assignment:\n"- ("Solution #" ++ show i ++ " (No assignment to variables returned)") ("Solution #" ++ show i ++ ":\n") s+ where sh i = showSMTResult "Unsatisfiable"+ ("Unknown #" ++ show i ++ "(No assignment to variables returned)") "Unknown. Potential assignment:\n"+ ("Solution #" ++ show i ++ " (No assignment to variables returned)") ("Solution #" ++ show i ++ ":\n") -- | Instances of 'SatModel' can be automatically extracted from models returned by the -- solvers. The idea is that the sbv infrastructure provides a stream of 'CW''s (constant-words)@@ -277,11 +279,20 @@ ExitSuccess -> if null errors then return $ Right $ map clean (filter (not . null) (lines contents)) else return $ Left errors- ExitFailure n -> return $ Left $ "Failed to invoke " ++ nm- ++ "\nExecutable: " ++ show execPath- ++ "\nOptions : " ++ unwords opts- ++ "\nExit code : " ++ show n+ ExitFailure n -> let errors' = if null (dropWhile isSpace errors)+ then "(No error message printed on stderr by the executable.)"+ else errors+ in return $ Left $ "Failed to complete the call to " ++ nm+ ++ "\nExecutable: " ++ show execPath+ ++ "\nOptions : " ++ unwords opts+ ++ "\nExit code : " ++ show n+ ++ "\nError message:"+ ++ "\n" ++ line ++ "\n"+ ++ intercalate "\n" (lines errors')+ ++ "\n" ++ line+ ++ "\nGiving up.." where clean = reverse . dropWhile isSpace . reverse . dropWhile isSpace+ line = take 78 $ repeat '=' standardSolver :: SMTConfig -> String -> ([String] -> a) -> ([String] -> a) -> IO a standardSolver config script failure success = do
Data/SBV/SMT/SMTLib.hs view
@@ -33,8 +33,17 @@ | Just sw <- s `lookup` aliasTable = (show sw, c) | True = (s, c) -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)+toSMTLib :: Bool -- ^ is this a sat problem?+ -> [(SW, String)] -- ^ inputs and aliasing names+ -> [(SW, CW)] -- ^ constants+ -> [((Int, Int, Int), [SW])] -- ^ auto-generated tables+ -> [(Int, ArrayInfo)] -- ^ user specified arrays+ -> [(String, SBVType)] -- ^ uninterpreted functions/constants+ -> [(String, [String])] -- ^ user given axioms+ -> Pgm -- ^ assignments+ -> SW -- ^ output variable+ -> SMTLibPgm+toSMTLib isSat inps consts tbls arrs uis axs asgnsSeq out = SMTLibPgm (aliasTable, pre, post) where logic | null tbls && null arrs && null uis = "QF_BV" | True = "QF_AUFBV"@@ -56,6 +65,8 @@ ++ concatMap declArray arrs ++ [ " ; --- uninterpreted constants ---" ] ++ concatMap declUI uis+ ++ [ " ; --- user given axioms ---" ]+ ++ map declAx axs ++ [ " ; --- assignments ---" ] ++ map cvtAsgn asgns post = [ " ; --- formula ---" ]@@ -83,6 +94,9 @@ in [ " :extrafuns ((" ++ iv ++ " BitVec[" ++ show at ++ "]))" , " :assumption (= (select " ++ nm ++ " " ++ iv ++ ") " ++ show sw ++ ")" ]++declAx :: (String, [String]) -> String+declAx (nm, ls) = (" ;; -- user given axiom: " ++ nm ++ "\n ") ++ intercalate "\n " ls declUI :: (String, SBVType) -> [String] declUI (i, t) = [" :extrafuns ((uninterpreted_" ++ i ++ " " ++ cvtType t ++ "))"]
Data/SBV/TestSuite/PrefixSum/PrefixSum.hs view
@@ -18,7 +18,8 @@ -- Test suite testSuite :: SBVTestSuite-testSuite = mkTestSuite $ \_ -> test [- "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 8 (0, (+)))- , "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax))- ]+testSuite = mkTestSuite $ \goldCheck -> test [+ "prefixSum1" ~: assert =<< isTheorem (flIsCorrect 8 (0, (+)))+ , "prefixSum2" ~: assert =<< isTheorem (flIsCorrect 16 (0, smax))+ , "prefixSum3" ~: runSymbolic (genPrefixSumInstance 16) `goldCheck` "prefixSum_16.gold"+ ]
Data/SBV/TestSuite/Uninterpreted/AUF.hs view
@@ -19,7 +19,8 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [- "auf-0" ~: assert =<< isTheorem thm- , "auf-1" ~: pgm `goldCheck` "auf-1.gold"+ "auf-0" ~: assert =<< isTheorem thm1+ , "auf-1" ~: assert =<< isTheorem thm2+ , "auf-2" ~: pgm `goldCheck` "auf-1.gold" ]- where pgm = runSymbolic $ forAll ["x", "y", "a", "initVal"] thm+ where pgm = runSymbolic $ forAll ["x", "y", "a", "initVal"] thm1
SBVUnitTest/GoldFiles/auf-1.gold view
@@ -12,6 +12,7 @@ ARRAYS UNINTERPRETED CONSTANTS uninterpreted_f :: SWord32 -> SWord64+AXIOMS DEFINE s4 :: SWord32 = s0 + s3 s5 :: SBool = s1 == s4
SBVUnitTest/GoldFiles/basic-2_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s1 - s0
SBVUnitTest/GoldFiles/basic-2_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s1 - s2
SBVUnitTest/GoldFiles/basic-2_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-2_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s0 - s1
SBVUnitTest/GoldFiles/basic-3_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-3_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-3_5.gold view
@@ -8,6 +8,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s3 :: SWord8 = s0 + s2 OUTPUTS
SBVUnitTest/GoldFiles/basic-4_1.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s0 - s0
SBVUnitTest/GoldFiles/basic-4_2.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s1 :: SWord8 = s0 * s0 s2 :: SWord8 = s1 - s1
SBVUnitTest/GoldFiles/basic-4_3.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-4_4.gold view
@@ -6,6 +6,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s1 :: SWord8 = s0 + s0 s2 :: SWord8 = s1 * s1
SBVUnitTest/GoldFiles/basic-4_5.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s1 OUTPUTS
SBVUnitTest/GoldFiles/basic-5_1.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s0 - s0
SBVUnitTest/GoldFiles/basic-5_2.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 * s0 s3 :: SWord8 = s2 - s2
SBVUnitTest/GoldFiles/basic-5_3.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-5_4.gold view
@@ -7,6 +7,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s2 :: SWord8 = s0 + s0 s3 :: SWord8 = s2 * s2
SBVUnitTest/GoldFiles/basic-5_5.gold view
@@ -8,6 +8,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s3 :: SWord8 = s0 + s2 OUTPUTS
SBVUnitTest/GoldFiles/ccitt.gold view
@@ -78,6 +78,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s4 :: SBool = s0 == s2 s5 :: SBool = s1 == s3
SBVUnitTest/GoldFiles/dogCatMouse.gold view
@@ -1,5 +1,4 @@-One solution found-Satisfiable. Model:+Only one solution found: s0 = 3 :: SWord16 s1 = 41 :: SWord16 s2 = 56 :: SWord16
SBVUnitTest/GoldFiles/legato.gold view
@@ -19,6 +19,7 @@ TABLES ARRAYS UNINTERPRETED CONSTANTS+AXIOMS DEFINE s10 :: SBool = s0 /= s2 s11 :: SBool = s0 /= s4
+ SBVUnitTest/GoldFiles/prefixSum_16.gold view
@@ -0,0 +1,117 @@+INPUTS+ s0 :: SWord32+ s1 :: SWord32+ s2 :: SWord32+ s3 :: SWord32+ s4 :: SWord32+ s5 :: SWord32+ s6 :: SWord32+ s7 :: SWord32+ s8 :: SWord32+ s9 :: SWord32+ s10 :: SWord32+ s11 :: SWord32+ s12 :: SWord32+ s13 :: SWord32+ s14 :: SWord32+ s15 :: SWord32+CONSTANTS+ s_2 = False+ s_1 = True+TABLES+ARRAYS+UNINTERPRETED CONSTANTS+ uninterpreted_flOp :: SWord32 -> SWord32 -> SWord32+ uninterpreted_u :: SWord32+AXIOMS+ -- user defined axiom: flOp is associative+ :assumption (forall (?x BitVec[32]) (?y BitVec[32]) (?z BitVec[32])+ (= (uninterpreted_flOp (uninterpreted_flOp ?x ?y) ?z)+ (uninterpreted_flOp ?x (uninterpreted_flOp ?y ?z))+ )+ )+ -- user defined axiom: u is left-unit for flOp+ :assumption (forall (?x BitVec[32])+ (= (uninterpreted_flOp uninterpreted_u ?x)+ ?x+ )+ )+DEFINE+ s16 :: SWord32 = uninterpreted_u+ s17 :: SWord32 = s16 uninterpreted_flOp s0+ s18 :: SBool = s0 == s17+ s19 :: SWord32 = s0 uninterpreted_flOp s1+ s20 :: SWord32 = s16 uninterpreted_flOp s19+ s21 :: SBool = s19 == s20+ s22 :: SWord32 = s19 uninterpreted_flOp s2+ s23 :: SWord32 = s20 uninterpreted_flOp s2+ s24 :: SBool = s22 == s23+ s25 :: SWord32 = s22 uninterpreted_flOp s3+ s26 :: SWord32 = s2 uninterpreted_flOp s3+ s27 :: SWord32 = s19 uninterpreted_flOp s26+ s28 :: SWord32 = s16 uninterpreted_flOp s27+ s29 :: SBool = s25 == s28+ s30 :: SWord32 = s25 uninterpreted_flOp s4+ s31 :: SWord32 = s28 uninterpreted_flOp s4+ s32 :: SBool = s30 == s31+ s33 :: SWord32 = s30 uninterpreted_flOp s5+ s34 :: SWord32 = s4 uninterpreted_flOp s5+ s35 :: SWord32 = s28 uninterpreted_flOp s34+ s36 :: SBool = s33 == s35+ s37 :: SWord32 = s33 uninterpreted_flOp s6+ s38 :: SWord32 = s35 uninterpreted_flOp s6+ s39 :: SBool = s37 == s38+ s40 :: SWord32 = s37 uninterpreted_flOp s7+ s41 :: SWord32 = s6 uninterpreted_flOp s7+ s42 :: SWord32 = s34 uninterpreted_flOp s41+ s43 :: SWord32 = s27 uninterpreted_flOp s42+ s44 :: SWord32 = s16 uninterpreted_flOp s43+ s45 :: SBool = s40 == s44+ s46 :: SWord32 = s40 uninterpreted_flOp s8+ s47 :: SWord32 = s44 uninterpreted_flOp s8+ s48 :: SBool = s46 == s47+ s49 :: SWord32 = s46 uninterpreted_flOp s9+ s50 :: SWord32 = s8 uninterpreted_flOp s9+ s51 :: SWord32 = s44 uninterpreted_flOp s50+ s52 :: SBool = s49 == s51+ s53 :: SWord32 = s49 uninterpreted_flOp s10+ s54 :: SWord32 = s51 uninterpreted_flOp s10+ s55 :: SBool = s53 == s54+ s56 :: SWord32 = s53 uninterpreted_flOp s11+ s57 :: SWord32 = s10 uninterpreted_flOp s11+ s58 :: SWord32 = s50 uninterpreted_flOp s57+ s59 :: SWord32 = s44 uninterpreted_flOp s58+ s60 :: SBool = s56 == s59+ s61 :: SWord32 = s56 uninterpreted_flOp s12+ s62 :: SWord32 = s59 uninterpreted_flOp s12+ s63 :: SBool = s61 == s62+ s64 :: SWord32 = s61 uninterpreted_flOp s13+ s65 :: SWord32 = s12 uninterpreted_flOp s13+ s66 :: SWord32 = s59 uninterpreted_flOp s65+ s67 :: SBool = s64 == s66+ s68 :: SWord32 = s64 uninterpreted_flOp s14+ s69 :: SWord32 = s66 uninterpreted_flOp s14+ s70 :: SBool = s68 == s69+ s71 :: SWord32 = s68 uninterpreted_flOp s15+ s72 :: SWord32 = s14 uninterpreted_flOp s15+ s73 :: SWord32 = s65 uninterpreted_flOp s72+ s74 :: SWord32 = s58 uninterpreted_flOp s73+ s75 :: SWord32 = s43 uninterpreted_flOp s74+ s76 :: SBool = s71 == s75+ s77 :: SBool = s70 & s76+ s78 :: SBool = s67 & s77+ s79 :: SBool = s63 & s78+ s80 :: SBool = s60 & s79+ s81 :: SBool = s55 & s80+ s82 :: SBool = s52 & s81+ s83 :: SBool = s48 & s82+ s84 :: SBool = s45 & s83+ s85 :: SBool = s39 & s84+ s86 :: SBool = s36 & s85+ s87 :: SBool = s32 & s86+ s88 :: SBool = s29 & s87+ s89 :: SBool = s24 & s88+ s90 :: SBool = s21 & s89+ s91 :: SBool = s18 & s90+OUTPUTS+ s91
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 0.9.8+Version: 0.9.9 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math Synopsis: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers. Description: Express properties about bit-precise Haskell programs and automatically prove