sbv 2.5 → 2.6
raw patch · 8 files changed
+26/−19 lines, 8 files
Files
- Data/SBV/BitVectors/Data.hs +10/−10
- Data/SBV/Compilers/C.hs +1/−1
- Data/SBV/SMT/SMTLib.hs +1/−1
- Data/SBV/SMT/SMTLib1.hs +2/−2
- Data/SBV/SMT/SMTLib2.hs +2/−2
- RELEASENOTES +8/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +1/−1
Data/SBV/BitVectors/Data.hs view
@@ -30,7 +30,7 @@ , sbvToSW, sbvToSymSW , SBVExpr(..), newExpr , cache, uncache, uncacheAI, HasKind(..)- , Op(..), NamedSymVar, UnintKind(..), getTableIndex, Pgm, Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..)+ , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials@@ -340,7 +340,7 @@ show (SBVApp op args) = unwords (show op : map show args) -- | A program is a sequence of assignments-type Pgm = S.Seq (SW, SBVExpr)+newtype SBVPgm = SBVPgm {pgmAssignments :: (S.Seq (SW, SBVExpr))} -- | 'NamedSymVar' pairs symbolic words and user given/automatically generated names type NamedSymVar = (SW, String)@@ -361,7 +361,7 @@ [(Int, ArrayInfo)] -- arrays (user specified) [(String, SBVType)] -- uninterpreted constants [(String, [String])] -- axioms- Pgm -- assignments+ SBVPgm -- assignments [SW] -- additional constraints (boolean) [SW] -- outputs @@ -394,7 +394,7 @@ ++ ["AXIOMS"] ++ map shax axs ++ ["DEFINE"]- ++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList xs)+ ++ map (\(s, e) -> " " ++ shs s ++ " = " ++ show e) (F.toList (pgmAssignments xs)) ++ ["CONSTRAINTS"] ++ map ((" " ++) . show) cstrs ++ ["OUTPUTS"]@@ -489,7 +489,7 @@ , rConstraints :: IORef [SW] , routs :: IORef [SW] , rtblMap :: IORef TableMap- , spgm :: IORef Pgm+ , spgm :: IORef SBVPgm , rconstMap :: IORef CnstMap , rexprMap :: IORef ExprMap , rArrayMap :: IORef ArrayMap@@ -639,7 +639,7 @@ KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y)) KReal -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True)) _ -> return ()- modifyIORef (spgm st) (flip (S.|>) (sw, e))+ modifyIORef (spgm st) (\(SBVPgm xs) -> SBVPgm (xs S.|> (sw, e))) modifyIORef (rexprMap st) (Map.insert e sw) return sw {-# INLINE newExpr #-}@@ -757,7 +757,7 @@ runSymbolic' currentRunMode (Symbolic c) = do ctr <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements cInfo <- newIORef []- pgm <- newIORef S.empty+ pgm <- newIORef (SBVPgm S.empty) emap <- newIORef Map.empty cmap <- newIORef Map.empty inps <- newIORef []@@ -798,7 +798,7 @@ _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW r <- runReaderT c st- rpgm <- readIORef pgm+ SBVPgm rpgm <- readIORef pgm inpsO <- reverse `fmap` readIORef inps outsO <- reverse `fmap` readIORef outs let swap (a, b) = (b, a)@@ -813,7 +813,7 @@ traceVals <- reverse `fmap` readIORef cInfo extraCstrs <- reverse `fmap` readIORef cstrs usorts <- reverse `fmap` readIORef sorts- return $ (r, Result boundInfo usorts traceVals cgMap inpsO cnsts tbls arrs unint axs rpgm extraCstrs outsO)+ return $ (r, Result boundInfo usorts traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO) ------------------------------------------------------------------------------- -- * Symbolic Words@@ -1141,4 +1141,4 @@ rnf (Cached f) = f `seq` () instance NFData a => NFData (SBV a) where rnf (SBV x y) = rnf x `seq` rnf y `seq` ()-instance NFData Pgm+instance NFData SBVPgm
Data/SBV/Compilers/C.hs view
@@ -381,7 +381,7 @@ -- | Generate the C program genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]-genCProg cfg fn proto (Result (hasIntegers, hasReals) usorts _tvals cgs ins preConsts tbls arrs _ _ asgns cstrs _) inVars outVars mbRet extDecls+genCProg cfg fn proto (Result (hasIntegers, hasReals) usorts _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs _) inVars outVars mbRet extDecls | isNothing (cgInteger cfg) && hasIntegers = error $ "SBV->C: Unbounded integers are not supported by the C compiler." ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation."
Data/SBV/SMT/SMTLib.hs view
@@ -29,7 +29,7 @@ -> [(Int, ArrayInfo)] -- ^ user specified arrays -> [(String, SBVType)] -- ^ uninterpreted functions/constants -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments+ -> SBVPgm -- ^ assignments -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> SMTLibPgm
Data/SBV/SMT/SMTLib1.hs view
@@ -51,7 +51,7 @@ -> [(Int, ArrayInfo)] -- ^ user specified arrays -> [(String, SBVType)] -- ^ uninterpreted functions/constants -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments+ -> SBVPgm -- ^ assignments -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String])@@ -101,7 +101,7 @@ ++ [ " ; --- formula ---" ] ++ [mkFormula isSat out] ++ [")"]- asgns = F.toList asgnsSeq+ asgns = F.toList (pgmAssignments asgnsSeq) mkCstr s = " :assumption (= " ++ show s ++ " bv1[1])" -- TODO: Does this work for SMT-Lib when the index/element types are signed?
Data/SBV/SMT/SMTLib2.hs view
@@ -68,11 +68,11 @@ -> [(Int, ArrayInfo)] -- ^ user specified arrays -> [(String, SBVType)] -- ^ uninterpreted functions/constants -> [(String, [String])] -- ^ user given axioms- -> Pgm -- ^ assignments+ -> SBVPgm -- ^ assignments -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String])-cvt (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, [])+cvt (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, []) where -- the logic is an over-approaximation logic | hasInteger || hasReal || not (null sorts)
RELEASENOTES view
@@ -1,7 +1,14 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 2.5+Latest Hackage released version: 2.6++======================================================================+Version 2.6, 2012-10-20++ - Workaround issues related hackage compilation, in particular to the+ problem with the new containers package release, which does provide+ an NFData instance for sequences. ====================================================================== Version 2.5, 2012-10-19
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Fri Oct 19 06:17:52 PDT 2012"+buildTime = "Fri Oct 19 18:57:09 PDT 2012"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 2.5+Version: 2.6 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT