diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -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 diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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." diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -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? diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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) diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,7 +1,14 @@ Hackage: GitHub: -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Fri Oct 19 06:17:52 PDT 2012" +buildTime = "Fri Oct 19 18:57:09 PDT 2012" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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