diff -Nru haskell-sbv-5.7/CHANGES.md haskell-sbv-5.9/CHANGES.md --- haskell-sbv-5.7/CHANGES.md 2015-12-21 23:39:04.000000000 +0000 +++ haskell-sbv-5.9/CHANGES.md 2016-01-06 02:02:35.000000000 +0000 @@ -1,7 +1,33 @@ * Hackage: * GitHub: -* Latest Hackage released version: 5.7, 2015-12-21 +* Latest Hackage released version: 5.9, 2016-01-05 + +### Version 5.9, 2016-01-05 + + * Default definition for 'symbolicMerge', which allows types that are + instances of 'Generic' to have an automatically derivable merge (i.e., + ite) instance. Thanks to Christian Conkle for the patch. + + * Add support for "non-model-vars," where we can now tell SBV not + to take into account certain variables from a model-building + perspective. This comes handy in doing an `allSat` calls where + there might be witness variables that we do not care the uniqueness + for. See "Data/SBV/Examples/Misc/Auxiliary.hs" for an example, and + the discussion in https://github.com/LeventErkok/sbv/issues/208 for + motivation. + + * Yices interface: If Reals are used, then pick the logic QF_UFLRA, instead + of QF_AUFLIA. Unfortunately, logic selection remains tricky since the SMTLib + story for logic selection is rather messy. Other solvers are not impacted + by this change. + +### Version 5.8, 2016-01-01 + + * Fix some typos + * Add 'svEnumFromThenTo' to the Dynamic interface, allowing dynamic construction + of [x, y .. z] and [x .. y] when the involved values are concrete. + * Add 'svExp' to the Dynamic interface, implementing exponentation ### Version 5.7, 2015-12-21 diff -Nru haskell-sbv-5.7/COPYRIGHT haskell-sbv-5.9/COPYRIGHT --- haskell-sbv-5.7/COPYRIGHT 2015-12-21 23:39:04.000000000 +0000 +++ haskell-sbv-5.9/COPYRIGHT 2016-01-06 02:02:35.000000000 +0000 @@ -1,4 +1,4 @@ -Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file diff -Nru haskell-sbv-5.7/Data/SBV/BitVectors/Model.hs haskell-sbv-5.9/Data/SBV/BitVectors/Model.hs --- haskell-sbv-5.7/Data/SBV/BitVectors/Model.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/BitVectors/Model.hs 2016-01-06 02:02:35.000000000 +0000 @@ -18,6 +18,8 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DefaultSignatures #-} module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral @@ -41,6 +43,8 @@ import Control.Monad.Reader (ask) import Control.Monad.Trans (liftIO) +import GHC.Generics (U1(..), M1(..), (:*:)(..), K1(..)) +import qualified GHC.Generics as G import GHC.Stack.Compat import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize) @@ -695,7 +699,7 @@ sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftLeft x i | not (isBounded x) - = error "SBV.sShiftRight: Shifted about should be a bounded quantity!" + = error "SBV.sShiftRight: Shifted amount should be a bounded quantity!" | True = ite (i .< 0) (select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z (-i)) @@ -712,7 +716,7 @@ sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftRight x i | not (isBounded x) - = error "SBV.sShiftRight: Shifted about should be a bounded quantity!" + = error "SBV.sShiftRight: Shifted amount should be a bounded quantity!" | True = ite (i .< 0) (select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z (-i)) @@ -1076,11 +1080,20 @@ -- provides all basic types as instances of this class, so users only need -- to declare instances for custom data-types of their programs as needed. -- +-- A 'Mergeable' instance may be automatically derived for a custom data-type +-- with a single constructor where the type of each field is an instance of +-- 'Mergeable', such as a record of symbolic values. Users only need to add +-- 'G.Generic' and 'Mergeable' to the @deriving@ clause for the data-type. See +-- 'Data.SBV.Examples.Puzzles.U2Bridge.Status' for an example and an +-- illustration of what the instance would look like if written by hand. +-- -- The function 'select' is a total-indexing function out of a list of choices -- with a default value, simulating array/list indexing. It's an n-way generalization -- of the 'ite' function. -- --- Minimal complete definition: 'symbolicMerge' +-- Minimal complete definition: None, if the type is instance of 'Generic'. Otherwise +-- 'symbolicMerge'. Note that most types subject to merging are likely to be +-- trivial instances of 'Generic'. class Mergeable a where -- | Merge two values based on the condition. The first argument states -- whether we force the then-and-else branches before the merging, at the @@ -1090,7 +1103,7 @@ symbolicMerge :: Bool -> SBool -> a -> a -> a -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@ - -- overflows + -- underflows/overflows. select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a -- NB. Earlier implementation of select used the binary-search trick -- on the index to chop down the search space. While that is a good trick @@ -1100,14 +1113,19 @@ -- list is really humongous, which is not very common in general. (Also, -- for the case when the list is bit-vectors, we use SMT tables anyhow.) select xs err ind - | isReal ind = error "SBV.select: unsupported real valued select/index expression" - | isFloat ind = error "SBV.select: unsupported float valued select/index expression" - | isDouble ind = error "SBV.select: unsupported double valued select/index expression" + | isReal ind = bad "real" + | isFloat ind = bad "float" + | isDouble ind = bad "double" | hasSign ind = ite (ind .< 0) err (walk xs ind err) | True = walk xs ind err - where walk [] _ acc = acc + where bad w = error $ "SBV.select: unsupported " ++ w ++ " valued select/index expression" + walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) + -- Default implementation for 'symbolicMerge' if the type is 'Generic' + default symbolicMerge :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a + symbolicMerge = symbolicMergeDefault + -- | If-then-else. This is by definition 'symbolicMerge' with both -- branches forced. This is typically the desired behavior, but also @@ -1270,6 +1288,38 @@ select xs (err1, err2, err3, err4, err5, err6, err7) ind = (select as err1 ind, select bs err2 ind, select cs err3 ind, select ds err4 ind, select es err5 ind, select fs err6 ind, select gs err7 ind) where (as, bs, cs, ds, es, fs, gs) = unzip7 xs +-- Arbitrary product types, using GHC.Generics +-- +-- NB: Because of the way GHC.Generics works, the implementation of +-- symbolicMerge' is recursive. The derived instance for @data T a = T a a a a@ +-- resembles that for (a, (a, (a, a))), not the flat 4-tuple (a, a, a, a). This +-- difference should have no effect in practice. Note also that, unlike the +-- hand-rolled tuple instances, the generic instance does not provide a custom +-- 'select' implementation, and so does not benefit from the SMT-table +-- implementation in the 'SBV a' instance. + +-- | Not exported. Symbolic merge using the generic representation provided by +-- 'G.Generics'. +symbolicMergeDefault :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a +symbolicMergeDefault force t x y = G.to $ symbolicMerge' force t (G.from x) (G.from y) + +-- | Not exported. Used only in 'symbolicMergeDefault'. Instances are provided for +-- the generic representations of product types where each element is Mergeable. +class GMergeable f where + symbolicMerge' :: Bool -> SBool -> f a -> f a -> f a + +instance GMergeable U1 where + symbolicMerge' _ _ _ _ = U1 + +instance (Mergeable c) => GMergeable (K1 i c) where + symbolicMerge' force t (K1 x) (K1 y) = K1 $ symbolicMerge force t x y + +instance (GMergeable f) => GMergeable (M1 i c f) where + symbolicMerge' force t (M1 x) (M1 y) = M1 $ symbolicMerge' force t x y + +instance (GMergeable f, GMergeable g) => GMergeable (f :*: g) where + symbolicMerge' force t (x1 :*: y1) (x2 :*: y2) = symbolicMerge' force t x1 x2 :*: symbolicMerge' force t y1 y2 + -- Bounded instances instance (SymWord a, Bounded a) => Bounded (SBV a) where minBound = literal minBound diff -Nru haskell-sbv-5.7/Data/SBV/BitVectors/Operations.hs haskell-sbv-5.9/Data/SBV/BitVectors/Operations.hs --- haskell-sbv-5.7/Data/SBV/BitVectors/Operations.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/BitVectors/Operations.hs 2016-01-06 02:02:35.000000000 +0000 @@ -13,7 +13,7 @@ ( -- ** Basic constructors svTrue, svFalse, svBool - , svInteger, svFloat, svDouble, svReal + , svInteger, svFloat, svDouble, svReal, svEnumFromThenTo -- ** Basic destructors , svAsBool, svAsInteger, svNumerator, svDenominator -- ** Basic operations @@ -28,6 +28,7 @@ , svIte, svLazyIte, svSymbolicMerge , svSelect , svSign, svUnsign + , svExp -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight @@ -76,7 +77,6 @@ svReal :: Rational -> SVal svReal d = SVal KReal (Left (CW KReal (CWAlgReal (fromRational d)))) - -------------------------------------------------------------------------------- -- Basic destructors @@ -100,7 +100,20 @@ svDenominator (SVal KReal (Left (CW KReal (CWAlgReal (AlgRational True r))))) = Just $ denominator r svDenominator _ = Nothing --------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- +-- | Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite +-- Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping +-- it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus +-- the lifting to Integers preserves the bounds; and then going back is just fine. So, things like @[1, 5 .. 200] :: [SInt8]@ work just +-- fine (end evaluate to empty list), since we see @[1, 5 .. -56]@ in the @Integer@ domain. Also note the explicit check for @s /= f@ +-- below to make sure we don't stutter and produce an infinite list. +svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal] +svEnumFromThenTo bf mbs bt + | Just bs <- mbs, Just f <- svAsInteger bf, Just s <- svAsInteger bs, Just t <- svAsInteger bt, s /= f = Just $ map (svInteger (kindOf bf)) [f, s .. t] + | Nothing <- mbs, Just f <- svAsInteger bf, Just t <- svAsInteger bt = Just $ map (svInteger (kindOf bf)) [f .. t] + | True = Nothing + +------------------------------------------------------------------------------------- -- Basic operations -- | Addition. @@ -139,6 +152,16 @@ where -- should never happen die = error "impossible: integer valued data found in Fractional instance" +-- | Exponentiation. +svExp :: SVal -> SVal -> SVal +svExp b e | hasSign (kindOf e) = error "svExp: exponentiation only works with unsigned exponents" + | True = prod $ zipWith (\use n -> svIte use n one) + (blastLE e) + (iterate (\x -> svTimes x x) b) + where blastLE x = map (svTestBit x) [0 .. intSizeOf x - 1] + prod = foldr svTimes one + one = svInteger (kindOf b) 1 + -- | Quotient: Overloaded operation whose meaning depends on the kind at which -- it is used: For unbounded integers, it corresponds to the SMT-Lib -- "div" operator ("Euclidean" division, which always has a @@ -534,7 +557,7 @@ svShiftLeft :: SVal -> SVal -> SVal svShiftLeft x i | not (isBounded x) - = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!" + = error "SBV.svShiftLeft: Shifted amount should be a bounded quantity!" | True = svIte (svLessThan i zi) (svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i)) @@ -550,7 +573,7 @@ svShiftRight :: SVal -> SVal -> SVal svShiftRight x i | not (isBounded x) - = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!" + = error "SBV.svShiftLeft: Shifted amount should be a bounded quantity!" | True = svIte (svLessThan i zi) (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i)) @@ -700,6 +723,7 @@ _ -> True -- | Quot/Rem operations require a nonzero check on the divisor. +-- nonzeroCheck :: CW -> CW -> Bool nonzeroCheck _ b = cwVal b /= CWInteger 0 diff -Nru haskell-sbv-5.7/Data/SBV/BitVectors/Symbolic.hs haskell-sbv-5.9/Data/SBV/BitVectors/Symbolic.hs --- haskell-sbv-5.7/Data/SBV/BitVectors/Symbolic.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/BitVectors/Symbolic.hs 2016-01-06 02:02:35.000000000 +0000 @@ -996,16 +996,16 @@ -- | Translation tricks needed for specific capabilities afforded by each solver data SolverCapabilities = SolverCapabilities { - capSolverName :: String -- ^ Name of the solver - , mbDefaultLogic :: Maybe String -- ^ set-logic string to use in case not automatically determined (if any) - , supportsMacros :: Bool -- ^ Does the solver understand SMT-Lib2 macros? - , supportsProduceModels :: Bool -- ^ Does the solver understand produce-models option setting - , supportsQuantifiers :: Bool -- ^ Does the solver understand SMT-Lib2 style quantifiers? - , supportsUninterpretedSorts :: Bool -- ^ Does the solver understand SMT-Lib2 style uninterpreted-sorts - , supportsUnboundedInts :: Bool -- ^ Does the solver support unbounded integers? - , supportsReals :: Bool -- ^ Does the solver support reals? - , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers? - , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? + capSolverName :: String -- ^ Name of the solver + , mbDefaultLogic :: Bool -> Maybe String -- ^ set-logic string to use in case not automatically determined (if any). If Bool is True, then reals are present. + , supportsMacros :: Bool -- ^ Does the solver understand SMT-Lib2 macros? + , supportsProduceModels :: Bool -- ^ Does the solver understand produce-models option setting + , supportsQuantifiers :: Bool -- ^ Does the solver understand SMT-Lib2 style quantifiers? + , supportsUninterpretedSorts :: Bool -- ^ Does the solver understand SMT-Lib2 style uninterpreted-sorts + , supportsUnboundedInts :: Bool -- ^ Does the solver support unbounded integers? + , supportsReals :: Bool -- ^ Does the solver support reals? + , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers? + , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? } -- | Rounding mode to be used for the IEEE floating-point operations. @@ -1051,6 +1051,7 @@ , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. + , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) , smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool , solver :: SMTSolver -- ^ The actual SMT solver. diff -Nru haskell-sbv-5.7/Data/SBV/Dynamic.hs haskell-sbv-5.9/Data/SBV/Dynamic.hs --- haskell-sbv-5.7/Data/SBV/Dynamic.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Dynamic.hs 2016-01-06 02:02:35.000000000 +0000 @@ -38,11 +38,13 @@ , svReal, svNumerator, svDenominator -- *** Symbolic equality , svEqual, svNotEqual + -- *** Constructing concrete lists + , svEnumFromThenTo -- *** Symbolic ordering , svLessThan, svGreaterThan, svLessEq, svGreaterEq -- *** Arithmetic operations , svPlus, svTimes, svMinus, svUNeg, svAbs - , svDivide, svQuot, svRem + , svDivide, svQuot, svRem, svExp -- *** Logical operations , svAnd, svOr, svXOr, svNot , svShl, svShr, svRol, svRor diff -Nru haskell-sbv-5.7/Data/SBV/Examples/BitPrecise/Legato.hs haskell-sbv-5.9/Data/SBV/Examples/BitPrecise/Legato.hs --- haskell-sbv-5.7/Data/SBV/Examples/BitPrecise/Legato.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Examples/BitPrecise/Legato.hs 2016-01-06 02:02:35.000000000 +0000 @@ -31,12 +31,17 @@ -- is indeed correct. ----------------------------------------------------------------------------- +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveAnyClass #-} + module Data.SBV.Examples.BitPrecise.Legato where import Data.Array (Array, Ix(..), (!), (//), array) import Data.SBV +import GHC.Generics (Generic) + ------------------------------------------------------------------ -- * Mostek architecture ------------------------------------------------------------------ @@ -68,10 +73,13 @@ -- | Abstraction of the machine: The CPU consists of memory, registers, and flags. -- Unlike traditional hardware, we assume the program is stored in some other memory area that -- we need not model. (No self modifying programs!) +-- +-- 'Mostek' is equipped with an automatically derived 'Mergeable' instance +-- because each field is 'Mergeable'. data Mostek = Mostek { memory :: Memory , registers :: Registers , flags :: Flags - } + } deriving (Generic, Mergeable) -- | Given a machine state, compute a value out of it type Extract a = Mostek -> a @@ -79,13 +87,6 @@ -- | Programs are essentially state transformers (on the machine state) type Program = Mostek -> Mostek --- | 'Mergeable' instance of 'Mostek' simply pushes the merging into record fields. -instance Mergeable Mostek where - symbolicMerge f b m1 m2 = Mostek { memory = symbolicMerge f b (memory m1) (memory m2) - , registers = symbolicMerge f b (registers m1) (registers m2) - , flags = symbolicMerge f b (flags m1) (flags m2) - } - ------------------------------------------------------------------ -- * Low-level operations ------------------------------------------------------------------ diff -Nru haskell-sbv-5.7/Data/SBV/Examples/Misc/Auxiliary.hs haskell-sbv-5.9/Data/SBV/Examples/Misc/Auxiliary.hs --- haskell-sbv-5.7/Data/SBV/Examples/Misc/Auxiliary.hs 1970-01-01 00:00:00.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Examples/Misc/Auxiliary.hs 2016-01-06 02:02:35.000000000 +0000 @@ -0,0 +1,63 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.Auxiliary +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates model construction with auxiliary variables. Sometimes we +-- need to introduce a variable in our problem as an existential variable, +-- but it's "internal" to the problem and we do not consider it as part of +-- the solution. Also, in an `allSat` scenario, we may not care for models +-- that only differ in these auxiliaries. SBV allows designating such variables +-- as `isNonModelVar` so we can still use them like any other variable, but without +-- considering them explicitly in model construction. +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Misc.Auxiliary where + +import Data.SBV + +-- | A simple predicate, based on two variables @x@ and @y@, true when +-- @0 <= x <= 1@ and @x - abs y@ is @0@. +problem :: Predicate +problem = do x <- free "x" + y <- free "y" + constrain $ x .>= 0 + constrain $ x .<= 1 + return $ x - abs y .== (0 :: SInteger) + +-- | Generate all satisfying assignments for our problem. We have: +-- +-- >>> allModels +-- Solution #1: +-- x = 0 :: Integer +-- y = 0 :: Integer +-- Solution #2: +-- x = 1 :: Integer +-- y = -1 :: Integer +-- Solution #3: +-- x = 1 :: Integer +-- y = 1 :: Integer +-- Found 3 different solutions. +-- +-- Note that solutions @2@ and @3@ share the value @x = 1@, since there are +-- multiple values of @y@ that make this particular choice of @x@ satisfy our constraint. +allModels :: IO AllSatResult +allModels = allSat problem + +-- | Generate all satisfying assignments, but we first tell SBV that @y@ should not be considered +-- as a model problem, i.e., it's auxiliary. We have: +-- +-- >>> modelsWithYAux +-- Solution #1: +-- x = 0 :: Integer +-- Solution #2: +-- x = 1 :: Integer +-- Found 2 different solutions. +-- +-- Note that we now have only two solutions, one for each unique value of @x@ that satisfy our +-- constraint. +modelsWithYAux :: IO AllSatResult +modelsWithYAux = allSatWith z3{isNonModelVar = (`elem` ["y"])} problem diff -Nru haskell-sbv-5.7/Data/SBV/Examples/Puzzles/U2Bridge.hs haskell-sbv-5.9/Data/SBV/Examples/Puzzles/U2Bridge.hs --- haskell-sbv-5.7/Data/SBV/Examples/Puzzles/U2Bridge.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Examples/Puzzles/U2Bridge.hs 2016-01-06 02:02:35.000000000 +0000 @@ -11,6 +11,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} @@ -19,7 +20,9 @@ import Control.Monad (unless) import Control.Monad.State (State, runState, put, get, modify, evalState) -import Data.Generics +import Data.Generics (Data) +import GHC.Generics (Generic) + import Data.SBV ------------------------------------------------------------- @@ -68,13 +71,31 @@ [here, there] = map literal [Here, There] -- | The status of the puzzle after each move +-- +-- This type is equipped with an automatically derived 'Mergeable' instance +-- because each field is 'Mergeable'. A 'Generic' instance must also be derived +-- for this to work, and the 'DeriveAnyClass' language extension must be +-- enabled. The derived 'Mergeable' instance simply walks down the structure +-- field by field and merges each one. An equivalent hand-written 'Mergeable' +-- instance is provided in a comment below. data Status = Status { time :: STime -- ^ elapsed time , flash :: SLocation -- ^ location of the flash , lBono :: SLocation -- ^ location of Bono , lEdge :: SLocation -- ^ location of Edge , lAdam :: SLocation -- ^ location of Adam , lLarry :: SLocation -- ^ location of Larry - } + } deriving (Generic, Mergeable) + +-- The derived Mergeable instance is equivalent to the following: +-- +-- instance Mergeable Status where +-- symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2) +-- , flash = symbolicMerge f t (flash s1) (flash s2) +-- , lBono = symbolicMerge f t (lBono s1) (lBono s2) +-- , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2) +-- , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2) +-- , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2) +-- } -- | Start configuration, time elapsed is 0 and everybody is 'here' start :: Status @@ -86,17 +107,6 @@ , lLarry = here } --- | Mergeable instance for 'Status' simply walks down the structure fields and --- merges them. -instance Mergeable Status where - symbolicMerge f t s1 s2 = Status { time = symbolicMerge f t (time s1) (time s2) - , flash = symbolicMerge f t (flash s1) (flash s2) - , lBono = symbolicMerge f t (lBono s1) (lBono s2) - , lEdge = symbolicMerge f t (lEdge s1) (lEdge s2) - , lAdam = symbolicMerge f t (lAdam s1) (lAdam s2) - , lLarry = symbolicMerge f t (lLarry s1) (lLarry s2) - } - -- | A puzzle move is modeled as a state-transformer type Move a = State Status a diff -Nru haskell-sbv-5.7/Data/SBV/Provers/ABC.hs haskell-sbv-5.9/Data/SBV/Provers/ABC.hs --- haskell-sbv-5.7/Data/SBV/Provers/ABC.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/ABC.hs 2016-01-06 02:02:35.000000000 +0000 @@ -27,7 +27,7 @@ , engine = standardEngine "SBV_ABC" "SBV_ABC_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "ABC" - , mbDefaultLogic = Nothing + , mbDefaultLogic = const Nothing , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = False diff -Nru haskell-sbv-5.7/Data/SBV/Provers/Boolector.hs haskell-sbv-5.9/Data/SBV/Provers/Boolector.hs --- haskell-sbv-5.7/Data/SBV/Provers/Boolector.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/Boolector.hs 2016-01-06 02:02:35.000000000 +0000 @@ -25,7 +25,7 @@ , engine = standardEngine "SBV_BOOLECTOR" "SBV_BOOLECTOR_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "Boolector" - , mbDefaultLogic = Nothing + , mbDefaultLogic = const Nothing , supportsMacros = False , supportsProduceModels = True , supportsQuantifiers = False diff -Nru haskell-sbv-5.7/Data/SBV/Provers/CVC4.hs haskell-sbv-5.9/Data/SBV/Provers/CVC4.hs --- haskell-sbv-5.7/Data/SBV/Provers/CVC4.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/CVC4.hs 2016-01-06 02:02:35.000000000 +0000 @@ -27,7 +27,7 @@ , engine = standardEngine "SBV_CVC4" "SBV_CVC4_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "CVC4" - , mbDefaultLogic = Just "ALL_SUPPORTED" -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary + , mbDefaultLogic = const (Just "ALL_SUPPORTED") -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = True diff -Nru haskell-sbv-5.7/Data/SBV/Provers/MathSAT.hs haskell-sbv-5.9/Data/SBV/Provers/MathSAT.hs --- haskell-sbv-5.7/Data/SBV/Provers/MathSAT.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/MathSAT.hs 2016-01-06 02:02:35.000000000 +0000 @@ -27,7 +27,7 @@ , engine = standardEngine "SBV_MATHSAT" "SBV_MATHSAT_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "MathSAT" - , mbDefaultLogic = Nothing + , mbDefaultLogic = const Nothing , supportsMacros = False , supportsProduceModels = True , supportsQuantifiers = True diff -Nru haskell-sbv-5.7/Data/SBV/Provers/Prover.hs haskell-sbv-5.9/Data/SBV/Provers/Prover.hs --- haskell-sbv-5.7/Data/SBV/Provers/Prover.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/Prover.hs 2016-01-06 02:02:35.000000000 +0000 @@ -66,6 +66,7 @@ , solverTweaks = tweaks , smtLibVersion = smtVersion , satCmd = "(check-sat)" + , isNonModelVar = const False -- i.e., everything is a model-variable by default , roundingMode = RoundNearestTiesToEven , useLogic = Nothing } @@ -412,7 +413,8 @@ curResult <- invoke nonEqConsts n sbvPgm case curResult of Nothing -> return [] - Just (SatResult r) -> let cont model = do rest <- unsafeInterleaveIO $ loop (n+1) (modelAssocs model : nonEqConsts) + Just (SatResult r) -> let cont model = do let modelOnlyAssocs = [v | v@(x, _) <- modelAssocs model, not (isNonModelVar config x)] + rest <- unsafeInterleaveIO $ loop (n+1) (modelOnlyAssocs : nonEqConsts) return (r : rest) in case r of Satisfiable _ (SMTModel []) -> return [r] diff -Nru haskell-sbv-5.7/Data/SBV/Provers/Yices.hs haskell-sbv-5.9/Data/SBV/Provers/Yices.hs --- haskell-sbv-5.7/Data/SBV/Provers/Yices.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/Yices.hs 2016-01-06 02:02:35.000000000 +0000 @@ -27,7 +27,7 @@ , engine = standardEngine "SBV_YICES" "SBV_YICES_OPTIONS" addTimeOut standardModel , capabilities = SolverCapabilities { capSolverName = "Yices" - , mbDefaultLogic = Just "QF_AUFLIA" + , mbDefaultLogic = logic , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = False @@ -39,3 +39,7 @@ } } where addTimeOut _ _ = error "Yices: Timeout values are not supported by Yices" + -- Yices doesn't like it if we don't set the logic; so pick one and hope for the best + logic hasReals + | hasReals = Just "QF_UFLRA" + | True = Just "QF_AUFLIA" diff -Nru haskell-sbv-5.7/Data/SBV/Provers/Z3.hs haskell-sbv-5.9/Data/SBV/Provers/Z3.hs --- haskell-sbv-5.7/Data/SBV/Provers/Z3.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/Provers/Z3.hs 2016-01-06 02:02:35.000000000 +0000 @@ -56,7 +56,7 @@ standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps)) , capabilities = SolverCapabilities { capSolverName = "Z3" - , mbDefaultLogic = Nothing + , mbDefaultLogic = const Nothing , supportsMacros = True , supportsProduceModels = True , supportsQuantifiers = True diff -Nru haskell-sbv-5.7/Data/SBV/SMT/SMT.hs haskell-sbv-5.9/Data/SBV/SMT/SMT.hs --- haskell-sbv-5.7/Data/SBV/SMT/SMT.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/SMT/SMT.hs 2016-01-06 02:02:35.000000000 +0000 @@ -97,7 +97,7 @@ _ -> "Found " ++ show c ++ " different solutions." ++ uniqueWarn sh i c = (ok, showSMTResult "Unsatisfiable" "Unknown" "Unknown. Potential model:\n" - ("Solution #" ++ show i ++ ":\n[Backend solver returned no assignment to variables.]") ("Solution #" ++ show i ++ ":\n") c) + ("Solution #" ++ show i ++ ":\nSatisfiable") ("Solution #" ++ show i ++ ":\n") c) where ok = case c of Satisfiable{} -> True _ -> False @@ -345,10 +345,18 @@ where cfg = resultConfig result -- | Show a model in human readable form. Ignore bindings to those variables that start --- with "__internal_sbv_"; as these are only for internal purposes +-- with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes showModel :: SMTConfig -> SMTModel -> String -showModel cfg = intercalate "\n" . display . map shM . filter (not . ignore) . modelAssocs - where ignore (s, _) = "__internal_sbv_" `isPrefixOf` s +showModel cfg model + | null allVars + = "[There are no variables bound by the model.]" + | null relevantVars + = "[There are no model-variables bound by the model.]" + | True + = intercalate "\n" . display . map shM $ relevantVars + where allVars = modelAssocs model + relevantVars = filter (not . ignore) allVars + ignore (s, _) = "__internal_sbv_" `isPrefixOf` s || isNonModelVar cfg s shM (s, v) = let vs = shCW cfg v in ((length s, s), (vlength vs, vs)) display svs = map line svs where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v diff -Nru haskell-sbv-5.7/Data/SBV/SMT/SMTLib2.hs haskell-sbv-5.9/Data/SBV/SMT/SMTLib2.hs --- haskell-sbv-5.7/Data/SBV/SMT/SMTLib2.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/Data/SBV/SMT/SMTLib2.hs 2016-01-06 02:02:35.000000000 +0000 @@ -117,7 +117,7 @@ | not (null usorts) = "has user-defined sorts" | hasNonBVArrays = "has non-bitvector arrays" | True = "cannot determine the SMTLib-logic to use" - in case mbDefaultLogic solverCaps of + in case mbDefaultLogic solverCaps hasReal of Nothing -> ["; " ++ why ++ ", no logic specified."] Just l -> ["(set-logic " ++ l ++ "); " ++ why ++ ", using solver-default logic."] | True diff -Nru haskell-sbv-5.7/debian/changelog haskell-sbv-5.9/debian/changelog --- haskell-sbv-5.7/debian/changelog 2015-12-28 21:34:10.000000000 +0000 +++ haskell-sbv-5.9/debian/changelog 2016-01-13 11:10:47.000000000 +0000 @@ -1,3 +1,15 @@ +haskell-sbv (5.9-1build1) xenial; urgency=medium + + * Rebuild for new GHC ABIs. + + -- Colin Watson Wed, 13 Jan 2016 11:10:47 +0000 + +haskell-sbv (5.9-1) unstable; urgency=medium + + * New upstream release + + -- Clint Adams Sun, 10 Jan 2016 21:50:25 -0500 + haskell-sbv (5.7-1) unstable; urgency=medium * New upstream release diff -Nru haskell-sbv-5.7/LICENSE haskell-sbv-5.9/LICENSE --- haskell-sbv-5.7/LICENSE 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/LICENSE 2016-01-06 02:02:35.000000000 +0000 @@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without diff -Nru haskell-sbv-5.7/sbv.cabal haskell-sbv-5.9/sbv.cabal --- haskell-sbv-5.7/sbv.cabal 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/sbv.cabal 2016-01-06 02:02:35.000000000 +0000 @@ -1,5 +1,5 @@ Name: sbv -Version: 5.7 +Version: 5.9 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT @@ -79,6 +79,7 @@ , Data.SBV.Examples.Misc.Enumerate , Data.SBV.Examples.Misc.Floating , Data.SBV.Examples.Misc.ModelExtract + , Data.SBV.Examples.Misc.Auxiliary , Data.SBV.Examples.Misc.NoDiv0 , Data.SBV.Examples.Misc.Word4 , Data.SBV.Examples.Polynomials.Polynomials diff -Nru haskell-sbv-5.7/SBVUnitTest/SBVUnitTestBuildTime.hs haskell-sbv-5.9/SBVUnitTest/SBVUnitTestBuildTime.hs --- haskell-sbv-5.7/SBVUnitTest/SBVUnitTestBuildTime.hs 2015-12-21 23:39:03.000000000 +0000 +++ haskell-sbv-5.9/SBVUnitTest/SBVUnitTestBuildTime.hs 2016-01-06 02:02:35.000000000 +0000 @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Mon Dec 21 15:35:40 PST 2015" +buildTime = "Tue Jan 5 17:59:03 PST 2016"