packages feed

sbv 10.10 → 10.11

raw patch · 69 files changed

+1079/−558 lines, 69 filesdep ~libBF

Dependency ranges changed: libBF

Files

CHANGES.md view
@@ -1,6 +1,26 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://github.com/LeventErkok/sbv> +### Version 10.11, 2024-07-26++  * Add Documentation.SBV.Examples.Puzzles.Tower module, solving the visible towers puzzle.++  * Fix several representation bugs related to arbitrary-precision floats. Thanks to Sirui+    Lu for the reports and patches.++  * Removed the generic Num a => Num (SBV a) instance. When used at a non-standard type, this+    created type-checking but invalid SBV programs. See https://github.com/LeventErkok/sbv/issues/706+    for details.++  * Add functions optLexicographic, optLexicographicWith, optPareto, optParetoWith, optIndependent, optIndependentWith+    which makes using optimization functions easier. These are simple wrappers over the existing optimization routines,+    simplifying their interface.++  * Change how optimization results are presented when the underlying metric space is different from the type+    being optimized. As noted in https://github.com/LeventErkok/sbv/issues/716, the format SBV used was confusing.+    We now be more explicit, and print the original value in its own right, along with the metric-space value.+    Thanks to Andrew Anderson for reporting.+ ### Version 10.10, 2024-05-11    * Add EqSymbolic, OrdSymbolic and Mergeable instances for NonEmpty type
Data/SBV.hs view
@@ -324,7 +324,6 @@   , sat, satWith   , dsat, dsatWith   , allSat, allSatWith-  , optimize, optimizeWith   , isVacuousProof, isVacuousProofWith   , isTheorem, isTheoremWith, isSatisfiable, isSatisfiableWith   , proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll@@ -368,6 +367,10 @@    -- * Optimization   -- $optiIntro+  , optimize, optimizeWith+  , optLexicographic, optLexicographicWith+  , optPareto, optParetoWith+  , optIndependent, optIndependentWith    -- ** Multiple optimization goals   -- $multiOpt@@ -431,7 +434,7 @@ import Data.SBV.Core.AlgReals import Data.SBV.Core.Data       hiding (free, free_, mkFreeVars,                                         output, symbolic, symbolics, mkSymVal,-                                        newArray, newArray_)+                                        newArray, newArray_, bvExtract, bvDrop, bvTake, (#)) import Data.SBV.Core.Model      hiding (assertWithPenalty, minimize, maximize,                                         solve, sBool, sBool_, sBools, sChar, sChar_, sChars,                                         sDouble, sDouble_, sDoubles, sFloat, sFloat_, sFloats,@@ -440,18 +443,17 @@                                         sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads,                                         sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s,                                         sInt64, sInt64_, sInt64s, sInteger, sInteger_, sIntegers,+                                        sWord, sWords, sWord_, sInt, sInts, sInt_,                                         sList, sList_, sLists, sTuple, sTuple_, sTuples,                                         sReal, sReal_, sReals, sString, sString_, sStrings,                                         sRational, sRational_, sRationals,                                         sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s,                                         sWord32, sWord32_, sWord32s, sWord64, sWord64_, sWord64s,                                         sMaybe, sMaybe_, sMaybes, sEither, sEither_, sEithers, sSet, sSet_, sSets,-                                        sBarrelRotateLeft, sBarrelRotateRight)--import qualified Data.SBV.Core.Model as M (sBarrelRotateLeft, sBarrelRotateRight)+                                        sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend, sObserve) -import           Data.SBV.Core.Sized       hiding (sWord, sWord_, sWords, sInt, sInt_, sInts, bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake)-import qualified Data.SBV.Core.Sized as CS+import qualified Data.SBV.Core.Model as M  (sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend)+import qualified Data.SBV.Core.Data  as CD (bvExtract, (#), bvDrop, bvTake)  import Data.SBV.Core.Kind @@ -497,7 +499,7 @@  --- $setup --- >>> -- For doctest purposes only:---- >>> :set -XDataKinds+--- >>> :set -XDataKinds -XFlexibleContexts -XTypeApplications -XRankNTypes --- >>> import Data.Proxy  -- | Show a value in detailed (cracked) form, if possible.@@ -1373,7 +1375,7 @@                                       -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold                                       -> SBV (bv n)             -- ^ Input bit vector of size @n@                                       -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@-bvExtract = CS.bvExtract+bvExtract = CD.bvExtract  -- | Join two bitvectors. --@@ -1384,7 +1386,7 @@        ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side          -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side          -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@-(#) = (CS.#)+(#) = (CD.#) infixr 5 #  -- | Zero extend a bit-vector.@@ -1398,7 +1400,7 @@                              , BVIsNonZero (m - n)                              ) => SBV (bv n)    -- ^ Input, of size @n@                                -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold-zeroExtend = CS.zeroExtend+zeroExtend = M.zeroExtend  -- | Sign extend a bit-vector. --@@ -1411,10 +1413,10 @@                              , n + 1 <= m                              , SFiniteBits (bv n)                              , SIntegral   (bv (m - n))-                             , BVIsNonZero   (m - n)+                             , BVIsNonZero (m - n)                              ) => SBV (bv n)  -- ^ Input, of size @n@                                -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold-signExtend = CS.signExtend+signExtend = M.signExtend  -- | Drop bits from the top of a bit-vector. --@@ -1430,7 +1432,7 @@                                  ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.                                    -> SBV (bv n)                 -- ^ Input, of size @n@                                    -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.-bvDrop = CS.bvDrop+bvDrop = CD.bvDrop  -- | Take bits from the top of a bit-vector. --@@ -1446,7 +1448,7 @@                                ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.                                  -> SBV (bv n)               -- ^ Input, of size @n@                                  -> SBV (bv i)               -- ^ Output, of size @i@-bvTake = CS.bvTake+bvTake = CD.bvTake  -- | A helper class to convert sized bit-vectors to/from bytes. class ByteConverter a where@@ -1706,5 +1708,46 @@                           internalConstraint (getRootState st) False [] eq                         newExpr st KBool $ SBVApp (SpecialRelOp ka iop) []++-- | Optimize lexicographically, with the default solver.+optLexicographic :: Satisfiable a => a -> IO SMTResult+optLexicographic = optLexicographicWith defaultSMTCfg++-- | Optimize lexicographically, using the given solver.+optLexicographicWith :: Satisfiable a => SMTConfig -> a -> IO SMTResult+optLexicographicWith config p = do+   res <- optimizeWith config Lexicographic p+   case res of+     LexicographicResult r -> pure r+     _                     -> error $ "A lexicographic optimization call resulted in a bad result:"+                                    ++ "\n" ++ show res++-- | Pareto front optimization, with the default solver.+optPareto :: Satisfiable a => Maybe Int -> a -> IO (Bool, [SMTResult])+optPareto = optParetoWith defaultSMTCfg++-- | Pareto front optimization, with the given solver. The optional integer argument is the number of fronts to return. If 'Nothing', then+-- we will return all pareto fronts. If the first component of the result is 'True' then we reached the pareto-query limit specified by+-- the user, so there might be more unqueried results remaining. If 'False', it means that all the pareto fronts are returned.+optParetoWith :: Satisfiable a => SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])+optParetoWith config mbLim p = do+   res <- optimizeWith config (Pareto mbLim) p+   case res of+     ParetoResult r -> pure r+     _              -> error $ "A pareto optimization call resulted in a bad result:"+                             ++ "\n" ++ show res++-- | Independent optimization, with the default solver. In each result, string is the name of the objective optimized given by the user.+optIndependent :: Satisfiable a => a -> IO [(String, SMTResult)]+optIndependent = optIndependentWith defaultSMTCfg++-- | Independent optimization, with the given solver. In each result, string is the name of the objective optimized given by the user.+optIndependentWith :: Satisfiable a => SMTConfig -> a -> IO [(String, SMTResult)]+optIndependentWith config p = do+   res <- optimizeWith config Independent p+   case res of+     IndependentResult r -> pure r+     _                   -> error $ "An independent optimization call resulted in a bad result:"+                                  ++ "\n" ++ show res  {- HLint ignore module "Use import/export shortcut" -}
Data/SBV/Client/BaseIO.hs view
@@ -25,20 +25,20 @@ module Data.SBV.Client.BaseIO where  import Data.SBV.Core.Data      (HasKind, Kind, Outputtable, Penalty, SymArray,-                                SymVal, SBool, SBV, SChar, SDouble, SFloat,+                                SymVal, SBool, SBV, SChar, SDouble, SFloat, SWord, SInt,                                 SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad, SFloatingPoint,                                 SInt8, SInt16, SInt32, SInt64, SInteger, SList,                                 SReal, SString, SV, SWord8, SWord16, SWord32,                                 SWord64, SEither, SRational, SMaybe, SSet, constrain, (.==))-import Data.SBV.Core.Sized     (SInt, SWord, IntN, WordN)+import Data.SBV.Core.Sized     (IntN, WordN) import Data.SBV.Core.Kind      (BVIsNonZero, ValidFloat) import Data.SBV.Core.Model     (Metric(..), SymTuple) import Data.SBV.Core.Symbolic  (Objective, OptimizeStyle, Result, VarContext, Symbolic, SBVRunMode, SMTConfig,                                 SVal, symbolicEnv, rPartitionVars, State(..)) import Data.SBV.Control.Types  (SMTOption) import Data.SBV.Provers.Prover (Provable, Satisfiable, SExecutable, ThmResult)-import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult,-                                OptimizeResult)+import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult, OptimizeResult)+import Data.SBV.Utils.Lib      (checkObservableName)  import GHC.TypeLits (KnownNat, TypeError, ErrorMessage(..)) import Data.Kind@@ -49,7 +49,6 @@ import Data.IORef(readIORef, writeIORef)  import qualified Data.SBV.Core.Data      as Trans-import qualified Data.SBV.Core.Sized     as Trans import qualified Data.SBV.Core.Model     as Trans import qualified Data.SBV.Core.Symbolic  as Trans import qualified Data.SBV.Provers.Prover as Trans@@ -890,6 +889,18 @@ -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.outputSVal' outputSVal :: SVal -> Symbolic () outputSVal = Trans.outputSVal++-- | A variant of observe that you can use at the top-level. This is useful with quick-check, for instance.+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sObserve'+sObserve :: SymVal a => String -> SBV a -> Symbolic ()+sObserve m x+  | Just bad <- checkObservableName m+  = error bad+  | True+  = do st <- symbolicEnv+       liftIO $ do xsv <- Trans.sbvToSV st x+                   Trans.recordObservable st m (const True) xsv  -- | Capturing non-matching instances for better error messages, conversions from sized type FromSizedErr (arg :: Type) =     'Text "fromSized: Cannot convert from type: " ':<>: 'ShowType arg
Data/SBV/Control/Utils.hs view
@@ -398,7 +398,7 @@ -- | A class which allows for sexpr-conversion to functions class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where   sexprToArg     :: fun -> [SExpr] -> Maybe a-  smtFunName     :: (MonadIO m, SolverContext m, MonadSymbolic m) => fun -> m ((String, Maybe [String]), Bool)+  smtFunName     :: (MonadIO m, SolverContext m) => fun -> m ((String, Maybe [String]), Bool)   smtFunSaturate :: fun -> SBV r   smtFunType     :: fun -> SBVType   smtFunDefault  :: fun -> Maybe r@@ -476,7 +476,7 @@ -- | Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI -- function itself will register it automatically. But there are cases where doing this explicitly can -- come in handy.-registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()+registerUISMTFunction :: (MonadIO m, SolverContext m) => SMTFunction fun a r => fun -> m () registerUISMTFunction f = do st                <- contextState                              (nmas, isCurried) <- smtFunName f                              io $ newUninterpreted st nmas (smtFunType f) (UINone isCurried)
Data/SBV/Core/Concrete.hs view
@@ -72,7 +72,9 @@ instance HasKind a => HasKind (RCSet a) where   kindOf _ = KSet (kindOf (Proxy @a)) --- | A constant value+-- | A constant value.+-- Note: If you add a new constructor here, make sure you add the+-- corresponding equality in the instance "Eq CVal" and "Ord CVal"! data CVal = CAlgReal  !AlgReal             -- ^ Algebraic real           | CInteger  !Integer             -- ^ Bit-vector/unbounded integer           | CFloat    !Float               -- ^ Float@@ -115,6 +117,7 @@   CFloat    a == CFloat    b = a `fpIsEqualObjectH` b   -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!   CDouble   a == CDouble   b = a `fpIsEqualObjectH` b   -- ditto   CRational a == CRational b = a == b+  CFP       a == CFP       b = a `arbFPIsEqualObjectH` b   CChar     a == CChar     b = a == b   CString   a == CString   b = a == b   CList     a == CList     b = a == b@@ -140,7 +143,7 @@   CFloat    a `compare` CFloat    b = a `fpCompareObjectH`         b   CDouble   a `compare` CDouble   b = a `fpCompareObjectH`         b   CRational a `compare` CRational b = a `compare`                  b-  CFP       a `compare` CFP       b = a `fprCompareObject`         b+  CFP       a `compare` CFP       b = a `arbFPCompareObjectH`      b   CChar     a `compare` CChar     b = a `compare`                  b   CString   a `compare` CString   b = a `compare`                  b   CList     a `compare` CList     b = a `compare`                  b@@ -466,7 +469,7 @@ mkConstCV KReal           a = normCV $ CV KReal      (CAlgReal  (fromInteger (toInteger a))) mkConstCV KFloat          a = normCV $ CV KFloat     (CFloat    (fromInteger (toInteger a))) mkConstCV KDouble         a = normCV $ CV KDouble    (CDouble   (fromInteger (toInteger a)))-mkConstCV k@KFP{}         a = normCV $ CV k          (CFP       (fromInteger (toInteger a)))+mkConstCV k@(KFP eb sb)   a = normCV $ CV k          (CFP       (fpFromInteger eb sb (toInteger a))) mkConstCV KRational       a = normCV $ CV KRational  (CRational (fromInteger (toInteger a))) mkConstCV KChar           a = error $ "Unexpected call to mkConstCV (Char) with value: "   ++ show (toInteger a) mkConstCV KString         a = error $ "Unexpected call to mkConstCV (String) with value: " ++ show (toInteger a)
Data/SBV/Core/Data.hs view
@@ -31,6 +31,7 @@  ( SBool, SWord8, SWord16, SWord32, SWord64  , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble  , SFloatingPoint, SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad+ , SWord, SInt, WordN, IntN  , SRational  , SChar, SString, SList  , SEither, SMaybe@@ -63,9 +64,10 @@  , OptimizeStyle(..), Penalty(..), Objective(..)  , QueryState(..), QueryT(..), SMTProblem(..), Constraint(..), Lambda(..), Forall(..), Exists(..), ExistsUnique(..), ForallN(..), ExistsN(..)  , QuantifiedBool(..), EqSymbolic(..), QNot(..), Skolemize(skolemize, taggedSkolemize)+ , bvExtract, (#), bvDrop, bvTake  ) where -import GHC.TypeLits (KnownNat, Nat, Symbol, KnownSymbol, symbolVal, AppendSymbol)+import GHC.TypeLits (KnownNat, Nat, Symbol, KnownSymbol, symbolVal, AppendSymbol, type (+), type (-), type (<=), natVal)  import GHC.Exts     (IsList(..)) @@ -91,6 +93,7 @@ import System.Random  import Data.SBV.Core.AlgReals+import Data.SBV.Core.Sized import Data.SBV.Core.SizedFloats import Data.SBV.Core.Kind import Data.SBV.Core.Concrete@@ -173,6 +176,12 @@ -- | A symbolic quad-precision float type SFPQuad = SBV FPQuad +-- | A symbolic unsigned bit-vector carrying its size info+type SWord (n :: Nat) = SBV (WordN n)++-- | A symbolic signed bit-vector carrying its size info+type SInt (n :: Nat) = SBV (IntN n)+ -- | A symbolic character. Note that this is the full unicode character set. -- see: <https://smt-lib.org/theories-UnicodeStrings.shtml> -- for details.@@ -866,6 +875,89 @@   symbolicEq (R1 l) (R1 r) = symbolicEq l r   symbolicEq (L1 _) (R1 _) = sFalse   symbolicEq (R1 _) (L1 _) = sFalse++-- We don't want to do a generic Num a => Num (SBV a) instance; since that would be dangerous. Liftings+-- would only work for types we already handle. If a user defines his own type and makes an instance+-- of it, it would do the wrong thing. See https://github.com/LeventErkok/sbv/issues/706 for a discussion.+-- So, we have to declare the instances individually. I played around doing this via iso-deriving and+-- other generic mechanisms, but failed to do so. The CPP solution here is crude, but it avoids the+-- code duplication.+#define MKSNUM(CSTR, TYPE, KIND)                                                            \+instance (CSTR) => Num (TYPE) where {                                                       \+  fromInteger i  = SBV $ SVal (KIND) $ Left $ mkConstCV (KIND) (fromIntegral i :: Integer); \+  SBV a + SBV b  = SBV $ a `svPlus`  b;                                                     \+  SBV a * SBV b  = SBV $ a `svTimes` b;                                                     \+  SBV a - SBV b  = SBV $ a `svMinus` b;                                                     \+  abs    (SBV a) = SBV $ svAbs    a;                                                        \+  signum (SBV a) = SBV $ svSignum a;                                                        \+  negate (SBV a) = SBV $ svUNeg   a;                                                        \+}++-- Derive basic instances we need+MKSNUM((),               SInteger,             KUnbounded)+MKSNUM((),               SWord8,               KBounded False  8)+MKSNUM((),               SWord16,              KBounded False 16)+MKSNUM((),               SWord32,              KBounded False 32)+MKSNUM((),               SWord64,              KBounded False 64)+MKSNUM((),               SInt8,                KBounded True   8)+MKSNUM((),               SInt16,               KBounded True  16)+MKSNUM((),               SInt32,               KBounded True  32)+MKSNUM((),               SInt64,               KBounded True  64)+MKSNUM((),               SFloat,               KFloat)+MKSNUM((),               SDouble,              KDouble)+MKSNUM((),               SReal,                KReal)+MKSNUM(KnownNat n,       SWord n,              KBounded False (intOfProxy (Proxy @n)))+MKSNUM(KnownNat n,       SInt  n,              KBounded True  (intOfProxy (Proxy @n)))+MKSNUM(ValidFloat eb sb, SFloatingPoint eb sb, KFP (intOfProxy (Proxy @eb)) (intOfProxy (Proxy @sb)))++-- | Extract a portion of bits to form a smaller bit-vector.+bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)+                                    , KnownNat i+                                    , KnownNat j+                                    , i + 1 <= n+                                    , j <= i+                                    , BVIsNonZero (i - j + 1)+                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@+                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold+                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@+                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@+bvExtract start end = SBV . svExtract i j . unSBV+   where i  = fromIntegral (natVal start)+         j  = fromIntegral (natVal end)++-- | Join two bitvectors.+(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)+       , KnownNat m, BVIsNonZero m, SymVal (bv m)+       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side+         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side+         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@+n # m = SBV $ svJoin (unSBV n) (unSBV m)+infixr 5 #++-- | Drop bits from the top of a bit-vector.+bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n+                                 , KnownNat i+                                 , i + 1 <= n+                                 , i + m - n <= 0+                                 , BVIsNonZero (n - i)+                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.+                                   -> SBV (bv n)                 -- ^ Input, of size @n@+                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.+bvDrop i = SBV . svExtract start 0 . unSBV+  where nv    = intOfProxy (Proxy @n)+        start = nv - fromIntegral (natVal i) - 1++-- | Take bits from the top of a bit-vector.+bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n+                               , KnownNat i, BVIsNonZero i+                               , i <= n+                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.+                                 -> SBV (bv n)               -- ^ Input, of size @n@+                                 -> SBV (bv i)               -- ^ Output, of size @i@+bvTake i = SBV . svExtract start end . unSBV+  where nv    = intOfProxy (Proxy @n)+        start = nv - 1+        end   = start - fromIntegral (natVal i) + 1  -- | A class of values that can be skolemized. Note that we don't export this class. Use -- the 'skolemize' function instead.
Data/SBV/Core/Floating.hs view
@@ -31,6 +31,8 @@        , svFloatingPointAsSWord        ) where +import Control.Monad (when)+ import Data.Bits (testBit) import Data.Int  (Int8,  Int16,  Int32,  Int64) import Data.Word (Word8, Word16, Word32, Word64)@@ -559,11 +561,17 @@    fromMetricSpace        = sComparableSWord32AsSFloat     msMinimize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @Float) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Minimize nm' (toMetricSpace o)     msMaximize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @Float) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Maximize nm' (toMetricSpace o) +   annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"+ -- | 'Double' instance for 'Metric' goes through the lexicographic ordering on 'Word64'. -- It implicitly makes sure that the value is not @NaN@. instance Metric Double where@@ -573,11 +581,17 @@    fromMetricSpace         = sComparableSWord64AsSDouble     msMinimize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @Double) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Minimize nm' (toMetricSpace o)     msMaximize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @Double) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Maximize nm' (toMetricSpace o) +   annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"+ -- | Real instance for FloatingPoint. NB. The methods haven't been subjected to much testing, so beware of any floating-point snafus here. instance ValidFloat eb sb => Real (FloatingPoint eb sb) where   toRational (FloatingPoint (FP _ _ r)) = case bfToRep r of@@ -661,10 +675,16 @@    fromMetricSpace                        = sComparableSWordAsSFloatingPoint     msMinimize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @(FloatingPoint eb sb)) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Minimize nm' (toMetricSpace o)     msMaximize nm o = do constrain $ sNot $ fpIsNaN o-                        addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o)+                        let nm' = annotateForMS (Proxy @(FloatingPoint eb sb)) nm+                        when (nm' /= nm) $ sObserve nm (unSBV o)+                        addSValOptGoal $ unSBV `fmap` Maximize nm' (toMetricSpace o)++   annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  -- Map SBV's rounding modes to LibBF's rmToRM :: SRoundingMode -> Maybe RoundMode
Data/SBV/Core/Model.hs view
@@ -33,6 +33,7 @@   , sBool, sBool_, sBools, sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s, sWord32, sWord32_, sWord32s   , sWord64, sWord64_, sWord64s, sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s, sInt64, sInt64_   , sInt64s, sInteger, sInteger_, sIntegers, sReal, sReal_, sReals, sFloat, sFloat_, sFloats, sDouble, sDouble_, sDoubles+  , sWord, sWord_, sWords, sInt, sInt_, sInts   , sFPHalf, sFPHalf_, sFPHalfs, sFPBFloat, sFPBFloat_, sFPBFloats, sFPSingle, sFPSingle_, sFPSingles, sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads   , sFloatingPoint, sFloatingPoint_, sFloatingPoints   , sChar, sChar_, sChars, sString, sString_, sStrings, sList, sList_, sLists@@ -47,26 +48,26 @@   , sAssert   , liftQRem, liftDMod, symbolicMergeWithKind   , genLiteral, genFromCV, genMkSymVar+  , zeroExtend, signExtend   , sbvQuickCheck, lambdaAsArray   )   where  import Control.Applicative    (ZipList(ZipList)) import Control.Monad          (when, unless, mplus)-import Control.Monad.Trans    (liftIO) import Control.Monad.IO.Class (MonadIO)  import GHC.Generics (M1(..), U1(..), (:*:)(..), K1(..)) import qualified GHC.Generics as G  import GHC.Stack+import GHC.TypeLits hiding (SChar)  import Data.Array  (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits   (Bits(..))-import Data.Char   (toLower, isDigit) import Data.Int    (Int8, Int16, Int32, Int64) import Data.Kind   (Type)-import Data.List   (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate, isPrefixOf)+import Data.List   (genericLength, genericIndex, genericTake, unzip4, unzip5, unzip6, unzip7, intercalate) import Data.Maybe  (fromMaybe, mapMaybe) import Data.String (IsString(..)) import Data.Word   (Word8, Word16, Word32, Word64)@@ -87,6 +88,7 @@ import qualified Data.Foldable as F (toList)  import Data.SBV.Core.AlgReals+import Data.SBV.Core.Sized import Data.SBV.Core.SizedFloats import Data.SBV.Core.Data import Data.SBV.Core.Symbolic@@ -98,7 +100,7 @@ import Data.SBV.Provers.Prover (defaultSMTCfg, SafeResult(..), defs2smt, prove) import Data.SBV.SMT.SMT        (ThmResult, showModel) -import Data.SBV.Utils.Lib     (isKString)+import Data.SBV.Utils.Lib     (isKString, checkObservableName) import Data.SBV.Utils.Numeric (fpIsEqualObjectH)  import Data.IORef (readIORef)@@ -250,6 +252,18 @@   fromCV  (CV _ (CFP r))     = FloatingPoint r   fromCV  c                  = error $ "SymVal.FPR: Unexpected non-arbitrary-precision value: " ++ show c +-- | 'SymVal' instance for 'WordN'+instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where+   literal  x = genLiteral  (kindOf x) x+   mkSymVal   = genMkSymVar (kindOf (undefined :: WordN n))+   fromCV     = genFromCV++-- | 'SymVal' instance for 'IntN'+instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where+   literal  x = genLiteral  (kindOf x) x+   mkSymVal   = genMkSymVar (kindOf (undefined :: IntN n))+   fromCV     = genFromCV+ toCV :: SymVal a => a -> CVal toCV a = case literal a of            SBV (SVal _ (Left cv)) -> cvVal cv@@ -609,6 +623,30 @@ sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb] sFloatingPoints = symbolics +-- | Generalization of 'Data.SBV.sWord'+sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)+sWord = symbolic++-- | Generalization of 'Data.SBV.sWord_'+sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)+sWord_ = free_++-- | Generalization of 'Data.SBV.sWord64s'+sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]+sWords = symbolics++-- | Generalization of 'Data.SBV.sInt'+sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)+sInt = symbolic++-- | Generalization of 'Data.SBV.sInt_'+sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)+sInt_ = free_++-- | Generalization of 'Data.SBV.sInts'+sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]+sInts = symbolics+ -- | Generalization of 'Data.SBV.sChar' sChar :: MonadSymbolic m => String -> m SChar sChar = symbolic@@ -746,18 +784,6 @@                   newExpr st k (SBVApp (Label m) [xsv])  --- | Check if an observable name is good.-checkObservableName :: String -> Maybe String-checkObservableName lbl-  | null lbl-  = Just "SBV.observe: Bad empty name!"-  | map toLower lbl `elem` smtLibReservedNames-  = Just $ "SBV.observe: The name chosen is reserved, please change it!: " ++ show lbl-  | "s" `isPrefixOf` lbl && all isDigit (drop 1 lbl)-  = Just $ "SBV.observe: Names of the form sXXX are internal to SBV, please use a different name: " ++ show lbl-  | True-  = Nothing- -- | Observe the value of an expression, if the given condition holds.  Such values are useful in model construction, as they are printed part of a satisfying model, or a -- counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained -- pairs in a particular run. Note that an observed expression is always symbolic, i.e., it won't be constant folded. Compare this to 'label'@@ -777,16 +803,6 @@ observe :: SymVal a => String -> SBV a -> SBV a observe = observeIf (const True) --- | A variant of observe that you can use at the top-level. This is useful with quick-check, for instance.-sObserve :: SymVal a => String -> SBV a -> Symbolic ()-sObserve m x-  | Just bad <- checkObservableName m-  = error bad-  | True-  = do st <- symbolicEnv-       liftIO $ do xsv <- sbvToSV st x-                   recordObservable st m (const True) xsv- -- | Symbolic Comparisons. Similar to 'Eq', we cannot implement Haskell's 'Ord' class -- since there is no way to return an 'Ordering' value from a symbolic comparison. -- Furthermore, 'OrdSymbolic' requires 'Mergeable' to implement if-then-else, for the@@ -1059,7 +1075,7 @@ -- @ -- -- It is similar to the standard 'Integral' class, except ranging over symbolic instances.-class (SymVal a, Num a, Bits a, Integral a) => SIntegral a+class (SymVal a, Num a, Num (SBV a), Bits a, Integral a) => SIntegral a  -- 'SIntegral' Instances, skips Real/Float/Bool instance SIntegral Word8@@ -1071,11 +1087,41 @@ instance SIntegral Int32 instance SIntegral Int64 instance SIntegral Integer+instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)+instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n) +-- | Zero extend a bit-vector.+zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)+                             , KnownNat m, BVIsNonZero m, SymVal (bv m)+                             , n + 1 <= m+                             , SIntegral (bv (m - n))+                             , BVIsNonZero (m - n)+                             ) => SBV (bv n)    -- ^ Input, of size @n@+                               -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold+zeroExtend n = SBV $ svZeroExtend i (unSBV n)+  where nv = intOfProxy (Proxy @n)+        mv = intOfProxy (Proxy @m)+        i  = fromIntegral (mv - nv)++-- | Sign extend a bit-vector.+signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)+                             , KnownNat m, BVIsNonZero m, SymVal (bv m)+                             , n + 1 <= m+                             , SFiniteBits (bv n)+                             , SIntegral   (bv (m - n))+                             , BVIsNonZero (m - n)+                             ) => SBV (bv n)  -- ^ Input, of size @n@+                               -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold+signExtend n = SBV $ svSignExtend i (unSBV n)+  where nv = intOfProxy (Proxy @n)+        mv = intOfProxy (Proxy @m)+        i  = fromIntegral (mv - nv)++ -- | Finite bit-length symbolic values. Essentially the same as 'SIntegral', but further leaves out 'Integer'. Loosely -- based on Haskell's @FiniteBits@ class, but with more methods defined and structured differently to fit into the -- symbolic world view. Minimal complete definition: 'sFiniteBitSize'.-class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where+class (Ord a, SymVal a, Num a, Num (SBV a), Bits a) => SFiniteBits a where     -- | Bit size.     sFiniteBitSize      :: SBV a -> Int     -- | Least significant bit of a word, always stored at index 0.@@ -1213,9 +1259,11 @@ instance SFiniteBits Int16  where sFiniteBitSize _ = 16 instance SFiniteBits Int32  where sFiniteBitSize _ = 32 instance SFiniteBits Int64  where sFiniteBitSize _ = 64+instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where sFiniteBitSize _ = intOfProxy (Proxy @n)+instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN  n) where sFiniteBitSize _ = intOfProxy (Proxy @n)  -- | Returns 1 if the boolean is 'sTrue', otherwise 0.-oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a+oneIf :: (Ord a, Num (SBV a), SymVal a) => SBool -> SBV a oneIf t = ite t 1 0  -- | Lift a pseudo-boolean op, performing checks@@ -1319,27 +1367,6 @@ isConcreteOne (SBV (SVal KReal (Left (CV KReal (CAlgReal v))))) = isExactRational v && v == 1 isConcreteOne _                                                 = False --- Num instance for symbolic words.-instance (Ord a, Num a, SymVal a) => Num (SBV a) where-  fromInteger = literal . fromIntegral-  SBV x + SBV y = SBV (svPlus x y)-  SBV x * SBV y = SBV (svTimes x y)-  SBV x - SBV y = SBV (svMinus x y)-  -- Abs is problematic for floating point, due to -0; case, so we carefully shuttle it down-  -- to the solver to avoid the can of worms. (Alternative would be to do an if-then-else here.)-  abs (SBV x) = SBV (svAbs x)-  signum a-    -- NB. The following "carefully" tests the number for == 0, as Float/Double's NaN and +/-0-    -- cases would cause trouble with explicit equality tests.-    | hasSign a = ite (a .> z) i-                $ ite (a .< z) (negate i) a-    | True      = ite (a .> z) i a-    where z = genLiteral (kindOf a) (0::Integer)-          i = genLiteral (kindOf a) (1::Integer)-  -- negate is tricky because on double/float -0 is different than 0; so we cannot-  -- just rely on the default definition; which would be 0-0, which is not -0!-  negate (SBV x) = SBV (svUNeg x)- -- | Symbolic exponentiation using bit blasting and repeated squaring. -- -- N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.@@ -1365,7 +1392,7 @@                           (iterate (\x -> x*x) b) infixr 8 .^ -instance (Ord a, SymVal a, Fractional a) => Fractional (SBV a) where+instance (Ord a, Num (SBV a), SymVal a, Fractional a) => Fractional (SBV a) where   fromRational  = literal . fromRational   SBV x / sy@(SBV y) | div0 = ite (sy .== 0) 0 res                      | True = res@@ -1394,7 +1421,7 @@ -- (See the separate definition below for 'SFloatingPoint'.)  Note that unless you use delta-sat via 'Data.SBV.Provers.dReal' on 'SReal', most -- of the fields are "undefined" for symbolic values. We will add methods as they are supported by SMTLib. Currently, the -- only symbolically available function in this class is 'sqrt' for 'SFloat', 'SDouble' and 'SFloatingPoint'.-instance (Ord a, SymVal a, Fractional a, Floating a) => Floating (SBV a) where+instance (Ord a, Num (SBV a), SymVal a, Fractional a, Floating a) => Floating (SBV a) where   pi      = fromRational . toRational $ (pi :: Double)   exp     = lift1FNS "exp"     exp   log     = lift1FNS "log"     log@@ -1520,7 +1547,7 @@ -- -1 has all bits set to True for both signed and unsigned values -- | Using 'popCount' or 'testBit' on non-concrete values will result in an -- error. Use 'sPopCount' or 'sTestBit' instead.-instance (Ord a, Num a, Bits a, SymVal a) => Bits (SBV a) where+instance (Ord a, Num (SBV a), Num a, Bits a, SymVal a) => Bits (SBV a) where   SBV x .&. SBV y    = SBV (svAnd x y)   SBV x .|. SBV y    = SBV (svOr x y)   SBV x `xor` SBV y  = SBV (svXOr x y)@@ -1634,7 +1661,7 @@ -- a concrete argument for obvious reasons. Other variants (succ, pred, [x..]) etc are similarly -- limited. While symbolic variants can be defined for many of these, they will just diverge -- as final sizes cannot be determined statically.-instance (Show a, Bounded a, Integral a, Num a, SymVal a) => Enum (SBV a) where+instance (Show a, Bounded a, Integral a, Num a, Num (SBV a), SymVal a) => Enum (SBV a) where   succ x     | v == (maxBound :: a) = error $ "Enum.succ{" ++ showType x ++ "}: tried to take `succ' of maxBound"     | True                 = fromIntegral $ v + 1@@ -1784,38 +1811,40 @@     = let (r1, r2) = sDivMod x y in (normCV a{ cvVal = CInteger r1 }, normCV b{ cvVal = CInteger r2 })   sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b) -instance SDivisible SWord64 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod+instance SDivisible SWord64 where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SWord32 where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SWord16 where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SWord8  where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SInt64  where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SInt32  where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SInt16  where {sQuotRem = liftQRem; sDivMod  = liftDMod}+instance SDivisible SInt8   where {sQuotRem = liftQRem; sDivMod  = liftDMod} -instance SDivisible SInt64 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod+-- | 'SDivisible' instance for 'WordN'+instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where+  sQuotRem x 0 = (0, x)+  sQuotRem x y = x `quotRem` y+  sDivMod  x 0 = (0, x)+  sDivMod  x y = x `divMod` y -instance SDivisible SWord32 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod+-- | 'SDivisible' instance for 'IntN'+instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where+  sQuotRem x 0 = (0, x)+  sQuotRem x y = x `quotRem` y+  sDivMod  x 0 = (0, x)+  sDivMod  x y = x `divMod` y -instance SDivisible SInt32 where+-- | 'SDivisible' instance for 'SWord'+instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where   sQuotRem = liftQRem   sDivMod  = liftDMod -instance SDivisible SWord16 where+-- | 'SDivisible' instance for 'SInt'+instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where   sQuotRem = liftQRem   sDivMod  = liftDMod -instance SDivisible SInt16 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod -instance SDivisible SWord8 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod--instance SDivisible SInt8 where-  sQuotRem = liftQRem-  sDivMod  = liftDMod- -- | Lift 'quotRem' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself. liftQRem :: (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)@@ -1842,7 +1871,7 @@ -- | Lift 'divMod' to symbolic words. Division by 0 is defined s.t. @x/0 = 0@; which -- holds even when @x@ is @0@ itself. Essentially, this is conversion from quotRem -- (truncate to 0) to divMod (truncate towards negative infinity)-liftDMod :: (Ord a, SymVal a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)+liftDMod :: (Ord a, SymVal a, Num a, Num (SBV a), SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) liftDMod x y   | isConcreteZero x   = (x, x)@@ -1920,7 +1949,7 @@    -- | Total indexing operation. @select xs default index@ is intuitively    -- the same as @xs !! index@, except it evaluates to @default@ if @index@    -- underflows/overflows.-   select :: (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a+   select :: (Ord b, SymVal b, Num b, Num (SBV 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    -- in general, it doesn't work for SBV since we do not have any notion of@@ -2347,6 +2376,32 @@    -- | Uninterpret a value, i.e., add this value as a completely undefined value/function that   -- the solver is free to instantiate to satisfy other constraints.+  --+  -- __Known issues__+  --+  -- Usually using an uninterpret function will register itself to the solver, but sometimes the lazyness+  -- of the evaluation might render this unreliable.+  --+  -- For example, when working with quantifiers and uninterpreted functions with the following code:+  --+  -- > runSMTWith z3 $ do+  -- >   let f = uninterpret "f" :: SInteger -> SInteger+  -- >   query $ do+  -- >     constrain $ \(Forall (b :: SInteger)) -> f b .== f b+  -- >     checkSat+  --+  -- The solver will complain about the unknown constant @f (Int)@.+  --+  -- A workaround of this is to explicit register them with 'Data.SBV.Control.registerUISMTFunction':+  --+  -- > runSMTWith z3 $ do+  -- >   let f = uninterpret "f" :: SInteger -> SInteger+  -- >   registerUISMTFunction f+  -- >   query $ do+  -- >     constrain $ \(Forall (b :: SInteger)) -> f b .== f b+  -- >     checkSat+  --+  -- See https://github.com/LeventErkok/sbv/issues/711 for more info.   uninterpret :: String -> a    -- | Uninterpret a value, with named arguments in case of functions. SBV will use these@@ -2919,7 +2974,7 @@ -- <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf>. -- -- Minimal completion: None. However, if @MetricSpace@ is not identical to the type, you want--- to define 'toMetricSpace' and possibly 'minimize'/'maximize' to add extra constraints as necessary.+-- to define 'toMetricSpace'/'annotateForMS', and possibly 'minimize'/'maximize' to add extra constraints as necessary. class Metric a where   -- | The metric space we optimize the goal over. Usually the same as the type itself, but not always!   -- For instance, signed bit-vectors are optimized over their unsigned counterparts, floats are@@ -2929,16 +2984,25 @@    -- | Compute the metric value to optimize.   toMetricSpace   :: SBV a -> SBV (MetricSpace a)+   -- | Compute the value itself from the metric corresponding to it.   fromMetricSpace :: SBV (MetricSpace a) -> SBV a +  -- | Annotate for the metric space, to clarify the new name. If this result is not identity,+  -- we will add an sObserve on the original.+  annotateForMS :: Proxy a -> String -> String+   -- | Minimizing a metric space   msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()-  msMinimize nm o = addSValOptGoal $ unSBV `fmap` Minimize nm (toMetricSpace o)+  msMinimize nm o = do let nm' = annotateForMS (Proxy @a) nm+                       when (nm' /= nm) $ sObserve nm (unSBV o)+                       addSValOptGoal $ unSBV `fmap` Minimize nm' (toMetricSpace o)    -- | Maximizing a metric space   msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()-  msMaximize nm o = addSValOptGoal $ unSBV `fmap` Maximize nm (toMetricSpace o)+  msMaximize nm o = do let nm' = annotateForMS (Proxy @a) nm+                       when (nm' /= nm) $ sObserve nm (unSBV o)+                       addSValOptGoal $ unSBV `fmap` Maximize nm' (toMetricSpace o)    -- if MetricSpace is the same, we can give a default definition   default toMetricSpace :: (a ~ MetricSpace a) => SBV a -> SBV (MetricSpace a)@@ -2947,11 +3011,16 @@   default fromMetricSpace :: (a ~ MetricSpace a) => SBV (MetricSpace a) -> SBV a   fromMetricSpace = id +  -- Annotations to indicate if the metric space transition was needed+  default annotateForMS :: (a ~ MetricSpace a) => Proxy a -> String -> String+  annotateForMS _ s = s+ -- Booleans assume True is greater than False instance Metric Bool where   type MetricSpace Bool = Word8-  toMetricSpace t       = ite t 1 0-  fromMetricSpace w     = w ./= 0+  toMetricSpace t   = ite t 1 0+  fromMetricSpace w = w ./= 0+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  -- | Generalization of 'Data.SBV.minimize' minimize :: (Metric a, MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()@@ -2972,23 +3041,37 @@ -- To optimize signed bounded values, we have to adjust to the range instance Metric Int8 where   type MetricSpace Int8 = Word8-  toMetricSpace    x    = sFromIntegral x + 128  -- 2^7-  fromMetricSpace  x    = sFromIntegral x - 128+  toMetricSpace   x = sFromIntegral x + 128  -- 2^7+  fromMetricSpace x = sFromIntegral x - 128+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  instance Metric Int16 where   type MetricSpace Int16 = Word16-  toMetricSpace    x     = sFromIntegral x + 32768  -- 2^15-  fromMetricSpace  x     = sFromIntegral x - 32768+  toMetricSpace   x = sFromIntegral x + 32768  -- 2^15+  fromMetricSpace x = sFromIntegral x - 32768+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  instance Metric Int32 where   type MetricSpace Int32 = Word32-  toMetricSpace    x     = sFromIntegral x + 2147483648 -- 2^31-  fromMetricSpace  x     = sFromIntegral x - 2147483648+  toMetricSpace   x = sFromIntegral x + 2147483648 -- 2^31+  fromMetricSpace x = sFromIntegral x - 2147483648+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  instance Metric Int64 where   type MetricSpace Int64 = Word64-  toMetricSpace    x     = sFromIntegral x + 9223372036854775808  -- 2^63-  fromMetricSpace  x     = sFromIntegral x - 9223372036854775808+  toMetricSpace   x = sFromIntegral x + 9223372036854775808  -- 2^63+  fromMetricSpace x = sFromIntegral x - 9223372036854775808+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"++-- | Optimizing 'WordN'+instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)++-- | Optimizing 'IntN'+instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where+  type MetricSpace (IntN n) = WordN n+  toMetricSpace   x = sFromIntegral x + 2 ^ (intOfProxy (Proxy @n) - 1)+  fromMetricSpace x = sFromIntegral x - 2 ^ (intOfProxy (Proxy @n) - 1)+  annotateForMS _ s = "toMetricSpace(" ++ s ++ ")"  -- Quickcheck interface on symbolic-booleans.. instance Testable SBool where
Data/SBV/Core/Operations.hs view
@@ -21,7 +21,7 @@   -- ** Basic destructors   , svAsBool, svAsInteger, svNumerator, svDenominator   -- ** Basic operations-  , svPlus, svTimes, svMinus, svUNeg, svAbs+  , svPlus, svTimes, svMinus, svUNeg, svAbs, svSignum   , svDivide, svQuot, svRem, svQuotRem   , svEqual, svNotEqual, svStrongEqual, svImplies, svSetEqual   , svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan@@ -180,6 +180,19 @@ -- | Absolute value. svAbs :: SVal -> SVal svAbs = liftSym1 (mkSymOp1 Abs) abs abs abs abs abs abs++-- | Signum. +--+-- NB. The following "carefully" tests the number for == 0, as Float/Double's NaN and +/-0+-- cases would cause trouble with explicit equality tests.+svSignum :: SVal -> SVal+svSignum a+  | hasSign a = svIte (a `svGreaterThan` z) i+              $ svIte (a `svLessThan`    z) (svUNeg i) a+  | True      = svIte (a `svGreaterThan` z) i a+  where k = kindOf a+        z = SVal k $ Left $ mkConstCV k (0 :: Integer)+        i = SVal k $ Left $ mkConstCV k (1 :: Integer)  -- | Division. svDivide :: SVal -> SVal -> SVal
Data/SBV/Core/Sized.hs view
@@ -15,18 +15,15 @@ {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE TypeApplications     #-} {-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}  {-# OPTIONS_GHC -Wall -Werror #-}  module Data.SBV.Core.Sized (         -- * Type-sized unsigned bit-vectors-          SWord, WordN, sWord, sWord_, sWords+          WordN         -- * Type-sized signed bit-vectors-        , SInt, IntN, sInt, sInt_, sInts-        -- * Bit-vector operations-        , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake+        , IntN        ) where  import Data.Bits@@ -35,22 +32,16 @@  import GHC.TypeLits -import Data.SBV.Core.Data import Data.SBV.Core.Kind-import Data.SBV.Core.Model-import Data.SBV.Core.Operations import Data.SBV.Core.Symbolic--import Data.SBV.SMT.SMT+import Data.SBV.Core.Concrete+import Data.SBV.Core.Operations  import Test.QuickCheck(Arbitrary(..))  -- | An unsigned bit-vector carrying its size info newtype WordN (n :: Nat) = WordN Integer deriving (Eq, Ord) --- | A symbolic unsigned bit-vector carrying its size info-type SWord (n :: Nat) = SBV (WordN n)- -- | Show instance for 'WordN' instance Show (WordN n) where   show (WordN v) = show v@@ -59,18 +50,9 @@ instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where   kindOf _ = KBounded False (intOfProxy (Proxy @n)) --- | 'SymVal' instance for 'WordN'-instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where-   literal  x = genLiteral  (kindOf x) x-   mkSymVal   = genMkSymVar (kindOf (undefined :: WordN n))-   fromCV     = genFromCV- -- | A signed bit-vector carrying its size info newtype IntN (n :: Nat) = IntN Integer deriving (Eq, Ord) --- | A symbolic signed bit-vector carrying its size info-type SInt (n :: Nat) = SBV (IntN n)- -- | Show instance for 'IntN' instance Show (IntN n) where   show (IntN v) = show v@@ -79,12 +61,6 @@ instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where   kindOf _ = KBounded True (intOfProxy (Proxy @n)) --- | 'SymVal' instance for 'IntN'-instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where-   literal  x = genLiteral  (kindOf x) x-   mkSymVal   = genMkSymVar (kindOf (undefined :: IntN n))-   fromCV     = genFromCV- -- Lift a unary operation via SVal lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n lift1 nm op x = uc $ op (c x)@@ -208,161 +184,6 @@    isSigned     = hasSign . kindOf    bit i        = 1 `shiftL` i    popCount     = fromIntegral . popCount . toInteger---- | 'SIntegral' instance for 'WordN'-instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)---- | 'SIntegral' instance for 'IntN'-instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)---- | 'SDivisible' instance for 'WordN'-instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where-  sQuotRem x 0 = (0, x)-  sQuotRem x y = x `quotRem` y-  sDivMod  x 0 = (0, x)-  sDivMod  x y = x `divMod` y---- | 'SDivisible' instance for 'IntN'-instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where-  sQuotRem x 0 = (0, x)-  sQuotRem x y = x `quotRem` y-  sDivMod  x 0 = (0, x)-  sDivMod  x y = x `divMod` y---- | 'SDivisible' instance for 'SWord'-instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where-  sQuotRem = liftQRem-  sDivMod  = liftDMod---- | 'SDivisible' instance for 'SInt'-instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where-  sQuotRem = liftQRem-  sDivMod  = liftDMod---- | 'SFiniteBits' instance for 'WordN'-instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where-   sFiniteBitSize _ = intOfProxy (Proxy @n)---- | 'SFiniteBits' instance for 'IntN'-instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where-   sFiniteBitSize _ = intOfProxy (Proxy @n)---- | Constructing models for 'WordN'-instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where-  parseCVs = genParse (kindOf (undefined :: WordN n))---- | Constructing models for 'IntN'-instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where-  parseCVs = genParse (kindOf (undefined :: IntN n))---- | Optimizing 'WordN'-instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)---- | Optimizing 'IntN'-instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where-  type MetricSpace (IntN n) = WordN n-  toMetricSpace    x        = sFromIntegral x + 2 ^ (intOfProxy (Proxy @n) - 1)-  fromMetricSpace  x        = sFromIntegral x - 2 ^ (intOfProxy (Proxy @n) - 1)---- | Generalization of 'Data.SBV.sWord'-sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)-sWord = symbolic---- | Generalization of 'Data.SBV.sWord_'-sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)-sWord_ = free_---- | Generalization of 'Data.SBV.sWord64s'-sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]-sWords = symbolics---- | Generalization of 'Data.SBV.sInt'-sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)-sInt = symbolic---- | Generalization of 'Data.SBV.sInt_'-sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)-sInt_ = free_---- | Generalization of 'Data.SBV.sInts'-sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]-sInts = symbolics---- | Extract a portion of bits to form a smaller bit-vector.-bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)-                                    , KnownNat i-                                    , KnownNat j-                                    , i + 1 <= n-                                    , j <= i-                                    , BVIsNonZero (i - j + 1)-                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@-                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold-                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@-                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@-bvExtract start end = SBV . svExtract i j . unSBV-   where i  = fromIntegral (natVal start)-         j  = fromIntegral (natVal end)---- | Join two bitvectors.-(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)-       , KnownNat m, BVIsNonZero m, SymVal (bv m)-       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side-         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side-         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@-n # m = SBV $ svJoin (unSBV n) (unSBV m)-infixr 5 #---- | Zero extend a bit-vector.-zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)-                             , KnownNat m, BVIsNonZero m, SymVal (bv m)-                             , n + 1 <= m-                             , SIntegral   (bv (m - n))-                             , BVIsNonZero (m - n)-                             ) => SBV (bv n)    -- ^ Input, of size @n@-                               -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold-zeroExtend n = SBV $ svZeroExtend i (unSBV n)-  where nv = intOfProxy (Proxy @n)-        mv = intOfProxy (Proxy @m)-        i  = fromIntegral (mv - nv)---- | Sign extend a bit-vector.-signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)-                             , KnownNat m, BVIsNonZero m, SymVal (bv m)-                             , n + 1 <= m-                             , SFiniteBits (bv n)-                             , SIntegral   (bv (m - n))-                             , BVIsNonZero (m - n)-                             ) => SBV (bv n)  -- ^ Input, of size @n@-                               -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold-signExtend n = SBV $ svSignExtend i (unSBV n)-  where nv = intOfProxy (Proxy @n)-        mv = intOfProxy (Proxy @m)-        i  = fromIntegral (mv - nv)---- | Drop bits from the top of a bit-vector.-bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n-                                 , KnownNat i-                                 , i + 1 <= n-                                 , i + m - n <= 0-                                 , BVIsNonZero (n - i)-                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.-                                   -> SBV (bv n)                 -- ^ Input, of size @n@-                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.-bvDrop i = SBV . svExtract start 0 . unSBV-  where nv    = intOfProxy (Proxy @n)-        start = nv - fromIntegral (natVal i) - 1---- | Take bits from the top of a bit-vector.-bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n-                               , KnownNat i, BVIsNonZero i-                               , i <= n-                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.-                                 -> SBV (bv n)               -- ^ Input, of size @n@-                                 -> SBV (bv i)               -- ^ Output, of size @i@-bvTake i = SBV . svExtract start end . unSBV-  where nv    = intOfProxy (Proxy @n)-        start = nv - 1-        end   = start - fromIntegral (natVal i) + 1  -- | Quickcheck instance for WordN instance KnownNat n => Arbitrary (WordN n) where
Data/SBV/Core/SizedFloats.hs view
@@ -30,7 +30,7 @@         , fpFromInteger, fpFromRational, fpFromFloat, fpFromDouble, fpEncodeFloat          -- * Internal operations-       , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp+       , arbFPIsEqualObjectH, arbFPCompareObjectH, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp        ) where  import Data.Char (intToDigit)@@ -55,9 +55,21 @@ --   An IEEE SP is @FloatingPoint  8 24@ --           DP is @FloatingPoint 11 53@ -- etc.-newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP-                                              deriving (Eq, Ord)+-- NB. Don't derive Ord for this type automatically, see notes below.+newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP deriving Eq +-- NB. Refrain from letting GHC derive @>@ and @>=@ and define+-- it ourselves. Why? Because the default definition of @x > y@+-- is @not (x <= y)@. But when one of the arguments is NaN, this does+-- the wrong thing, since NaN doesn't compare to other values. (i.e., the+-- comparison should be always False, but the default will give+-- you the wrong result.)+instance Ord (FloatingPoint eb sb) where+  FloatingPoint f0 <  FloatingPoint f1 = f0 <  f1+  FloatingPoint f0 <= FloatingPoint f1 = f0 <= f1+  f0               >  f1               = f1 <  f0       -- See the note above+  f0               >= f1               = f1 <= f0       -- See the note above+ -- | Abbreviation for IEEE half precision float, bit width 16 = 5 + 11. type FPHalf = FloatingPoint 5 11 @@ -87,8 +99,26 @@              , fpSignificandSize :: Int              , fpValue           :: BigFloat              }-             deriving (Ord, Eq, G.Data)+             deriving (Eq, G.Data) +-- Manually implemented instance as GHC generated a non-IEEE 754 compliant instance.+-- Note that we cannot pack the values in a tuple and then compare them as that will+-- also give non-IEEE 754 compilant results.+--+-- NB. Refrain from letting GHC derive @>@ and @>=@ and define+-- it ourselves. Why? Because the default definition of @x > y@+-- is @not (x <= y)@. But when one of the arguments is NaN, this does+-- the wrong thing, since NaN doesn't compare to other values. (i.e., the+-- comparison should be always False, but the default will give+-- you the wrong result.)+instance Ord FP where+  FP eb0 sb0 v0 <  FP eb1 sb1 v1 | (eb0, sb0) /= (eb1, sb1) = error $ "FP.<: comparing FPs with different precision: "  <> show (eb0, sb0) <> show (eb1, sb1)+                                 | True                     = v0 <  v1+  FP eb0 sb0 v0 <= FP eb1 sb1 v1 | (eb0, sb0) /= (eb1, sb1) = error $ "FP.<=: comparing FPs with different precision: " <> show (eb0, sb0) <> show (eb1, sb1)+                                 | True                     = v0 <= v1+  f0 >  f1 = f1 <  f0  -- See note above+  f0 >= f1 = f1 <= f0  -- See note above+ instance Show FP where   show = bfRemoveRedundantExp . bfToString 10 False False @@ -203,14 +233,27 @@        mkB sz val = "#b" ++ pad sz (showIntAtBase 2 intToDigit val "")        pad l str = replicate (l - length str) '0' ++ str --- | Structural comparison only, for internal map indexes-fprCompareObject :: FP -> FP -> Ordering-fprCompareObject (FP eb sb a) (FP eb' sb' b) = case (eb, sb) `compare` (eb', sb') of-                                                 LT -> LT-                                                 GT -> GT-                                                 EQ -> a `BF.bfCompare` b-+-- | Check that two arbitrary floats are the exact same values, i.e., +0/-0 does not+-- compare equal, and NaN's compare equal to themselves+arbFPIsEqualObjectH :: FP -> FP -> Bool+arbFPIsEqualObjectH (FP eb sb a) (FP eb' sb' b) = case (eb, sb) `compare` (eb', sb') of+                                                    LT                                 -> False+                                                    GT                                 -> False+                                                    EQ | BF.bfIsNaN a                  -> BF.bfIsNaN b+                                                       | BF.bfIsZero a && BF.bfIsNeg a -> BF.bfIsZero b && BF.bfIsNeg b+                                                       | BF.bfIsZero a && BF.bfIsPos a -> BF.bfIsZero b && BF.bfIsPos b+                                                       | True                          -> a == b +-- | Ordering for arbitrary floats, avoiding the +0/-0/NaN issues. Note that this is+-- essentially used for indexing into a map, so we need to be total.+--+-- This function uses the bfCompare function provided by the libBF. As per the libBF's documentation,+-- it has the semantics: -0 < 0, NaN == NaN, and NaN is larger than all other numbers.+arbFPCompareObjectH :: FP -> FP -> Ordering+arbFPCompareObjectH (FP eb sb a) (FP eb' sb' b) = case (eb, sb) `compare` (eb', sb') of+                                                    LT -> LT+                                                    GT -> GT+                                                    EQ -> BF.bfCompare a b -- | Compute the signum of a big float bfSignum :: BigFloat -> BigFloat bfSignum r | BF.bfIsNaN  r = r@@ -366,9 +409,9 @@ fpFromFloat  8 24 f = let fw          = floatToWord f                           (sgn, e, s) = (fw `testBit` 31, fromIntegral (fw `shiftR` 23) .&. 0xFF, fromIntegral fw .&. 0x7FFFFF)                       in fpFromRawRep sgn (e, 8) (s, 24)-fpFromFloat eb sb f = error $ "SBV.fprFromFloat: Unexpected input: " ++ show (eb, sb, f)+fpFromFloat eb sb f = error $ "SBV.fpFromFloat: Unexpected input: " ++ show (eb, sb, f)  -- | Convert from a IEEE double. fpFromDouble :: Int -> Int -> Double -> FP fpFromDouble 11 53 d = FP 11 54 $ BF.bfFromDouble d-fpFromDouble eb sb d = error $ "SBV.fprFromDouble: Unexpected input: " ++ show (eb, sb, d)+fpFromDouble eb sb d = error $ "SBV.fpFromDouble: Unexpected input: " ++ show (eb, sb, d)
Data/SBV/Core/Symbolic.hs view
@@ -51,7 +51,7 @@   , addInternInput, addUserInput   , getUserName', getUserName   , lookupInput , getSValPathCondition, extendSValPathCondition-  , getTableIndex+  , getTableIndex, sObserve   , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, mkNewState, runSymbolicInState, State(..), SMTDef(..), smtDefGivenName, withNewIncState, IncState(..), incrementInternalCounter   , inSMTMode, SBVRunMode(..), IStage(..), Result(..), ResultInp(..), UICodeKind(..)   , registerKind, registerLabel, recordObservable@@ -111,7 +111,7 @@ import Data.SBV.Core.Concrete import Data.SBV.SMT.SMTLibNames import Data.SBV.Utils.TDiff (Timing)-import Data.SBV.Utils.Lib   (stringToQFS)+import Data.SBV.Utils.Lib   (stringToQFS, checkObservableName)  import Data.SBV.Control.Types @@ -2098,6 +2098,16 @@                                            $ noInteractive [ "Adding an optimization objective:"                                                            , "  Objective: " ++ show obj                                                            ]++-- | Generalization of 'Data.SBV.sObserve'+sObserve :: MonadSymbolic m => String -> SVal -> m ()+sObserve m x+  | Just bad <- checkObservableName m+  = error bad+  | True+  = do st <- symbolicEnv+       liftIO $ do xsv <- svToSV st x+                   recordObservable st m (const True) xsv  -- | Generalization of 'Data.SBV.outputSVal' outputSVal :: MonadSymbolic m => SVal -> m ()
Data/SBV/Either.hs view
@@ -104,9 +104,9 @@ -- | Case analysis for symbolic 'Either's. If the value 'isLeft', apply the -- first function; if it 'isRight', apply the second function. ----- >>> either (*2) (*3) (sLeft 3)+-- >>> either (*2) (*3) (sLeft (3 :: SInteger)) -- 6 :: SInteger--- >>> either (*2) (*3) (sRight 3)+-- >>> either (*2) (*3) (sRight (3 :: SInteger)) -- 9 :: SInteger -- >>> let f = uninterpret "f" :: SInteger -> SInteger -- >>> let g = uninterpret "g" :: SInteger -> SInteger
Data/SBV/Internals.hs view
@@ -73,7 +73,6 @@ import Data.SBV.Core.Data hiding (Forall(..), Exists(..), ForallN(..), ExistsN(..), ExistsUnique(..), Skolemize(..), QNot(..))  import Data.SBV.Core.Kind       (BVIsNonZero, ValidFloat)-import Data.SBV.Core.Sized      (SWord) import Data.SBV.Core.Model      (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod) import Data.SBV.Core.Symbolic   (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..)) @@ -101,6 +100,7 @@  --- $setup --- >>> -- For doctest purposes only:+--  >>> :set -XScopedTypeVariables --- >>> import Data.SBV  -- | Send an arbitrary string to the solver in a query.
Data/SBV/Maybe.hs view
@@ -10,6 +10,7 @@ -- Symbolic option type, symbolic version of Haskell's 'Maybe' type. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE FlexibleInstances   #-} {-# LANGUAGE Rank2Types          #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -193,7 +194,7 @@                     newExpr st kb $ SBVApp Ite [noVal, br1, br2]  -- | Custom 'Num' instance over 'SMaybe'-instance {-# OVERLAPPING #-} (Ord a, SymVal a, Num a) => Num (SBV (Maybe a)) where+instance (Ord a, SymVal a, Num a, Num (SBV a)) => Num (SBV (Maybe a)) where   (+)         = map2 (+)   (-)         = map2 (-)   (*)         = map2 (*)
Data/SBV/SMT/SMT.hs view
@@ -17,6 +17,7 @@ {-# LANGUAGE Rank2Types                 #-} {-# LANGUAGE ScopedTypeVariables        #-} {-# LANGUAGE TypeApplications           #-}+{-# LANGUAGE UndecidableInstances       #-} {-# LANGUAGE ViewPatterns               #-}  {-# OPTIONS_GHC -Wall -Werror #-}@@ -74,7 +75,7 @@ import Data.SBV.Core.Data import Data.SBV.Core.Symbolic (SMTEngine, State(..), mustIgnoreVar) import Data.SBV.Core.Concrete (showCV)-import Data.SBV.Core.Kind     (showBaseKind, intOfProxy)+import Data.SBV.Core.Kind     (showBaseKind, intOfProxy, BVIsNonZero)  import Data.SBV.Core.SizedFloats(FloatingPoint(..)) @@ -313,6 +314,14 @@     | intOfProxy (Proxy @eb) == ei , intOfProxy (Proxy @sb) == si = Just (FloatingPoint fp, r)   parseCVs _                                                      = Nothing +-- | Constructing models for 'WordN'+instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where+  parseCVs = genParse (kindOf (undefined :: WordN n))++-- | Constructing models for 'IntN'+instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where+  parseCVs = genParse (kindOf (undefined :: IntN n))+ -- | @CV@ as extracted from a model; trivial definition instance SatModel CV where   parseCVs (cv : r) = Just (cv, r)@@ -584,9 +593,11 @@ showModelUI :: SMTConfig -> (String, (Bool, SBVType, Either String ([([CV], CV)], CV))) -> String showModelUI cfg (nm, (isCurried, SBVType ts, interp))   = intercalate "\n" $ case interp of-                         Left  e  -> ["  " ++ l | l <- [sig, e]]-                         Right ds -> ["  " ++ l | l <- sig : mkBody ds]+                         Left  e  -> ["  " ++ trim l | l <- [sig, e]]+                         Right ds -> ["  " ++ trim l | l <- sig : mkBody ds]   where noOfArgs = length ts - 1++        trim = reverse . dropWhile isSpace . reverse          (ats, rt) = case map showBaseKind ts of                      []  -> error $ "showModelUI: Unexpected type: " ++ show (SBVType ts)
Data/SBV/SMT/SMTLib2.hs view
@@ -1046,7 +1046,7 @@         sh inp@(SBVApp op@(SeqOp SBVReverse{}) args) = "(" ++ ops ++ " " ++ unwords (map cvtSV args) ++ ")"           where ops = case op `M.lookup` functionMap of                         Just s  -> s-                        Nothing -> error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp+                        Nothing -> error $ "*** SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp          sh (SBVApp (SeqOp op) args) = "(" ++ show op ++ " " ++ unwords (map cvtSV args) ++ ")" @@ -1110,7 +1110,16 @@                                  , "*** Note that uninterpreted kinds only support equality."                                  , "*** If you believe this is in error, please report!"                                  ]-            else error $ "SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp+            else error $ unlines [ ""+                                 , "*** SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " ++ show inp+                                 , "***"+                                 , "*** Applied to arguments of type: " ++ intercalate ", " (nub (map (show . kindOf) args))+                                 , "***"+                                 , "*** This can happen if the Num instance isn't properly defined for a lifted kind."+                                 , "*** (See https://github.com/LeventErkok/sbv/issues/698 for a discussion.)"+                                 , "***"+                                 , "*** If you believe this is in error, please report!"+                                 ]           where smtOpBVTable  = [ (Plus,          lift2   "bvadd")                                 , (Minus,         lift2   "bvsub")                                 , (Times,         lift2   "bvmul")
Data/SBV/Tools/BoundedList.hs view
@@ -14,6 +14,7 @@ -- bounded prefix of this list, at which point these functions come in handy. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE OverloadedLists     #-} {-# LANGUAGE Rank2Types          #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -71,11 +72,11 @@         go i b s = lcase s (return b) (\h t -> do { fbh <- f b h; go (i-1) fbh t })  -- | Bounded sum.-bsum :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a+bsum :: (SymVal a, Num a, Num (SBV a), Ord a) => Int -> SList a -> SBV a bsum i = bfoldl i (+) 0  -- | Bounded product.-bprod :: (SymVal a, Num a, Ord a) => Int -> SList a -> SBV a+bprod :: (SymVal a, Num a, Num (SBV a), Ord a) => Int -> SList a -> SBV a bprod i = bfoldl i (*) 1  -- | Bounded map.
Data/SBV/Tools/Overflow.hs view
@@ -34,7 +34,6 @@ import Data.SBV.Core.Kind import Data.SBV.Core.Model import Data.SBV.Core.Operations-import Data.SBV.Core.Sized  import GHC.TypeLits
Data/SBV/Tools/Polynomial.hs view
@@ -30,7 +30,6 @@  import Data.SBV.Core.Data import Data.SBV.Core.Kind-import Data.SBV.Core.Sized import Data.SBV.Core.Model  import GHC.TypeLits
Data/SBV/Tools/Range.hs view
@@ -11,6 +11,7 @@  {-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}  {-# OPTIONS_GHC -Wall -Werror #-} @@ -27,6 +28,8 @@ import Data.SBV import Data.SBV.Control +import Data.Proxy+ import Data.SBV.Internals hiding (Range, free_)  -- $setup@@ -153,7 +156,7 @@                                      Unsatisfiable{} -> return Nothing                                      Unknown{}       -> error "Solver said Unknown!"                                      ProofError{}    -> error (show res)-                                     _               -> return $ getModelObjectiveValue objName m+                                     _               -> return $ getModelObjectiveValue (annotateForMS (Proxy @a) objName) m              mi <- getBound minimize             ma <- getBound maximize
Data/SBV/Trans.hs view
@@ -133,7 +133,7 @@   , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..)    -- ** Observing expressions-  , observe+  , observe, sObserve    -- ** Programmable model extraction   , SatModel(..), Modelable(..), displayModels, extractModels@@ -168,7 +168,6 @@ import Data.SBV.Core.Kind import Data.SBV.Core.Model import Data.SBV.Core.Floating-import Data.SBV.Core.Sized import Data.SBV.Core.Symbolic  import Data.SBV.Provers.Prover
Data/SBV/Utils/Lib.hs view
@@ -18,15 +18,19 @@                           , joinArgs, splitArgs                           , stringToQFS, qfsToString                           , isKString+                          , checkObservableName                           )                           where -import Data.Char    (isSpace, chr, ord)+import Data.Char    (isSpace, chr, ord, toLower, isDigit)+import Data.List    (isPrefixOf) import Data.Dynamic (fromDynamic, toDyn, Typeable) import Data.Maybe   (fromJust, isJust, isNothing)  import Numeric (readHex, showHex) +import Data.SBV.SMT.SMTLibNames (smtLibReservedNames)+ -- | We have a nasty issue with the usual String/List confusion in Haskell. However, we can -- do a simple dynamic trick to determine where we are. The ice is thin here, but it seems to work. isKString :: forall a. Typeable a => a -> Bool@@ -131,3 +135,16 @@          | oc >= 0x20 && oc <= 0x7E = [c]          | True                     = "\\u{" ++ showHex oc "" ++ "}"          where oc = ord c++-- | Check if an observable name is good.+checkObservableName :: String -> Maybe String+checkObservableName lbl+  | null lbl+  = Just "SBV.observe: Bad empty name!"+  | map toLower lbl `elem` smtLibReservedNames+  = Just $ "SBV.observe: The name chosen is reserved, please change it!: " ++ show lbl+  | "s" `isPrefixOf` lbl && all isDigit (drop 1 lbl)+  = Just $ "SBV.observe: Names of the form sXXX are internal to SBV, please use a different name: " ++ show lbl+  | True+  = Nothing+
Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs view
@@ -13,6 +13,8 @@ -- purposes, such as efficiency, or reliability. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts #-}+ {-# OPTIONS_GHC -Wall -Werror #-}  module Documentation.SBV.Examples.CodeGeneration.Uninterpreted where
Documentation/SBV/Examples/Lists/BoundedMutex.hs view
@@ -12,6 +12,7 @@  {-# LANGUAGE DeriveAnyClass      #-} {-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE OverloadedLists     #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving  #-}
Documentation/SBV/Examples/Misc/FirstOrderLogic.hs view
@@ -32,7 +32,7 @@ -- $setup -- >>> -- For doctest purposes only, ignore. -- >>> import Data.SBV--- >>> :set -XDataKinds+-- >>> :set -XDataKinds -XScopedTypeVariables  -- | An uninterpreted sort for demo purposes, named 'U' data U
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -199,14 +199,10 @@ -- bits for the significand explicitly stored, includes the hidden bit. We have: -- -- >>> fp54Bounds--- Objective "max": Optimal model:---   x   = 61440 :: FloatingPoint 5 4---   max =   503 :: WordN 9---   min =   503 :: WordN 9--- Objective "min": Optimal model:---   x   = 0.000007629 :: FloatingPoint 5 4---   max =         257 :: WordN 9---   min =         257 :: WordN 9+-- Objective "toMetricSpace(max)": Optimal model:+--   x = 61440 :: FloatingPoint 5 4+-- Objective "toMetricSpace(min)": Optimal model:+--   x = 0.000007629 :: FloatingPoint 5 4 -- -- An important note is in order. When printing floats in decimal, one can get correct yet surprising results. -- There's a large body of publications in how to render floats in decimal, or in bases that are not powers of@@ -218,13 +214,18 @@ -- decimal notation one should be very careful about the printed representation and the numeric value; while -- they will match in value (if there are no bugs!), they can print quite differently! (Also keep in -- mind the rounding modes that impact how the conversion is done.)+--+-- One final note: When printing the models, we skip optimization variables that are not named @x@. See the+-- call to `Data.SBV.Core.Symbolic.isNonModelVal`. When we optimize floating-point values, the underlying engine actually optimizes+-- with bit-vector values, producing intermediate results. We skip those here to simplify the presentation. fp54Bounds :: IO OptimizeResult-fp54Bounds = optimize Independent $ do x :: SFloatingPoint 5 4 <- sFloatingPoint "x"+fp54Bounds = optimizeWith z3{isNonModelVar = (/= "x")}+                          Independent $ do x :: SFloatingPoint 5 4 <- sFloatingPoint "x" -                                       constrain $ fpIsPoint x-                                       constrain $ x .> 0+                                           constrain $ fpIsPoint x+                                           constrain $ x .> 0 -                                       maximize "max" x-                                       minimize "min" x+                                           maximize "max" x+                                           minimize "min" x -                                       pure sTrue+                                           pure sTrue
Documentation/SBV/Examples/Optimization/Enumerate.hs view
@@ -51,6 +51,8 @@                     $ ite (x .== 5) sSat                                     sSun +  annotateForMS _ s = "DayAsWord8(" ++ s ++ ")"+ -- | Identify weekend days isWeekend :: SDay -> SBool isWeekend = (`sElem` weekend)@@ -61,8 +63,9 @@ -- -- >>> almostWeekend -- Optimal model:---   almostWeekend = Fri :: Day---   last-day      =   4 :: Word8+--   last-day             = Fri :: Day+--   almostWeekend        = Fri :: Day+--   DayAsWord8(last-day) =   4 :: Word8 almostWeekend :: IO OptimizeResult almostWeekend = optimize Lexicographic $ do                     day <- free "almostWeekend"@@ -74,8 +77,9 @@ -- -- >>> weekendJustOver -- Optimal model:---   weekendJustOver = Mon :: Day---   first-day       =   0 :: Word8+--   first-day             = Mon :: Day+--   weekendJustOver       = Mon :: Day+--   DayAsWord8(first-day) =   0 :: Word8 weekendJustOver :: IO OptimizeResult weekendJustOver = optimize Lexicographic $ do                       day <- free "weekendJustOver"@@ -87,8 +91,9 @@ -- -- >>> firstWeekend -- Optimal model:---   firstWeekend  = Sat :: Day---   first-weekend =   5 :: Word8+--   first-weekend             = Sat :: Day+--   firstWeekend              = Sat :: Day+--   DayAsWord8(first-weekend) =   5 :: Word8 firstWeekend :: IO OptimizeResult firstWeekend = optimize Lexicographic $ do                       day <- free "firstWeekend"
Documentation/SBV/Examples/Puzzles/Birthday.hs view
@@ -7,7 +7,6 @@ -- Stability : experimental -- -- This is a formalization of the Cheryl's birthday problem, which went viral in April 2015.--- (See <http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html>.) -- -- Here's the puzzle: --
+ Documentation/SBV/Examples/Puzzles/Tower.hs view
@@ -0,0 +1,153 @@+-----------------------------------------------------------------------------+-- |+-- Module    : Documentation.SBV.Examples.Puzzles.Tower+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Solves the tower puzzle, <http://www.chiark.greenend.org.uk/%7Esgtatham/puzzles/js/towers.html>.+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module Documentation.SBV.Examples.Puzzles.Tower where++import Control.Monad+import Data.Array hiding (inRange)+import Data.SBV+import Data.SBV.Control++-------------------------------------------------------------------+-- * Modeling Towers+-------------------------------------------------------------------++-- | Count of visible towers as an array.+type Count a = Array Integer a++-- | The grid itself. The indexes are tuples, first coordinate increases as you go from+-- left to right, and the second increases as you go from top to bottom.+type Grid a = Array (Integer, Integer) a++-- | The problem has 4 counts, from top, left, bottom, and right. And the grid itself.+type Problem a = (Count a, Count a, Count a, Count a, Grid a)++-- | Example problem. Encodes:+--+-- @+--     - - 3 - - 4+--   -     2       5+--   -   2         -+--   4             -+--   2             -+--   -             2+--   3             -+--     - - 3 4 - -+-- @+problem :: Problem (Maybe Integer)+problem = (top, left, bot, right, grid)+  where build ix es = accumArray (\_ a -> a) Nothing ix [(i, Just v) | (i, v) <- es]++        top   = build  (1, 6)          [(3, 3), (6, 4)]+        left  = build  (1, 6)          [(3, 4), (4, 2), (6, 3)]+        bot   = build  (1, 6)          [(3, 3), (4, 4)]+        right = build  (1, 6)          [(1, 5), (5, 2)]+        grid  = build ((1, 1), (6, 6)) [((3, 1), 2), ((2, 2), 2)]++-- | Given a concrete partial board, turn it into a symbolic board, by filling in the+-- empty cells with symbolic variables.+symProblem :: Problem (Maybe Integer) -> Symbolic (Problem SInteger)+symProblem (t, l, b, r, g) = (,,,,) <$> fill t <*> fill l <*> fill b <*> fill r <*> fill g+ where fill :: Traversable f => f (Maybe Integer) -> Symbolic (f SInteger)+       fill = mapM (maybe free_ (pure . literal))++-------------------------------------------------------------------+-- * Counting visible towers+-------------------------------------------------------------------++-- | Given a list of tower heights, count the number of visible ones in the given order.+-- We simply keep track of the tallest we have seen so far, and increment the count for+-- each tower we see if it's taller than the tallest seen so far.+visible :: [SInteger] -> SInteger+visible = go 0 0+ where go _            visibleSofar []     = visibleSofar+       go tallestSofar visibleSofar (x:xs) = go (tallestSofar `smax` x)+                                                (ite (x .> tallestSofar) (1 + visibleSofar) visibleSofar)+                                                xs++-------------------------------------------------------------------+-- * Building constraints+-------------------------------------------------------------------++-- | Build the constraints for a given problem. We scan the elements and add the required+-- visibility counts for each row and column, viewed both in the correct order and in the backwards order.+tower :: Problem SInteger -> Symbolic ()+tower (top, left, bot, right, grid) = do+  let (minX, maxX) = bounds top+      (minY, maxY) = bounds left++  -- Constraints from top and bottom+  forM_ [minX .. maxX] $ \x -> do+      let reqT = top ! x+          reqB = bot ! x+          elts = [grid ! (x, y) | y <- [minY .. maxY]]+      mapM_ (\e -> constrain (inRange e (literal 1, literal maxY))) elts+      constrain $ distinct elts+      constrain $ reqT .== visible elts+      constrain $ reqB .== visible (reverse elts)++  -- Constraints from left and right+  forM_ [minY .. maxY] $ \y -> do+      let reqL = left  ! y+          reqR = right ! y+          elts = [grid ! (x, y) | x <- [minX .. maxX]]+      mapM_ (\e -> constrain (inRange e (literal 1, literal maxX))) elts+      constrain $ distinct elts+      constrain $ reqL .== visible elts+      constrain $ reqR .== visible (reverse elts)++-------------------------------------------------------------------+-- * Example run+-------------------------------------------------------------------++-- | Solve the puzzle descibed above. We get:+--+-- >>> example+--   1 2 3 2 2 4+-- 1 6 5 2 4 3 1 5+-- 3 3 2 5 6 1 4 2+-- 4 2 4 1 5 6 3 2+-- 2 5 3 6 1 4 2 3+-- 2 1 6 4 3 2 5 2+-- 3 4 1 3 2 5 6 1+--   3 2 3 4 2 1+example :: IO ()+example = runSMT $ do+        sp <- symProblem problem+        tower sp+        query $ do cs <- checkSat+                   case cs of+                     Unsat -> io $ putStrLn "Unsolvable"+                     Sat   -> display sp+                     _     -> error $ "Unexpected result: " ++ show cs+ where display :: Problem SInteger -> Query ()+       display (top, left, bot, right, grid) = do+          let (minX, maxX) = bounds top+              (minY, maxY) = bounds left++          -- Display top row+          io $ putStr "  "+          topVals <- forM [minX .. maxX] $ \x -> getValue (top ! x)+          io $ putStrLn $ unwords (map show topVals)++          -- Display each row, sandwiched between left/right+          forM_ [minY .. maxY] $ \y -> do+             lv <- getValue (left  ! y)+             rv <- getValue (right ! y)+             row <- forM [minX .. maxX] $ \x -> getValue (grid ! (x, y))+             io $ putStrLn $ unwords (map show (lv : row ++ [rv]))++          -- Finish with bottom row+          io $ putStr "  "+          botVals <- forM [minX .. maxX] $ \x -> getValue (bot ! x)+          io $ putStrLn $ unwords (map show botVals)
Documentation/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -222,7 +222,7 @@         disp :: Int -> (Bool, [(Bool, U2Member, U2Member)]) -> IO ()         disp i (_, ss)          | lss /= n = error $ "Expected " ++ show n ++ " results; got: " ++ show lss-         | True     = do putStrLn $ "Solution #" ++ show i ++ ": "+         | True     = do putStrLn $ "Solution #" ++ show i ++ ":"                          go False 0 ss                          return ()          where lss  = length ss
Documentation/SBV/Examples/WeakestPreconditions/Sum.hs view
@@ -237,15 +237,15 @@ Following proof obligations failed: ===================================   Measure for loop "i < n" is negative:-    State  : SumS {n = 0, i = -1, s = 0}-    Measure: -1+    State  : SumS {n = -1, i = -2, s = 1}+    Measure: -3   Measure for loop "i < n" does not decrease:-    Before : SumS {n = 0, i = -1, s = 0}-    Measure: -1-    After  : SumS {n = 0, i = 0, s = 0}-    Measure: 0+    Before : SumS {n = -1, i = -2, s = 1}+    Measure: -3+    After  : SumS {n = -1, i = -1, s = 0}+    Measure: -2  Clearly, as @i@ increases, so does our bogus measure @n+i@. Note that in this case the counterexample has-@i@ as a negative value, as the SMT solver finds a counter-example to induction, not+@i@ and @n@ as a negative value, as the SMT solver finds a counter-example to induction, not necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof. -}
README.md view
@@ -104,7 +104,9 @@ The following people made major contributions to SBV, by developing new features and contributing to the design in significant ways: Joel Burget, Brian Huffman, Brian Schroeder, and Jeffrey Young.  The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:+Andreas Abel, Ara Adkins,+Andrew Anderson, Kanishka Azimi, Markus Barenhoff, Reid Barton,
SBVTestSuite/GoldFiles/allSat8.gold view
@@ -63,4 +63,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch!  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.10-inplace:Data.SBV.Control.Utils+  error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.11-inplace:Data.SBV.Control.Utils
SBVTestSuite/GoldFiles/arbFp_opt_1.gold view
@@ -1,3 +1,4 @@ Optimal model:-  s0 = 65504.0 :: FloatingPoint 5 11-  x  =   64511 :: Word16+  x                = 65504.0 :: FloatingPoint 5 11+  s0               = 65504.0 :: FloatingPoint 5 11+  toMetricSpace(x) =   64511 :: Word16
SBVTestSuite/GoldFiles/nested1.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples.  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested2.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples.  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested3.gold view
@@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples.  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested4.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples.  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.10-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1938:48 in sbv-10.11-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/noOpt1.gold view
@@ -31,4 +31,4 @@ *** Use "sat" for plain satisfaction  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Provers/Prover.hs:261:27 in sbv-10.10-inplace:Data.SBV.Provers.Prover+  error, called at ./Data/SBV/Provers/Prover.hs:261:27 in sbv-10.11-inplace:Data.SBV.Provers.Prover
SBVTestSuite/GoldFiles/noOpt2.gold view
@@ -33,4 +33,4 @@ *** Use "optimize"/"optimizeWith" to calculate optimal satisfaction!  CallStack (from HasCallStack):-  error, called at ./Data/SBV/Provers/Prover.hs:608:33 in sbv-10.10-inplace:Data.SBV.Provers.Prover+  error, called at ./Data/SBV/Provers/Prover.hs:608:33 in sbv-10.11-inplace:Data.SBV.Provers.Prover
SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = 127 :: Int8-  m = 255 :: Word8+  m                = 127 :: Int8+  x                = 127 :: Int8+  toMetricSpace(m) = 255 :: Word8
SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = -128 :: Int8-  m =    0 :: Word8+  m                = -128 :: Int8+  x                = -128 :: Int8+  toMetricSpace(m) =    0 :: Word8
SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = 32767 :: Int16-  m = 65535 :: Word16+  m                = 32767 :: Int16+  x                = 32767 :: Int16+  toMetricSpace(m) = 65535 :: Word16
SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = -32768 :: Int16-  m =      0 :: Word16+  m                = -32768 :: Int16+  x                = -32768 :: Int16+  toMetricSpace(m) =      0 :: Word16
SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = 2147483647 :: Int32-  m = 4294967295 :: Word32+  m                = 2147483647 :: Int32+  x                = 2147483647 :: Int32+  toMetricSpace(m) = 4294967295 :: Word32
SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = -2147483648 :: Int32-  m =           0 :: Word32+  m                = -2147483648 :: Int32+  x                = -2147483648 :: Int32+  toMetricSpace(m) =           0 :: Word32
SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x =  9223372036854775807 :: Int64-  m = 18446744073709551615 :: Word64+  m                =  9223372036854775807 :: Int64+  x                =  9223372036854775807 :: Int64+  toMetricSpace(m) = 18446744073709551615 :: Word64
SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold view
@@ -1,3 +1,4 @@ Optimal model:-  x = -9223372036854775808 :: Int64-  m =                    0 :: Word64+  m                = -9223372036854775808 :: Int64+  x                = -9223372036854775808 :: Int64+  toMetricSpace(m) =                    0 :: Word64
SBVTestSuite/GoldFiles/optFloat1a.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     = -3.4028235e38 :: Float+  min-x                = -3.4028235e38 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -13,7 +13,21 @@            Octal: -0o3.77777774p+126          Decimal: -3.4028235e38              Hex: -0xf.fffffp+124-  min-x =       8388608 :: Word32+  x                    = -3.4028235e38 :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 1 11111110 11111111111111111111111+      Hex layout: FF7F FFFF+       Precision: Single+            Sign: Negative+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: -0b1.11111111111111111111111p+127+           Octal: -0o3.77777774p+126+         Decimal: -3.4028235e38+             Hex: -0xf.fffffp+124+  toMetricSpace(min-x) =       8388608 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 0000 0000 1000 0000 0000 0000 0000 0000
SBVTestSuite/GoldFiles/optFloat1b.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     = -Infinity :: Float+  min-x                = -Infinity :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -10,7 +10,18 @@         Exponent: 128 (Stored: 255, Bias: 127)   Classification: FP_INFINITE            Value: -Infinity-  min-x =   8388607 :: Word32+  x                    = -Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 1 11111111 00000000000000000000000+      Hex layout: FF80 0000+       Precision: Single+            Sign: Negative+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: -Infinity+  toMetricSpace(min-x) =   8388607 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 0000 0000 0111 1111 1111 1111 1111 1111
SBVTestSuite/GoldFiles/optFloat1c.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     = 3.4028235e38 :: Float+  max-x                = 3.4028235e38 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -13,7 +13,21 @@            Octal: 0o3.77777774p+126          Decimal: 3.4028235e38              Hex: 0xf.fffffp+124-  max-x =   4286578687 :: Word32+  x                    = 3.4028235e38 :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 0 11111110 11111111111111111111111+      Hex layout: 7F7F FFFF+       Precision: Single+            Sign: Positive+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1.11111111111111111111111p+127+           Octal: 0o3.77777774p+126+         Decimal: 3.4028235e38+             Hex: 0xf.fffffp+124+  toMetricSpace(max-x) =   4286578687 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1111 1111 0111 1111 1111 1111 1111 1111
SBVTestSuite/GoldFiles/optFloat1d.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     =   Infinity :: Float+  max-y                =   Infinity :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -10,7 +10,18 @@         Exponent: 128 (Stored: 255, Bias: 127)   Classification: FP_INFINITE            Value: Infinity-  max-y = 4286578688 :: Word32+  x                    =   Infinity :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------+   Binary layout: 0 11111111 00000000000000000000000+      Hex layout: 7F80 0000+       Precision: Single+            Sign: Positive+        Exponent: 128 (Stored: 255, Bias: 127)+  Classification: FP_INFINITE+           Value: Infinity+  toMetricSpace(max-y) = 4286578688 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1111 1111 1000 0000 0000 0000 0000 0000
SBVTestSuite/GoldFiles/optFloat2a.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     = -1.7976931348623157e308 :: Double+  min-x                = -1.7976931348623157e308 :: Double                   6    5          4         3         2         1         0                   3 21098765432 1098765432109876543210987654321098765432109876543210                   S ----E11---- ------------------------S52-------------------------@@ -13,7 +13,21 @@            Octal: -0o1.777777777777777774p+1023          Decimal: -1.7976931348623157e308              Hex: -0xf.ffffffffffff8p+1020-  min-x =        4503599627370496 :: Word64+  x                    = -1.7976931348623157e308 :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 1 11111111110 1111111111111111111111111111111111111111111111111111+      Hex layout: FFEF FFFF FFFF FFFF+       Precision: Double+            Sign: Negative+        Exponent: 1023 (Stored: 2046, Bias: 1023)+  Classification: FP_NORMAL+          Binary: -0b1.1111111111111111111111111111111111111111111111111111p+1023+           Octal: -0o1.777777777777777774p+1023+         Decimal: -1.7976931348623157e308+             Hex: -0xf.ffffffffffff8p+1020+  toMetricSpace(min-x) =        4503599627370496 :: Word64                   6    5           4            3           2            1           0                   3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 0000 0000 0001 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000
SBVTestSuite/GoldFiles/optFloat2b.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     =        -Infinity :: Double+  min-x                =        -Infinity :: Double                   6    5          4         3         2         1         0                   3 21098765432 1098765432109876543210987654321098765432109876543210                   S ----E11---- ------------------------S52-------------------------@@ -10,7 +10,18 @@         Exponent: 1024 (Stored: 2047, Bias: 1023)   Classification: FP_INFINITE            Value: -Infinity-  min-x = 4503599627370495 :: Word64+  x                    =        -Infinity :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 1 11111111111 0000000000000000000000000000000000000000000000000000+      Hex layout: FFF0 0000 0000 0000+       Precision: Double+            Sign: Negative+        Exponent: 1024 (Stored: 2047, Bias: 1023)+  Classification: FP_INFINITE+           Value: -Infinity+  toMetricSpace(min-x) = 4503599627370495 :: Word64                   6    5           4            3           2            1           0                   3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 0000 0000 0000 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111
SBVTestSuite/GoldFiles/optFloat2c.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     = 1.7976931348623157e308 :: Double+  max-x                = 1.7976931348623157e308 :: Double                   6    5          4         3         2         1         0                   3 21098765432 1098765432109876543210987654321098765432109876543210                   S ----E11---- ------------------------S52-------------------------@@ -13,7 +13,21 @@            Octal: 0o1.777777777777777774p+1023          Decimal: 1.7976931348623157e308              Hex: 0xf.ffffffffffff8p+1020-  max-x =   18442240474082181119 :: Word64+  x                    = 1.7976931348623157e308 :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 0 11111111110 1111111111111111111111111111111111111111111111111111+      Hex layout: 7FEF FFFF FFFF FFFF+       Precision: Double+            Sign: Positive+        Exponent: 1023 (Stored: 2046, Bias: 1023)+  Classification: FP_NORMAL+          Binary: 0b1.1111111111111111111111111111111111111111111111111111p+1023+           Octal: 0o1.777777777777777774p+1023+         Decimal: 1.7976931348623157e308+             Hex: 0xf.ffffffffffff8p+1020+  toMetricSpace(max-x) =   18442240474082181119 :: Word64                   6    5           4            3           2            1           0                   3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1111 1111 1110 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111 1111
SBVTestSuite/GoldFiles/optFloat2d.gold view
@@ -1,5 +1,5 @@ Optimal model:-  x     =             Infinity :: Double+  max-y                =             Infinity :: Double                   6    5          4         3         2         1         0                   3 21098765432 1098765432109876543210987654321098765432109876543210                   S ----E11---- ------------------------S52-------------------------@@ -10,7 +10,18 @@         Exponent: 1024 (Stored: 2047, Bias: 1023)   Classification: FP_INFINITE            Value: Infinity-  max-y = 18442240474082181120 :: Word64+  x                    =             Infinity :: Double+                  6    5          4         3         2         1         0+                  3 21098765432 1098765432109876543210987654321098765432109876543210+                  S ----E11---- ------------------------S52-------------------------+   Binary layout: 0 11111111111 0000000000000000000000000000000000000000000000000000+      Hex layout: 7FF0 0000 0000 0000+       Precision: Double+            Sign: Positive+        Exponent: 1024 (Stored: 2047, Bias: 1023)+  Classification: FP_INFINITE+           Value: Infinity+  toMetricSpace(max-y) = 18442240474082181120 :: Word64                   6    5           4            3           2            1           0                   3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1111 1111 1111 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000
SBVTestSuite/GoldFiles/optFloat3.gold view
@@ -1,5 +1,5 @@ Optimal model:-  max-x+y        = 3.4028235e38 :: Float+  max-x+y                       = 3.4028235e38 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -13,10 +13,24 @@            Octal: 0o3.77777774p+126          Decimal: 3.4028235e38              Hex: 0xf.fffffp+124-  x              = 1.7014117e38 :: Float+  metric-max-x+y                = 3.4028235e38 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------+   Binary layout: 0 11111110 11111111111111111111111+      Hex layout: 7F7F FFFF+       Precision: Single+            Sign: Positive+        Exponent: 127 (Stored: 254, Bias: 127)+  Classification: FP_NORMAL+          Binary: 0b1.11111111111111111111111p+127+           Octal: 0o3.77777774p+126+         Decimal: 3.4028235e38+             Hex: 0xf.fffffp+124+  x                             = 1.7014117e38 :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------    Binary layout: 0 11111101 11111111111111111111111       Hex layout: 7EFF FFFF        Precision: Single@@ -27,7 +41,7 @@            Octal: 0o1.77777776p+126          Decimal: 1.7014117e38              Hex: 0x7.fffff8p+124-  y              = 1.7014117e38 :: Float+  y                             = 1.7014117e38 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -41,7 +55,7 @@            Octal: 0o1.77777776p+126          Decimal: 1.7014117e38              Hex: 0x7.fffff8p+124-  metric-max-x+y =   4286578687 :: Word32+  toMetricSpace(metric-max-x+y) =   4286578687 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1111 1111 0111 1111 1111 1111 1111 1111
SBVTestSuite/GoldFiles/optFloat4.gold view
@@ -1,5 +1,5 @@ Optimal model:-  min-x+y        =    3.0e-45 :: Float+  metric-min-x+y                =    3.0e-45 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -13,10 +13,24 @@            Octal: 0o4p-150          Decimal: 3.0e-45              Hex: 0x1p-148-  x              =    1.0e-45 :: Float+  min-x+y                       =    3.0e-45 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------+   Binary layout: 0 00000000 00000000000000000000010+      Hex layout: 0000 0002+       Precision: Single+            Sign: Positive+        Exponent: -126 (Subnormal, with fixed exponent value. Stored: 0, Bias: 127)+  Classification: FP_SUBNORMAL+          Binary: 0b1p-148+           Octal: 0o4p-150+         Decimal: 3.0e-45+             Hex: 0x1p-148+  x                             =    1.0e-45 :: Float+                  3  2          1         0+                  1 09876543 21098765432109876543210+                  S ---E8--- ----------S23----------    Binary layout: 0 00000000 00000000000000000000001       Hex layout: 0000 0001        Precision: Single@@ -27,7 +41,7 @@            Octal: 0o2p-150          Decimal: 1.0e-45              Hex: 0x8p-152-  y              =    1.0e-45 :: Float+  y                             =    1.0e-45 :: Float                   3  2          1         0                   1 09876543 21098765432109876543210                   S ---E8--- ----------S23----------@@ -41,7 +55,7 @@            Octal: 0o2p-150          Decimal: 1.0e-45              Hex: 0x8p-152-  metric-min-x+y = 2147483650 :: Word32+  toMetricSpace(metric-min-x+y) = 2147483650 :: Word32                   3 2            1           0                   1098 7654 3210 9876 5432 1098 7654 3210    Binary layout: 1000 0000 0000 0000 0000 0000 0000 0010
SBVTestSuite/GoldFiles/query_uisatex1.gold view
@@ -167,8 +167,8 @@   s0 = 0 :: Integer    q1 :: Integer -> Integer-  q1 0    = 1 -  q1 (-3) = 9 +  q1 0    = 1+  q1 (-3) = 9   q1 3    = 75   q1 _    = 12 @@ -179,16 +179,16 @@    q3 :: Float -> Bool -> Integer -> Float   q3 9.6 False 8   = Infinity-  q3 9.6 True  121 = -0.0    -  q3 _   _     _   = 8.6     +  q3 9.6 True  121 = -0.0+  q3 _   _     _   = 8.6    q4 :: Char -> String -> Float-  q4 'r' "foo" = 3.5 +  q4 'r' "foo" = 3.5   q4 'c' "tey" = 92.0   q4 _   _     = 78.0    q5 :: [Integer] -> [Float] -> Integer   q5 [5]   [8.2,0.0] = 210-  q5 [9,5] [8.2,9.0] = 21 -  q5 _     _         = 7  +  q5 [9,5] [8.2,9.0] = 21+  q5 _     _         = 7 DONE!
SBVTestSuite/GoldFiles/uiSat_test1.gold view
@@ -93,12 +93,12 @@  RESULT: Solution #1:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False Solution #2:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True Solution #3:   q1 :: Bool -> Bool   q1 _ = True
SBVTestSuite/GoldFiles/uiSat_test2.gold view
@@ -298,65 +298,65 @@ RESULT: Solution #1:   q2 :: Bool -> Bool -> Bool   q2 True True = False-  q2 _    _    = True +  q2 _    _    = True Solution #2:   q2 :: Bool -> Bool -> Bool   q2 True True  = False   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #3:   q2 :: Bool -> Bool -> Bool   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #4:   q2 :: Bool -> Bool -> Bool   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #5:   q2 :: Bool -> Bool -> Bool   q2 True  True = False   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #6:   q2 :: Bool -> Bool -> Bool-  q2 True  True  = True -  q2 False False = True +  q2 True  True  = True+  q2 False False = True   q2 _     _     = False Solution #7:   q2 :: Bool -> Bool -> Bool-  q2 False False = True +  q2 False False = True   q2 _     _     = False Solution #8:   q2 :: Bool -> Bool -> Bool-  q2 True True  = True -  q2 True False = True +  q2 True True  = True+  q2 True False = True   q2 _    _     = False Solution #9:   q2 :: Bool -> Bool -> Bool-  q2 True False = True +  q2 True False = True   q2 _    _     = False Solution #10:   q2 :: Bool -> Bool -> Bool-  q2 True  False = True -  q2 False True  = True +  q2 True  False = True+  q2 False True  = True   q2 _     _     = False Solution #11:   q2 :: Bool -> Bool -> Bool-  q2 True True = True +  q2 True True = True   q2 _    _    = False Solution #12:   q2 :: Bool -> Bool -> Bool-  q2 True  True = True -  q2 False True = True +  q2 True  True = True+  q2 False True = True   q2 _     _    = False Solution #13:   q2 :: Bool -> Bool -> Bool-  q2 False True = True +  q2 False True = True   q2 _     _    = False Solution #14:   q2 :: Bool -> Bool -> Bool   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #15:   q2 :: Bool -> Bool -> Bool   q2 _ _ = True
SBVTestSuite/GoldFiles/uiSat_test3.gold view
@@ -1886,54 +1886,54 @@ RESULT: Solution #1:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool   q2 True True = False-  q2 _    _    = True +  q2 _    _    = True Solution #2:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 False True  = True -  q2 False False = True +  q2 False True  = True+  q2 False False = True   q2 _     _     = False Solution #3:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 False True  = True -  q2 False False = True +  q2 False True  = True+  q2 False False = True   q2 _     _     = False Solution #4:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 False False = True +  q2 False False = True   q2 _     _     = False Solution #5:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True True = True +  q2 True True = True   q2 _    _    = False Solution #6:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True True = True +  q2 True True = True   q2 _    _    = False Solution #7:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool   q2 _ _ = False@@ -1942,39 +1942,39 @@   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True False = True +  q2 True False = True   q2 _    _     = False Solution #9:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True True  = True -  q2 True False = True +  q2 True True  = True+  q2 True False = True   q2 _    _     = False Solution #10:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True True  = True -  q2 True False = True +  q2 True True  = True+  q2 True False = True   q2 _    _     = False Solution #11:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True False = True +  q2 True False = True   q2 _    _     = False Solution #12:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 True True = True +  q2 True True = True   q2 _    _    = False Solution #13:   q1 :: Bool -> Bool@@ -1982,19 +1982,19 @@    q2 :: Bool -> Bool -> Bool   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #14:   q1 :: Bool -> Bool-  q1 False = True +  q1 False = True   q1 _     = False    q2 :: Bool -> Bool -> Bool   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #15:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool   q2 _ _ = True@@ -2010,7 +2010,7 @@    q2 :: Bool -> Bool -> Bool   q2 True True = False-  q2 _    _    = True +  q2 _    _    = True Solution #18:   q1 :: Bool -> Bool   q1 _ = True@@ -2018,135 +2018,135 @@   q2 :: Bool -> Bool -> Bool   q2 True  True  = False   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #19:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #20:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #21:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True  False = True -  q2 False True  = True +  q2 True  False = True+  q2 False True  = True   q2 _     _     = False Solution #22:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True  True = True -  q2 False True = True +  q2 True  True = True+  q2 False True = True   q2 _     _    = False Solution #23:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 False True = True +  q2 False True = True   q2 _     _    = False Solution #24:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 False True = True +  q2 False True = True   q2 _     _    = False Solution #25:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 False True = True -  q2 True  True = True +  q2 False True = True+  q2 True  True = True   q2 _     _    = False Solution #26:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 False True = True -  q2 True  True = True +  q2 False True = True+  q2 True  True = True   q2 _     _    = False Solution #27:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 True False = True -  q2 True True  = True +  q2 True False = True+  q2 True True  = True   q2 _    _     = False Solution #28:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 False True  = False   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #29:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 True  True = True -  q2 False True = True +  q2 True  True = True+  q2 False True = True   q2 _     _    = False Solution #30:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 True True = True +  q2 True True = True   q2 _    _    = False Solution #31:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 False True = True +  q2 False True = True   q2 _     _    = False Solution #32:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 False True  = True -  q2 True  False = True +  q2 False True  = True+  q2 True  False = True   q2 _     _     = False Solution #33:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 True  True  = False   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #34:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 True False = True +  q2 True False = True   q2 _    _     = False Solution #35:   q1 :: Bool -> Bool@@ -2154,34 +2154,34 @@    q2 :: Bool -> Bool -> Bool   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #36:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 False False = False-  q2 _     _     = True +  q2 _     _     = True Solution #37:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 False True = True +  q2 False True = True   q2 _     _    = False Solution #38:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 True False = True +  q2 True False = True   q2 _    _     = False Solution #39:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool@@ -2191,25 +2191,25 @@   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True  False = True -  q2 False False = True +  q2 True  False = True+  q2 False False = True   q2 _     _     = False Solution #41:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True  False = True -  q2 False False = True +  q2 True  False = True+  q2 False False = True   q2 _     _     = False Solution #42:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 False False = True +  q2 False False = True   q2 _     _     = False Solution #43:   q1 :: Bool -> Bool@@ -2218,10 +2218,10 @@   q2 :: Bool -> Bool -> Bool   q2 True False = False   q2 True True  = False-  q2 _    _     = True +  q2 _    _     = True Solution #44:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool@@ -2232,24 +2232,24 @@    q2 :: Bool -> Bool -> Bool   q2 True True = False-  q2 _    _    = True +  q2 _    _    = True Solution #46:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 True True = False-  q2 _    _    = True +  q2 _    _    = True Solution #47:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 True False = False   q2 True True  = False-  q2 _    _     = True +  q2 _    _     = True Solution #48:   q1 :: Bool -> Bool   q1 _ = False@@ -2257,23 +2257,23 @@   q2 :: Bool -> Bool -> Bool   q2 True  True = False   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #49:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 True  False = True -  q2 False False = True +  q2 True  False = True+  q2 False False = True   q2 _     _     = False Solution #50:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 False False = True +  q2 False False = True   q2 _     _     = False Solution #51:   q1 :: Bool -> Bool@@ -2281,78 +2281,78 @@    q2 :: Bool -> Bool -> Bool   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #52:   q1 :: Bool -> Bool-  q1 False = True +  q1 False = True   q1 _     = False    q2 :: Bool -> Bool -> Bool   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #53:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #54:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool   q2 False True = False-  q2 _     _    = True +  q2 _     _    = True Solution #55:   q1 :: Bool -> Bool   q1 _ = True    q2 :: Bool -> Bool -> Bool-  q2 True  True  = True -  q2 False False = True +  q2 True  True  = True+  q2 False False = True   q2 _     _     = False Solution #56:   q1 :: Bool -> Bool   q1 True = False-  q1 _    = True +  q1 _    = True    q2 :: Bool -> Bool -> Bool-  q2 True  True  = True -  q2 False False = True +  q2 True  True  = True+  q2 False False = True   q2 _     _     = False Solution #57:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #58:   q1 :: Bool -> Bool-  q1 True = True +  q1 True = True   q1 _    = False    q2 :: Bool -> Bool -> Bool-  q2 True  True  = True -  q2 False False = True +  q2 True  True  = True+  q2 False False = True   q2 _     _     = False Solution #59:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 True  True  = True -  q2 False False = True +  q2 True  True  = True+  q2 False False = True   q2 _     _     = False Solution #60:   q1 :: Bool -> Bool   q1 _ = False    q2 :: Bool -> Bool -> Bool-  q2 False False = True +  q2 False False = True   q2 _     _     = False Solution #61:   q1 :: Bool -> Bool@@ -2360,7 +2360,7 @@    q2 :: Bool -> Bool -> Bool   q2 True False = False-  q2 _    _     = True +  q2 _    _     = True Solution #62:   q1 :: Bool -> Bool   q1 _ = False
SBVTestSuite/TestSuite/Arrays/Query.hs view
@@ -9,6 +9,7 @@ -- Test suite for query mode arrays ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts    #-} {-# LANGUAGE ScopedTypeVariables #-}  {-# OPTIONS_GHC -Wall -Werror #-}
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -25,7 +25,7 @@  module TestSuite.Basics.ArithSolver(tests) where -import Data.SBV.Internals hiding (free, free_)+import Data.SBV.Internals hiding (free, free_, (#)) import Utils.SBVTestFramework  import Data.List (genericIndex, isInfixOf, isPrefixOf, isSuffixOf, genericTake, genericDrop, genericLength)@@ -349,7 +349,7 @@ genDoubles :: [TestTree] genDoubles = genIEEE754 "genDoubles" ds -genIEEE754 :: (IEEEFloating a, Show a) => String -> [a] -> [TestTree]+genIEEE754 :: (IEEEFloating a, Num (SBV a), Show a) => String -> [a] -> [TestTree] genIEEE754 origin vs =  [tst1 ("pred_"   ++ nm, x, y)    | (nm, x, y)    <- preds]                      ++ [tst1 ("unary_"  ++ nm, x, y)    | (nm, x, y)    <- uns]                      ++ [tst2 ("binary_" ++ nm, x, y, r) | (nm, x, y, r) <- bins]
SBVTestSuite/TestSuite/Basics/BoundedList.hs view
@@ -9,6 +9,7 @@ -- Test the bounded sequence/list functions. ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts           #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedLists            #-} {-# LANGUAGE ScopedTypeVariables        #-}
SBVTestSuite/TestSuite/Basics/PseudoBoolean.hs view
@@ -9,6 +9,8 @@ -- Test the pseudo-boolean functions ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts #-}+ {-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}  module TestSuite.Basics.PseudoBoolean(tests)  where
SBVTestSuite/TestSuite/CantTypeCheck/Misc.hs view
@@ -9,8 +9,8 @@ -- Test suite for things that should not type-check ----------------------------------------------------------------------------- -{-# LANGUAGE DataKinds         #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE FlexibleInstances    #-}  -- Defer type-errors is essential here! {-# OPTIONS_GHC -Wall -Werror -Wno-orphans -Wno-deferred-type-errors -fdefer-type-errors #-}@@ -25,11 +25,22 @@ instance NFData (IO Bool) where   rnf iob = rnf (unsafePerformIO iob) `seq` () +type Val = (Integer, Integer)++instance Num Val where+  (+)         = undefined+  (*)         = undefined+  (-)         = undefined+  signum      = undefined+  abs         = undefined+  fromInteger = undefined+ tests :: TestTree tests = testGroup "CantTypeCheck.Misc" [            testCase "noTypeCheckBad01"  $ shouldNotTypeCheck $ isTheorem t1          , testCase "noTypeCheckBad02"  $ shouldNotTypeCheck $ isTheorem t2          , testCase "noTypeCheckBad03"  $ shouldNotTypeCheck   runSko+         , testCase "noTypeCheckBad04"  $ shouldNotTypeCheck   runNoNum          , testCase "noTypeCheckGood01" $                      assertIsSat t1          , testCase "noTypeCheckGood02" $                      assertIsSat t2 @@ -52,3 +63,10 @@         -- Oh the horrors of "deferring type errors"         runSko :: IO Bool         runSko = isSatisfiable $ sko (Forall (literal 3))++        -- can't add SBV Val+        noNumSBV :: SBV Val -> SBV Val -> SBV Val+        noNumSBV x y = x + y++        runNoNum :: IO Bool+        runNoNum = isSatisfiable noNumSBV
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 10.10+Version     : 10.11 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@@ -19,7 +19,7 @@ Data-Files         : SBVTestSuite/GoldFiles/*.gold Extra-Doc-Files    : INSTALL, README.md, COPYRIGHT, CHANGES.md -Tested-With        : GHC==9.8.1+Tested-With        : GHC==9.10.1  source-repository head     type:       git@@ -94,7 +94,7 @@                   , text                   , directory                   , time-                  , libBF            >= 0.6.7+                  , libBF            >= 0.6.8                   , process                   , syb                   , uniplate@@ -202,6 +202,7 @@                   , Documentation.SBV.Examples.Puzzles.Rabbits                   , Documentation.SBV.Examples.Puzzles.SendMoreMoney                   , Documentation.SBV.Examples.Puzzles.Sudoku+                  , Documentation.SBV.Examples.Puzzles.Tower                   , Documentation.SBV.Examples.Puzzles.U2Bridge                   , Documentation.SBV.Examples.Queries.Abducts                   , Documentation.SBV.Examples.Queries.AllSat