sbv 5.8 → 5.9
raw patch · 17 files changed
+211/−52 lines, 17 files
Files
- CHANGES.md +20/−1
- Data/SBV/BitVectors/Model.hs +56/−6
- Data/SBV/BitVectors/Symbolic.hs +11/−10
- Data/SBV/Examples/BitPrecise/Legato.hs +9/−8
- Data/SBV/Examples/Misc/Auxiliary.hs +63/−0
- Data/SBV/Examples/Puzzles/U2Bridge.hs +23/−13
- Data/SBV/Provers/ABC.hs +1/−1
- Data/SBV/Provers/Boolector.hs +1/−1
- Data/SBV/Provers/CVC4.hs +1/−1
- Data/SBV/Provers/MathSAT.hs +1/−1
- Data/SBV/Provers/Prover.hs +3/−1
- Data/SBV/Provers/Yices.hs +5/−1
- Data/SBV/Provers/Z3.hs +1/−1
- Data/SBV/SMT/SMT.hs +12/−4
- Data/SBV/SMT/SMTLib2.hs +1/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +2/−1
CHANGES.md view
@@ -1,7 +1,26 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.8, 2016-01-01+* Latest Hackage released version: 5.9, 2016-01-05++### Version 5.9, 2016-01-05++ * Default definition for 'symbolicMerge', which allows types that are+ instances of 'Generic' to have an automatically derivable merge (i.e.,+ ite) instance. Thanks to Christian Conkle for the patch.++ * Add support for "non-model-vars," where we can now tell SBV not+ to take into account certain variables from a model-building+ perspective. This comes handy in doing an `allSat` calls where+ there might be witness variables that we do not care the uniqueness+ for. See "Data/SBV/Examples/Misc/Auxiliary.hs" for an example, and+ the discussion in https://github.com/LeventErkok/sbv/issues/208 for+ motivation.++ * Yices interface: If Reals are used, then pick the logic QF_UFLRA, instead+ of QF_AUFLIA. Unfortunately, logic selection remains tricky since the SMTLib+ story for logic selection is rather messy. Other solvers are not impacted+ by this change. ### Version 5.8, 2016-01-01
Data/SBV/BitVectors/Model.hs view
@@ -18,6 +18,8 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DefaultSignatures #-} module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral@@ -41,6 +43,8 @@ import Control.Monad.Reader (ask) import Control.Monad.Trans (liftIO) +import GHC.Generics (U1(..), M1(..), (:*:)(..), K1(..))+import qualified GHC.Generics as G import GHC.Stack.Compat import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize)@@ -1076,11 +1080,20 @@ -- provides all basic types as instances of this class, so users only need -- to declare instances for custom data-types of their programs as needed. --+-- A 'Mergeable' instance may be automatically derived for a custom data-type+-- with a single constructor where the type of each field is an instance of+-- 'Mergeable', such as a record of symbolic values. Users only need to add+-- 'G.Generic' and 'Mergeable' to the @deriving@ clause for the data-type. See+-- 'Data.SBV.Examples.Puzzles.U2Bridge.Status' for an example and an+-- illustration of what the instance would look like if written by hand.+-- -- The function 'select' is a total-indexing function out of a list of choices -- with a default value, simulating array/list indexing. It's an n-way generalization -- of the 'ite' function. ----- Minimal complete definition: 'symbolicMerge'+-- Minimal complete definition: None, if the type is instance of 'Generic'. Otherwise+-- 'symbolicMerge'. Note that most types subject to merging are likely to be+-- trivial instances of 'Generic'. class Mergeable a where -- | Merge two values based on the condition. The first argument states -- whether we force the then-and-else branches before the merging, at the@@ -1090,7 +1103,7 @@ symbolicMerge :: Bool -> SBool -> a -> a -> a -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@- -- overflows+ -- underflows/overflows. select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a -- NB. Earlier implementation of select used the binary-search trick -- on the index to chop down the search space. While that is a good trick@@ -1100,15 +1113,20 @@ -- list is really humongous, which is not very common in general. (Also, -- for the case when the list is bit-vectors, we use SMT tables anyhow.) select xs err ind- | isReal ind = error "SBV.select: unsupported real valued select/index expression"- | isFloat ind = error "SBV.select: unsupported float valued select/index expression"- | isDouble ind = error "SBV.select: unsupported double valued select/index expression"+ | isReal ind = bad "real"+ | isFloat ind = bad "float"+ | isDouble ind = bad "double" | hasSign ind = ite (ind .< 0) err (walk xs ind err) | True = walk xs ind err- where walk [] _ acc = acc+ where bad w = error $ "SBV.select: unsupported " ++ w ++ " valued select/index expression"+ walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) + -- Default implementation for 'symbolicMerge' if the type is 'Generic'+ default symbolicMerge :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a+ symbolicMerge = symbolicMergeDefault + -- | If-then-else. This is by definition 'symbolicMerge' with both -- branches forced. This is typically the desired behavior, but also -- see 'iteLazy' should you need more laziness.@@ -1269,6 +1287,38 @@ where i a b = symbolicMerge f t a b select xs (err1, err2, err3, err4, err5, err6, err7) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind, select gs err7 ind) where (as, bs, cs, ds, es, fs, gs) = unzip7 xs++-- Arbitrary product types, using GHC.Generics+--+-- NB: Because of the way GHC.Generics works, the implementation of+-- symbolicMerge' is recursive. The derived instance for @data T a = T a a a a@+-- resembles that for (a, (a, (a, a))), not the flat 4-tuple (a, a, a, a). This+-- difference should have no effect in practice. Note also that, unlike the+-- hand-rolled tuple instances, the generic instance does not provide a custom+-- 'select' implementation, and so does not benefit from the SMT-table+-- implementation in the 'SBV a' instance.++-- | Not exported. Symbolic merge using the generic representation provided by+-- 'G.Generics'.+symbolicMergeDefault :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a+symbolicMergeDefault force t x y = G.to $ symbolicMerge' force t (G.from x) (G.from y)++-- | Not exported. Used only in 'symbolicMergeDefault'. Instances are provided for+-- the generic representations of product types where each element is Mergeable.+class GMergeable f where+ symbolicMerge' :: Bool -> SBool -> f a -> f a -> f a++instance GMergeable U1 where+ symbolicMerge' _ _ _ _ = U1++instance (Mergeable c) => GMergeable (K1 i c) where+ symbolicMerge' force t (K1 x) (K1 y) = K1 $ symbolicMerge force t x y++instance (GMergeable f) => GMergeable (M1 i c f) where+ symbolicMerge' force t (M1 x) (M1 y) = M1 $ symbolicMerge' force t x y++instance (GMergeable f, GMergeable g) => GMergeable (f :*: g) where+ symbolicMerge' force t (x1 :*: y1) (x2 :*: y2) = symbolicMerge' force t x1 x2 :*: symbolicMerge' force t y1 y2 -- Bounded instances instance (SymWord a, Bounded a) => Bounded (SBV a) where
Data/SBV/BitVectors/Symbolic.hs view
@@ -996,16 +996,16 @@ -- | Translation tricks needed for specific capabilities afforded by each solver data SolverCapabilities = SolverCapabilities {- capSolverName :: String -- ^ Name of the solver- , mbDefaultLogic :: Maybe String -- ^ set-logic string to use in case not automatically determined (if any)- , supportsMacros :: Bool -- ^ Does the solver understand SMT-Lib2 macros?- , supportsProduceModels :: Bool -- ^ Does the solver understand produce-models option setting- , supportsQuantifiers :: Bool -- ^ Does the solver understand SMT-Lib2 style quantifiers?- , supportsUninterpretedSorts :: Bool -- ^ Does the solver understand SMT-Lib2 style uninterpreted-sorts- , supportsUnboundedInts :: Bool -- ^ Does the solver support unbounded integers?- , supportsReals :: Bool -- ^ Does the solver support reals?- , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers?- , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers?+ capSolverName :: String -- ^ Name of the solver+ , mbDefaultLogic :: Bool -> Maybe String -- ^ set-logic string to use in case not automatically determined (if any). If Bool is True, then reals are present.+ , supportsMacros :: Bool -- ^ Does the solver understand SMT-Lib2 macros?+ , supportsProduceModels :: Bool -- ^ Does the solver understand produce-models option setting+ , supportsQuantifiers :: Bool -- ^ Does the solver understand SMT-Lib2 style quantifiers?+ , supportsUninterpretedSorts :: Bool -- ^ Does the solver understand SMT-Lib2 style uninterpreted-sorts+ , supportsUnboundedInts :: Bool -- ^ Does the solver support unbounded integers?+ , supportsReals :: Bool -- ^ Does the solver support reals?+ , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers?+ , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? } -- | Rounding mode to be used for the IEEE floating-point operations.@@ -1051,6 +1051,7 @@ , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.+ , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) , smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool , solver :: SMTSolver -- ^ The actual SMT solver.
Data/SBV/Examples/BitPrecise/Legato.hs view
@@ -31,12 +31,17 @@ -- is indeed correct. ----------------------------------------------------------------------------- +{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveAnyClass #-}+ module Data.SBV.Examples.BitPrecise.Legato where import Data.Array (Array, Ix(..), (!), (//), array) import Data.SBV +import GHC.Generics (Generic)+ ------------------------------------------------------------------ -- * Mostek architecture ------------------------------------------------------------------@@ -68,23 +73,19 @@ -- | Abstraction of the machine: The CPU consists of memory, registers, and flags. -- Unlike traditional hardware, we assume the program is stored in some other memory area that -- we need not model. (No self modifying programs!)+--+-- 'Mostek' is equipped with an automatically derived 'Mergeable' instance+-- because each field is 'Mergeable'. data Mostek = Mostek { memory :: Memory , registers :: Registers , flags :: Flags- }+ } deriving (Generic, Mergeable) -- | Given a machine state, compute a value out of it type Extract a = Mostek -> a -- | Programs are essentially state transformers (on the machine state) type Program = Mostek -> Mostek---- | 'Mergeable' instance of 'Mostek' simply pushes the merging into record fields.-instance Mergeable Mostek where- symbolicMerge f b m1 m2 = Mostek { memory = symbolicMerge f b (memory m1) (memory m2)- , registers = symbolicMerge f b (registers m1) (registers m2)- , flags = symbolicMerge f b (flags m1) (flags m2)- } ------------------------------------------------------------------ -- * Low-level operations
+ Data/SBV/Examples/Misc/Auxiliary.hs view
@@ -0,0 +1,63 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Misc.Auxiliary+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Demonstrates model construction with auxiliary variables. Sometimes we+-- need to introduce a variable in our problem as an existential variable,+-- but it's "internal" to the problem and we do not consider it as part of+-- the solution. Also, in an `allSat` scenario, we may not care for models+-- that only differ in these auxiliaries. SBV allows designating such variables+-- as `isNonModelVar` so we can still use them like any other variable, but without+-- considering them explicitly in model construction.+-----------------------------------------------------------------------------++module Data.SBV.Examples.Misc.Auxiliary where++import Data.SBV++-- | A simple predicate, based on two variables @x@ and @y@, true when+-- @0 <= x <= 1@ and @x - abs y@ is @0@.+problem :: Predicate+problem = do x <- free "x"+ y <- free "y"+ constrain $ x .>= 0+ constrain $ x .<= 1+ return $ x - abs y .== (0 :: SInteger)++-- | Generate all satisfying assignments for our problem. We have:+--+-- >>> allModels+-- Solution #1:+-- x = 0 :: Integer+-- y = 0 :: Integer+-- Solution #2:+-- x = 1 :: Integer+-- y = -1 :: Integer+-- Solution #3:+-- x = 1 :: Integer+-- y = 1 :: Integer+-- Found 3 different solutions.+--+-- Note that solutions @2@ and @3@ share the value @x = 1@, since there are+-- multiple values of @y@ that make this particular choice of @x@ satisfy our constraint.+allModels :: IO AllSatResult+allModels = allSat problem++-- | Generate all satisfying assignments, but we first tell SBV that @y@ should not be considered+-- as a model problem, i.e., it's auxiliary. We have:+--+-- >>> modelsWithYAux+-- Solution #1:+-- x = 0 :: Integer+-- Solution #2:+-- x = 1 :: Integer+-- Found 2 different solutions.+--+-- Note that we now have only two solutions, one for each unique value of @x@ that satisfy our+-- constraint.+modelsWithYAux :: IO AllSatResult+modelsWithYAux = allSatWith z3{isNonModelVar = (`elem` ["y"])} problem
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -19,7 +20,9 @@ import Control.Monad (unless) import Control.Monad.State (State, runState, put, get, modify, evalState) -import Data.Generics+import Data.Generics (Data)+import GHC.Generics (Generic)+ import Data.SBV -------------------------------------------------------------@@ -68,14 +71,32 @@ [here, there] = map literal [Here, There] -- | The status of the puzzle after each move+--+-- This type is equipped with an automatically derived 'Mergeable' instance+-- because each field is 'Mergeable'. A 'Generic' instance must also be derived+-- for this to work, and the 'DeriveAnyClass' language extension must be+-- enabled. The derived 'Mergeable' instance simply walks down the structure+-- field by field and merges each one. An equivalent hand-written 'Mergeable'+-- instance is provided in a comment below. data Status = Status { time :: STime -- ^ elapsed time , flash :: SLocation -- ^ location of the flash , lBono :: SLocation -- ^ location of Bono , lEdge :: SLocation -- ^ location of Edge , lAdam :: SLocation -- ^ location of Adam , lLarry :: SLocation -- ^ location of Larry- }+ } deriving (Generic, Mergeable) +-- The derived Mergeable instance is equivalent to the following:+--+-- instance Mergeable Status where+-- symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2)+-- , flash = symbolicMerge f t (flash s1) (flash s2)+-- , lBono = symbolicMerge f t (lBono s1) (lBono s2)+-- , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2)+-- , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2)+-- , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2)+-- }+ -- | Start configuration, time elapsed is 0 and everybody is 'here' start :: Status start = Status { time = 0@@ -85,17 +106,6 @@ , lAdam = here , lLarry = here }---- | Mergeable instance for 'Status' simply walks down the structure fields and--- merges them.-instance Mergeable Status where- symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2)- , flash = symbolicMerge f t (flash s1) (flash s2)- , lBono = symbolicMerge f t (lBono s1) (lBono s2)- , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2)- , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2)- , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2)- } -- | A puzzle move is modeled as a state-transformer type Move a = State Status a
Data/SBV/Provers/ABC.hs view
@@ -27,7 +27,7 @@ , engine = standardEngine "SBV_ABC" "SBV_ABC_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "ABC"- , mbDefaultLogic = Nothing+ , mbDefaultLogic = const Nothing , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = False
Data/SBV/Provers/Boolector.hs view
@@ -25,7 +25,7 @@ , engine = standardEngine "SBV_BOOLECTOR" "SBV_BOOLECTOR_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "Boolector"- , mbDefaultLogic = Nothing+ , mbDefaultLogic = const Nothing , supportsMacros = False , supportsProduceModels = True , supportsQuantifiers = False
Data/SBV/Provers/CVC4.hs view
@@ -27,7 +27,7 @@ , engine = standardEngine "SBV_CVC4" "SBV_CVC4_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "CVC4"- , mbDefaultLogic = Just "ALL_SUPPORTED" -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary+ , mbDefaultLogic = const (Just "ALL_SUPPORTED") -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = True
Data/SBV/Provers/MathSAT.hs view
@@ -27,7 +27,7 @@ , engine = standardEngine "SBV_MATHSAT" "SBV_MATHSAT_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "MathSAT"- , mbDefaultLogic = Nothing+ , mbDefaultLogic = const Nothing , supportsMacros = False , supportsProduceModels = True , supportsQuantifiers = True
Data/SBV/Provers/Prover.hs view
@@ -66,6 +66,7 @@ , solverTweaks = tweaks , smtLibVersion = smtVersion , satCmd = "(check-sat)"+ , isNonModelVar = const False -- i.e., everything is a model-variable by default , roundingMode = RoundNearestTiesToEven , useLogic = Nothing }@@ -412,7 +413,8 @@ curResult <- invoke nonEqConsts n sbvPgm case curResult of Nothing -> return []- Just (SatResult r) -> let cont model = do rest <- unsafeInterleaveIO $ loop (n+1) (modelAssocs model : nonEqConsts)+ Just (SatResult r) -> let cont model = do let modelOnlyAssocs = [v | v@(x, _) <- modelAssocs model, not (isNonModelVar config x)]+ rest <- unsafeInterleaveIO $ loop (n+1) (modelOnlyAssocs : nonEqConsts) return (r : rest) in case r of Satisfiable _ (SMTModel []) -> return [r]
Data/SBV/Provers/Yices.hs view
@@ -27,7 +27,7 @@ , engine = standardEngine "SBV_YICES" "SBV_YICES_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "Yices"- , mbDefaultLogic = Just "QF_AUFLIA"+ , mbDefaultLogic = logic , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = False@@ -39,3 +39,7 @@ } } where addTimeOut _ _ = error "Yices: Timeout values are not supported by Yices"+ -- Yices doesn't like it if we don't set the logic; so pick one and hope for the best+ logic hasReals+ | hasReals = Just "QF_UFLRA"+ | True = Just "QF_AUFLIA"
Data/SBV/Provers/Z3.hs view
@@ -56,7 +56,7 @@ standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps)) , capabilities = SolverCapabilities { capSolverName = "Z3"- , mbDefaultLogic = Nothing+ , mbDefaultLogic = const Nothing , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = True
Data/SBV/SMT/SMT.hs view
@@ -97,7 +97,7 @@ _ -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn sh i c = (ok, showSMTResult "Unsatisfiable" "Unknown" "Unknown. Potential model:\n"- ("Solution #" ++ show i ++ ":\n[Backend solver returned no assignment to variables.]") ("Solution #" ++ show i ++ ":\n") c)+ ("Solution #" ++ show i ++ ":\nSatisfiable") ("Solution #" ++ show i ++ ":\n") c) where ok = case c of Satisfiable{} -> True _ -> False@@ -345,10 +345,18 @@ where cfg = resultConfig result -- | Show a model in human readable form. Ignore bindings to those variables that start--- with "__internal_sbv_"; as these are only for internal purposes+-- with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes showModel :: SMTConfig -> SMTModel -> String-showModel cfg = intercalate "\n" . display . map shM . filter (not . ignore) . modelAssocs- where ignore (s, _) = "__internal_sbv_" `isPrefixOf` s+showModel cfg model+ | null allVars+ = "[There are no variables bound by the model.]"+ | null relevantVars+ = "[There are no model-variables bound by the model.]"+ | True+ = intercalate "\n" . display . map shM $ relevantVars+ where allVars = modelAssocs model+ relevantVars = filter (not . ignore) allVars+ ignore (s, _) = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s shM (s, v) = let vs = shCW cfg v in ((length s, s), (vlength vs, vs)) display svs = map line svs where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v
Data/SBV/SMT/SMTLib2.hs view
@@ -117,7 +117,7 @@ | not (null usorts) = "has user-defined sorts" | hasNonBVArrays = "has non-bitvector arrays" | True = "cannot determine the SMTLib-logic to use"- in case mbDefaultLogic solverCaps of+ in case mbDefaultLogic solverCaps hasReal of Nothing -> ["; " ++ why ++ ", no logic specified."] Just l -> ["(set-logic " ++ l ++ "); " ++ why ++ ", using solver-default logic."] | True
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Fri Jan 1 12:25:00 PST 2016"+buildTime = "Tue Jan 5 17:59:03 PST 2016"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 5.8+Version: 5.9 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@@ -79,6 +79,7 @@ , Data.SBV.Examples.Misc.Enumerate , Data.SBV.Examples.Misc.Floating , Data.SBV.Examples.Misc.ModelExtract+ , Data.SBV.Examples.Misc.Auxiliary , Data.SBV.Examples.Misc.NoDiv0 , Data.SBV.Examples.Misc.Word4 , Data.SBV.Examples.Polynomials.Polynomials