sbv 7.4 → 7.5
raw patch · 37 files changed
+644/−303 lines, 37 filesdep ~Globdep ~QuickCheckdep ~bytestring
Dependency ranges changed: Glob, QuickCheck, bytestring, crackNum, doctest, hlint, tasty, tasty-golden, tasty-hunit, template-haskell
Files
- CHANGES.md +85/−17
- COPYRIGHT +1/−1
- Data/SBV.hs +13/−15
- Data/SBV/Control.hs +1/−1
- Data/SBV/Control/Query.hs +2/−1
- Data/SBV/Control/Types.hs +7/−4
- Data/SBV/Control/Utils.hs +19/−11
- Data/SBV/Core/Concrete.hs +0/−1
- Data/SBV/Core/Kind.hs +1/−1
- Data/SBV/Core/Model.hs +150/−106
- Data/SBV/Core/Splittable.hs +2/−43
- Data/SBV/Examples/CodeGeneration/PopulationCount.hs +1/−1
- Data/SBV/Examples/Misc/Word4.hs +0/−4
- Data/SBV/Examples/Optimization/VM.hs +1/−1
- Data/SBV/Examples/Queries/CaseSplit.hs +1/−1
- Data/SBV/Internals.hs +1/−2
- Data/SBV/SMT/SMT.hs +21/−23
- Data/SBV/SMT/SMTLib2.hs +3/−1
- Data/SBV/SMT/Utils.hs +70/−0
- Data/SBV/Tools/Polynomial.hs +3/−4
- Data/SBV/Tools/STree.hs +2/−4
- LICENSE +1/−1
- README.md +4/−4
- SBVTestSuite/GoldFiles/exceptionLocal1.gold +68/−0
- SBVTestSuite/GoldFiles/exceptionLocal2.gold +28/−0
- SBVTestSuite/GoldFiles/exceptionRemote1.gold +3/−0
- SBVTestSuite/GoldFiles/query1.gold +15/−15
- SBVTestSuite/GoldFiles/query_badOption.gold +4/−7
- SBVTestSuite/GoldFiles/temperature.gold +1/−5
- SBVTestSuite/SBVTest.hs +4/−1
- SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +21/−0
- SBVTestSuite/TestSuite/Basics/ArithSolver.hs +23/−0
- SBVTestSuite/TestSuite/Basics/Exceptions.hs +67/−0
- SBVTestSuite/TestSuite/Puzzles/Temperature.hs +5/−1
- SBVTestSuite/TestSuite/Queries/BadOption.hs +1/−1
- SBVTestSuite/Utils/SBVTestFramework.hs +7/−3
- sbv.cabal +8/−23
CHANGES.md view
@@ -1,8 +1,75 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.4, 2017-11-03+* Latest Hackage released version: 7.5, 2018-01-13 +### Version 7.5, Released 2018-01-13++ * Remove obsolote references to tactics in a few haddock comments. Thanks+ to Matthew Pickering for reporting.++ * Added logic 'Logic_NONE', to be used in cases where SBV should not+ try to set the logic. This is useful when there is no viable value to+ set, and the back-end solver doesn't understand the SMT-Lib convention+ of using "ALL" as the logic name. (One example of this is the Yices+ solver.)++ * SBV now returns SMTException (instead of just calling error) in case+ the backend solver responds with error message. The type SMTException+ can be caught by the user programs, and it includes many fields as an+ indication of what went wrong. (The command sent, what was expected,+ what was seen, etc.) Note that if this exception is ever caught, the+ backend solver is no longer alive: You should either just throw it,+ or perform proper clean-up on your user code as required to set up+ a new context. The provided show instance formats the exception nicely+ for display purposes. See https://github.com/LeventErkok/sbv/issues/335+ for details and thanks to Brian Huffman for reporting.++ * SIntegral class now has Integral as a super-class, which ensures the+ base-type it's used at is Integral. This was already true for all instances,+ so we are just making it more explicit.++ * Improve the implementation of .^ (exponentiation) to cover more cases,+ in particular signed exponents are now OK so long as they are concrete+ and positive, following Haskell convention.++ * Removed the 'FromBits' class. Its functionality is now merged with the+ new 'SFiniteBits' class, see below.++ * Introduce 'SFiniteBits' class, which only incorporates finite-words in it,+ i.e., SWord/SInt for 8-16-32-64. In particular it leaves out SInteger,+ SFloat, SDouble, and SReal. Important in recognizing bit-vectors of+ finite size, essentially. Here are the methods:++ class (SymWord a, Num a, Bits a) => SFiniteBits a where+ sFiniteBitSize :: SBV a -> Int -- ^ Bit size+ lsb :: SBV a -> SBool -- ^ Least significant bit of a word, always stored at index 0.+ msb :: SBV a -> SBool -- ^ Most significant bit of a word, always stored at the last position.+ blastBE :: SBV a -> [SBool] -- ^ Big-endian blasting of a word into its bits. Also see the 'FromBits' class.+ blastLE :: SBV a -> [SBool] -- ^ Little-endian blasting of a word into its bits. Also see the 'FromBits' class.+ fromBitsBE :: [SBool] -> SBV a -- ^ Reconstruct from given bits, given in little-endian+ fromBitsLE :: [SBool] -> SBV a -- ^ Reconstruct from given bits, given in little-endian+ sTestBit :: SBV a -> Int -> SBool -- ^ Replacement for 'testBit', returning 'SBool' instead of 'Bool'+ sExtractBits :: SBV a -> [Int] -> [SBool] -- ^ Variant of 'sTestBit', where we want to extract multiple bit positions.+ sPopCount :: SBV a -> SWord8 -- ^ Variant of 'popCount', returning a symbolic value.+ setBitTo :: SBV a -> Int -> SBool -> SBV a -- ^ A combo of 'setBit' and 'clearBit', when the bit to be set is symbolic.+ fullAdder :: SBV a -> SBV a -> (SBool, SBV a) -- ^ Full adder, returns carry-out from the addition. Only for unsigned quantities.+ fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) -- ^ Full multipler, returns both high and low-order bits. Only for unsigned quantities.+ sCountLeadingZeros :: SBV a -> SWord8 -- ^ Count leading zeros in a word, big-endian interpretation+ sCountTrailingZeros :: SBV a -> SWord8 -- ^ Count trailing zeros in a word, big-endian interpretation++ Note that the functions 'sFiniteBitSize', 'sCountLeadingZeros', and 'sCountTrailingZeros' are+ new. Others have existed in SBV before, we are just grouping them together now in this new class.++ * Tightened certain signatures where SBV was too liberal, using the SFiniteBits class. New signatures are:++ sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a+ crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b+ readSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e+ writeSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e++ Thanks to Thomas DuBuisson for reporting.+ ### Version 7.4, 2017-11-03 * Export queryDebug from the Control module, allowing custom queries to print@@ -35,7 +102,7 @@ of unbounded integers, which is not supported by SMTLib. Thanks to Robert for reporting the issue and identifying the root cause. - * Rework how quantifiers are handled: We now generate separte asserts for+ * Rework how quantifiers are handled: We now generate separate asserts for prefix-existentials. This allows for better (smaller) quantified code, while preserving semantics. @@ -135,7 +202,7 @@ * Changed the way `satWithAny` and `proveWithAny` works. Previously, these two functions ran multiple solvers, and took the result of the first- one to finish, killing all the others. In addition, they *waitied* for+ one to finish, killing all the others. In addition, they *waited* for the still-running solvers to finish cleaning-up, as sending a 'ThreadKilled' is usually not instantaneous. Furthermore, a solver might simply take its time! We now send the interrupt but do not wait for the process to@@ -288,7 +355,7 @@ minimize "name-of-goal" $ x + 2*y Minimizes the arithmetic goal x+2*y, where x and y can be bit-vectors, reals,- or integers. Such goals will be lexicographicly optimized, i.e., in the order+ or integers. Such goals will be lexicographically optimized, i.e., in the order given. If there are multiple goals, then user can also ask for independent optimization results, or pareto-fronts. @@ -312,7 +379,8 @@ mechanism. If the old code is needed, please contact for help: They can be resurrected in your own code if absolutely necessary. - * SBV now implements tactics, which allow the user to navigate the proof process.+ * (NB. This feature is deprecated in 7.0, see above for its replacement.)+ SBV now implements tactics, which allow the user to navigate the proof process. This is an advanced feature that most users will have no need of, but can become handy when dealing with complicated problems. Users can, for instance, implement case-splitting in a proof to guide the underlying solver through. Here is the list@@ -454,7 +522,7 @@ * 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+ * Add 'svExp' to the Dynamic interface, implementing exponentiation ### Version 5.7, 2015-12-21 @@ -495,7 +563,7 @@ it simply returns its final argument. Use in coordination with 'safe' and 'safeWith', see below. * Implement 'safe' and 'safeWith', which statically determine all calls to 'sAssert'- being safe to execute. Any vilations will be flagged. + being safe to execute. Any violations will be flagged. * SBV->C: Translate 'sAssert' calls to dynamic checks in the generated C code. If this is not desired, use the 'cgIgnoreSAssert' function to turn it off.@@ -725,7 +793,7 @@ changes. The introduction of the Dynamic SBV variant (i.e., one that does not mandate a phantom type as in "SBV Word8" etc. allows library writers more flexibility as they deal with arbitrary bit-vector sizes. The main- customor of these changes are the Cryptol language and the associated+ customer of these changes are the Cryptol language and the associated toolset, but other developers building on top of SBV can find it useful as well. NB: The "strongly-typed" aspect of SBV is still the main way end-users should interact with SBV, and nothing changed in that respect!@@ -767,7 +835,7 @@ * isPositiveZeroFP * isPointFP (corresponds to a real number, i.e., neither NaN nor infinity) - * Reimplement sbvTestBit, by Brian Huffman. This version is much faster at large+ * Re-implement sbvTestBit, by Brian Huffman. This version is much faster at large word sizes, as it avoids the costly mask generation. * Code changes to suppress warnings with GHC7.10. General clean-up.@@ -902,7 +970,7 @@ lazy at the Word instance, but not at lists/tuples etc. Thanks to Brian Huffman for reporting this bug. - * Add a few constant-folding optimizations for 'sDiv'and 'sRem'+ * Add a few constant-folding optimizations for 'sDiv' and 'sRem' * Boolector: Modify output parser to conform to the new Boolector output format. This means that you need at least v2.0.0 of Boolector installed if you want to use that@@ -1133,7 +1201,7 @@ ### Version 2.3, 2012-07-20 - * Maintanence release, no new features.+ * Maintenance release, no new features. * Tweak cabal dependencies to avoid using packages that are newer than those that come with ghc-7.4.2. Apparently this is a no-no that breaks many things, see the discussion in this thread:@@ -1143,7 +1211,7 @@ ### Version 2.2, 2012-07-17 - * Maintanence release, no new features.+ * Maintenance release, no new features. * Update cabal dependencies, in particular fix the regression with respect to latest version of the containers package.@@ -1241,10 +1309,10 @@ * Add a hook so users can add custom script segments for SMT solvers. The new "solverTweaks" field in the SMTConfig data-type can be used for this purpose. The need for this came about due to the need to workaround a Z3 v3.2 issue- detalied below:+ detailed below: http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks As a consequence, mixed Integer/BV problems can cause soundness issues in Z3- and does in SBV. Unfortunately, it is too severe for SBV to add the woraround+ and does in SBV. Unfortunately, it is too severe for SBV to add the workaround option, as it slows down the solver as a side effect as well. Thus, we are making this optionally available if/when needed. (Note that the work-around should not be necessary with Z3 v3.3; which is not released yet.)@@ -1321,7 +1389,7 @@ is useful for quickCheck and genTest functions for filtering acceptable test values. (Calls to pConstrain will be rejected for sat/prove calls.) * Add "isVacuous" which can be used to check that the constraints added- via constrain are satisfable. This is useful to prevent vacuous passes,+ via constrain are satisfiable. This is useful to prevent vacuous passes, i.e., when a proof is not just passing because the constraints imposed are inconsistent. (Also added accompanying isVacuousWith.) * Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_"@@ -1515,7 +1583,7 @@ ### Version 0.9.14, 2011-03-19 - * Reimplement sharing using Stable names, inspired+ * Re-implement sharing using Stable names, inspired by the Data.Reify techniques. This avoids tricks with unsafe memory stashing, and hence is safe. Thus, issues with respect to CAFs are now resolved.@@ -1545,7 +1613,7 @@ Bug fixes: * Output naming bug, reported by Josef Svenningsson- * Specification bug in Legatos multipler example+ * Specification bug in Legatos multiplier example ### Version 0.9.11, 2011-02-16
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2010-2017, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2018, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV.hs view
@@ -152,15 +152,11 @@ -- ** Operations on symbolic values -- *** Word level- , sTestBit, sExtractBits, sPopCount, sShiftLeft, sShiftRight, sRotateLeft, sRotateRight, sSignedShiftArithRight, sFromIntegral, setBitTo, oneIf- , lsb, msb, label+ , sShiftLeft, sShiftRight, sRotateLeft, sRotateRight, sSignedShiftArithRight, sFromIntegral, oneIf+ , label - -- *** Addition and Multiplication with high-bits- , fullAdder, fullMultiplier -- *** Exponentiation , (.^)- -- *** Blasting/Unblasting- , blastBE, blastLE, FromBits(..) -- *** Splitting, joining, and extending , Splittable(..) @@ -169,6 +165,8 @@ -- ** Symbolic integral numbers , SIntegral+ -- ** Symbolic finite bits+ , SFiniteBits(..) -- ** Division , SDivisible(..) -- ** The Boolean class@@ -211,6 +209,9 @@ -- * Running a symbolic computation , runSMT, runSMTWith + -- * Solver exceptions+ , SMTException(..)+ -- * Optimization -- $optiIntro , OptimizeStyle(..), Penalty(..), Objective(..), minimize, maximize, assertSoft@@ -274,8 +275,10 @@ import qualified Language.Haskell.TH as TH import Data.Generics-import Data.SBV.Control.Utils(SMTValue) +import Data.SBV.SMT.Utils (SMTException(..))+import Data.SBV.Control.Utils (SMTValue)+ -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing -- problems with constraints, like the following: --@@ -738,9 +741,9 @@ Such constraints are useful when used in conjunction with 'getUnsatCore' function where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable.-This feature is enabled by the following tactic:+This feature is enabled by the following option: - @ tactic $ SetOptions [ProduceUnsatCores True] @+ @ setOption $ ProduceUnsatCores True @ See "Data.SBV.Examples.Misc.UnsatCore" for an example use case. @@ -784,12 +787,7 @@ As we discussed SBV does not check that a given constraints is not vacuous. That is, that it can never be satisfied. This is usually the right behavior, since checking vacuity can be costly. The functions 'isVacuous' and 'isVacuousWith' should be used-to explicitly check for constraint vacuity if desired. Alternatively, the tactic:-- @ 'tactic' $ 'CheckConstrVacuity' True @--can be given which will force SBV to run an explicit check that constraints are not vacuous. (And complain if they are!)-Note that this adds an extra call to the solver for each constraint, and thus can be rather costly.+to explicitly check for constraint vacuity if desired. -} {- $uninterpreted
Data/SBV/Control.hs view
@@ -46,7 +46,7 @@ -- * Entering and exiting assertion stack , getAssertionStackDepth, push, pop, inNewAssertionStack - -- * Tactics+ -- * Higher level tactics , caseSplit -- * Resetting the solver state
Data/SBV/Control/Query.hs view
@@ -471,7 +471,8 @@ -- the conditions lead to a satisfiable result, returns @Just@ that result. If none of them -- do, returns @Nothing@. Note that we automatically generate a coverage case and search -- for it automatically as well. In that latter case, the string returned will be "Coverage".--- The first argument controls printing progress messages +-- The first argument controls printing progress messages See "Data.SBV.Examples.Queries.CaseSplit"+-- for an example use case. caseSplit :: Bool -> [(String, SBool)] -> Query (Maybe (String, SMTResult)) caseSplit printCases cases = do cfg <- getConfig go cfg (cases ++ [("Coverage", bnot (bOr (map snd cases)))])
Data/SBV/Control/Types.hs view
@@ -146,10 +146,12 @@ opt xs = "(set-option " ++ unwords xs ++ ")" info xs = "(set-info " ++ unwords xs ++ ")"- logic l = "(set-logic " ++ show l ++ ")" + logic Logic_NONE = "; NB. not setting the logic per user request of Logic_NONE"+ logic l = "(set-logic " ++ show l ++ ")"+ -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the--- user can override this choice using the tactic 'SetOptions' This is especially handy if one is experimenting with custom+-- user can override this choice using a call to 'setLogic' This is especially handy if one is experimenting with custom -- logics that might be supported on new solvers. See <http://smtlib.cs.uiowa.edu/logics.shtml> for the official list. data Logic = AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.@@ -178,8 +180,9 @@ | UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols. | QF_FPBV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors. | QF_FP -- ^ Quantifier-free formulas over the theory of floating point numbers.- | QF_FD -- ^ Quantifier-free finite domains- | Logic_ALL -- ^ The catch-all value+ | QF_FD -- ^ Quantifier-free finite domains.+ | Logic_ALL -- ^ The catch-all value.+ | Logic_NONE -- ^ Use this value when you want SBV to simply not set the logic. | CustomLogic String -- ^ In case you need a really custom string! deriving (Generic, NFData)
Data/SBV/Control/Utils.hs view
@@ -57,7 +57,7 @@ , QueryState(..), SVal(..), Quantifier(..), cache , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..) , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities- , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..)+ , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..), SMTSolver(..) ) import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar) @@ -65,13 +65,15 @@ import Data.SBV.Core.Operations (svNot, svNotEqual, svOr) import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib)-import Data.SBV.SMT.Utils (showTimeoutValue, annotateWithName, alignDiagnostic, alignPlain, debug, mergeSExpr)+import Data.SBV.SMT.Utils (showTimeoutValue, annotateWithName, alignPlain, debug, mergeSExpr, SMTException(..)) import Data.SBV.Utils.SExpr import Data.SBV.Control.Types import qualified Data.Set as Set (toList) +import qualified Control.Exception as C+ import GHC.Stack -- | 'Query' as a 'SolverContext'.@@ -598,15 +600,21 @@ -- empty the response channel first extras <- retrieveResponse "terminating upon unexpected response" (Just 5000000) - error $ unlines $ [ ""- , "*** Data.SBV: Unexpected response from the solver."- , "*** Context : " `alignDiagnostic` ctx- , "*** Sent : " `alignDiagnostic` sent- , "*** Expected: " `alignDiagnostic` expected- , "*** Received: " `alignDiagnostic` unlines (received : extras)- ]- ++ [ "*** Reason : " `alignDiagnostic` unlines r | Just r <- [mbReason]]- ++ [ "*** Hint : " `alignDiagnostic` unlines r | Just r <- [mbHint]]+ cfg <- getConfig++ let exc = SMTException { smtExceptionDescription = "Data.SBV: Unexpected response from the solver, context: " ++ ctx+ , smtExceptionSent = sent+ , smtExceptionExpected = expected+ , smtExceptionReceived = received+ , smtExceptionStdOut = unlines extras+ , smtExceptionStdErr = Nothing+ , smtExceptionExitCode = Nothing+ , smtExceptionConfig = cfg+ , smtExceptionReason = mbReason+ , smtExceptionHint = mbHint+ }++ io $ C.throwIO exc -- | Convert a query result to an SMT Problem runProofOn :: SMTConfig -> Bool -> [String] -> Result -> SMTProblem
Data/SBV/Core/Concrete.hs view
@@ -72,7 +72,6 @@ CWUserSort a `compare` CWUserSort b = a `compare` b -- | 'CW' represents a concrete word of a fixed size:--- Endianness is mostly irrelevant (see the 'FromBits' class). -- For signed words, the most significant digit is considered to be the sign. data CW = CW { _cwKind :: !Kind , cwVal :: !CWVal
Data/SBV/Core/Kind.hs view
@@ -87,7 +87,7 @@ isEnumeration = not (null constrs) && all (null . G.constrFields) constrs mbEnumFields | isEnumeration = check constrs []- | True = Left $ sortName ++ "is not a finite non-empty enumeration"+ | True = Left $ sortName ++ " is not a finite non-empty enumeration" check [] sofar = Right $ reverse sofar check (c:cs) sofar = case checkConstr c of Nothing -> check cs (show c : sofar)
Data/SBV/Core/Model.hs view
@@ -27,11 +27,9 @@ {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module Data.SBV.Core.Model (- Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), Metric(..), assertSoft, SIntegral- , ite, iteLazy, sTestBit, sExtractBits, sPopCount, setBitTo, sFromIntegral- , sShiftLeft, sShiftRight, sRotateLeft, sRotateRight, sSignedShiftArithRight, (.^)- , oneIf, blastBE, blastLE, fullAdder, fullMultiplier- , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_+ Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), Metric(..), assertSoft, SIntegral, SFiniteBits(..)+ , ite, iteLazy, sFromIntegral, sShiftLeft, sShiftRight, sRotateLeft, sRotateRight, sSignedShiftArithRight, (.^)+ , oneIf, genVar, genVar_, forall, forall_, exists, exists_ , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed , sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64@@ -73,12 +71,6 @@ import Data.SBV.Utils.Boolean --- | Newer versions of GHC (Starting with 7.8 I think), distinguishes between FiniteBits and Bits classes.--- We should really use FiniteBitSize for SBV which would make things better. In the interim, just work--- around pesky warnings..-ghcBitSize :: Bits a => a -> Int-ghcBitSize x = fromMaybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") (bitSizeMaybe x)- mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b) @@ -530,7 +522,7 @@ -- @ -- -- It is similar to the standard 'Integral' class, except ranging over symbolic instances.-class (SymWord a, Num a, Bits a) => SIntegral a+class (SymWord a, Num a, Bits a, Integral a) => SIntegral a -- 'SIntegral' Instances, skips Real/Float/Bool instance SIntegral Word8@@ -543,6 +535,127 @@ instance SIntegral Int64 instance SIntegral Integer +-- | 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 (SymWord a, Num a, Bits a) => SFiniteBits a where+ -- | Bit size.+ sFiniteBitSize :: SBV a -> Int+ -- | Least significant bit of a word, always stored at index 0.+ lsb :: SBV a -> SBool+ -- | Most significant bit of a word, always stored at the last position.+ msb :: SBV a -> SBool+ -- | Big-endian blasting of a word into its bits.+ blastBE :: SBV a -> [SBool]+ -- | Little-endian blasting of a word into its bits.+ blastLE :: SBV a -> [SBool]+ -- | Reconstruct from given bits, given in little-endian.+ fromBitsBE :: [SBool] -> SBV a+ -- | Reconstruct from given bits, given in little-endian.+ fromBitsLE :: [SBool] -> SBV a+ -- | Replacement for 'testBit', returning 'SBool' instead of 'Bool'.+ sTestBit :: SBV a -> Int -> SBool+ -- | Variant of 'sTestBit', where we want to extract multiple bit positions.+ sExtractBits :: SBV a -> [Int] -> [SBool]+ -- | Variant of 'popCount', returning a symbolic value.+ sPopCount :: SBV a -> SWord8+ -- | A combo of 'setBit' and 'clearBit', when the bit to be set is symbolic.+ setBitTo :: SBV a -> Int -> SBool -> SBV a+ -- | Full adder, returns carry-out from the addition. Only for unsigned quantities.+ fullAdder :: SBV a -> SBV a -> (SBool, SBV a)+ -- | Full multipler, returns both high and low-order bits. Only for unsigned quantities.+ fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)+ -- | Count leading zeros in a word, big-endian interpretation.+ sCountLeadingZeros :: SBV a -> SWord8+ -- | Count trailing zeros in a word, big-endian interpretation.+ sCountTrailingZeros :: SBV a -> SWord8++ -- Default implementations+ lsb (SBV v) = SBV (svTestBit v 0)+ msb x = sTestBit x (sFiniteBitSize x - 1)++ blastBE = reverse . blastLE+ blastLE x = map (sTestBit x) [0 .. intSizeOf x - 1]++ fromBitsBE = fromBitsLE . reverse+ fromBitsLE bs+ | length bs /= w+ = error $ "SBV.SFiniteBits.fromBitsLE/BE: Expected: " ++ show w ++ " bits, received: " ++ show (length bs)+ | True+ = result+ where w = sFiniteBitSize result+ result = go 0 0 bs++ go !acc _ [] = acc+ go !acc !i (x:xs) = go (ite x (setBit acc i) acc) (i+1) xs++ sTestBit (SBV x) i = SBV (svTestBit x i)+ sExtractBits x = map (sTestBit x)++ -- NB. 'sPopCount' returns an 'SWord8', which can overflow when used on quantities that have+ -- more than 255 bits. For the regular interface, this suffices for all types we support.+ -- For the Dynamic interface, if we ever implement this, this will fail for bit-vectors+ -- larger than that many bits. The alternative would be to return SInteger here, but that+ -- seems a total overkill for most use cases. If such is required, users are encouraged+ -- to define their own variants, which is rather easy.+ sPopCount x+ | isConcrete x = go 0 x+ | True = sum [ite b 1 0 | b <- blastLE x]+ where -- concrete case+ go !c 0 = c+ go !c w = go (c+1) (w .&. (w-1))++ setBitTo x i b = ite b (setBit x i) (clearBit x i)++ fullAdder a b+ | isSigned a = error "fullAdder: only works on unsigned numbers"+ | True = (a .> s ||| b .> s, s)+ where s = a + b++ -- N.B. The higher-order bits are determined using a simple shift-add multiplier,+ -- thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently+ -- with properties involving this function, at least with the current state of the art.+ fullMultiplier a b+ | isSigned a = error "fullMultiplier: only works on unsigned numbers"+ | True = (go (sFiniteBitSize a) 0 a, a*b)+ where go 0 p _ = p+ go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p)+ (o, p'') = shiftIn c p'+ (_, x') = shiftIn o x+ in go (n-1) p'' x'+ shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))+ where mask = ite k (bit (sFiniteBitSize v - 1)) 0++ -- See the note for 'sPopCount' for a comment on why we return 'SWord8'+ sCountLeadingZeros x = fromIntegral m - go m+ where m = sFiniteBitSize x - 1++ -- NB. When i is 0 below, which happens when x is 0 as we count all the way down,+ -- we return -1, which is equal to 2^n-1, giving us: n-1-(2^n-1) = n-2^n = n, as required, i.e., the bit-size.+ go :: Int -> SWord8+ go i | i < 0 = i8+ | True = ite (sTestBit x i) i8 (go (i-1))+ where i8 = literal (fromIntegral i :: Word8)++ -- See the note for 'sPopCount' for a comment on why we return 'SWord8'+ sCountTrailingZeros x = go 0+ where m = sFiniteBitSize x++ go :: Int -> SWord8+ go i | i >= m = i8+ | True = ite (sTestBit x i) i8 (go (i+1))+ where i8 = literal (fromIntegral i :: Word8)++-- 'SIntegral' Instances, skips Real/Float/Bool/Integer+instance SFiniteBits Word8 where sFiniteBitSize _ = 8+instance SFiniteBits Word16 where sFiniteBitSize _ = 16+instance SFiniteBits Word32 where sFiniteBitSize _ = 32+instance SFiniteBits Word64 where sFiniteBitSize _ = 64+instance SFiniteBits Int8 where sFiniteBitSize _ = 8+instance SFiniteBits Int16 where sFiniteBitSize _ = 16+instance SFiniteBits Int32 where sFiniteBitSize _ = 32+instance SFiniteBits Int64 where sFiniteBitSize _ = 64+ -- | Returns 1 if the boolean is true, otherwise 0. oneIf :: (Num a, SymWord a) => SBool -> SBV a oneIf t = ite t 1 0@@ -671,12 +784,27 @@ -- | Symbolic exponentiation using bit blasting and repeated squaring. ----- N.B. The exponent must be unsigned. Signed exponents will be rejected.+-- N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected. (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b-b .^ e | isSigned e = error "(.^): exponentiation only works with unsigned exponents"- | True = product $ zipWith (\use n -> ite use n 1)- (blastLE e)- (iterate (\x -> x*x) b)+b .^ e+ | isConcrete e, Just (x :: Integer) <- unliteral (sFromIntegral e)+ = if x >= 0 then let go n v+ | n == 0 = 1+ | even n = go (n `div` 2) (v * v)+ | True = v * go (n `div` 2) (v * v)+ in go x b+ else error $ "(.^): exponentiation: negative exponent: " ++ show x+ | not (isBounded e) || isSigned e+ = error $ "(.^): exponentiation only works with unsigned bounded symbolic exponents, kind: " ++ show (kindOf e)+ | True+ = -- NB. We can't simply use sTestBit and blastLE since they have SFiniteBit requirement+ -- but we want to have SIntegral here only.+ let SBV expt = e+ expBit i = SBV (svTestBit expt i)+ blasted = map expBit [0 .. intSizeOf e - 1]+ in product $ zipWith (\use n -> ite use n 1)+ blasted+ (iterate (\x -> x*x) b) instance (SymWord a, Fractional a) => Fractional (SBV a) where fromRational = literal . fromRational@@ -773,40 +901,6 @@ | True = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sPopCount instead." --- | Replacement for 'testBit'. Since 'testBit' requires a 'Bool' to be returned,--- we cannot implement it for symbolic words. Index 0 is the least-significant bit.-sTestBit :: SBV a -> Int -> SBool-sTestBit (SBV x) i = SBV (svTestBit x i)---- | Variant of 'sTestBit', where we want to extract multiple bit positions.-sExtractBits :: SBV a -> [Int] -> [SBool]-sExtractBits x = map (sTestBit x)---- | Replacement for 'popCount'. Since 'popCount' returns an 'Int', we cannot implement--- it for symbolic words. Here, we return an 'SWord8', which can overflow when used on--- quantities that have more than 255 bits. Currently, that's only the 'SInteger' type--- that SBV supports, all other types are safe. Even with 'SInteger', this will only--- overflow if there are at least 256-bits set in the number, and the smallest such--- number is 2^256-1, which is a pretty darn big number to worry about for practical--- purposes. In any case, we do not support 'sPopCount' for unbounded symbolic integers,--- as the only possible implementation wouldn't symbolically terminate. So the only overflow--- issue is with really-really large concrete 'SInteger' values.-sPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8-sPopCount x- | isReal x = error "SBV.sPopCount: Called on a real value" -- can't really happen due to types, but being overcautious- | isConcrete x = go 0 x- | not (isBounded x) = error "SBV.sPopCount: Called on an infinite precision symbolic value"- | True = sum [ite b 1 0 | b <- blastLE x]- where -- concrete case- go !c 0 = c- go !c w = go (c+1) (w .&. (w-1))---- | Generalization of 'setBit' based on a symbolic boolean. Note that 'setBit' and--- 'clearBit' are still available on Symbolic words, this operation comes handy when--- the condition to set/clear happens to be symbolic.-setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a-setBitTo x i b = ite b (setBit x i) (clearBit x i)- -- | Conversion between integral-symbolic values, akin to Haskell's fromIntegral sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b sFromIntegral x@@ -850,13 +944,14 @@ -- then it explicitly treats its msb as a sign-bit, and uses it as the bit that -- gets shifted in. Useful when using the underlying unsigned bit representation to implement -- custom signed operations. Note that there is no direct Haskell analogue of this function.-sSignedShiftArithRight:: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a+sSignedShiftArithRight:: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a sSignedShiftArithRight x i | isSigned i = error "sSignedShiftArithRight: shift amount should be unsigned"- | isSigned x = sShiftRight x i+ | isSigned x = ssa x i | True = ite (msb x)- (complement (sShiftRight (complement x) i))- (sShiftRight x i)+ (complement (ssa (complement x) i))+ (ssa x i)+ where ssa = liftViaSVal svShiftRight -- | Generalization of 'rotateL', when the shift-amount is symbolic. Since Haskell's -- 'rotateL' only takes an 'Int' as the shift amount, it cannot be used when we have@@ -869,57 +964,6 @@ -- a symbolic amount to shift with. The first argument should be a bounded quantity. sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a sRotateRight = liftViaSVal svRotateRight---- | Full adder. Returns the carry-out from the addition.------ N.B. Only works for unsigned types. Signed arguments will be rejected.-fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a)-fullAdder a b- | isSigned a = error "fullAdder: only works on unsigned numbers"- | True = (a .> s ||| b .> s, s)- where s = a + b---- | Full multiplier: Returns both the high-order and the low-order bits in a tuple,--- thus fully accounting for the overflow.------ N.B. Only works for unsigned types. Signed arguments will be rejected.------ N.B. The higher-order bits are determined using a simple shift-add multiplier,--- thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently--- with properties involving this function, at least with the current state of the art.-fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)-fullMultiplier a b- | isSigned a = error "fullMultiplier: only works on unsigned numbers"- | True = (go (ghcBitSize a) 0 a, a*b)- where go 0 p _ = p- go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p)- (o, p'') = shiftIn c p'- (_, x') = shiftIn o x- in go (n-1) p'' x'- shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))- where mask = ite k (bit (ghcBitSize v - 1)) 0---- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class.-blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]-blastLE x- | isReal x = error "SBV.blastLE: Called on a real value"- | not (isBounded x) = error "SBV.blastLE: Called on an infinite precision value"- | True = map (sTestBit x) [0 .. intSizeOf x - 1]---- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class.-blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]-blastBE = reverse . blastLE---- | Least significant bit of a word, always stored at index 0.-lsb :: SBV a -> SBool-lsb x = sTestBit x 0---- | Most significant bit of a word, always stored at the last position.-msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool-msb x- | isReal x = error "SBV.msb: Called on a real value"- | not (isBounded x) = error "SBV.msb: Called on an infinite precision value"- | True = sTestBit x (intSizeOf x - 1) -- Enum instance. These instances are suitable for use with concrete values, -- and will be less useful for symbolic values around. Note that `fromEnum` requires
Data/SBV/Core/Splittable.hs view
@@ -13,16 +13,15 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE BangPatterns #-} -module Data.SBV.Core.Splittable (Splittable(..), FromBits(..), checkAndConvert) where+module Data.SBV.Core.Splittable (Splittable(..)) where import Data.Bits (Bits(..)) import Data.Word (Word8, Word16, Word32, Word64) import Data.SBV.Core.Operations import Data.SBV.Core.Data-import Data.SBV.Core.Model+import Data.SBV.Core.Model () -- instances only infixr 5 # -- | Splitting an @a@ into two @b@'s and joining back.@@ -77,43 +76,3 @@ split (SBV x) = (SBV (svExtract 15 8 x), SBV (svExtract 7 0 x)) SBV a # SBV b = SBV (svJoin a b) extend b = 0 # b---- | Unblasting a value from symbolic-bits. The bits can be given little-endian--- or big-endian. For a signed number in little-endian, we assume the very last bit--- is the sign digit. This is a bit awkward, but it is more consistent with the "reverse" view of--- little-big-endian representations------ Minimal complete definition: 'fromBitsLE'-class FromBits a where- fromBitsLE, fromBitsBE :: [SBool] -> a- fromBitsBE = fromBitsLE . reverse---- | Construct a symbolic word from its bits given in little-endian-fromBinLE :: (Num a, Bits a, SymWord a) => [SBool] -> SBV a-fromBinLE = go 0 0- where go !acc _ [] = acc- go !acc !i (x:xs) = go (ite x (setBit acc i) acc) (i+1) xs---- | Perform a sanity check that we should receive precisely the same--- number of bits as required by the resulting type. The input is little-endian-checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a-checkAndConvert sz xs- | sz /= l- = error $ "SBV.fromBits.SWord" ++ ssz ++ ": Expected " ++ ssz ++ " elements, got: " ++ show l- | True- = fromBinLE xs- where l = length xs- ssz = show sz--instance FromBits SBool where- fromBitsLE [x] = x- fromBitsLE xs = error $ "SBV.fromBits.SBool: Expected 1 element, got: " ++ show (length xs)--instance FromBits SWord8 where fromBitsLE = checkAndConvert 8-instance FromBits SInt8 where fromBitsLE = checkAndConvert 8-instance FromBits SWord16 where fromBitsLE = checkAndConvert 16-instance FromBits SInt16 where fromBitsLE = checkAndConvert 16-instance FromBits SWord32 where fromBitsLE = checkAndConvert 32-instance FromBits SInt32 where fromBitsLE = checkAndConvert 32-instance FromBits SWord64 where fromBitsLE = checkAndConvert 64-instance FromBits SInt64 where fromBitsLE = checkAndConvert 64
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -64,7 +64,7 @@ -} -- | States the correctness of faster population-count algorithm, with respect--- to the reference slow version. Turns out Z3's default tactic is rather slow+-- to the reference slow version. Turns out Z3's default solver is rather slow -- for this one, but there's a magic incantation to make it go fast. -- See <https://github.com/Z3Prover/z3/issues/1150> for details. --
Data/SBV/Examples/Misc/Word4.hs view
@@ -138,10 +138,6 @@ -- | SIntegral instance, using default methods instance SIntegral Word4 --- | Conversion from bits-instance FromBits SWord4 where- fromBitsLE = checkAndConvert 4- -- | Joining/splitting to/from Word8 instance Splittable Word8 Word4 where split x = (Word4 (x `shiftR` 4), word4 x)
Data/SBV/Examples/Optimization/VM.hs view
@@ -13,7 +13,7 @@ import Data.SBV --- | The allocation problem. Inspired by: <http://rise4fun.com/z3opt/tutorialcontent/guide#h25>+-- | The allocation problem. Inspired by: <http://rise4fun.com/Z3/tutorialcontent/optimization#h25> -- -- - We have three virtual machines (VMs) which require 100, 50 and 15 GB hard disk respectively. --
Data/SBV/Examples/Queries/CaseSplit.hs view
@@ -6,7 +6,7 @@ -- Maintainer : erkokl@gmail.com -- Stability : experimental ----- A couple of demonstrations for the caseSplit tactic.+-- A couple of demonstrations for the 'caseSplit' function. ----------------------------------------------------------------------------- module Data.SBV.Examples.Queries.CaseSplit where
Data/SBV/Internals.hs view
@@ -22,7 +22,7 @@ , module Data.SBV.Core.Data -- * Operations useful for instantiating SBV type classes- , genLiteral, genFromCW, CW(..), genMkSymVar, checkAndConvert, genParse, showModel, SMTModel(..), liftQRem, liftDMod+ , genLiteral, genFromCW, CW(..), genMkSymVar, genParse, showModel, SMTModel(..), liftQRem, liftDMod -- * Compilation to C, extras , compileToC', compileToCLib'@@ -48,7 +48,6 @@ import Data.SBV.Core.Data import Data.SBV.Core.Model (genLiteral, genFromCW, genMkSymVar, liftQRem, liftDMod) import Data.SBV.Core.Symbolic (IStage(..))-import Data.SBV.Core.Splittable (checkAndConvert) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen
Data/SBV/SMT/SMT.hs view
@@ -62,7 +62,7 @@ import Data.SBV.Core.Data import Data.SBV.Core.Symbolic (SMTEngine, State(..)) -import Data.SBV.SMT.Utils (showTimeoutValue, alignPlain, alignDiagnostic, debug, mergeSExpr)+import Data.SBV.SMT.Utils (showTimeoutValue, alignPlain, alignDiagnostic, debug, mergeSExpr, SMTException(..)) import Data.SBV.Utils.PrettyNum import Data.SBV.Utils.Lib (joinArgs, splitArgs)@@ -489,7 +489,8 @@ Just execPath -> runSolver cfg ctx execPath opts pgm continuation `C.catches`- [ C.Handler (\(e :: C.ErrorCall) -> C.throw e)+ [ C.Handler (\(e :: SMTException) -> C.throwIO e)+ , C.Handler (\(e :: C.ErrorCall) -> C.throwIO e) , C.Handler (\(e :: C.SomeException) -> error $ unlines [ "Failed to start the external solver:\n" ++ show e , "Make sure you can start " ++ show execPath , "from the command line without issues."@@ -699,12 +700,12 @@ let isOption = "(set-option" `isPrefixOf` dropWhile isSpace l - reason | isOption = [ "*** Backend solver reports it does not support this option."- , "*** Check the spelling, and if correct please report this as a"- , "*** bug/feature request with the solver!"+ reason | isOption = [ "Backend solver reports it does not support this option."+ , "Check the spelling, and if correct please report this as a"+ , "bug/feature request with the solver!" ]- | True = [ "*** Failed to establish solver context. Running in debug mode might provide"- , "*** more information. Please report this as an issue!"+ | True = [ "Check solver response for further information. If your code is correct,"+ , "please report this as an issue either with SBV or the solver itself!" ] -- put a sync point here before we die so we consume everything@@ -719,22 +720,19 @@ let out = intercalate "\n" . lines $ outOrig err = intercalate "\n" . lines $ errOrig - error $ unlines $ [""- , "*** Data.SBV: Unexpected non-success response from " ++ nm ++ ":"- , "***"- , "*** Sent : " `alignDiagnostic` l- , "*** Expected : success"- , "*** Received : " `alignDiagnostic` (r ++ "\n" ++ extras)- ]- ++ [ "*** Stdout : " `alignDiagnostic` out | not $ null out]- ++ [ "*** Stderr : " `alignDiagnostic` err | not $ null err]- ++ [ "*** Exit code : " ++ show ex- , "***"- , "*** Executable: " ++ execPath- , "*** Options : " ++ joinArgs opts- , "***"- ]- ++ reason+ exc = SMTException { smtExceptionDescription = "Data.SBV: Unexpected non-success response from " ++ nm+ , smtExceptionSent = l+ , smtExceptionExpected = "success"+ , smtExceptionReceived = r ++ "\n" ++ extras+ , smtExceptionStdOut = out+ , smtExceptionStdErr = Just err+ , smtExceptionExitCode = Just ex+ , smtExceptionConfig = cfg { solver = (solver cfg) {executable = execPath } }+ , smtExceptionReason = Just reason+ , smtExceptionHint = Nothing+ }++ C.throwIO exc -- Mark in the log, mostly. sendAndGetSuccess Nothing "; Automatically generated by SBV. Do not edit."
Data/SBV/SMT/SMTLib2.hs view
@@ -52,7 +52,9 @@ , "*** Only one setOption call to 'SetLogic' is allowed, found: " ++ show (length ls) , "*** " ++ unwords (map show ls) ]- = ["(set-logic " ++ show l ++ ") ; NB. User specified."]+ = case l of+ Logic_NONE -> ["; NB. Not setting the logic per user request of Logic_NONE"]+ _ -> ["(set-logic " ++ show l ++ ") ; NB. User specified."] -- Otherwise, we try to determine the most suitable logic. -- NB. This isn't really fool proof!
Data/SBV/SMT/Utils.hs view
@@ -9,6 +9,8 @@ -- A few internally used types/routines ----------------------------------------------------------------------------- +{-# LANGUAGE NamedFieldPuns #-}+ module Data.SBV.SMT.Utils ( SMTLibConverter , SMTLibIncConverter@@ -18,14 +20,20 @@ , alignPlain , debug , mergeSExpr+ , SMTException(..) ) where +import qualified Control.Exception as C+ import Data.SBV.Core.Data+import Data.SBV.Utils.Lib (joinArgs) import Data.List (intercalate) import qualified Data.Set as Set (Set) +import System.Exit (ExitCode(..))+ -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.) type SMTLibConverter a = Set.Set Kind -- ^ Kinds used in the problem -> Bool -- ^ is this a sat problem?@@ -119,3 +127,65 @@ skipBar (_:cs) = skipBar cs skipBar [] = [] -- Oh dear, line finished, but the string didn't. We're in trouble. Ignore! +-- | An SMT exception generated by the back-end solver and is thrown from SBV. If the solver+-- ever responds with a non-success value for a command, SBV will throw an 'SMTException',+-- it so the user can process it as required. The provided 'Show' instance will render the failure+-- nicely. Note that if you ever catch this exception, the solver is no longer alive: You should either+-- throw the exception up, or do other proper clean-up before continuing.+data SMTException = SMTException {+ smtExceptionDescription :: String+ , smtExceptionSent :: String+ , smtExceptionExpected :: String+ , smtExceptionReceived :: String+ , smtExceptionStdOut :: String+ , smtExceptionStdErr :: Maybe String+ , smtExceptionExitCode :: Maybe ExitCode+ , smtExceptionConfig :: SMTConfig+ , smtExceptionReason :: Maybe [String]+ , smtExceptionHint :: Maybe [String]+ }++-- | SMTExceptions are throwable. A simple "show" will render this exception nicely+-- though of course you can inspect the individual fields as necessary.+instance C.Exception SMTException++-- | A fairly nice rendering of the exception, for display purposes.+instance Show SMTException where+ show SMTException { smtExceptionDescription+ , smtExceptionSent+ , smtExceptionExpected+ , smtExceptionReceived+ , smtExceptionStdOut+ , smtExceptionStdErr+ , smtExceptionExitCode+ , smtExceptionConfig+ , smtExceptionReason+ , smtExceptionHint+ }++ = let grp1 = [ ""+ , "*** " ++ smtExceptionDescription ++ ":"+ , "***"+ , "*** Sent : " `alignDiagnostic` smtExceptionSent+ , "*** Expected : " `alignDiagnostic` smtExceptionExpected+ , "*** Received : " `alignDiagnostic` smtExceptionReceived+ ]++ grp2 = ["*** Stdout : " `alignDiagnostic` smtExceptionStdOut | not $ null smtExceptionStdOut ]+ ++ ["*** Stderr : " `alignDiagnostic` err | Just err <- [smtExceptionStdErr], not $ null err]+ ++ ["*** Exit code : " `alignDiagnostic` show ec | Just ec <- [smtExceptionExitCode] ]+ ++ ["*** Executable: " `alignDiagnostic` executable (solver smtExceptionConfig) ]+ ++ ["*** Options : " `alignDiagnostic` joinArgs (options (solver smtExceptionConfig) smtExceptionConfig) ]++ grp3 = ["*** Reason : " `alignDiagnostic` unlines rsn | Just rsn <- [smtExceptionReason]]+ ++ ["*** Hint : " `alignDiagnostic` unlines hnt | Just hnt <- [smtExceptionHint ]]++ sep1+ | null grp2 = []+ | True = ["***"]++ sep2+ | null grp3 = []+ | True = ["***"]++ in unlines $ grp1 ++ sep1 ++ grp2 ++ sep2 ++ grp3
Data/SBV/Tools/Polynomial.hs view
@@ -26,7 +26,6 @@ import Data.SBV.Core.Data import Data.SBV.Core.Model-import Data.SBV.Core.Splittable import Data.SBV.Utils.Boolean @@ -134,7 +133,7 @@ -- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients. -- See the remarks for the 'pMult' function for this design choice-polyMult :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a+polyMult :: SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a polyMult (x, y, red) | isReal x = error $ "SBV.polyMult: Received a real value: " ++ show x@@ -149,7 +148,7 @@ mul _ [] ps = ps mul as (b:bs) ps = mul (false:as) bs (ites b (as `addPoly` ps) ps) -polyDivMod :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)+polyDivMod :: SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a) polyDivMod x y | isReal x = error $ "SBV.polyDivMod: Received a real value: " ++ show x@@ -240,7 +239,7 @@ -- | Compute CRC's over polynomials, i.e., symbolic words. The first -- 'Int' argument plays the same role as the one in the 'crcBV' function.-crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b+crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b crc n m p | isReal m || isReal p = error $ "SBV.crc: Received a real value: " ++ show (m, p)
Data/SBV/Tools/STree.hs view
@@ -17,8 +17,6 @@ module Data.SBV.Tools.STree (STree, readSTree, writeSTree, mkSTree) where -import Data.Bits (Bits(..))- import Data.SBV.Core.Data import Data.SBV.Core.Model @@ -43,7 +41,7 @@ -- | Reading a value. We bit-blast the index and descend down the full tree -- according to bit-values.-readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e+readSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e readSTree s i = walk (blastBE i) s where walk [] (SLeaf v) = v walk (b:bs) (SBin l r) = ite b (walk bs r) (walk bs l)@@ -51,7 +49,7 @@ -- | Writing a value, similar to how reads are done. The important thing is that the tree -- representation keeps updates to a minimum.-writeSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e+writeSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e writeSTree s i j = walk (blastBE i) s where walk [] _ = SLeaf j walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r)
LICENSE view
@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2017, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2018, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
README.md view
@@ -7,13 +7,13 @@ ### Build Status - Linux:- - GHC 8.0.1 [![Build1][3]][1]- - GHC 8.0.2 [![Build1][4]][1]- - GHC 8.2.1 [![Build1][5]][1]+ - GHC 8.0.2 [![Build1][3]][1]+ - GHC 8.2.1 [![Build1][4]][1]+ - GHC 8.2.2 [![Build1][5]][1] - Mac OSX: - GHC 8.2.1 [![Build1][6]][1] - Windows:- - GHC 8.0.2 [![Build5][7]][2]+ - GHC 8.2.2 [![Build5][7]][2] [1]: https://travis-ci.org/LeventErkok/sbv [2]: https://ci.appveyor.com/project/LeventErkok/sbv
+ SBVTestSuite/GoldFiles/exceptionLocal1.gold view
@@ -0,0 +1,68 @@+** Calling: yices-smt2 --incremental+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+** Backend solver Yices does not support global decls.+** Some incremental calls, such as pop, will be limited.+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_BV)+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] (define-fun s2 () (_ BitVec 1) #b0)+[GOOD] (define-fun s68 () (_ BitVec 32) #x00000001)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "x"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s1 () (_ BitVec 1) ((_ extract 0 0) s0))+[GOOD] (define-fun s3 () Bool (distinct s1 s2))+[GOOD] (define-fun s4 () Bool (not s3))+[GOOD] (define-fun s5 () (_ BitVec 32) (bvmul s0 s0))+[GOOD] (define-fun s6 () (_ BitVec 32) (bvmul s5 s5))+[GOOD] (define-fun s7 () (_ BitVec 32) (bvmul s6 s6))+[GOOD] (define-fun s8 () (_ BitVec 32) (bvmul s7 s7))+[GOOD] (define-fun s9 () (_ BitVec 32) (bvmul s8 s8))+[GOOD] (define-fun s10 () (_ BitVec 32) (bvmul s9 s9))+[GOOD] (define-fun s11 () (_ BitVec 32) (bvmul s10 s10))+[GOOD] (define-fun s12 () (_ BitVec 32) (bvmul s11 s11))+[GOOD] (define-fun s13 () (_ BitVec 32) (bvmul s12 s12))+[GOOD] (define-fun s14 () (_ BitVec 32) (bvmul s13 s13))+[GOOD] (define-fun s15 () (_ BitVec 32) (bvmul s14 s14))+[GOOD] (define-fun s16 () (_ BitVec 32) (bvmul s15 s15))+[GOOD] (define-fun s17 () (_ BitVec 32) (bvmul s16 s16))+[GOOD] (define-fun s18 () (_ BitVec 32) (bvmul s17 s17))+[GOOD] (define-fun s19 () (_ BitVec 32) (bvmul s18 s18))+[GOOD] (define-fun s20 () (_ BitVec 32) (bvmul s19 s19))+[GOOD] (define-fun s21 () (_ BitVec 32) (bvmul s20 s20))+[GOOD] (define-fun s22 () (_ BitVec 32) (bvmul s21 s21))+[GOOD] (define-fun s23 () (_ BitVec 32) (bvmul s22 s22))+[GOOD] (define-fun s24 () (_ BitVec 32) (bvmul s23 s23))+[GOOD] (define-fun s25 () (_ BitVec 32) (bvmul s24 s24))+[GOOD] (define-fun s26 () (_ BitVec 32) (bvmul s25 s25))+[GOOD] (define-fun s27 () (_ BitVec 32) (bvmul s26 s26))+[GOOD] (define-fun s28 () (_ BitVec 32) (bvmul s27 s27))+[GOOD] (define-fun s29 () (_ BitVec 32) (bvmul s28 s28))+[GOOD] (define-fun s30 () (_ BitVec 32) (bvmul s29 s29))+[GOOD] (define-fun s31 () (_ BitVec 32) (bvmul s30 s30))+[GOOD] (define-fun s32 () (_ BitVec 32) (bvmul s31 s31))+[GOOD] (define-fun s33 () (_ BitVec 32) (bvmul s32 s32))+[GOOD] (define-fun s34 () (_ BitVec 32) (bvmul s33 s33))+[FAIL] (define-fun s35 () (_ BitVec 32) (bvmul s34 s34))+CAUGHT SMT EXCEPTION+*** Data.SBV: Unexpected non-success response from Yices:+***+*** Sent : (define-fun s35 () (_ BitVec 32) (bvmul s34 s34))+*** Expected : success+*** Received : (error "at line 42, column 35: in bvmul: maximal polynomial degree exceeded")+***+*** Exit code : ExitSuccess+*** Executable: /usr/local/bin/yices-smt2+*** Options : --incremental+***+*** Reason : Check solver response for further information. If your code is correct,+*** please report this as an issue either with SBV or the solver itself!
+ SBVTestSuite/GoldFiles/exceptionLocal2.gold view
@@ -0,0 +1,28 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic QF_LIA) ; NB. User specified.+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] (define-fun s1 () Real (/ 2.0 1.0))+[GOOD] ; --- skolem constants ---+[FAIL] (declare-fun s0 () Real) ; tracks user variable "x"+CAUGHT SMT EXCEPTION+*** Data.SBV: Unexpected non-success response from Z3:+***+*** Sent : (declare-fun s0 () Real) ; tracks user variable "x"+*** Expected : success+*** Received : (error "line 10 column 23: logic does not support reals")+***+*** Exit code : ExitFailure (-15)+*** Executable: /usr/local/bin/z3+*** Options : -nw -in -smt2+***+*** Reason : Check solver response for further information. If your code is correct,+*** please report this as an issue either with SBV or the solver itself!
+ SBVTestSuite/GoldFiles/exceptionRemote1.gold view
@@ -0,0 +1,3 @@++FINAL: "OK, we got: Data.SBV: Unexpected response from the solver, context: assert"+DONE!
SBVTestSuite/GoldFiles/query1.gold view
@@ -76,7 +76,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version)-[RECV] (:version "4.5.1")+[RECV] (:version "4.6.1") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -107,7 +107,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.5.1")+[RECV] (:version "4.6.1") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)@@ -153,19 +153,19 @@ (declare-fun hey () Bool) (proof (let (($x215 (<= s0 6)))- (let (($x216 (not $x215)))- (let (($x223 (or (not bey) $x216)))- (let ((@x221 (monotonicity (rewrite (= (> s0 6) $x216)) (= (=> bey (> s0 6)) (=> bey $x216)))))- (let ((@x227 (trans @x221 (rewrite (= (=> bey $x216) $x223)) (= (=> bey (> s0 6)) $x223))))- (let ((@x228 (mp (asserted (=> bey (> s0 6))) @x227 $x223)))- (let (($x240 (>= s0 6)))- (let (($x239 (not $x240)))- (let (($x249 (or (not hey) $x239)))- (let ((@x242 (monotonicity (rewrite (= (<= 6 s0) $x240)) (= (not (<= 6 s0)) $x239))))- (let ((@x244 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) @x242 (= (< s0 6) $x239))))- (let ((@x253 (trans (monotonicity @x244 (= (=> hey (< s0 6)) (=> hey $x239))) (rewrite (= (=> hey $x239) $x249)) (= (=> hey (< s0 6)) $x249))))- (let ((@x254 (mp (asserted (=> hey (< s0 6))) @x253 $x249)))- (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x240 $x215)) (unit-resolution @x254 (asserted hey) $x239) (unit-resolution @x228 (asserted bey) $x216) false))))))))))))))))+ (let (($x216 (not $x215)))+ (let (($x223 (or (not bey) $x216)))+ (let ((@x221 (monotonicity (rewrite (= (> s0 6) $x216)) (= (=> bey (> s0 6)) (=> bey $x216)))))+ (let ((@x227 (trans @x221 (rewrite (= (=> bey $x216) $x223)) (= (=> bey (> s0 6)) $x223))))+ (let ((@x228 (mp (asserted (=> bey (> s0 6))) @x227 $x223)))+ (let (($x240 (>= s0 6)))+ (let (($x239 (not $x240)))+ (let (($x249 (or (not hey) $x239)))+ (let ((@x242 (monotonicity (rewrite (= (<= 6 s0) $x240)) (= (not (<= 6 s0)) $x239))))+ (let ((@x244 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) @x242 (= (< s0 6) $x239))))+ (let ((@x253 (trans (monotonicity @x244 (= (=> hey (< s0 6)) (=> hey $x239))) (rewrite (= (=> hey $x239) $x249)) (= (=> hey (< s0 6)) $x249))))+ (let ((@x254 (mp (asserted (=> hey (< s0 6))) @x253 $x249)))+ (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x240 $x215)) (unit-resolution @x254 (asserted hey) $x239) (unit-resolution @x228 (asserted bey) $x216) false)))))))))))))))) [SEND, TimeOut: 90000ms] (get-assertions) [RECV] ((! s7 :named |a > 0|)
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -7,7 +7,6 @@ [FAIL] (set-option :there-is-no-such-option bad argument) - *** Data.SBV: Unexpected non-success response from Z3: *** *** Sent : (set-option :there-is-no-such-option bad argument)@@ -34,13 +33,11 @@ *** verbose (unsigned int) (default: 0) *** warning (bool) (default: true) *** well_sorted_check (bool) (default: false)")-*** Exit code : ExitFailure (-15) ***+*** Exit code : ExitFailure (-15) *** Executable: /usr/local/bin/z3 *** Options : -nw -in -smt2 ***-*** Backend solver reports it does not support this option.-*** Check the spelling, and if correct please report this as a-*** bug/feature request with the solver!--CallStack (from HasCallStack):+*** Reason : Backend solver reports it does not support this option.+*** Check the spelling, and if correct please report this as a+*** bug/feature request with the solver!
SBVTestSuite/GoldFiles/temperature.gold view
@@ -1,5 +1,1 @@-Solution #1:- s0 = 16 :: Integer-Solution #2:- s0 = 28 :: Integer-Found 2 different solutions.+[("s0",16 :: Integer),("s0",28 :: Integer)]
SBVTestSuite/SBVTest.hs view
@@ -13,6 +13,7 @@ import qualified TestSuite.Basics.ArithNoSolver import qualified TestSuite.Basics.ArithSolver import qualified TestSuite.Basics.BasicTests+import qualified TestSuite.Basics.Exceptions import qualified TestSuite.Basics.GenBenchmark import qualified TestSuite.Basics.Higher import qualified TestSuite.Basics.Index@@ -113,7 +114,8 @@ -- | The following tests can only be run locally localOnlyTests :: TestTree localOnlyTests = testGroup "SBVLocalOnlyTests" [- TestSuite.Queries.BasicQuery.tests+ TestSuite.Basics.Exceptions.testsLocal+ , TestSuite.Queries.BasicQuery.tests , TestSuite.Queries.BadOption.tests , TestSuite.Queries.Int_ABC.tests , TestSuite.Queries.Int_Boolector.tests@@ -130,6 +132,7 @@ , TestSuite.Basics.AllSat.tests , TestSuite.Basics.ArithNoSolver.tests , TestSuite.Basics.BasicTests.tests+ , TestSuite.Basics.Exceptions.testsRemote , TestSuite.Basics.GenBenchmark.tests , TestSuite.Basics.Higher.tests , TestSuite.Basics.Index.tests
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -60,6 +60,7 @@ ++ genShiftRotTest "rotateR_gen" sRotateRight ++ genShiftMixSize ++ genBlasts+ ++ genCounts ++ genIntCasts genBinTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]@@ -188,6 +189,26 @@ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s] ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s] where mkTest (x, r) = testCase ("blast-" ++ x) (r `showsAs` "True")++genCounts :: [TestTree]+genCounts = map mkTest $+ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord8 )) | x <- sw8s ]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord8 )) | x <- sw8s ]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt8 )) | x <- si8s ]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt8 )) | x <- si8s ]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord16)) | x <- sw16s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord16)) | x <- sw16s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt16 )) | x <- si16s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt16 )) | x <- si16s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord32)) | x <- sw32s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord32)) | x <- sw32s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt32 )) | x <- si32s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt32 )) | x <- si32s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SWord64)) | x <- sw64s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SWord64)) | x <- sw64s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsBE (blastLE x) :: SInt64 )) | x <- si64s]+ ++ [(show x, sCountTrailingZeros x .== sCountLeadingZeros (fromBitsLE (blastBE x) :: SInt64 )) | x <- si64s]+ where mkTest (x, r) = testCase ("count-" ++ x) (r `showsAs` "True") genIntCasts :: [TestTree] genIntCasts = map mkTest $ cast w8s ++ cast w16s ++ cast w32s ++ cast w64s
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -61,6 +61,7 @@ ++ genShiftRotTest "rotateR_gen" sRotateRight ++ genShiftMixSize ++ genBlasts+ ++ genCounts ++ genIntCasts) genBinTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [TestTree]@@ -208,6 +209,28 @@ mkThm from to v = isTheorem $ do a <- free "x" constrain $ a .== literal v return $ a .== from (to a)++genCounts :: [TestTree]+genCounts = map mkTest $ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord8 ) blastBE x) | x <- w8s ]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord8 ) blastLE x) | x <- w8s ]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt8 ) blastBE x) | x <- i8s ]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt8 ) blastLE x) | x <- i8s ]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord16) blastBE x) | x <- w16s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord16) blastLE x) | x <- w16s]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt16 ) blastBE x) | x <- i16s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt16 ) blastLE x) | x <- i16s]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord32) blastBE x) | x <- w32s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord32) blastLE x) | x <- w32s]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt32 ) blastBE x) | x <- i32s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt32 ) blastLE x) | x <- i32s]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SWord64) blastBE x) | x <- w64s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SWord64) blastLE x) | x <- w64s]+ ++ [(show x, mkThm (fromBitsLE :: [SBool] -> SInt64 ) blastBE x) | x <- i64s]+ ++ [(show x, mkThm (fromBitsBE :: [SBool] -> SInt64 ) blastLE x) | x <- i64s]+ where mkTest (x, t) = testCase ("genCounts.count-" ++ show x) (assert t)+ mkThm from to v = isTheorem $ do a <- free "x"+ constrain $ a .== literal v+ return $ sCountTrailingZeros a .== sCountLeadingZeros (from (to a)) genIntCasts :: [TestTree] genIntCasts = map mkTest $ cast w8s ++ cast w16s ++ cast w32s ++ cast w64s
+ SBVTestSuite/TestSuite/Basics/Exceptions.hs view
@@ -0,0 +1,67 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.Exceptions+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test the exception mechanism+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module TestSuite.Basics.Exceptions(testsLocal, testsRemote) where++import Data.SBV.Control+import Utils.SBVTestFramework++import qualified Control.Exception as C++-- Test suite+testsLocal :: TestTree+testsLocal =+ testGroup "Basics.exceptions.local"+ [ goldenCapturedIO "exceptionLocal1" yicesExc+ , goldenCapturedIO "exceptionLocal2" z3Exc1+ ]++-- Yices throws an exception for this since exponent is too large+yicesExc :: FilePath -> IO ()+yicesExc rf = runSMTWith yices{verbose=True, redirectVerbose=Just rf} exc+ `C.catch` \(e :: SMTException) -> do appendFile rf "CAUGHT SMT EXCEPTION"+ appendFile rf (show e)+ where exc = do x <- sWord32 "x"+ constrain $ lsb x ==> (x * (x .^ (-1::SWord32))) .== 1+ query $ do cs <- checkSat+ cs `seq` return ()++testsRemote :: TestTree+testsRemote =+ testGroup "Basics.exceptions.remote"+ [ goldenCapturedIO "exceptionRemote1" z3Exc2+ ]++-- Create the case where we ask for integer-logic, but use reals+z3Exc1 :: FilePath -> IO ()+z3Exc1 rf = runSMTWith z3{verbose=True, redirectVerbose=Just rf} exc+ `C.catch` \(e :: SMTException) -> do appendFile rf "CAUGHT SMT EXCEPTION"+ appendFile rf (show e)+ where exc = do setLogic QF_LIA+ x <- sReal "x"+ constrain $ x .== 2+ query $ do cs <- checkSat+ cs `seq` return ()++-- Similar to above, except linear logic, but use non-linear constructs+z3Exc2 :: FilePath -> IO ()+z3Exc2 rf = do r <- runSMT z3ExcCatch `C.catch` \(e :: SMTException) -> return ("OK, we got: " ++ smtExceptionDescription e)+ appendFile rf ("\nFINAL: " ++ show r ++ "\nDONE!\n")+ where z3ExcCatch = do setLogic QF_LIA+ x <- sInteger "x"+ y <- sInteger "y"+ query $ do constrain $ x*y .== x*x+ cs <- checkSat+ return $ show cs++{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
SBVTestSuite/TestSuite/Puzzles/Temperature.hs view
@@ -13,12 +13,16 @@ import Utils.SBVTestFramework +import Data.List (sort)+import qualified Data.Map as M+ -- Test suite tests :: TestTree tests = testGroup "Puzzles.Temperature"- [ goldenVsStringShow "temperature" (allSat (revOf `fmap` exists_))+ [ goldenVsStringShow "temperature" result ]+ where result = (sort . concatMap M.toList . getModelDictionaries) `fmap` allSat (revOf `fmap` exists_) type Temp = SInteger
SBVTestSuite/TestSuite/Queries/BadOption.hs view
@@ -23,7 +23,7 @@ testGroup "Basics.QueryIndividual" [ goldenCapturedIO "query_badOption" $ \rf -> runSMTWith z3{verbose=True, redirectVerbose=Just rf} q `C.catch`- (\(e::C.SomeException) -> appendFile rf ("\n\n" ++ unlines (init (lines (show e)))))+ (\(e::C.SomeException) -> appendFile rf ("\n" ++ show e)) ] q :: Symbolic ()
SBVTestSuite/Utils/SBVTestFramework.hs view
@@ -15,7 +15,7 @@ module Utils.SBVTestFramework ( showsAs , runSAT, numberOfModels- , assertIsThm, assertIsntThm, assertIsSat, assertIsntSat+ , assert, assertIsThm, assertIsntThm, assertIsSat, assertIsntSat , goldenString , goldenVsStringShow , goldenCapturedIO@@ -35,8 +35,8 @@ import System.Directory (removeFile) import System.Environment (lookupEnv) -import Test.Tasty (testGroup, TestTree, TestName)-import Test.Tasty.HUnit (assert, Assertion, testCase)+import Test.Tasty (testGroup, TestTree, TestName)+import Test.Tasty.HUnit ((@?), Assertion, testCase, AssertionPredicable) import Test.Tasty.Golden (goldenVsString) import Test.Tasty.Golden.Advanced (goldenTest)@@ -86,6 +86,10 @@ Nothing -> return 100 return (env, perc)++-- | Generic assertion. This is less safe than usual, but will do.+assert :: AssertionPredicable t => t -> Assertion+assert t = t @? "assertion-failure" -- | Checks that a particular result shows as @s@ showsAs :: Show a => a -> String -> Assertion
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 7.4+Version: 7.5 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@@ -7,7 +7,7 @@ . For details, please see: <http://leventerkok.github.com/sbv/> -Copyright: Levent Erkok, 2010-2017+Copyright: Levent Erkok, 2010-2018 License: BSD3 License-file: LICENSE Stability: Experimental@@ -48,10 +48,7 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4.9 && < 5- , ghc- , QuickCheck >= 2.9.2- , crackNum >= 1.9- , template-haskell >= 2.11+ , ghc, QuickCheck, crackNum, template-haskell , array, async, containers, deepseq, directory, filepath, time , pretty, process, mtl, random, syb, data-binary-ieee754 , generic-deriving@@ -155,12 +152,8 @@ , Rank2Types , ScopedTypeVariables Build-depends : base >= 4.9, data-binary-ieee754, filepath, syb- , sbv, directory, random, mtl- , template-haskell >= 2.11- , bytestring >= 0.9- , tasty >= 0.11.2.3- , tasty-golden >= 2.3.1.1- , tasty-hunit >= 0.9.2+ , sbv, directory, random, mtl, containers+ , template-haskell, bytestring, tasty, tasty-golden, tasty-hunit Hs-Source-Dirs : SBVTestSuite main-is : SBVTest.hs Other-modules : Utils.SBVTestFramework@@ -170,6 +163,7 @@ , TestSuite.Basics.ArithNoSolver , TestSuite.Basics.ArithSolver , TestSuite.Basics.BasicTests+ , TestSuite.Basics.Exceptions , TestSuite.Basics.GenBenchmark , TestSuite.Basics.Higher , TestSuite.Basics.Index@@ -240,12 +234,7 @@ Test-Suite SBVDocTest Build-Depends: base, directory, filepath, random- , doctest >= 0.13- , Glob >= 0.7- , bytestring >= 0.9- , tasty >= 0.11.2.3- , tasty-golden >= 2.3.1.1- , tasty-hunit >= 0.9.2+ , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit , sbv default-language: Haskell2010 Hs-Source-Dirs : SBVTestSuite@@ -255,11 +244,7 @@ Test-Suite SBVHLint build-depends: base, directory, filepath, random- , hlint >= 2.0.9- , bytestring >= 0.9- , tasty >= 0.11.2.3- , tasty-golden >= 2.3.1.1- , tasty-hunit >= 0.9.2+ , hlint, bytestring, tasty, tasty-golden, tasty-hunit , sbv default-language: Haskell2010 hs-source-dirs: SBVTestSuite