sbv 7.1 → 7.2
raw patch · 50 files changed
+1648/−1163 lines, 50 filesdep ~doctest
Dependency ranges changed: doctest
Files
- CHANGES.md +25/−1
- Data/SBV.hs +3/−0
- Data/SBV/Compilers/C.hs +12/−12
- Data/SBV/Control/Utils.hs +32/−11
- Data/SBV/Core/Model.hs +20/−51
- Data/SBV/Core/Operations.hs +143/−48
- Data/SBV/Core/Symbolic.hs +72/−51
- Data/SBV/Examples/CodeGeneration/PopulationCount.hs +29/−29
- Data/SBV/Provers/Prover.hs +49/−15
- Data/SBV/Provers/Z3.hs +1/−12
- Data/SBV/SMT/SMTLib.hs +1/−1
- Data/SBV/SMT/SMTLib2.hs +26/−21
- Data/SBV/SMT/Utils.hs +14/−14
- README.md +18/−9
- SBVTestSuite/GoldFiles/crcUSB5_2.gold +132/−132
- SBVTestSuite/GoldFiles/noTravis_query1.gold +0/−193
- SBVTestSuite/GoldFiles/noTravis_query_abc.gold +0/−34
- SBVTestSuite/GoldFiles/noTravis_query_boolector.gold +0/−54
- SBVTestSuite/GoldFiles/noTravis_query_cvc4.gold +0/−60
- SBVTestSuite/GoldFiles/noTravis_query_mathsat.gold +0/−55
- SBVTestSuite/GoldFiles/noTravis_query_yices.gold +0/−54
- SBVTestSuite/GoldFiles/optQuant1.gold +5/−0
- SBVTestSuite/GoldFiles/optQuant2.gold +5/−0
- SBVTestSuite/GoldFiles/optQuant3.gold +5/−0
- SBVTestSuite/GoldFiles/optQuant4.gold +5/−0
- SBVTestSuite/GoldFiles/optQuant5.gold +5/−0
- SBVTestSuite/GoldFiles/popCount1.gold +29/−29
- SBVTestSuite/GoldFiles/popCount2.gold +29/−29
- SBVTestSuite/GoldFiles/query1.gold +193/−0
- SBVTestSuite/GoldFiles/query_abc.gold +34/−0
- SBVTestSuite/GoldFiles/query_badOption.gold +1/−1
- SBVTestSuite/GoldFiles/query_boolector.gold +54/−0
- SBVTestSuite/GoldFiles/query_cvc4.gold +60/−0
- SBVTestSuite/GoldFiles/query_mathsat.gold +55/−0
- SBVTestSuite/GoldFiles/query_yices.gold +54/−0
- SBVTestSuite/SBVDocTest.hs +20/−7
- SBVTestSuite/SBVHLint.hs +5/−5
- SBVTestSuite/SBVTest.hs +103/−90
- SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +97/−58
- SBVTestSuite/TestSuite/Basics/ArithSolver.hs +103/−58
- SBVTestSuite/TestSuite/Basics/SmallShifts.hs +60/−0
- SBVTestSuite/TestSuite/Optimization/Quantified.hs +81/−0
- SBVTestSuite/TestSuite/Queries/BasicQuery.hs +3/−3
- SBVTestSuite/TestSuite/Queries/Int_ABC.hs +1/−1
- SBVTestSuite/TestSuite/Queries/Int_Boolector.hs +1/−1
- SBVTestSuite/TestSuite/Queries/Int_CVC4.hs +1/−1
- SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs +1/−1
- SBVTestSuite/TestSuite/Queries/Int_Yices.hs +1/−1
- SBVTestSuite/Utils/SBVTestFramework.hs +56/−19
- sbv.cabal +4/−2
CHANGES.md view
@@ -1,7 +1,31 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.1, 2017-07-29+* Latest Hackage released version: 7.2, 2017-08-29++### Version 7.2, 2017-08-29++ * Reworked implementation of shifts and rotates: When a signed quantity was+ being shifted right by more than its size, SBV used to return 0. Robert Dockins pointed+ out that the correct answer is actually -1 in such cases. The new implementation+ merges the dynamic and typed interfaces, and drops support for non-constant shifts+ 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+ prefix-existentials. This allows for better (smaller) quantified code, while+ preserving semantics.++ * Rework the interaction between quantifiers and optimization routines.+ Optimization routines now properly handle quantified formulas, so long as the+ quantified metric does not involve any universal quantification itself. Thanks+ to Matthew Danish for reporting the issue.+ + * Development/Infrastructure: Lots of work around the continuous integration+ for SBV. We now build/test on Linux/Mac/Windows on every commit. Thanks to+ Travis/Appveyor for providing free remote infrastructure. There are still+ gotchas and some reductions in tests due to host capacity issues. If you+ would like to be involved and improve the test suite, please get in touch! ### Version 7.1, 2017-07-29
Data/SBV.hs view
@@ -98,6 +98,9 @@ -- -- * Z3 from Microsoft: <http://github.com/Z3Prover/z3/wiki> --+-- SBV requires recent versions of these solvers; please see the file+-- @SMTSolverVersions.md@ in the source distribution for specifics.+-- -- SBV also allows calling these solvers in parallel, either getting results from multiple solvers -- or returning the fastest one. (See 'proveWithAll', 'proveWithAny', etc.) --
Data/SBV/Compilers/C.hs view
@@ -418,7 +418,7 @@ = tbd "Explicit constraints" | not (null arrs) = tbd "User specified arrays"- | needsExistentials (map fst ins)+ | needsExistentials (map fst (fst ins)) = error "SBV->C: Cannot compile functions with existentially quantified variables." | True = [pre, header, post]@@ -455,7 +455,7 @@ $$ vcat (map text ls) $$ text "" - typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, (s, _)) <- ins]+ typeWidth = getMax 0 $ [len (kindOf s) | (s, _) <- assignments] ++ [len (kindOf s) | (_, (s, _)) <- fst ins] where len KReal{} = 5 len KFloat{} = 6 -- SFloat len KDouble{} = 7 -- SDouble@@ -662,6 +662,12 @@ , (And, "&"), (Or, "|"), (XOr, "^") ] + -- see if we can find a constant shift; makes the output way more readable+ getShiftAmnt def [_, sw] = case sw `lookup` consts of+ Just (CW _ (CWInteger i)) -> integer i+ _ -> def+ getShiftAmnt def _ = def+ p :: Op -> [Doc] -> Doc p (ArrRead _) _ = tbd "User specified arrays (ArrRead)" p (ArrEq _ _) _ = tbd "User specified arrays (ArrEq)"@@ -675,8 +681,8 @@ p Join [a, b] = join (let (s1 : s2 : _) = opArgs in (s1, s2, a, b)) p (Rol i) [a] = rotate True i a (head opArgs) p (Ror i) [a] = rotate False i a (head opArgs)- p (Shl i) [a] = shift True i a (head opArgs)- p (Shr i) [a] = shift False i a (head opArgs)+ p Shl [a, i] = shift True (getShiftAmnt i opArgs) a -- The order of i/a being reversed here is+ p Shr [a, i] = shift False (getShiftAmnt i opArgs) a -- intentional and historical (from the days when Shl/Shr had a constant parameter.) p Not [a] = case kindOf (head opArgs) of -- be careful about booleans, bitwise complement is not correct for them! KBool -> text "!" <> a@@ -749,13 +755,7 @@ where res = a <+> text divOp <+> b wrap = parens (b <+> text "== 0") <+> text "?" <+> def <+> text ":" <+> parens res - shift toLeft i a s- | i < 0 = shift (not toLeft) (-i) a s- | i == 0 = a- | True = case kindOf s of- KBounded _ sz | i >= sz -> mkConst cfg $ mkConstCW (kindOf s) (0::Integer)- KReal -> tbd $ "Shift for real quantity: " ++ show (toLeft, i, s)- _ -> a <+> text cop <+> int i+ shift toLeft i a = a <+> text cop <+> i where cop | toLeft = "<<" | True = ">>" @@ -768,7 +768,7 @@ KBounded False sz -> parens (a <+> text cop <+> int i) <+> text "|" <+> parens (a <+> text cop' <+> int (sz - i))- KUnbounded -> shift toLeft i a s -- For SInteger, rotate is the same as shift in Haskell+ KUnbounded -> shift toLeft (int i) a -- For SInteger, rotate is the same as shift in Haskell _ -> tbd $ "Rotation for unbounded quantity: " ++ show (toLeft, i, s) where (cop, cop') | toLeft = ("<<", ">>") | True = (">>", "<<")
Data/SBV/Control/Utils.hs view
@@ -9,17 +9,18 @@ -- Query related utils. ----------------------------------------------------------------------------- -{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.Control.Utils ( io , ask, send, getValue, getUninterpretedValue, getValueCW, getUnsatAssumptions, SMTValue(..)- , getQueryState, modifyQueryState, getConfig, getObjectives, getSBVAssertions, getQuantifiedInputs+ , getQueryState, modifyQueryState, getConfig, getObjectives, getSBVAssertions, getSBVPgm, getQuantifiedInputs , checkSat, checkSatUsing, getAllSatResult , inNewContext, freshVar, freshVar_ , parse@@ -32,6 +33,7 @@ import Data.List (sortBy, elemIndex, partition, groupBy, tails) +import Data.Char (isPunctuation, isSpace) import Data.Ord (comparing) import Data.Function (on) @@ -53,7 +55,7 @@ , QueryState(..), SVal(..), Quantifier(..), cache , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..) , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities- , Result(..), SMTProblem(..), trueSW, SymWord(..)+ , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..) ) import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar) @@ -101,6 +103,11 @@ getObjectives = do State{rOptGoals} <- get io $ reverse <$> readIORef rOptGoals +-- | Get the program+getSBVPgm :: Query SBVPgm+getSBVPgm = do State{spgm} <- get+ io $ readIORef spgm+ -- | Get the assertions put in via 'sAssert' getSBVAssertions :: Query [(String, Maybe CallStack, SW)] getSBVAssertions = do State{rAsserts} <- get@@ -201,8 +208,14 @@ _ -> do case queryTimeOutValue of Nothing -> queryDebug ["[FAIL] " `alignPlain` s] Just i -> queryDebug [("[FAIL, TimeOut: " ++ showTimeoutValue i ++ "] ") `alignPlain` s]- unexpected "Command" s "success" Nothing r Nothing ++ let cmd = case words (dropWhile (\c -> isSpace c || isPunctuation c) s) of+ (c:_) -> c+ _ -> "Command"++ unexpected cmd s "success" Nothing r Nothing+ else io $ querySend queryTimeOutValue s -- fire and forget. if you use this, you're on your own! -- | Retrieve a responses from the solver until it produces a synchronization tag. We make the tag@@ -385,11 +398,19 @@ ECon "unknown" -> return Unk _ -> bad r Nothing --- | What are the top level inputs?+-- | What are the top level inputs? Trackers are returned as top level existentials getQuantifiedInputs :: Query [(Quantifier, NamedSymVar)] getQuantifiedInputs = do State{rinps} <- get- liftIO $ reverse <$> readIORef rinps+ (rQinps, rTrackers) <- liftIO $ readIORef rinps + let qinps = reverse rQinps+ trackers = map (EX,) $ reverse rTrackers++ -- separate the existential prefix, which will go first+ (preQs, postQs) = span (\(q, _) -> q == EX) qinps++ return $ preQs ++ trackers ++ postQs+ -- | Repeatedly issue check-sat, after refuting the previous model. -- The bool is true if the model is unique upto prefix existentials. getAllSatResult :: Query (Bool, Bool, [SMTResult])@@ -583,7 +604,7 @@ go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar) go ((EX, (v, _)):rest) (us, sofar) = go rest (us, Right (v, reverse us) : sofar) - qinps = if isSat then is else map flipQ is+ qinps = if isSat then fst is else map flipQ (fst is) skolemMap = skolemize qinps o = case outputs of
Data/SBV/Core/Model.hs view
@@ -9,7 +9,6 @@ -- Instance declarations for our symbolic world ----------------------------------------------------------------------------- -{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE PatternGuards #-}@@ -21,6 +20,12 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DefaultSignatures #-} +-- Keep GHC quiet.. I wish we can be more specific on these as opposed to module+-- level turning of redundant-constraints. Note that his is not needed >= GHC 8.0.2+-- since they removed this constraint from -Wall, see: https://ghc.haskell.org/trac/ghc/ticket/10635+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# 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@@ -527,8 +532,7 @@ -- It is similar to the standard 'Integral' class, except ranging over symbolic instances. class (SymWord a, Num a, Bits a) => SIntegral a --- 'SIntegral' Instances, including all possible variants except 'Bool', since booleans--- are not numbers.+-- 'SIntegral' Instances, skips Real/Float/Bool instance SIntegral Word8 instance SIntegral Word16 instance SIntegral Word32@@ -818,35 +822,28 @@ y st = do xsw <- sbvToSW st x newExpr st kTo (SBVApp (KindCast kFrom kTo) [xsw]) +-- | Lift a binary operation thru it's dynamic counterpart. Note that+-- we still want the actual functions here as differ in their type+-- compared to their dynamic counterparts, but the implementations+-- are the same.+liftViaSVal :: (SVal -> SVal -> SVal) -> SBV a -> SBV b -> SBV c+liftViaSVal f (SBV a) (SBV b) = SBV $ f a b+ -- | Generalization of 'shiftL', when the shift-amount is symbolic. Since Haskell's -- 'shiftL' only takes an 'Int' as the shift amount, it cannot be used when we have--- a symbolic amount to shift with. The first argument should be a bounded quantity.+-- a symbolic amount to shift with. sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a-sShiftLeft x i- | not (isBounded x)- = 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))- (select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z i )- where z = genLiteral (kindOf x) (0::Integer)+sShiftLeft = liftViaSVal svShiftLeft -- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's -- 'shiftR' only takes an 'Int' as the shift amount, it cannot be used when we have--- a symbolic amount to shift with. The first argument should be a bounded quantity.+-- a symbolic amount to shift with. -- -- NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, -- following the usual Haskell convention. See 'sSignedShiftArithRight' for a variant -- that explicitly uses the msb as the sign bit, even for unsigned underlying types. sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a-sShiftRight x i- | not (isBounded x)- = 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))- (select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z i )- where z = genLiteral (kindOf x) (0::Integer)+sShiftRight = liftViaSVal svShiftRight -- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent -- to 'sShiftRight' when the argument is signed. However, if the argument is unsigned,@@ -865,41 +862,13 @@ -- 'rotateL' only takes an 'Int' as the shift amount, it cannot be used when we have -- a symbolic amount to shift with. The first argument should be a bounded quantity. sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a-sRotateLeft x i- | not (isBounded x)- = sShiftLeft x i- | isBounded i && bit si <= toInteger sx -- wrap-around not possible- = ite (i .< 0)- (select [x `rotateR` k | k <- [0 .. bit si - 1]] z (-i))- (select [x `rotateL` k | k <- [0 .. bit si - 1]] z i )- | True- = ite (i .< 0)- (select [x `rotateR` k | k <- [0 .. sx - 1]] z ((-i) `sRem` n))- (select [x `rotateL` k | k <- [0 .. sx - 1]] z ( i `sRem` n))- where sx = ghcBitSize x- si = ghcBitSize i- z = genLiteral (kindOf x) (0::Integer)- n = genLiteral (kindOf i) (toInteger sx)+sRotateLeft = liftViaSVal svRotateLeft -- | Generalization of 'rotateR', when the shift-amount is symbolic. Since Haskell's -- 'rotateR' only takes an 'Int' as the shift amount, it cannot be used when we have -- 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 x i- | not (isBounded x)- = sShiftRight x i- | isBounded i && bit si <= toInteger sx -- wrap-around not possible- = ite (i .< 0)- (select [x `rotateL` k | k <- [0 .. bit si - 1]] z (-i))- (select [x `rotateR` k | k <- [0 .. bit si - 1]] z i)- | True- = ite (i .< 0)- (select [x `rotateL` k | k <- [0 .. sx - 1]] z ((-i) `sRem` n))- (select [x `rotateR` k | k <- [0 .. sx - 1]] z ( i `sRem` n))- where sx = ghcBitSize x- si = ghcBitSize i- z = genLiteral (kindOf x) (0::Integer)- n = genLiteral (kindOf i) (toInteger sx)+sRotateRight = liftViaSVal svRotateRight -- | Full adder. Returns the carry-out from the addition. --
Data/SBV/Core/Operations.hs view
@@ -152,9 +152,9 @@ -- | Division. svDivide :: SVal -> SVal -> SVal-svDivide = liftSym2 (mkSymOp Quot) rationalCheck (/) die (/) (/)- where -- should never happen- die = error "impossible: integer valued data found in Fractional instance"+svDivide = liftSym2 (mkSymOp Quot) rationalCheck (/) idiv (/) (/)+ where idiv x 0 = x+ idiv x y = x `div` y -- | Exponentiation. svExp :: SVal -> SVal -> SVal@@ -344,44 +344,54 @@ -- operation in SMT-Lib. svShl :: SVal -> Int -> SVal svShl x i- | i < 0 = svShr x (-i)- | i == 0 = x- | True = liftSym1 (mkSymOp1 (Shl i))- (noRealUnary "shiftL") (`shiftL` i)- (noFloatUnary "shiftL") (noDoubleUnary "shiftL") x+ | i <= 0+ = x+ | isBounded x, i >= intSizeOf x+ = svInteger k 0+ | True+ = x `svShiftLeft` svInteger k (fromIntegral i)+ where k = kindOf x -- | Shift right by a constant amount. Translates to either "bvlshr" -- (logical shift right) or "bvashr" (arithmetic shift right) in -- SMT-Lib, depending on whether @x@ is a signed bitvector. svShr :: SVal -> Int -> SVal svShr x i- | i < 0 = svShl x (-i)- | i == 0 = x- | True = liftSym1 (mkSymOp1 (Shr i))- (noRealUnary "shiftR") (`shiftR` i)- (noFloatUnary "shiftR") (noDoubleUnary "shiftR") x+ | i <= 0+ = x+ | isBounded x, i >= intSizeOf x+ = if not (hasSign x)+ then z+ else svIte (x `svLessThan` z) neg1 z+ | True+ = x `svShiftRight` svInteger k (fromIntegral i)+ where k = kindOf x+ z = svInteger k 0+ neg1 = svInteger k (-1) -- | Rotate-left, by a constant svRol :: SVal -> Int -> SVal svRol x i- | i < 0 = svRor x (-i)- | i == 0 = x- | True = case kindOf x of- KBounded _ sz -> liftSym1 (mkSymOp1 (Rol (i `mod` sz)))- (noRealUnary "rotateL") (rot True sz i)- (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x- _ -> svShl x i -- for unbounded Integers, rotateL is the same as shiftL in Haskell+ | i <= 0+ = x+ | True+ = case kindOf x of+ KBounded _ sz -> liftSym1 (mkSymOp1 (Rol (i `mod` sz)))+ (noRealUnary "rotateL") (rot True sz i)+ (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x+ _ -> svShl x i -- for unbounded Integers, rotateL is the same as shiftL in Haskell -- | Rotate-right, by a constant svRor :: SVal -> Int -> SVal svRor x i- | i < 0 = svRol x (-i)- | i == 0 = x- | True = case kindOf x of- KBounded _ sz -> liftSym1 (mkSymOp1 (Ror (i `mod` sz)))- (noRealUnary "rotateR") (rot False sz i)- (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x- _ -> svShr x i -- for unbounded integers, rotateR is the same as shiftR in Haskell+ | i <= 0+ = x+ | True+ = case kindOf x of+ KBounded _ sz -> liftSym1 (mkSymOp1 (Ror (i `mod` sz)))+ (noRealUnary "rotateR") (rot False sz i)+ (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x+ _ -> svShr x i -- for unbounded integers, rotateR is the same as shiftR in Haskell -- | Generic rotation. Since the underlying representation is just Integers, rotations has to be -- careful on the bit-size.@@ -611,36 +621,121 @@ | True = svFalse -- | Generalization of 'svShl', where the shift-amount is symbolic.--- The first argument should be a bounded quantity. svShiftLeft :: SVal -> SVal -> SVal-svShiftLeft x i- | not (isBounded x)- = 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))- (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z i)- where z = svInteger (kindOf x) 0- zi = svInteger (kindOf i) 0+svShiftLeft = svShift True -- | Generalization of 'svShr', where the shift-amount is symbolic.--- The first argument should be a bounded quantity. -- -- NB. If the shiftee is signed, then this is an arithmetic shift; -- otherwise it's logical. svShiftRight :: SVal -> SVal -> SVal-svShiftRight x i- | not (isBounded x)- = error "SBV.svShiftLeft: Shifted amount should be a bounded quantity!"+svShiftRight = svShift False++-- | Generic shifting of bounded quantities. The shift amount must be non-negative and within the bounds of the argument+-- for bit vectors. For negative shift amounts, the result is returned unchanged. For overshifts, left-shift produces 0,+-- right shift produces 0 or -1 depending on the result being signed.+svShift :: Bool -> SVal -> SVal -> SVal+svShift toLeft x i+ | Just r <- constFoldValue+ = r+ | cannotOverShift+ = svIte (i `svLessThan` svInteger ki 0) -- Negative shift, no change+ x+ regularShiftValue | True- = svIte (svLessThan i zi)- (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i))- (svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z i)- where z = svInteger (kindOf x) 0- zi = svInteger (kindOf i) 0+ = svIte (i `svLessThan` svInteger ki 0) -- Negative shift, no change+ x+ $ svIte (i `svGreaterEq` svInteger ki (fromIntegral (intSizeOf x))) -- Overshift, by at least the bit-width of x+ overShiftValue+ regularShiftValue + where nm | toLeft = "shiftLeft"+ | True = "shiftRight"++ kx = kindOf x+ ki = kindOf i++ -- Constant fold the result if possible. If either quantity is unbounded, then we only support constants+ -- as there's no easy/meaningful way to map this combo to SMTLib. Should be rarely needed, if ever!+ -- We also perform basic sanity check here so that if we go past here, we know we have bitvectors only.+ constFoldValue+ | Just iv <- getConst i, iv == 0+ = Just x++ | Just xv <- getConst x, xv == 0+ = Just x++ | Just xv <- getConst x, Just iv <- getConst i+ = Just $ SVal kx . Left $! normCW $ CW kx (CWInteger (xv `opC` shiftAmount iv))++ | isInteger x || isInteger i+ = bailOut $ "Not yet implemented unbounded/non-constants shifts for " ++ show (kx, ki) ++ ", please file a request!"++ | not (isBounded x && isBounded i)+ = bailOut $ "Unexpected kinds: " ++ show (kx, ki)++ | True+ = Nothing++ where bailOut m = error $ "SBV." ++ nm ++ ": " ++ m++ getConst (SVal _ (Left (CW _ (CWInteger val)))) = Just val+ getConst _ = Nothing++ opC | toLeft = shiftL+ | True = shiftR++ -- like fromIntegral, but more paranoid+ shiftAmount :: Integer -> Int+ shiftAmount iv+ | iv <= 0 = 0+ | isInteger i, iv > fromIntegral (maxBound :: Int) = bailOut $ "Unsupported constant unbounded shift with amount: " ++ show iv+ | isInteger x = fromIntegral iv+ | iv >= fromIntegral ub = ub+ | not (isBounded x && isBounded i) = bailOut $ "Unsupported kinds: " ++ show (kx, ki)+ | True = fromIntegral iv+ where ub = intSizeOf x++ -- Overshift is not possible if the bit-size of x won't even fit into the bit-vector size+ -- of i. Note that this is a *necessary* check, Consider for instance if we're shifting a+ -- 32-bit value using a 1-bit shift amount (which can happen if the value is 1 with minimal+ -- shift widths). We would compare 1 >= 32, but stuffing 32 into bit-vector of size 1 would+ -- overflow. See https://github.com/LeventErkok/sbv/issues/323 for this case. Thus, we+ -- make sure that the bit-vector would fit as a value.+ cannotOverShift = maxRepresentable <= fromIntegral (intSizeOf x)+ where maxRepresentable :: Integer+ maxRepresentable+ | hasSign i = bit (intSizeOf i - 1) - 1+ | True = bit (intSizeOf i ) - 1++ -- An overshift occurs if we're shifting by more than or equal to the bit-width of x+ -- For shift-left: this value is always 0+ -- For shift-right:+ -- If x is unsigned: 0+ -- If x is signed and is less than 0, then -1 else 0+ overShiftValue | toLeft = zx+ | hasSign x = svIte (x `svLessThan` zx) neg1 zx+ | True = zx+ where zx = svInteger kx 0+ neg1 = svInteger kx (-1)++ -- Regular shift, we know that the shift value fits into the bit-width of x, since it's between 0 and sizeOf x. So, we can just+ -- turn it into a properly sized argument and ship it to SMTLib+ regularShiftValue = SVal kx $ Right $ cache result+ where result st = do sw1 <- svToSW st x+ sw2 <- svToSW st i++ let op | toLeft = Shl+ | True = Shr++ adjustedShift <- if kx == ki+ then return sw2+ else newExpr st kx (SBVApp (KindCast ki kx) [sw2])++ newExpr st kx (SBVApp op [sw1, adjustedShift])+ -- | Generalization of 'svRol', where the rotation amount is symbolic.--- The first argument should be a bounded quantity.+-- If the first argument is not bounded, then the this is the same as shift. svRotateLeft :: SVal -> SVal -> SVal svRotateLeft x i | not (isBounded x)@@ -660,7 +755,7 @@ n = svInteger (kindOf i) (toInteger sx) -- | Generalization of 'svRor', where the rotation amount is symbolic.--- The first argument should be a bounded quantity.+-- If the first argument is not bounded, then the this is the same as shift. svRotateRight :: SVal -> SVal -> SVal svRotateRight x i | not (isBounded x)
Data/SBV/Core/Symbolic.hs view
@@ -9,18 +9,19 @@ -- Symbolic values ----------------------------------------------------------------------------- +{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PatternGuards #-} {-# LANGUAGE NamedFieldPuns #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE Rank2Types #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Data.SBV.Core.Symbolic@@ -54,6 +55,7 @@ , SArr(..), readSArr, writeSArr, mergeSArr, newSArr, eqSArr ) where +import Control.Arrow (first, second, (***)) import Control.DeepSeq (NFData(..)) import Control.Monad (when, unless) import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)@@ -136,8 +138,8 @@ | Or | XOr | Not- | Shl Int- | Shr Int+ | Shl+ | Shr | Rol Int | Ror Int | Extract Int Int -- Extract i j: extract bits i to j. Least significant bit is 0 (big-endian)@@ -219,8 +221,8 @@ -- Show instance for 'Op'. Note that this is largely for debugging purposes, not used -- for being read by any tool. instance Show Op where- show (Shl i) = "<<" ++ show i- show (Shr i) = ">>" ++ show i+ show Shl = "<<"+ show Shr = ">>" show (Rol i) = "<<<" ++ show i show (Ror i) = ">>>" ++ show i show (Extract i j) = "choose [" ++ show i ++ ":" ++ show j ++ "]"@@ -281,8 +283,8 @@ -- Show instance for 'SBVExpr'. Again, only for debugging purposes. instance Show SBVExpr where show (SBVApp Ite [t, a, b]) = unwords ["if", show t, "then", show a, "else", show b]- show (SBVApp (Shl i) [a]) = unwords [show a, "<<", show i]- show (SBVApp (Shr i) [a]) = unwords [show a, ">>", show i]+ show (SBVApp Shl [a, i]) = unwords [show a, "<<", show i]+ show (SBVApp Shr [a, i]) = unwords [show a, ">>", show i] show (SBVApp (Rol i) [a]) = unwords [show a, "<<<", show i] show (SBVApp (Ror i) [a]) = unwords [show a, ">>>", show i] show (SBVApp (PseudoBoolean pb) args) = unwords (show pb : map show args)@@ -352,19 +354,19 @@ rnf (AssertSoft s a p) = rnf s `seq` rnf a `seq` rnf p `seq` () -- | Result of running a symbolic computation-data Result = Result { reskinds :: Set.Set Kind -- ^ kinds used in the program- , resTraces :: [(String, CW)] -- ^ quick-check counter-example information (if any)- , resUISegs :: [(String, [String])] -- ^ uninterpeted code segments- , resInputs :: [(Quantifier, NamedSymVar)] -- ^ inputs (possibly existential)- , resConsts :: [(SW, CW)] -- ^ constants- , resTables :: [((Int, Kind, Kind), [SW])] -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts- , resArrays :: [(Int, ArrayInfo)] -- ^ arrays (user specified)- , resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants- , resAxioms :: [(String, [String])] -- ^ axioms- , resAsgns :: SBVPgm -- ^ assignments- , resConstraints :: [(Maybe String, SW)] -- ^ additional constraints (boolean)- , resAssertions :: [(String, Maybe CallStack, SW)] -- ^ assertions- , resOutputs :: [SW] -- ^ outputs+data Result = Result { reskinds :: Set.Set Kind -- ^ kinds used in the program+ , resTraces :: [(String, CW)] -- ^ quick-check counter-example information (if any)+ , resUISegs :: [(String, [String])] -- ^ uninterpeted code segments+ , resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs (possibly existential) + tracker vars+ , resConsts :: [(SW, CW)] -- ^ constants+ , resTables :: [((Int, Kind, Kind), [SW])] -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts+ , resArrays :: [(Int, ArrayInfo)] -- ^ arrays (user specified)+ , resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants+ , resAxioms :: [(String, [String])] -- ^ axioms+ , resAsgns :: SBVPgm -- ^ assignments+ , resConstraints :: [(Maybe String, SW)] -- ^ additional constraints (boolean)+ , resAssertions :: [(String, Maybe CallStack, SW)] -- ^ assertions+ , resOutputs :: [SW] -- ^ outputs } -- Show instance for 'Result'. Only for debugging purposes.@@ -378,7 +380,8 @@ show (Result kinds _ cgs is cs ts as uis axs xs cstrs asserts os) = intercalate "\n" $ (if null usorts then [] else "SORTS" : map (" " ++) usorts) ++ ["INPUTS"]- ++ map shn is+ ++ map shn (fst is)+ ++ (if null (snd is) then [] else "TRACKER VARS" : map (shn . (EX,)) (snd is)) ++ ["CONSTANTS"] ++ map shc cs ++ ["TABLES"]@@ -545,7 +548,7 @@ , rctr :: IORef Int , rUsedKinds :: IORef KindSet , rUsedLbls :: IORef (Set.Set String)- , rinps :: IORef [(Quantifier, NamedSymVar)]+ , rinps :: IORef ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- User defined, and internal existential , rConstraints :: IORef [(Maybe String, SW)] , routs :: IORef [SW] , rtblMap :: IORef TableMap@@ -678,7 +681,7 @@ SMTMode _ False _ -> ALL CodeGen -> ALL Concrete{} -> ALL- modifyState st rinps ((q, (sw, "__internal_sbv_" ++ nm)):)+ modifyState st rinps (first ((:) (q, (sw, "__internal_sbv_" ++ nm)))) $ noInteractive [ "Internal variable creation:" , " Named: " ++ nm ]@@ -802,7 +805,19 @@ -- @randomCW@ is used for generating random values for this variable -- when used for 'quickCheck' or 'genTest' purposes. svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal-svMkSymVar mbQ k mbNm st = do+svMkSymVar = svMkSymVarGen False++-- | Create an existentially quantified tracker variable+svMkTrackerVar :: Kind -> String -> State -> IO SVal+svMkTrackerVar k nm = svMkSymVarGen True (Just EX) k (Just nm)++-- | Create a symbolic value, based on the quantifier we have. If an+-- explicit quantifier is given, we just use that. If not, then we+-- pick the quantifier appropriately based on the run-mode.+-- @randomCW@ is used for generating random values for this variable+-- when used for 'quickCheck' or 'genTest' purposes.+svMkSymVarGen :: Bool -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal+svMkSymVarGen isTracker mbQ k mbNm st = do rm <- readIORef (runMode st) let varInfo = case mbNm of@@ -817,7 +832,7 @@ mkS q = do (sw, internalName) <- newSW st k let nm = fromMaybe internalName mbNm- introduceUserName st nm k q sw+ introduceUserName st isTracker nm k q sw mkC = do cw <- randomCW k do registerKind st k@@ -835,22 +850,28 @@ (_ , Concrete{}) -> noUI mkC -- | Introduce a new user name. We die if repeated.-introduceUserName :: State -> String -> Kind -> Quantifier -> SW -> IO SVal-introduceUserName st nm k q sw = do is <- readIORef (rinps st)- if nm `elem` [n | (_, (_, n)) <- is]- then error $ "SBV: Repeated user given name: " ++ show nm ++ ". Please use unique names."- else do let newInp olds = case q of- EX -> (sw, nm) : olds- ALL -> noInteractive [ "Adding a new universally quantified: "- , " Name : " ++ show nm- , " Kind : " ++ show k- , " Quantifier: Universal"- , " Node : " ++ show sw- , "Only existential variables are supported in query mode."- ]- modifyState st rinps ((q, (sw, nm)):)- $ modifyIncState st rNewInps newInp- return $ SVal k $ Right $ cache (const (return sw))+introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SW -> IO SVal+introduceUserName st isTracker nm k q sw = do+ (is, ints) <- readIORef (rinps st)+ if nm `elem` [n | (_, (_, n)) <- is] ++ [n | (_, n) <- ints]+ then error $ "SBV: Repeated user given name: " ++ show nm ++ ". Please use unique names."+ else if isTracker && q == ALL+ then error $ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " ++ show nm+ else do let newInp olds = case q of+ EX -> (sw, nm) : olds+ ALL -> noInteractive [ "Adding a new universally quantified variable: "+ , " Name : " ++ show nm+ , " Kind : " ++ show k+ , " Quantifier: Universal"+ , " Node : " ++ show sw+ , "Only existential variables are supported in query mode."+ ]+ if isTracker+ then modifyState st rinps (second ((:) (sw, nm)))+ $ noInteractive ["Adding a new tracker variable in interactive mode: " ++ show nm]+ else modifyState st rinps (first ((:) (q, (sw, nm))))+ $ modifyIncState st rNewInps newInp+ return $ SVal k $ Right $ cache (const (return sw)) -- | Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere -- string, use for commenting purposes. The second argument is intended to hold the multiple-lines@@ -876,7 +897,7 @@ pgm <- newIORef (SBVPgm S.empty) emap <- newIORef Map.empty cmap <- newIORef Map.empty- inps <- newIORef []+ inps <- newIORef ([], []) outs <- newIORef [] tables <- newIORef Map.empty arrays <- newIORef IMap.empty@@ -938,7 +959,7 @@ , rAsserts=asserts, rUsedKinds=usedKinds, rCgMap=cgs, rCInfo=cInfo, rConstraints=cstrs } = do SBVPgm rpgm <- readIORef pgm- inpsO <- reverse <$> readIORef inps+ inpsO <- (reverse *** reverse) <$> readIORef inps outsO <- reverse <$> readIORef outs let swap (a, b) = (b, a) swapc ((_, a), b) = (b, a)@@ -986,7 +1007,7 @@ -- create the tracking variable here for the metric let mkGoal nm orig = liftIO $ do origSW <- svToSW st orig- track <- svMkSymVar (Just EX) (kindOf orig) (Just nm) st+ track <- svMkTrackerVar (kindOf orig) nm st trackSW <- svToSW st track return (origSW, trackSW)
Data/SBV/Examples/CodeGeneration/PopulationCount.hs view
@@ -191,36 +191,36 @@ -- }; -- const SWord64 s11 = s0 & 0x00000000000000ffULL; -- const SWord8 s12 = table0[s11];--- const SWord64 s13 = s0 >> 8;--- const SWord64 s14 = 0x00000000000000ffULL & s13;--- const SWord8 s15 = table0[s14];--- const SWord8 s16 = s12 + s15;--- const SWord64 s17 = s13 >> 8;--- const SWord64 s18 = 0x00000000000000ffULL & s17;--- const SWord8 s19 = table0[s18];--- const SWord8 s20 = s16 + s19;--- const SWord64 s21 = s17 >> 8;--- const SWord64 s22 = 0x00000000000000ffULL & s21;--- const SWord8 s23 = table0[s22];--- const SWord8 s24 = s20 + s23;--- const SWord64 s25 = s21 >> 8;--- const SWord64 s26 = 0x00000000000000ffULL & s25;--- const SWord8 s27 = table0[s26];--- const SWord8 s28 = s24 + s27;--- const SWord64 s29 = s25 >> 8;--- const SWord64 s30 = 0x00000000000000ffULL & s29;--- const SWord8 s31 = table0[s30];--- const SWord8 s32 = s28 + s31;--- const SWord64 s33 = s29 >> 8;--- const SWord64 s34 = 0x00000000000000ffULL & s33;--- const SWord8 s35 = table0[s34];--- const SWord8 s36 = s32 + s35;--- const SWord64 s37 = s33 >> 8;--- const SWord64 s38 = 0x00000000000000ffULL & s37;--- const SWord8 s39 = table0[s38];--- const SWord8 s40 = s36 + s39;+-- const SWord64 s14 = s0 >> 8;+-- const SWord64 s15 = 0x00000000000000ffULL & s14;+-- const SWord8 s16 = table0[s15];+-- const SWord8 s17 = s12 + s16;+-- const SWord64 s18 = s14 >> 8;+-- const SWord64 s19 = 0x00000000000000ffULL & s18;+-- const SWord8 s20 = table0[s19];+-- const SWord8 s21 = s17 + s20;+-- const SWord64 s22 = s18 >> 8;+-- const SWord64 s23 = 0x00000000000000ffULL & s22;+-- const SWord8 s24 = table0[s23];+-- const SWord8 s25 = s21 + s24;+-- const SWord64 s26 = s22 >> 8;+-- const SWord64 s27 = 0x00000000000000ffULL & s26;+-- const SWord8 s28 = table0[s27];+-- const SWord8 s29 = s25 + s28;+-- const SWord64 s30 = s26 >> 8;+-- const SWord64 s31 = 0x00000000000000ffULL & s30;+-- const SWord8 s32 = table0[s31];+-- const SWord8 s33 = s29 + s32;+-- const SWord64 s34 = s30 >> 8;+-- const SWord64 s35 = 0x00000000000000ffULL & s34;+-- const SWord8 s36 = table0[s35];+-- const SWord8 s37 = s33 + s36;+-- const SWord64 s38 = s34 >> 8;+-- const SWord64 s39 = 0x00000000000000ffULL & s38;+-- const SWord8 s40 = table0[s39];+-- const SWord8 s41 = s37 + s40; -- <BLANKLINE>--- return s40;+-- return s41; -- } -- == END: "popCount.c" ================== genPopCountInC :: IO ()
Data/SBV/Provers/Prover.hs view
@@ -37,8 +37,13 @@ import System.Directory (getCurrentDirectory) import Data.Time (getZonedTime, NominalDiffTime, UTCTime, getCurrentTime, diffUTCTime)-import Data.List (intercalate, isPrefixOf)+import Data.List (intercalate, isPrefixOf, nub) +import Data.Maybe (mapMaybe)++import qualified Data.Map.Strict as M+import qualified Data.Foldable as S (toList)+ import Data.SBV.Core.Data import Data.SBV.Core.Symbolic import Data.SBV.SMT.SMT@@ -197,6 +202,7 @@ optimizeWith config style = runWithQuery True opt config where opt = do objectives <- Control.getObjectives qinps <- Control.getQuantifiedInputs+ spgm <- Control.getSBVPgm when (null objectives) $ error $ unlines [ ""@@ -210,21 +216,49 @@ , "*** Please use a solver that has support, such as z3" ] - let needsUniversalOpt = let universals = [s | (ALL, (s, _)) <- qinps]- check (x, y) nm = [nm | any (`elem` universals) [x, y]]- isUniversal (Maximize nm xy) = check xy nm- isUniversal (Minimize nm xy) = check xy nm- isUniversal (AssertSoft nm xy _) = check xy nm- in concatMap isUniversal objectives+ let universals = [s | (ALL, s) <- qinps] - unless (null needsUniversalOpt) $- error $ unlines [ ""- , "*** Data.SBV: Problem needs optimization of universally quantified metric(s):"- , "***"- , "*** " ++ unwords needsUniversalOpt- , "***"- , "*** Optimization is only meaningful existentially quantified values."- ]+ firstUniversal+ | null universals = error "Data.SBV: Impossible happened! Universal optimization with no universals!"+ | True = minimum (map (nodeId . fst) universals)++ nodeId (SW _ n) = n++ mappings :: M.Map SW SBVExpr+ mappings = M.fromList (S.toList (pgmAssignments spgm))++ chaseUniversal entry = map snd $ go entry []+ where go x sofar+ | nx >= firstUniversal+ = nub $ [unm | unm@(u, _) <- universals, nx >= nodeId u] ++ sofar+ | True+ = let oVars (LkUp _ a b) = [a, b]+ oVars (IEEEFP (FP_Cast _ _ o)) = [o]+ oVars _ = []+ vars = case x `M.lookup` mappings of+ Nothing -> []+ Just (SBVApp o ss) -> nub (oVars o ++ ss)+ in foldr go sofar vars+ where nx = nodeId x++ let needsUniversalOpt = let tag _ [] = Nothing+ tag nm xs = Just (nm, xs)+ needsUniversal (Maximize nm (x, _)) = tag nm (chaseUniversal x)+ needsUniversal (Minimize nm (x, _)) = tag nm (chaseUniversal x)+ needsUniversal (AssertSoft nm (x, _) _) = tag nm (chaseUniversal x)+ in mapMaybe needsUniversal objectives++ unless (null universals || null needsUniversalOpt) $+ let len = maximum $ 0 : [length nm | (nm, _) <- needsUniversalOpt]+ pad n = n ++ replicate (len - length n) ' '+ in error $ unlines $ [ ""+ , "*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):"+ , "***"+ ]+ ++ [ "*** " ++ pad s ++ " [Depends on: " ++ intercalate ", " xs ++ "]" | (s, xs) <- needsUniversalOpt ]+ ++ [ "***"+ , "*** Optimization is only meaningful with existentially quantified metrics."+ ] let optimizerDirectives = concatMap minmax objectives ++ priority style where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"
Data/SBV/Provers/Z3.hs view
@@ -13,20 +13,9 @@ module Data.SBV.Provers.Z3(z3) where -import Data.Char (toLower)- import Data.SBV.Core.Data import Data.SBV.SMT.SMT -import qualified System.Info as S(os)---- Choose the correct prefix character for passing options--- TBD: Is there a more foolproof way of determining this?-optionPrefix :: Char-optionPrefix- | map toLower S.os `elem` ["linux", "darwin"] = '-'- | True = '/' -- windows- -- | The description of the Z3 SMT solver. -- The default executable is @\"z3\"@, which must be in your path. You can use the @SBV_Z3@ environment variable to point to the executable on your system. -- The default options are @\"-nw -in -smt2\"@, which is valid for Z3 4.1. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options.@@ -34,7 +23,7 @@ z3 = SMTSolver { name = Z3 , executable = "z3"- , options = map (optionPrefix:) . modConfig ["nw", "in", "smt2"]+ , options = modConfig ["-nw", "-in", "-smt2"] , engine = standardEngine "SBV_Z3" "SBV_Z3_OPTIONS" , capabilities = SolverCapabilities { supportsQuantifiers = True
Data/SBV/SMT/SMTLib.hs view
@@ -64,7 +64,7 @@ needsQuantifiers | isSat = ALL `elem` quantifiers | True = EX `elem` quantifiers- where quantifiers = map fst qinps+ where quantifiers = map fst (fst qinps) -- | Convert to SMTLib-2 format toIncSMTLib2 :: SMTLibIncConverter [String]
Data/SBV/SMT/SMTLib2.hs view
@@ -31,7 +31,7 @@ -- | Translate a problem into an SMTLib2 script cvt :: SMTLibConverter [String]-cvt kindInfo isSat comments inputs skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm+cvt kindInfo isSat comments (inputs, trackerVars) skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out cfg = pgm where hasInteger = KUnbounded `Set.member` kindInfo hasReal = KReal `Set.member` kindInfo hasFloat = KFloat `Set.member` kindInfo@@ -98,6 +98,8 @@ ++ map (declConst cfg) consts ++ [ "; --- skolem constants ---" ] ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" ++ userName s | Right (s, ss) <- skolemInps]+ ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ]+ ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType [] s ++ ") ; tracks " ++ nm | (s, nm) <- trackerVars] ++ [ "; --- constant tables ---" ] ++ concatMap constTable constTables ++ [ "; --- skolemized tables ---" ]@@ -108,22 +110,33 @@ ++ concatMap declUI uis ++ [ "; --- user given axioms ---" ] ++ map declAx axs- ++ [ "; --- formula ---" ]++ ++ map (declDef cfg skolemMap tableMap) preQuantifierAssigns ++ ["(assert (forall (" ++ intercalate "\n " ["(" ++ show s ++ " " ++ swType s ++ ")" | s <- foralls] ++ ")" | not (null foralls) ]-- ++ map mkAssign asgns+ ++ map mkAssign postQuantifierAssigns ++ delayedAsserts delayedEqualities ++ finalAssert + -- identify the assignments that can come before the first quantifier+ (preQuantifierAssigns, postQuantifierAssigns)+ | null foralls+ = ([], asgns) -- the apparent "switch" here is OK; rest of the code works correctly if there are no foralls.+ | True+ = span pre asgns+ where first = nodeId (minimum foralls)+ pre (s, _) = nodeId s < first++ nodeId (SW _ n) = n+ noOfCloseParens | null foralls = 0- | True = length asgns + 2 + (if null delayedEqualities then 0 else 1)+ | True = length postQuantifierAssigns + 2 + (if null delayedEqualities then 0 else 1) foralls = [s | Left s <- skolemInps] forallArgs = concatMap ((" " ++) . show) foralls@@ -485,25 +498,19 @@ sh (SBVApp (Extract i j) [a]) | ensureBV = "((_ extract " ++ show i ++ " " ++ show j ++ ") " ++ ssw a ++ ")" sh (SBVApp (Rol i) [a])- | bvOp = rot ssw "rotate_left" i a- | intOp = sh (SBVApp (Shl i) [a]) -- Haskell treats rotateL as shiftL for unbounded values+ | bvOp = rot ssw "rotate_left" i a | True = bad sh (SBVApp (Ror i) [a]) | bvOp = rot ssw "rotate_right" i a- | intOp = sh (SBVApp (Shr i) [a]) -- Haskell treats rotateR as shiftR for unbounded values | True = bad - sh (SBVApp (Shl i) [a])- | bvOp = shft rm ssw "bvshl" "bvshl" i a- | i < 0 = sh (SBVApp (Shr (-i)) [a]) -- flip sign/direction- | intOp = "(* " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftL by multiplication by 2^i+ sh (SBVApp Shl [a, i])+ | bvOp = shft ssw "bvshl" "bvshl" a i | True = bad - sh (SBVApp (Shr i) [a])- | bvOp = shft rm ssw "bvlshr" "bvashr" i a- | i < 0 = sh (SBVApp (Shl (-i)) [a]) -- flip sign/direction- | intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i+ sh (SBVApp Shr [a, i])+ | bvOp = shft ssw "bvlshr" "bvashr" a i | True = bad sh (SBVApp op args)@@ -670,11 +677,9 @@ rot :: (SW -> String) -> String -> Int -> SW -> String rot ssw o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssw x ++ ")" -shft :: RoundingMode -> (SW -> String) -> String -> String -> Int -> SW -> String-shft rm ssw oW oS c x = "(" ++ o ++ " " ++ ssw x ++ " " ++ cvtCW rm c' ++ ")"- where s = hasSign x- c' = mkConstCW (kindOf x) c- o = if s then oS else oW+shft :: (SW -> String) -> String -> String -> SW -> SW -> String+shft ssw oW oS x c = "(" ++ o ++ " " ++ ssw x ++ " " ++ ssw c ++ ")"+ where o = if hasSign x then oS else oW -- Various casts handleKindCast :: Kind -> Kind -> String -> String
Data/SBV/SMT/Utils.hs view
@@ -27,20 +27,20 @@ import qualified Data.Set as Set (Set) -- | 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?- -> [String] -- ^ extra comments to place on top- -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names- -> [Either SW (SW, [SW])] -- ^ skolemized inputs- -> [(SW, CW)] -- ^ constants- -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables- -> [(Int, ArrayInfo)] -- ^ user specified arrays- -> [(String, SBVType)] -- ^ uninterpreted functions/constants- -> [(String, [String])] -- ^ user given axioms- -> SBVPgm -- ^ assignments- -> [(Maybe String, SW)] -- ^ extra constraints- -> SW -- ^ output variable- -> SMTConfig -- ^ configuration+type SMTLibConverter a = Set.Set Kind -- ^ Kinds used in the problem+ -> Bool -- ^ is this a sat problem?+ -> [String] -- ^ extra comments to place on top+ -> ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs and aliasing names and trackers+ -> [Either SW (SW, [SW])] -- ^ skolemized inputs+ -> [(SW, CW)] -- ^ constants+ -> [((Int, Kind, Kind), [SW])] -- ^ auto-generated tables+ -> [(Int, ArrayInfo)] -- ^ user specified arrays+ -> [(String, SBVType)] -- ^ uninterpreted functions/constants+ -> [(String, [String])] -- ^ user given axioms+ -> SBVPgm -- ^ assignments+ -> [(Maybe String, SW)] -- ^ extra constraints+ -> SW -- ^ output variable+ -> SMTConfig -- ^ configuration -> a -- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)
README.md view
@@ -1,15 +1,24 @@ ## SBV: SMT Based Verification in Haskell +[](http://hackage.haskell.org/package/sbv)+ Please see: http://leventerkok.github.io/sbv/ -[](http://hackage.haskell.org/package/sbv)+### Build Status -| Linux: GHC 8.0.1 | Linux: GHC 8.0.2 | Linux: GHC 8.2.1 | Mac OSX: GHC 8.0.2|-|-------------------|-------------------|-------------------|-------------------|-| [![Build1][1]][5] | [![Build2][2]][5] | [![Build3][3]][5] | [![Build4][4]][5] |+ - Linux:+ - GHC 8.0.1 [![Build1][3]][1]+ - GHC 8.0.2 [![Build1][4]][1]+ - GHC 8.2.1 [![Build1][5]][1]+ - Mac OSX:+ - GHC 8.2.1 [![Build1][6]][1]+ - Windows:+ - GHC 8.0.2 [![Build5][7]][2] -[1]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/1-[2]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/2-[3]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/3-[4]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/4-[5]: https://travis-ci.org/LeventErkok/sbv+[1]: https://travis-ci.org/LeventErkok/sbv+[2]: https://ci.appveyor.com/project/LeventErkok/sbv+[3]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/1+[4]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/2+[5]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/3+[6]: https://travis-matrix-badges.herokuapp.com/repos/LeventErkok/sbv/branches/master/4+[7]: https://ci.appveyor.com/api/projects/status/github/LeventErkok/sbv?svg=true
SBVTestSuite/GoldFiles/crcUSB5_2.gold view
@@ -88,138 +88,138 @@ SWord16 crcUSB5(const SWord16 msg) { const SWord16 s0 = msg;- const SWord16 s1 = s0 << 5;- const SBool s2 = (SBool) ((s1 >> 15) & 1);- const SBool s4 = s2 != false;- const SBool s5 = (SBool) ((s1 >> 14) & 1);- const SBool s6 = false != s5;- const SBool s7 = (SBool) ((s1 >> 13) & 1);- const SBool s8 = false != s7;- const SBool s9 = (SBool) ((s1 >> 12) & 1);- const SBool s10 = false != s9;- const SBool s11 = !s10;- const SBool s12 = s4 ? s11 : s10;- const SBool s13 = (SBool) ((s1 >> 11) & 1);- const SBool s14 = false != s13;- const SBool s15 = !s14;- const SBool s16 = s6 ? s15 : s14;- const SBool s17 = (SBool) ((s1 >> 10) & 1);- const SBool s18 = false != s17;- const SBool s19 = !s18;- const SBool s20 = s4 ? s19 : s18;- const SBool s21 = !s20;- const SBool s22 = s8 ? s21 : s20;- const SBool s23 = (SBool) ((s1 >> 9) & 1);- const SBool s24 = false != s23;- const SBool s25 = !s24;- const SBool s26 = s6 ? s25 : s24;- const SBool s27 = !s26;- const SBool s28 = s12 ? s27 : s26;- const SBool s29 = (SBool) ((s1 >> 8) & 1);- const SBool s30 = false != s29;- const SBool s31 = !s30;- const SBool s32 = s8 ? s31 : s30;- const SBool s33 = !s32;- const SBool s34 = s16 ? s33 : s32;- const SBool s35 = (SBool) ((s1 >> 7) & 1);- const SBool s36 = false != s35;- const SBool s37 = !s36;- const SBool s38 = s12 ? s37 : s36;- const SBool s39 = !s38;- const SBool s40 = s22 ? s39 : s38;- const SBool s41 = (SBool) ((s1 >> 6) & 1);- const SBool s42 = false != s41;- const SBool s43 = !s42;- const SBool s44 = s16 ? s43 : s42;- const SBool s45 = !s44;- const SBool s46 = s28 ? s45 : s44;- const SBool s47 = (SBool) ((s1 >> 5) & 1);- const SBool s48 = false != s47;- const SBool s49 = !s48;- const SBool s50 = s22 ? s49 : s48;- const SBool s51 = !s50;- const SBool s52 = s34 ? s51 : s50;- const SBool s53 = !s4;- const SBool s54 = s4 ? s53 : s4;- const SBool s55 = !s6;- const SBool s56 = s6 ? s55 : s6;- const SBool s57 = !s8;- const SBool s58 = s8 ? s57 : s8;- const SBool s59 = !s12;- const SBool s60 = s12 ? s59 : s12;- const SBool s61 = !s16;- const SBool s62 = s16 ? s61 : s16;- const SBool s63 = !s22;- const SBool s64 = s22 ? s63 : s22;- const SBool s65 = !s28;- const SBool s66 = s28 ? s65 : s28;- const SBool s67 = !s34;- const SBool s68 = s34 ? s67 : s34;- const SBool s69 = !s40;- const SBool s70 = s40 ? s69 : s40;- const SBool s71 = !s46;- const SBool s72 = s46 ? s71 : s46;- const SBool s73 = !s52;- const SBool s74 = s52 ? s73 : s52;- const SBool s75 = (SBool) ((s1 >> 4) & 1);- const SBool s76 = false != s75;- const SBool s77 = !s76;- const SBool s78 = s28 ? s77 : s76;- const SBool s79 = !s78;- const SBool s80 = s40 ? s79 : s78;- const SBool s81 = (SBool) ((s1 >> 3) & 1);- const SBool s82 = false != s81;- const SBool s83 = !s82;- const SBool s84 = s34 ? s83 : s82;- const SBool s85 = !s84;- const SBool s86 = s46 ? s85 : s84;- const SBool s87 = (SBool) ((s1 >> 2) & 1);- const SBool s88 = false != s87;- const SBool s89 = !s88;- const SBool s90 = s40 ? s89 : s88;- const SBool s91 = !s90;- const SBool s92 = s52 ? s91 : s90;- const SBool s93 = (SBool) ((s1 >> 1) & 1);- const SBool s94 = false != s93;- const SBool s95 = !s94;- const SBool s96 = s46 ? s95 : s94;- const SBool s97 = (SBool) ((s1 >> 0) & 1);- const SBool s98 = false != s97;- const SBool s99 = !s98;- const SBool s100 = s52 ? s99 : s98;- const SWord16 s103 = s100 ? 0x0001U : 0x0000U;- const SWord16 s105 = s103 | 0x0002U;- const SWord16 s106 = s96 ? s105 : s103;- const SWord16 s108 = s106 | 0x0004U;- const SWord16 s109 = s92 ? s108 : s106;- const SWord16 s111 = s109 | 0x0008U;- const SWord16 s112 = s86 ? s111 : s109;- const SWord16 s114 = s112 | 0x0010U;- const SWord16 s115 = s80 ? s114 : s112;- const SWord16 s117 = s115 | 0x0020U;- const SWord16 s118 = s74 ? s117 : s115;- const SWord16 s120 = s118 | 0x0040U;- const SWord16 s121 = s72 ? s120 : s118;- const SWord16 s123 = s121 | 0x0080U;- const SWord16 s124 = s70 ? s123 : s121;- const SWord16 s126 = s124 | 0x0100U;- const SWord16 s127 = s68 ? s126 : s124;- const SWord16 s129 = s127 | 0x0200U;- const SWord16 s130 = s66 ? s129 : s127;- const SWord16 s132 = s130 | 0x0400U;- const SWord16 s133 = s64 ? s132 : s130;- const SWord16 s135 = s133 | 0x0800U;- const SWord16 s136 = s62 ? s135 : s133;- const SWord16 s138 = s136 | 0x1000U;- const SWord16 s139 = s60 ? s138 : s136;- const SWord16 s141 = s139 | 0x2000U;- const SWord16 s142 = s58 ? s141 : s139;- const SWord16 s144 = s142 | 0x4000U;- const SWord16 s145 = s56 ? s144 : s142;- const SWord16 s147 = s145 | 0x8000U;- const SWord16 s148 = s54 ? s147 : s145;- const SWord16 s149 = s1 | s148;+ const SWord16 s2 = s0 << 5;+ const SBool s3 = (SBool) ((s2 >> 15) & 1);+ const SBool s5 = s3 != false;+ const SBool s6 = (SBool) ((s2 >> 14) & 1);+ const SBool s7 = false != s6;+ const SBool s8 = (SBool) ((s2 >> 13) & 1);+ const SBool s9 = false != s8;+ const SBool s10 = (SBool) ((s2 >> 12) & 1);+ const SBool s11 = false != s10;+ const SBool s12 = !s11;+ const SBool s13 = s5 ? s12 : s11;+ const SBool s14 = (SBool) ((s2 >> 11) & 1);+ const SBool s15 = false != s14;+ const SBool s16 = !s15;+ const SBool s17 = s7 ? s16 : s15;+ const SBool s18 = (SBool) ((s2 >> 10) & 1);+ const SBool s19 = false != s18;+ const SBool s20 = !s19;+ const SBool s21 = s5 ? s20 : s19;+ const SBool s22 = !s21;+ const SBool s23 = s9 ? s22 : s21;+ const SBool s24 = (SBool) ((s2 >> 9) & 1);+ const SBool s25 = false != s24;+ const SBool s26 = !s25;+ const SBool s27 = s7 ? s26 : s25;+ const SBool s28 = !s27;+ const SBool s29 = s13 ? s28 : s27;+ const SBool s30 = (SBool) ((s2 >> 8) & 1);+ const SBool s31 = false != s30;+ const SBool s32 = !s31;+ const SBool s33 = s9 ? s32 : s31;+ const SBool s34 = !s33;+ const SBool s35 = s17 ? s34 : s33;+ const SBool s36 = (SBool) ((s2 >> 7) & 1);+ const SBool s37 = false != s36;+ const SBool s38 = !s37;+ const SBool s39 = s13 ? s38 : s37;+ const SBool s40 = !s39;+ const SBool s41 = s23 ? s40 : s39;+ const SBool s42 = (SBool) ((s2 >> 6) & 1);+ const SBool s43 = false != s42;+ const SBool s44 = !s43;+ const SBool s45 = s17 ? s44 : s43;+ const SBool s46 = !s45;+ const SBool s47 = s29 ? s46 : s45;+ const SBool s48 = (SBool) ((s2 >> 5) & 1);+ const SBool s49 = false != s48;+ const SBool s50 = !s49;+ const SBool s51 = s23 ? s50 : s49;+ const SBool s52 = !s51;+ const SBool s53 = s35 ? s52 : s51;+ const SBool s54 = !s5;+ const SBool s55 = s5 ? s54 : s5;+ const SBool s56 = !s7;+ const SBool s57 = s7 ? s56 : s7;+ const SBool s58 = !s9;+ const SBool s59 = s9 ? s58 : s9;+ const SBool s60 = !s13;+ const SBool s61 = s13 ? s60 : s13;+ const SBool s62 = !s17;+ const SBool s63 = s17 ? s62 : s17;+ const SBool s64 = !s23;+ const SBool s65 = s23 ? s64 : s23;+ const SBool s66 = !s29;+ const SBool s67 = s29 ? s66 : s29;+ const SBool s68 = !s35;+ const SBool s69 = s35 ? s68 : s35;+ const SBool s70 = !s41;+ const SBool s71 = s41 ? s70 : s41;+ const SBool s72 = !s47;+ const SBool s73 = s47 ? s72 : s47;+ const SBool s74 = !s53;+ const SBool s75 = s53 ? s74 : s53;+ const SBool s76 = (SBool) ((s2 >> 4) & 1);+ const SBool s77 = false != s76;+ const SBool s78 = !s77;+ const SBool s79 = s29 ? s78 : s77;+ const SBool s80 = !s79;+ const SBool s81 = s41 ? s80 : s79;+ const SBool s82 = (SBool) ((s2 >> 3) & 1);+ const SBool s83 = false != s82;+ const SBool s84 = !s83;+ const SBool s85 = s35 ? s84 : s83;+ const SBool s86 = !s85;+ const SBool s87 = s47 ? s86 : s85;+ const SBool s88 = (SBool) ((s2 >> 2) & 1);+ const SBool s89 = false != s88;+ const SBool s90 = !s89;+ const SBool s91 = s41 ? s90 : s89;+ const SBool s92 = !s91;+ const SBool s93 = s53 ? s92 : s91;+ const SBool s94 = (SBool) ((s2 >> 1) & 1);+ const SBool s95 = false != s94;+ const SBool s96 = !s95;+ const SBool s97 = s47 ? s96 : s95;+ const SBool s98 = (SBool) ((s2 >> 0) & 1);+ const SBool s99 = false != s98;+ const SBool s100 = !s99;+ const SBool s101 = s53 ? s100 : s99;+ const SWord16 s104 = s101 ? 0x0001U : 0x0000U;+ const SWord16 s106 = s104 | 0x0002U;+ const SWord16 s107 = s97 ? s106 : s104;+ const SWord16 s109 = s107 | 0x0004U;+ const SWord16 s110 = s93 ? s109 : s107;+ const SWord16 s112 = s110 | 0x0008U;+ const SWord16 s113 = s87 ? s112 : s110;+ const SWord16 s115 = s113 | 0x0010U;+ const SWord16 s116 = s81 ? s115 : s113;+ const SWord16 s118 = s116 | 0x0020U;+ const SWord16 s119 = s75 ? s118 : s116;+ const SWord16 s121 = s119 | 0x0040U;+ const SWord16 s122 = s73 ? s121 : s119;+ const SWord16 s124 = s122 | 0x0080U;+ const SWord16 s125 = s71 ? s124 : s122;+ const SWord16 s127 = s125 | 0x0100U;+ const SWord16 s128 = s69 ? s127 : s125;+ const SWord16 s130 = s128 | 0x0200U;+ const SWord16 s131 = s67 ? s130 : s128;+ const SWord16 s133 = s131 | 0x0400U;+ const SWord16 s134 = s65 ? s133 : s131;+ const SWord16 s136 = s134 | 0x0800U;+ const SWord16 s137 = s63 ? s136 : s134;+ const SWord16 s139 = s137 | 0x1000U;+ const SWord16 s140 = s61 ? s139 : s137;+ const SWord16 s142 = s140 | 0x2000U;+ const SWord16 s143 = s59 ? s142 : s140;+ const SWord16 s145 = s143 | 0x4000U;+ const SWord16 s146 = s57 ? s145 : s143;+ const SWord16 s148 = s146 | 0x8000U;+ const SWord16 s149 = s55 ? s148 : s146;+ const SWord16 s150 = s2 | s149; - return s149;+ return s150; } == END: "crcUSB5.c" ==================
− SBVTestSuite/GoldFiles/noTravis_query1.gold
@@ -1,193 +0,0 @@-** 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-unsat-cores true)-[GOOD] (set-option :produce-unsat-assumptions true)-[GOOD] (set-option :produce-proofs true)-[GOOD] (set-option :produce-interpolants true)-[GOOD] (set-option :random-seed 123)-[GOOD] (set-option :produce-assertions true)-[GOOD] (set-option :smt.mbqi true)-[GOOD] (set-option :produce-assignments true)-[GOOD] (set-info :status sat)-[GOOD] (set-info :bad what)-[GOOD] (set-option :produce-models true)-[GOOD] (set-logic ALL)-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s_2 () Bool false)-[GOOD] (define-fun s_1 () Bool true)-[GOOD] (define-fun s6 () Int 0)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"-[GOOD] (declare-fun s1 () Int) ; tracks user variable "b"-[GOOD] (declare-fun s2 () (_ FloatingPoint 8 24)) ; tracks user variable "c"-[GOOD] (declare-fun s3 () Bool) ; tracks user variable "d"-[GOOD] (declare-fun s4 () Real) ; tracks user variable "e"-[GOOD] (declare-fun s5 () (_ BitVec 8))-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s7 () Bool (> s0 s6))-[GOOD] (define-fun s8 () Bool (> s1 s6))-[GOOD] (assert (! s7 :named |a > 0|))-[GOOD] (assert s8)-[GOOD] (define-fun s9 () Int 2)-[GOOD] (define-fun s11 () Int 5)-[GOOD] (define-fun s10 () Int (+ s0 s9))-[GOOD] (define-fun s12 () Bool (>= s10 s11))-[GOOD] (assert s12)-[GOOD] (define-fun s14 () Int 12)-[GOOD] (define-fun s13 () Int (+ s0 s1))-[GOOD] (define-fun s15 () Bool (< s13 s14))-[GOOD] (assert (! s15 :named |a+b_<_12|))-[SEND] (get-option :diagnostic-output-channel)-[RECV] stdout-[SEND] (get-option :produce-assertions)-[RECV] true-[SEND] (get-option :produce-assignments)-[RECV] true-[SEND] (get-option :produce-proofs)-[RECV] true-[SEND] (get-option :produce-interpolants)-[RECV] true-[SEND] (get-option :produce-unsat-assumptions)-[RECV] unsupported-[SEND] (get-option :produce-unsat-cores)-[SKIP] ; :produce-unsat-assumptions line: 44 position: 0-[RECV] true-[SEND] (get-option :random-seed)-[RECV] 123-[SEND] (get-option :reproducible-resource-limit)-[RECV] unsupported-[SEND] (get-option :verbosity)-[SKIP] ; :reproducible-resource-limit line: 47 position: 0-[RECV] 0-[SEND] (get-option :smt.mbqi)-[RECV] true-[SEND] (get-option :smt.mbqi)-[RECV] true-[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")-[SEND] (get-info :status)-[RECV] (:status sat)-[GOOD] (define-fun s16 () Int 4)-[GOOD] (define-fun s17 () Bool (> s0 s16))-[GOOD] (assert (! s17 :named |later, a > 4|))-[SEND] (check-sat)-[RECV] sat-[GOOD] (set-info :status unknown)-[GOOD] (define-fun s18 () Bool (> s0 s9))-[GOOD] (declare-const __assumption_proxy_s18_19 Bool)-[GOOD] (assert (= __assumption_proxy_s18_19 s18))-[SEND] (check-sat-assuming (__assumption_proxy_s18_19))-[RECV] sat-[GOOD] (declare-const __assumption_proxy_s18_20 Bool)-[GOOD] (assert (= __assumption_proxy_s18_20 s18))-[SEND] (check-sat-assuming (__assumption_proxy_s18_20))-[RECV] sat-[SEND] (get-assignment)-[RECV] ((s_1 true) (s7 true) (|a > 0| true) (s15 true) (s_2 false) (s8 true) (a+b_<_12 true) (s17 true) (|later, a > 4| true) (s18 true) (s12 true))-[SEND] (get-info :assertion-stack-levels)-[RECV] (:assertion-stack-levels 0)-[SEND] (get-info :authors)-[RECV] (:authors "Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger")-[SEND] (get-info :error-behavior)-[RECV] (:error-behavior continued-execution)-[SEND] (get-info :name)-[RECV] (:name "Z3")-[SEND] (get-info :reason-unknown)-[RECV] (:reason-unknown "unknown")-[SEND] (get-info :version)-[RECV] (:version "4.5.1")-[SEND] (get-info :memory)-[RECV] unsupported-[SEND] (get-info :time)-[SKIP] ; :memory line: 73 position: 0-[RECV] unsupported-[SEND] (get-value (s0))-[SKIP] ; :time line: 74 position: 0-[RECV] ((s0 5))-[SEND] (get-value (s1))-[RECV] ((s1 1))-[GOOD] (define-fun s21 () Int 100)-[GOOD] (define-fun s23 () Int 9)-[GOOD] (define-fun s22 () Bool (> s0 s21))-[GOOD] (define-fun s24 () Bool (> s0 s23))-[GOOD] (declare-const __assumption_proxy_s22_25 Bool)-[GOOD] (assert (= __assumption_proxy_s22_25 s22))-[GOOD] (declare-const __assumption_proxy_s24_26 Bool)-[GOOD] (assert (= __assumption_proxy_s24_26 s24))-[SEND] (check-sat-assuming (__assumption_proxy_s22_25 __assumption_proxy_s24_26))-[RECV] unsat-[SEND] (get-unsat-assumptions)-[RECV] (a+b_<_12 __assumption_proxy_s22_25)-*** In call to 'getUnsatAssumptions'-***-*** Unexpected assumption named: "a+b_<_12"-*** Was expecting one of : ["s22","s24"]-***-*** This can happen if unsat-cores are also enabled. Ignoring.-[GOOD] (push 5)-[GOOD] (pop 3)-[GOOD] (define-fun s27 () Int 6)-[GOOD] (define-fun s28 () Bool (> s0 s27))-[GOOD] (assert (! s28 :named |bey|))-[GOOD] (define-fun s29 () Bool (< s0 s27))-[GOOD] (assert (! s29 :named |hey|))-[SEND] (check-sat)-[RECV] unsat-[SEND, TimeOut: 4000ms] (get-unsat-core)-[RECV] (bey hey)-[SEND] (get-proof)-[RECV] ((set-logic ALL)- (declare-fun bey () Bool)- (declare-fun hey () Bool)- (proof- (let (($x232 (<= s0 6)))- (let (($x233 (not $x232)))- (let (($x236 (or (not bey) $x233)))- (let ((@x238 (monotonicity (rewrite (= (> s0 6) $x233)) (= (or (not bey) (> s0 6)) $x236))))- (let ((@x231 (rewrite (= (=> bey (> s0 6)) (or (not bey) (> s0 6))))))- (let ((@x241 (mp (asserted (=> bey (> s0 6))) (trans @x231 @x238 (= (=> bey (> s0 6)) $x236)) $x236)))- (let (($x252 (>= s0 6)))- (let (($x250 (not $x252)))- (let (($x254 (or (not hey) $x250)))- (let ((@x256 (monotonicity (rewrite (= (< s0 6) $x250)) (= (or (not hey) (< s0 6)) $x254))))- (let ((@x249 (rewrite (= (=> hey (< s0 6)) (or (not hey) (< s0 6))))))- (let ((@x259 (mp (asserted (=> hey (< s0 6))) (trans @x249 @x256 (= (=> hey (< s0 6)) $x254)) $x254)))- (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x252 $x232)) (unit-resolution @x259 (asserted hey) $x250) (unit-resolution @x241 (asserted bey) $x233) false)))))))))))))))-[SEND, TimeOut: 6000ms] (get-assertions)--[RECV] ((! s7 :named |a > 0|)- s8- s12- (! s15 :named |a+b_<_12|)- (! s17 :named |later, a > 4|)- (= __assumption_proxy_s18_19 s18)- (= __assumption_proxy_s18_20 s18)- (= __assumption_proxy_s22_25 s22)- (= __assumption_proxy_s24_26 s24)- (! s28 :named |bey|)- (! s29 :named |hey|))-[SEND] (echo "there we go")-[RECV] "there we go"-*** Solver : Z3-*** Exit code: ExitSuccess-- FINAL:Satisfiable. Model:- a = 332 :: Integer- b = 3 :: Integer- c = 2.3 :: Float- d = True :: Bool- e = 3.12 :: Real- s5 = -12 :: Int8-DONE!
− SBVTestSuite/GoldFiles/noTravis_query_abc.gold
@@ -1,34 +0,0 @@-** Calling: abc -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"-[ISSUE] ; Automatically generated by SBV. Do not edit.-** Skipping heart-beat for the solver ABC-** Backend solver ABC does not support global decls.-** Some incremental calls, such as pop, will be limited.-[ISSUE] (set-option :diagnostic-output-channel "stdout")-[ISSUE] (set-option :produce-models true)-[ISSUE] (set-logic QF_BV)-[ISSUE] ; --- uninterpreted sorts ----[ISSUE] ; --- literal constants ----[ISSUE] (define-fun s_2 () Bool false)-[ISSUE] (define-fun s_1 () Bool true)-[ISSUE] (define-fun s2 () (_ BitVec 32) #x00000000)-[ISSUE] ; --- skolem constants ----[ISSUE] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"-[ISSUE] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"-[ISSUE] ; --- constant tables ----[ISSUE] ; --- skolemized tables ----[ISSUE] ; --- arrays ----[ISSUE] ; --- uninterpreted constants ----[ISSUE] ; --- user given axioms ----[ISSUE] ; --- formula ----[ISSUE] (define-fun s3 () Bool (bvsgt s0 s2))-[ISSUE] (define-fun s4 () Bool (bvsgt s1 s2))-[ISSUE] (assert s3)-[ISSUE] (assert s4)-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ((s0 #x1))-[SEND] (get-value (s1))-[RECV] ((s1 #x1))-*** Solver : ABC-*** Exit code: ExitSuccess
− SBVTestSuite/GoldFiles/noTravis_query_boolector.gold
@@ -1,54 +0,0 @@-** Calling: boolector --smt2 --smt2-model --no-exit-codes --incremental-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-** Backend solver Boolector 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 32) #x00000000)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))-[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))-[GOOD] (assert s3)-[GOOD] (assert s4)-[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)-[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)-[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))-[GOOD] (define-fun s8 () Bool (bvsle s6 s7))-[GOOD] (assert s8)-[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)-[GOOD] (define-fun s10 () Bool (bvslt s0 s9))-[GOOD] (assert s10)-[GOOD] (define-fun s11 () Bool (bvslt s1 s5))-[GOOD] (assert s11)-[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)-[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))-[GOOD] (define-fun s14 () Bool (bvslt s12 s13))-[GOOD] (assert s14)-[GOOD] (define-fun s15 () Bool (bvslt s0 s5))-[GOOD] (assert s15)-[SEND] (check-sat)-[RECV] sat-[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)-[GOOD] (define-fun s17 () Bool (bvsge s0 s16))-[GOOD] (assert s17)-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ((s0 #b00000000000000000000000000000001))-[SEND] (get-value (s1))-[RECV] ((s1 #b00000000000000000000000000000001))-*** Solver : Boolector-*** Exit code: ExitSuccess
− SBVTestSuite/GoldFiles/noTravis_query_cvc4.gold
@@ -1,60 +0,0 @@-** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-[GOOD] (set-option :global-declarations true)-[GOOD] (set-option :diagnostic-output-channel "stdout")-[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 32) #x00000000)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))-[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))-[GOOD] (assert (! s3 :named |a > 0|))-[GOOD] (assert s4)-[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)-[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)-[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))-[GOOD] (define-fun s8 () Bool (bvsle s6 s7))-[GOOD] (assert s8)-[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)-[GOOD] (define-fun s10 () Bool (bvslt s0 s9))-[GOOD] (assert s10)-[GOOD] (define-fun s11 () Bool (bvslt s1 s5))-[GOOD] (assert s11)-[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)-[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))-[GOOD] (define-fun s14 () Bool (bvslt s12 s13))-[GOOD] (assert (! s14 :named |a+b_<_12|))-[GOOD] (push 1)-[GOOD] (define-fun s15 () Bool (bvslt s0 s5))-[GOOD] (assert s15)-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ((s0 (_ bv1 32)))-[GOOD] (pop 1)-[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)-[GOOD] (define-fun s17 () Bool (bvsgt s0 s16))-[GOOD] (assert (! s17 :named |extra|))-[GOOD] (assert s11)-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ((s0 (_ bv2 32)))-[SEND] (get-value (s1))-[RECV] ((s1 (_ bv1 32)))-*** Solver : CVC4-*** Exit code: ExitSuccess-*** Std-out :
− SBVTestSuite/GoldFiles/noTravis_query_mathsat.gold
@@ -1,55 +0,0 @@-** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4-[GOOD] ; Automatically generated by SBV. Do not edit.-[GOOD] (set-option :print-success true)-** Backend solver MathSAT does not support global decls.-** Some incremental calls, such as pop, will be limited.-[GOOD] (set-option :diagnostic-output-channel "stdout")-[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 32) #x00000000)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))-[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))-[GOOD] (assert (! s3 :named |a > 0|))-[GOOD] (assert s4)-[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)-[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)-[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))-[GOOD] (define-fun s8 () Bool (bvsle s6 s7))-[GOOD] (assert s8)-[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)-[GOOD] (define-fun s10 () Bool (bvslt s0 s9))-[GOOD] (assert s10)-[GOOD] (define-fun s11 () Bool (bvslt s1 s5))-[GOOD] (assert s11)-[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)-[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))-[GOOD] (define-fun s14 () Bool (bvslt s12 s13))-[GOOD] (assert (! s14 :named |a+b_<_12|))-[GOOD] (define-fun s15 () Bool (bvslt s0 s5))-[GOOD] (assert s15)-[SEND] (check-sat)-[RECV] sat-[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)-[GOOD] (define-fun s17 () Bool (bvsge s0 s16))-[GOOD] (assert (! s17 :named |extra|))-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ( (s0 (_ bv1 32)) )-[SEND] (get-value (s1))-[RECV] ( (s1 (_ bv1 32)) )-*** Solver : MathSAT-*** Exit code: ExitSuccess
− SBVTestSuite/GoldFiles/noTravis_query_yices.gold
@@ -1,54 +0,0 @@-** 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 32) #x00000000)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"-[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))-[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))-[GOOD] (assert (! s3 :named |a > 0|))-[GOOD] (assert s4)-[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)-[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)-[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))-[GOOD] (define-fun s8 () Bool (bvsle s6 s7))-[GOOD] (assert s8)-[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)-[GOOD] (define-fun s10 () Bool (bvslt s0 s9))-[GOOD] (assert s10)-[GOOD] (define-fun s11 () Bool (bvslt s1 s5))-[GOOD] (assert s11)-[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)-[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))-[GOOD] (define-fun s14 () Bool (bvslt s12 s13))-[GOOD] (assert (! s14 :named |a+b_<_12|))-[GOOD] (define-fun s15 () Bool (bvslt s0 s5))-[GOOD] (assert s15)-[SEND] (check-sat)-[RECV] sat-[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)-[GOOD] (define-fun s17 () Bool (bvsge s0 s16))-[GOOD] (assert (! s17 :named |extra|))-[SEND] (check-sat)-[RECV] sat-[SEND] (get-value (s0))-[RECV] ((s0 #b00000000000000000000000000000001))-[SEND] (get-value (s1))-[RECV] ((s1 #b00000000000000000000000000000001))-*** Solver : Yices-*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/optQuant1.gold view
@@ -0,0 +1,5 @@+*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):+***+*** goal [Depends on: x]+***+*** Optimization is only meaningful with existentially quantified metrics.
+ SBVTestSuite/GoldFiles/optQuant2.gold view
@@ -0,0 +1,5 @@+Optimal model:+ a = 0 :: Integer+ b1 = 1 :: Integer+ b2 = 1 :: Integer+ goal = 0 :: Integer
+ SBVTestSuite/GoldFiles/optQuant3.gold view
@@ -0,0 +1,5 @@+Optimal model:+ a = 0 :: Integer+ b1 = 1 :: Integer+ b2 = 1 :: Integer+ goal = 0 :: Integer
+ SBVTestSuite/GoldFiles/optQuant4.gold view
@@ -0,0 +1,5 @@+Optimal model:+ a = 0 :: Integer+ b1 = 1 :: Integer+ b2 = 1 :: Integer+ goal = 0 :: Integer
+ SBVTestSuite/GoldFiles/optQuant5.gold view
@@ -0,0 +1,5 @@+*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):+***+*** goal [Depends on: x, y]+***+*** Optimization is only meaningful with existentially quantified metrics.
SBVTestSuite/GoldFiles/popCount1.gold view
@@ -104,35 +104,35 @@ }; const SWord64 s11 = s0 & 0x00000000000000ffULL; const SWord8 s12 = table0[s11];- const SWord64 s13 = s0 >> 8;- const SWord64 s14 = 0x00000000000000ffULL & s13;- const SWord8 s15 = table0[s14];- const SWord8 s16 = s12 + s15;- const SWord64 s17 = s13 >> 8;- const SWord64 s18 = 0x00000000000000ffULL & s17;- const SWord8 s19 = table0[s18];- const SWord8 s20 = s16 + s19;- const SWord64 s21 = s17 >> 8;- const SWord64 s22 = 0x00000000000000ffULL & s21;- const SWord8 s23 = table0[s22];- const SWord8 s24 = s20 + s23;- const SWord64 s25 = s21 >> 8;- const SWord64 s26 = 0x00000000000000ffULL & s25;- const SWord8 s27 = table0[s26];- const SWord8 s28 = s24 + s27;- const SWord64 s29 = s25 >> 8;- const SWord64 s30 = 0x00000000000000ffULL & s29;- const SWord8 s31 = table0[s30];- const SWord8 s32 = s28 + s31;- const SWord64 s33 = s29 >> 8;- const SWord64 s34 = 0x00000000000000ffULL & s33;- const SWord8 s35 = table0[s34];- const SWord8 s36 = s32 + s35;- const SWord64 s37 = s33 >> 8;- const SWord64 s38 = 0x00000000000000ffULL & s37;- const SWord8 s39 = table0[s38];- const SWord8 s40 = s36 + s39;+ const SWord64 s14 = s0 >> 8;+ const SWord64 s15 = 0x00000000000000ffULL & s14;+ const SWord8 s16 = table0[s15];+ const SWord8 s17 = s12 + s16;+ const SWord64 s18 = s14 >> 8;+ const SWord64 s19 = 0x00000000000000ffULL & s18;+ const SWord8 s20 = table0[s19];+ const SWord8 s21 = s17 + s20;+ const SWord64 s22 = s18 >> 8;+ const SWord64 s23 = 0x00000000000000ffULL & s22;+ const SWord8 s24 = table0[s23];+ const SWord8 s25 = s21 + s24;+ const SWord64 s26 = s22 >> 8;+ const SWord64 s27 = 0x00000000000000ffULL & s26;+ const SWord8 s28 = table0[s27];+ const SWord8 s29 = s25 + s28;+ const SWord64 s30 = s26 >> 8;+ const SWord64 s31 = 0x00000000000000ffULL & s30;+ const SWord8 s32 = table0[s31];+ const SWord8 s33 = s29 + s32;+ const SWord64 s34 = s30 >> 8;+ const SWord64 s35 = 0x00000000000000ffULL & s34;+ const SWord8 s36 = table0[s35];+ const SWord8 s37 = s33 + s36;+ const SWord64 s38 = s34 >> 8;+ const SWord64 s39 = 0x00000000000000ffULL & s38;+ const SWord8 s40 = table0[s39];+ const SWord8 s41 = s37 + s40; - return s40;+ return s41; } == END: "popCount.c" ==================
SBVTestSuite/GoldFiles/popCount2.gold view
@@ -104,35 +104,35 @@ }; const SWord64 s11 = s0 & 0x00000000000000ffULL; const SWord8 s12 = s11 >= 256 ? 0 : table0[s11];- const SWord64 s13 = s0 >> 8;- const SWord64 s14 = 0x00000000000000ffULL & s13;- const SWord8 s15 = s14 >= 256 ? 0 : table0[s14];- const SWord8 s16 = s12 + s15;- const SWord64 s17 = s13 >> 8;- const SWord64 s18 = 0x00000000000000ffULL & s17;- const SWord8 s19 = s18 >= 256 ? 0 : table0[s18];- const SWord8 s20 = s16 + s19;- const SWord64 s21 = s17 >> 8;- const SWord64 s22 = 0x00000000000000ffULL & s21;- const SWord8 s23 = s22 >= 256 ? 0 : table0[s22];- const SWord8 s24 = s20 + s23;- const SWord64 s25 = s21 >> 8;- const SWord64 s26 = 0x00000000000000ffULL & s25;- const SWord8 s27 = s26 >= 256 ? 0 : table0[s26];- const SWord8 s28 = s24 + s27;- const SWord64 s29 = s25 >> 8;- const SWord64 s30 = 0x00000000000000ffULL & s29;- const SWord8 s31 = s30 >= 256 ? 0 : table0[s30];- const SWord8 s32 = s28 + s31;- const SWord64 s33 = s29 >> 8;- const SWord64 s34 = 0x00000000000000ffULL & s33;- const SWord8 s35 = s34 >= 256 ? 0 : table0[s34];- const SWord8 s36 = s32 + s35;- const SWord64 s37 = s33 >> 8;- const SWord64 s38 = 0x00000000000000ffULL & s37;- const SWord8 s39 = s38 >= 256 ? 0 : table0[s38];- const SWord8 s40 = s36 + s39;+ const SWord64 s14 = s0 >> 8;+ const SWord64 s15 = 0x00000000000000ffULL & s14;+ const SWord8 s16 = s15 >= 256 ? 0 : table0[s15];+ const SWord8 s17 = s12 + s16;+ const SWord64 s18 = s14 >> 8;+ const SWord64 s19 = 0x00000000000000ffULL & s18;+ const SWord8 s20 = s19 >= 256 ? 0 : table0[s19];+ const SWord8 s21 = s17 + s20;+ const SWord64 s22 = s18 >> 8;+ const SWord64 s23 = 0x00000000000000ffULL & s22;+ const SWord8 s24 = s23 >= 256 ? 0 : table0[s23];+ const SWord8 s25 = s21 + s24;+ const SWord64 s26 = s22 >> 8;+ const SWord64 s27 = 0x00000000000000ffULL & s26;+ const SWord8 s28 = s27 >= 256 ? 0 : table0[s27];+ const SWord8 s29 = s25 + s28;+ const SWord64 s30 = s26 >> 8;+ const SWord64 s31 = 0x00000000000000ffULL & s30;+ const SWord8 s32 = s31 >= 256 ? 0 : table0[s31];+ const SWord8 s33 = s29 + s32;+ const SWord64 s34 = s30 >> 8;+ const SWord64 s35 = 0x00000000000000ffULL & s34;+ const SWord8 s36 = s35 >= 256 ? 0 : table0[s35];+ const SWord8 s37 = s33 + s36;+ const SWord64 s38 = s34 >> 8;+ const SWord64 s39 = 0x00000000000000ffULL & s38;+ const SWord8 s40 = s39 >= 256 ? 0 : table0[s39];+ const SWord8 s41 = s37 + s40; - return s40;+ return s41; } == END: "popCount.c" ==================
+ SBVTestSuite/GoldFiles/query1.gold view
@@ -0,0 +1,193 @@+** 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-unsat-cores true)+[GOOD] (set-option :produce-unsat-assumptions true)+[GOOD] (set-option :produce-proofs true)+[GOOD] (set-option :produce-interpolants true)+[GOOD] (set-option :random-seed 123)+[GOOD] (set-option :produce-assertions true)+[GOOD] (set-option :smt.mbqi true)+[GOOD] (set-option :produce-assignments true)+[GOOD] (set-info :status sat)+[GOOD] (set-info :bad what)+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic ALL)+[GOOD] ; --- uninterpreted sorts ---+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] (define-fun s6 () Int 0)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"+[GOOD] (declare-fun s1 () Int) ; tracks user variable "b"+[GOOD] (declare-fun s2 () (_ FloatingPoint 8 24)) ; tracks user variable "c"+[GOOD] (declare-fun s3 () Bool) ; tracks user variable "d"+[GOOD] (declare-fun s4 () Real) ; tracks user variable "e"+[GOOD] (declare-fun s5 () (_ BitVec 8))+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s7 () Bool (> s0 s6))+[GOOD] (define-fun s8 () Bool (> s1 s6))+[GOOD] (assert (! s7 :named |a > 0|))+[GOOD] (assert s8)+[GOOD] (define-fun s9 () Int 2)+[GOOD] (define-fun s11 () Int 5)+[GOOD] (define-fun s10 () Int (+ s0 s9))+[GOOD] (define-fun s12 () Bool (>= s10 s11))+[GOOD] (assert s12)+[GOOD] (define-fun s14 () Int 12)+[GOOD] (define-fun s13 () Int (+ s0 s1))+[GOOD] (define-fun s15 () Bool (< s13 s14))+[GOOD] (assert (! s15 :named |a+b_<_12|))+[SEND] (get-option :diagnostic-output-channel)+[RECV] stdout+[SEND] (get-option :produce-assertions)+[RECV] true+[SEND] (get-option :produce-assignments)+[RECV] true+[SEND] (get-option :produce-proofs)+[RECV] true+[SEND] (get-option :produce-interpolants)+[RECV] true+[SEND] (get-option :produce-unsat-assumptions)+[RECV] unsupported+[SEND] (get-option :produce-unsat-cores)+[SKIP] ; :produce-unsat-assumptions line: 44 position: 0+[RECV] true+[SEND] (get-option :random-seed)+[RECV] 123+[SEND] (get-option :reproducible-resource-limit)+[RECV] unsupported+[SEND] (get-option :verbosity)+[SKIP] ; :reproducible-resource-limit line: 47 position: 0+[RECV] 0+[SEND] (get-option :smt.mbqi)+[RECV] true+[SEND] (get-option :smt.mbqi)+[RECV] true+[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")+[SEND] (get-info :status)+[RECV] (:status sat)+[GOOD] (define-fun s16 () Int 4)+[GOOD] (define-fun s17 () Bool (> s0 s16))+[GOOD] (assert (! s17 :named |later, a > 4|))+[SEND] (check-sat)+[RECV] sat+[GOOD] (set-info :status unknown)+[GOOD] (define-fun s18 () Bool (> s0 s9))+[GOOD] (declare-const __assumption_proxy_s18_19 Bool)+[GOOD] (assert (= __assumption_proxy_s18_19 s18))+[SEND] (check-sat-assuming (__assumption_proxy_s18_19))+[RECV] sat+[GOOD] (declare-const __assumption_proxy_s18_20 Bool)+[GOOD] (assert (= __assumption_proxy_s18_20 s18))+[SEND] (check-sat-assuming (__assumption_proxy_s18_20))+[RECV] sat+[SEND] (get-assignment)+[RECV] ((s_1 true) (s7 true) (|a > 0| true) (s15 true) (s_2 false) (s8 true) (a+b_<_12 true) (s17 true) (|later, a > 4| true) (s18 true) (s12 true))+[SEND] (get-info :assertion-stack-levels)+[RECV] (:assertion-stack-levels 0)+[SEND] (get-info :authors)+[RECV] (:authors "Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger")+[SEND] (get-info :error-behavior)+[RECV] (:error-behavior continued-execution)+[SEND] (get-info :name)+[RECV] (:name "Z3")+[SEND] (get-info :reason-unknown)+[RECV] (:reason-unknown "unknown")+[SEND] (get-info :version)+[RECV] (:version "4.5.1")+[SEND] (get-info :memory)+[RECV] unsupported+[SEND] (get-info :time)+[SKIP] ; :memory line: 73 position: 0+[RECV] unsupported+[SEND] (get-value (s0))+[SKIP] ; :time line: 74 position: 0+[RECV] ((s0 5))+[SEND] (get-value (s1))+[RECV] ((s1 1))+[GOOD] (define-fun s21 () Int 100)+[GOOD] (define-fun s23 () Int 9)+[GOOD] (define-fun s22 () Bool (> s0 s21))+[GOOD] (define-fun s24 () Bool (> s0 s23))+[GOOD] (declare-const __assumption_proxy_s22_25 Bool)+[GOOD] (assert (= __assumption_proxy_s22_25 s22))+[GOOD] (declare-const __assumption_proxy_s24_26 Bool)+[GOOD] (assert (= __assumption_proxy_s24_26 s24))+[SEND] (check-sat-assuming (__assumption_proxy_s22_25 __assumption_proxy_s24_26))+[RECV] unsat+[SEND] (get-unsat-assumptions)+[RECV] (a+b_<_12 __assumption_proxy_s22_25)+*** In call to 'getUnsatAssumptions'+***+*** Unexpected assumption named: "a+b_<_12"+*** Was expecting one of : ["s22","s24"]+***+*** This can happen if unsat-cores are also enabled. Ignoring.+[GOOD] (push 5)+[GOOD] (pop 3)+[GOOD] (define-fun s27 () Int 6)+[GOOD] (define-fun s28 () Bool (> s0 s27))+[GOOD] (assert (! s28 :named |bey|))+[GOOD] (define-fun s29 () Bool (< s0 s27))+[GOOD] (assert (! s29 :named |hey|))+[SEND] (check-sat)+[RECV] unsat+[SEND, TimeOut: 80000ms] (get-unsat-core)+[RECV] (bey hey)+[SEND] (get-proof)+[RECV] ((set-logic ALL)+ (declare-fun bey () Bool)+ (declare-fun hey () Bool)+ (proof+ (let (($x232 (<= s0 6)))+ (let (($x233 (not $x232)))+ (let (($x236 (or (not bey) $x233)))+ (let ((@x238 (monotonicity (rewrite (= (> s0 6) $x233)) (= (or (not bey) (> s0 6)) $x236))))+ (let ((@x231 (rewrite (= (=> bey (> s0 6)) (or (not bey) (> s0 6))))))+ (let ((@x241 (mp (asserted (=> bey (> s0 6))) (trans @x231 @x238 (= (=> bey (> s0 6)) $x236)) $x236)))+ (let (($x252 (>= s0 6)))+ (let (($x250 (not $x252)))+ (let (($x254 (or (not hey) $x250)))+ (let ((@x256 (monotonicity (rewrite (= (< s0 6) $x250)) (= (or (not hey) (< s0 6)) $x254))))+ (let ((@x249 (rewrite (= (=> hey (< s0 6)) (or (not hey) (< s0 6))))))+ (let ((@x259 (mp (asserted (=> hey (< s0 6))) (trans @x249 @x256 (= (=> hey (< s0 6)) $x254)) $x254)))+ (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x252 $x232)) (unit-resolution @x259 (asserted hey) $x250) (unit-resolution @x241 (asserted bey) $x233) false)))))))))))))))+[SEND, TimeOut: 90000ms] (get-assertions)++[RECV] ((! s7 :named |a > 0|)+ s8+ s12+ (! s15 :named |a+b_<_12|)+ (! s17 :named |later, a > 4|)+ (= __assumption_proxy_s18_19 s18)+ (= __assumption_proxy_s18_20 s18)+ (= __assumption_proxy_s22_25 s22)+ (= __assumption_proxy_s24_26 s24)+ (! s28 :named |bey|)+ (! s29 :named |hey|))+[SEND] (echo "there we go")+[RECV] "there we go"+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:Satisfiable. Model:+ a = 332 :: Integer+ b = 3 :: Integer+ c = 2.3 :: Float+ d = True :: Bool+ e = 3.12 :: Real+ s5 = -12 :: Int8+DONE!
+ SBVTestSuite/GoldFiles/query_abc.gold view
@@ -0,0 +1,34 @@+** Calling: abc -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"+[ISSUE] ; Automatically generated by SBV. Do not edit.+** Skipping heart-beat for the solver ABC+** Backend solver ABC does not support global decls.+** Some incremental calls, such as pop, will be limited.+[ISSUE] (set-option :diagnostic-output-channel "stdout")+[ISSUE] (set-option :produce-models true)+[ISSUE] (set-logic QF_BV)+[ISSUE] ; --- uninterpreted sorts ---+[ISSUE] ; --- literal constants ---+[ISSUE] (define-fun s_2 () Bool false)+[ISSUE] (define-fun s_1 () Bool true)+[ISSUE] (define-fun s2 () (_ BitVec 32) #x00000000)+[ISSUE] ; --- skolem constants ---+[ISSUE] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"+[ISSUE] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"+[ISSUE] ; --- constant tables ---+[ISSUE] ; --- skolemized tables ---+[ISSUE] ; --- arrays ---+[ISSUE] ; --- uninterpreted constants ---+[ISSUE] ; --- user given axioms ---+[ISSUE] ; --- formula ---+[ISSUE] (define-fun s3 () Bool (bvsgt s0 s2))+[ISSUE] (define-fun s4 () Bool (bvsgt s1 s2))+[ISSUE] (assert s3)+[ISSUE] (assert s4)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #x1))+[SEND] (get-value (s1))+[RECV] ((s1 #x1))+*** Solver : ABC+*** Exit code: ExitSuccess
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -43,4 +43,4 @@ *** bug/feature request with the solver! CallStack (from HasCallStack):- error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.1-56ITrlqRjAjFzgs28xEVp3:Data.SBV.SMT.SMT+ error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.2-BmAQsjRcnLN24H2yOFpcOt:Data.SBV.SMT.SMT
+ SBVTestSuite/GoldFiles/query_boolector.gold view
@@ -0,0 +1,54 @@+** Calling: boolector --smt2 --smt2-model --no-exit-codes --incremental+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+** Backend solver Boolector 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 32) #x00000000)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"+[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))+[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))+[GOOD] (assert s3)+[GOOD] (assert s4)+[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)+[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)+[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))+[GOOD] (define-fun s8 () Bool (bvsle s6 s7))+[GOOD] (assert s8)+[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)+[GOOD] (define-fun s10 () Bool (bvslt s0 s9))+[GOOD] (assert s10)+[GOOD] (define-fun s11 () Bool (bvslt s1 s5))+[GOOD] (assert s11)+[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)+[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))+[GOOD] (define-fun s14 () Bool (bvslt s12 s13))+[GOOD] (assert s14)+[GOOD] (define-fun s15 () Bool (bvslt s0 s5))+[GOOD] (assert s15)+[SEND] (check-sat)+[RECV] sat+[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)+[GOOD] (define-fun s17 () Bool (bvsge s0 s16))+[GOOD] (assert s17)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #b00000000000000000000000000000001))+[SEND] (get-value (s1))+[RECV] ((s1 #b00000000000000000000000000000001))+*** Solver : Boolector+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/query_cvc4.gold view
@@ -0,0 +1,60 @@+** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[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 32) #x00000000)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"+[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))+[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))+[GOOD] (assert (! s3 :named |a > 0|))+[GOOD] (assert s4)+[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)+[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)+[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))+[GOOD] (define-fun s8 () Bool (bvsle s6 s7))+[GOOD] (assert s8)+[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)+[GOOD] (define-fun s10 () Bool (bvslt s0 s9))+[GOOD] (assert s10)+[GOOD] (define-fun s11 () Bool (bvslt s1 s5))+[GOOD] (assert s11)+[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)+[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))+[GOOD] (define-fun s14 () Bool (bvslt s12 s13))+[GOOD] (assert (! s14 :named |a+b_<_12|))+[GOOD] (push 1)+[GOOD] (define-fun s15 () Bool (bvslt s0 s5))+[GOOD] (assert s15)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (_ bv1 32)))+[GOOD] (pop 1)+[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)+[GOOD] (define-fun s17 () Bool (bvsgt s0 s16))+[GOOD] (assert (! s17 :named |extra|))+[GOOD] (assert s11)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (_ bv2 32)))+[SEND] (get-value (s1))+[RECV] ((s1 (_ bv1 32)))+*** Solver : CVC4+*** Exit code: ExitSuccess+*** Std-out :
+ SBVTestSuite/GoldFiles/query_mathsat.gold view
@@ -0,0 +1,55 @@+** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+** Backend solver MathSAT does not support global decls.+** Some incremental calls, such as pop, will be limited.+[GOOD] (set-option :diagnostic-output-channel "stdout")+[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 32) #x00000000)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"+[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))+[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))+[GOOD] (assert (! s3 :named |a > 0|))+[GOOD] (assert s4)+[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)+[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)+[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))+[GOOD] (define-fun s8 () Bool (bvsle s6 s7))+[GOOD] (assert s8)+[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)+[GOOD] (define-fun s10 () Bool (bvslt s0 s9))+[GOOD] (assert s10)+[GOOD] (define-fun s11 () Bool (bvslt s1 s5))+[GOOD] (assert s11)+[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)+[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))+[GOOD] (define-fun s14 () Bool (bvslt s12 s13))+[GOOD] (assert (! s14 :named |a+b_<_12|))+[GOOD] (define-fun s15 () Bool (bvslt s0 s5))+[GOOD] (assert s15)+[SEND] (check-sat)+[RECV] sat+[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)+[GOOD] (define-fun s17 () Bool (bvsge s0 s16))+[GOOD] (assert (! s17 :named |extra|))+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ( (s0 (_ bv1 32)) )+[SEND] (get-value (s1))+[RECV] ( (s1 (_ bv1 32)) )+*** Solver : MathSAT+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/query_yices.gold view
@@ -0,0 +1,54 @@+** 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 32) #x00000000)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () (_ BitVec 32)) ; tracks user variable "a"+[GOOD] (declare-fun s1 () (_ BitVec 32)) ; tracks user variable "b"+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s3 () Bool (bvsgt s0 s2))+[GOOD] (define-fun s4 () Bool (bvsgt s1 s2))+[GOOD] (assert (! s3 :named |a > 0|))+[GOOD] (assert s4)+[GOOD] (define-fun s5 () (_ BitVec 32) #x00000002)+[GOOD] (define-fun s7 () (_ BitVec 32) #x0000000f)+[GOOD] (define-fun s6 () (_ BitVec 32) (bvadd s0 s5))+[GOOD] (define-fun s8 () Bool (bvsle s6 s7))+[GOOD] (assert s8)+[GOOD] (define-fun s9 () (_ BitVec 32) #x00000003)+[GOOD] (define-fun s10 () Bool (bvslt s0 s9))+[GOOD] (assert s10)+[GOOD] (define-fun s11 () Bool (bvslt s1 s5))+[GOOD] (assert s11)+[GOOD] (define-fun s13 () (_ BitVec 32) #x0000000c)+[GOOD] (define-fun s12 () (_ BitVec 32) (bvadd s0 s1))+[GOOD] (define-fun s14 () Bool (bvslt s12 s13))+[GOOD] (assert (! s14 :named |a+b_<_12|))+[GOOD] (define-fun s15 () Bool (bvslt s0 s5))+[GOOD] (assert s15)+[SEND] (check-sat)+[RECV] sat+[GOOD] (define-fun s16 () (_ BitVec 32) #x00000001)+[GOOD] (define-fun s17 () Bool (bvsge s0 s16))+[GOOD] (assert (! s17 :named |extra|))+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 #b00000000000000000000000000000001))+[SEND] (get-value (s1))+[RECV] ((s1 #b00000000000000000000000000000001))+*** Solver : Yices+*** Exit code: ExitSuccess
SBVTestSuite/SBVDocTest.hs view
@@ -3,18 +3,31 @@ import System.FilePath.Glob (glob) import Test.DocTest (doctest) +import Data.Char (toLower)+import Data.List (isSuffixOf)+ import System.Exit (exitSuccess) -import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..))+import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), CIOS(..)) main :: IO ()-main = do testEnv <- getTestEnvironment+main = do (testEnv, _) <- getTestEnvironment putStrLn $ "SBVDocTest: Test platform: " ++ show testEnv case testEnv of- TestEnvLocal -> runDocTest- TestEnvTravis _ -> runDocTest- TestEnvUnknown -> do putStrLn "Unknown test environment, skipping doctests"- exitSuccess- where runDocTest = glob "Data/SBV/**/*.hs" >>= doctest+ TestEnvLocal -> runDocTest False+ TestEnvCI CIWindows -> runDocTest True+ TestEnvCI _ -> runDocTest False+ TestEnvUnknown -> do putStrLn "Unknown test environment, skipping doctests"+ exitSuccess+ where runDocTest windowsSkip = do allFiles <- glob "Data/SBV/**/*.hs"+ let testFiles+ | windowsSkip = filter (not . bad) allFiles+ | True = allFiles+ doctest testFiles++ -- The following test has a path encoded in its output, and hence fails on Windows+ -- since it has the c:\blah\blah format. Skip it:+ bad fn = "nodiv0.hs" `isSuffixOf` map toLower fn+
SBVTestSuite/SBVHLint.hs view
@@ -14,15 +14,15 @@ main :: IO () main = do- testEnv <- getTestEnvironment+ (testEnv, _) <- getTestEnvironment putStrLn $ "SBVHLint: Test platform: " ++ show testEnv case testEnv of- TestEnvLocal -> runHLint- TestEnvTravis _ -> runHLint- TestEnvUnknown -> do putStrLn "Unknown test environment, skipping hlint run"- exitSuccess+ TestEnvLocal -> runHLint+ TestEnvCI{} -> runHLint+ TestEnvUnknown -> do putStrLn "Unknown test environment, skipping hlint run"+ exitSuccess where runHLint = do hints <- hlint arguments if null hints then exitSuccess
SBVTestSuite/SBVTest.hs view
@@ -3,7 +3,7 @@ import Test.Tasty -import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), TravisOS(..), pickTests)+import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), CIOS(..), pickTests) import System.Exit (exitSuccess) @@ -21,6 +21,7 @@ import qualified TestSuite.Basics.QRem import qualified TestSuite.Basics.Quantifiers import qualified TestSuite.Basics.Recursive+import qualified TestSuite.Basics.SmallShifts import qualified TestSuite.Basics.SquashReals import qualified TestSuite.Basics.TOut import qualified TestSuite.BitPrecise.BitTricks@@ -48,6 +49,7 @@ import qualified TestSuite.Optimization.Basics import qualified TestSuite.Optimization.Combined import qualified TestSuite.Optimization.ExtensionField+import qualified TestSuite.Optimization.Quantified import qualified TestSuite.Optimization.Reals import qualified TestSuite.Polynomials.Polynomials import qualified TestSuite.Puzzles.Coins@@ -78,101 +80,112 @@ import qualified TestSuite.Uninterpreted.Sort import qualified TestSuite.Uninterpreted.Uninterpreted --- On Travis, the build machines are subject to time-out limits. So, we cannot really run--- everything yet remain within the timeout bounds. Here, we randomly pick a subset; with--- the hope that over many runs this tests larger parts of the test-suite.-travisFilter :: TravisOS -> TestTree -> IO TestTree-travisFilter te tt = do putStrLn $ "Travis: Reducing tests by " ++ show (100-p) ++ "% for running on " ++ show te- pickTests p tt- where p = case te of- TravisLinux -> 30- TravisOSX -> 10- TravisWindows -> 100 -- Travis doesn't actually have Windows, just keep this at 100 for now.+-- On remote machines for Appveyor/Travis, the build machines doesn't have enough memory+-- and/or powerful enough to run our heavy tests; so we skip tests for Windows hosts and+-- reduce them for OSX. For Linux, we run them all. Note that this is only for remote+-- hosts; when we run locally, all tests are run.+--+-- TODO: Would be nice to run them all on Windows/OSX on remote hosts as well.+ciFilter :: CIOS -> Int -> TestTree -> IO TestTree+ciFilter _ 100 tt = return tt+ciFilter os n tt = do putStrLn $ "OS: " ++ show os ++ ", Running only " ++ show n ++ "% of tests."+ pickTests n tt main :: IO ()-main = do testEnv <- getTestEnvironment+main = do (testEnv, testPercentage) <- getTestEnvironment putStrLn $ "SBVTest: Test platform: " ++ show testEnv - let allTestCases = testGroup "Tests" [tc | (_, tc) <- allTests]- allTravisTestCases = testGroup "Tests" [tc | (True, tc) <- allTests]- case testEnv of- TestEnvLocal -> defaultMain allTestCases- TestEnvTravis os -> defaultMain =<< travisFilter os allTravisTestCases TestEnvUnknown -> do putStrLn "Unknown test environment, skipping tests" exitSuccess --- If the first Bool is True, then that test can run on Travis-allTests :: [(Bool, TestTree)]-allTests = [ (True, TestSuite.Arrays.Memory.tests)- , (True, TestSuite.Basics.AllSat.tests)- , (True, TestSuite.Basics.ArithNoSolver.tests)- , (True, TestSuite.Basics.ArithSolver.tests)- , (True, TestSuite.Basics.BasicTests.tests)- , (True, TestSuite.Basics.GenBenchmark.tests)- , (True, TestSuite.Basics.Higher.tests)- , (True, TestSuite.Basics.Index.tests)- , (True, TestSuite.Basics.IteTest.tests)- , (True, TestSuite.Basics.ProofTests.tests)- , (True, TestSuite.Basics.PseudoBoolean.tests)- , (True, TestSuite.Basics.QRem.tests)- , (True, TestSuite.Basics.Quantifiers.tests)- , (True, TestSuite.Basics.Recursive.tests)- , (True, TestSuite.Basics.SquashReals.tests)- , (True, TestSuite.Basics.TOut.tests)- , (True, TestSuite.BitPrecise.BitTricks.tests)- , (True, TestSuite.BitPrecise.Legato.tests)- , (True, TestSuite.BitPrecise.MergeSort.tests)- , (True, TestSuite.BitPrecise.PrefixSum.tests)- , (True, TestSuite.CodeGeneration.AddSub.tests)- , (True, TestSuite.CodeGeneration.CgTests.tests)- , (True, TestSuite.CodeGeneration.CRC_USB5.tests)- , (True, TestSuite.CodeGeneration.Fibonacci.tests)- , (True, TestSuite.CodeGeneration.Floats.tests)- , (True, TestSuite.CodeGeneration.GCD.tests)- , (True, TestSuite.CodeGeneration.PopulationCount.tests)- , (True, TestSuite.CodeGeneration.Uninterpreted.tests)- , (True, TestSuite.CRC.CCITT.tests)- , (True, TestSuite.CRC.CCITT_Unidir.tests)- , (True, TestSuite.CRC.GenPoly.tests)- , (True, TestSuite.CRC.Parity.tests)- , (True, TestSuite.CRC.USB5.tests)- , (True, TestSuite.Crypto.AES.tests)- , (True, TestSuite.Crypto.RC4.tests)- , (True, TestSuite.Existentials.CRCPolynomial.tests)- , (True, TestSuite.GenTest.GenTests.tests)- , (True, TestSuite.Optimization.AssertSoft.tests)- , (True, TestSuite.Optimization.Basics.tests)- , (True, TestSuite.Optimization.Combined.tests)- , (True, TestSuite.Optimization.ExtensionField.tests)- , (True, TestSuite.Optimization.Reals.tests)- , (True, TestSuite.Polynomials.Polynomials.tests)- , (True, TestSuite.Puzzles.Coins.tests)- , (True, TestSuite.Puzzles.Counts.tests)- , (True, TestSuite.Puzzles.DogCatMouse.tests)- , (True, TestSuite.Puzzles.Euler185.tests)- , (True, TestSuite.Puzzles.MagicSquare.tests)- , (True, TestSuite.Puzzles.NQueens.tests)- , (True, TestSuite.Puzzles.PowerSet.tests)- , (True, TestSuite.Puzzles.Sudoku.tests)- , (True, TestSuite.Puzzles.Temperature.tests)- , (True, TestSuite.Puzzles.U2Bridge.tests)- , (False, TestSuite.Queries.BasicQuery.tests)- , (False, TestSuite.Queries.BadOption.tests)- , (True, TestSuite.Queries.Enums.tests)- , (True, TestSuite.Queries.FreshVars.tests)- , (False, TestSuite.Queries.Int_ABC.tests)- , (False, TestSuite.Queries.Int_Boolector.tests)- , (False, TestSuite.Queries.Int_CVC4.tests)- , (False, TestSuite.Queries.Int_Mathsat.tests)- , (False, TestSuite.Queries.Int_Yices.tests)- , (True, TestSuite.Queries.Int_Z3.tests)- , (True, TestSuite.Queries.Interpolants.tests)- , (True, TestSuite.Queries.Uninterpreted.tests)- , (True, TestSuite.Uninterpreted.AUF.tests)- , (True, TestSuite.Uninterpreted.Axioms.tests)- , (True, TestSuite.Uninterpreted.Function.tests)- , (True, TestSuite.Uninterpreted.Sort.tests)- , (True, TestSuite.Uninterpreted.Uninterpreted.tests)- ]+ TestEnvLocal -> defaultMain $ testGroup "Local" [heavyTests, localOnlyTests, otherTests]++ TestEnvCI os -> do reducedHeavyTests <- ciFilter os testPercentage heavyTests+ defaultMain $ testGroup "Remote" [reducedHeavyTests, otherTests]++-- | The following tests take too long/too burdensome for remote tests, so we run only a percentage of them+heavyTests :: TestTree+heavyTests = testGroup "SBVHeavyTests" [TestSuite.Basics.ArithSolver.tests]++-- | The following tests can only be run locally+localOnlyTests :: TestTree+localOnlyTests = testGroup "SBVLocalOnlyTests" [+ TestSuite.Queries.BasicQuery.tests+ , TestSuite.Queries.BadOption.tests+ , TestSuite.Queries.Int_ABC.tests+ , TestSuite.Queries.Int_Boolector.tests+ , TestSuite.Queries.Int_CVC4.tests+ , TestSuite.Queries.Int_Mathsat.tests+ , TestSuite.Queries.Int_Yices.tests+ ]++-- | Remaining tests+otherTests :: TestTree+otherTests = testGroup "SBVOtherTests" [+ TestSuite.Arrays.Memory.tests+ , TestSuite.Basics.AllSat.tests+ , TestSuite.Basics.ArithNoSolver.tests+ , TestSuite.Basics.BasicTests.tests+ , TestSuite.Basics.GenBenchmark.tests+ , TestSuite.Basics.Higher.tests+ , TestSuite.Basics.Index.tests+ , TestSuite.Basics.IteTest.tests+ , TestSuite.Basics.ProofTests.tests+ , TestSuite.Basics.PseudoBoolean.tests+ , TestSuite.Basics.QRem.tests+ , TestSuite.Basics.Quantifiers.tests+ , TestSuite.Basics.Recursive.tests+ , TestSuite.Basics.SmallShifts.tests+ , TestSuite.Basics.SquashReals.tests+ , TestSuite.Basics.TOut.tests+ , TestSuite.BitPrecise.BitTricks.tests+ , TestSuite.BitPrecise.Legato.tests+ , TestSuite.BitPrecise.MergeSort.tests+ , TestSuite.BitPrecise.PrefixSum.tests+ , TestSuite.CodeGeneration.AddSub.tests+ , TestSuite.CodeGeneration.CgTests.tests+ , TestSuite.CodeGeneration.CRC_USB5.tests+ , TestSuite.CodeGeneration.Fibonacci.tests+ , TestSuite.CodeGeneration.Floats.tests+ , TestSuite.CodeGeneration.GCD.tests+ , TestSuite.CodeGeneration.PopulationCount.tests+ , TestSuite.CodeGeneration.Uninterpreted.tests+ , TestSuite.CRC.CCITT.tests+ , TestSuite.CRC.CCITT_Unidir.tests+ , TestSuite.CRC.GenPoly.tests+ , TestSuite.CRC.Parity.tests+ , TestSuite.CRC.USB5.tests+ , TestSuite.Crypto.AES.tests+ , TestSuite.Crypto.RC4.tests+ , TestSuite.Existentials.CRCPolynomial.tests+ , TestSuite.GenTest.GenTests.tests+ , TestSuite.Optimization.AssertSoft.tests+ , TestSuite.Optimization.Basics.tests+ , TestSuite.Optimization.Combined.tests+ , TestSuite.Optimization.ExtensionField.tests+ , TestSuite.Optimization.Quantified.tests+ , TestSuite.Optimization.Reals.tests+ , TestSuite.Polynomials.Polynomials.tests+ , TestSuite.Puzzles.Coins.tests+ , TestSuite.Puzzles.Counts.tests+ , TestSuite.Puzzles.DogCatMouse.tests+ , TestSuite.Puzzles.Euler185.tests+ , TestSuite.Puzzles.MagicSquare.tests+ , TestSuite.Puzzles.NQueens.tests+ , TestSuite.Puzzles.PowerSet.tests+ , TestSuite.Puzzles.Sudoku.tests+ , TestSuite.Puzzles.Temperature.tests+ , TestSuite.Puzzles.U2Bridge.tests+ , TestSuite.Queries.Enums.tests+ , TestSuite.Queries.FreshVars.tests+ , TestSuite.Queries.Int_Z3.tests+ , TestSuite.Queries.Interpolants.tests+ , TestSuite.Queries.Uninterpreted.tests+ , TestSuite.Uninterpreted.AUF.tests+ , TestSuite.Uninterpreted.Axioms.tests+ , TestSuite.Uninterpreted.Function.tests+ , TestSuite.Uninterpreted.Sort.tests+ , TestSuite.Uninterpreted.Uninterpreted.tests+ ]
SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs view
@@ -10,18 +10,18 @@ -- the constant folding based arithmetic implementation in SBV ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE TupleSections #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TupleSections #-} module TestSuite.Basics.ArithNoSolver(tests) where +import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord)+ import Data.SBV.Internals-import Data.Maybe(fromJust, fromMaybe) import Utils.SBVTestFramework-import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) -ghcBitSize :: Bits a => a -> Int-ghcBitSize x = fromMaybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") (bitSizeMaybe x)+import Data.Maybe (fromJust, isJust) -- Test suite tests :: TestTree@@ -29,33 +29,36 @@ genReals ++ genFloats ++ genQRems- ++ genBinTest "+" (+)- ++ genBinTest "-" (-)- ++ genBinTest "*" (*)- ++ genUnTest "negate" negate- ++ genUnTest "abs" abs- ++ genUnTest "signum" signum- ++ genBinTest ".&." (.&.)- ++ genBinTest ".|." (.|.)- ++ genBoolTest "<" (<) (.<)- ++ genBoolTest "<=" (<=) (.<=)- ++ genBoolTest ">" (>) (.>)- ++ genBoolTest ">=" (>=) (.>=)- ++ genBoolTest "==" (==) (.==)- ++ genBoolTest "/=" (/=) (./=)- ++ genBinTest "xor" xor- ++ genUnTest "complement" complement- ++ genIntTest "shift" shift- ++ genIntTest "rotate" rotate- ++ genIntTestS "setBit" setBit- ++ genIntTestS "clearBit" clearBit- ++ genIntTestS "complementBit" complementBit- ++ genIntTest "shift" shift- ++ genIntTestS "shiftL" shiftL- ++ genIntTestS "shiftR" shiftR- ++ genIntTest "rotate" rotate- ++ genIntTestS "rotateL" rotateL- ++ genIntTestS "rotateR" rotateR+ ++ genBinTest "+" (+)+ ++ genBinTest "-" (-)+ ++ genBinTest "*" (*)+ ++ genUnTest "negate" negate+ ++ genUnTest "abs" abs+ ++ genUnTest "signum" signum+ ++ genBinTest ".&." (.&.)+ ++ genBinTest ".|." (.|.)+ ++ genBoolTest "<" (<) (.<)+ ++ genBoolTest "<=" (<=) (.<=)+ ++ genBoolTest ">" (>) (.>)+ ++ genBoolTest ">=" (>=) (.>=)+ ++ genBoolTest "==" (==) (.==)+ ++ genBoolTest "/=" (/=) (./=)+ ++ genBinTest "xor" xor+ ++ genUnTest "complement" complement+ ++ genIntTest False "setBit" setBit+ ++ genIntTest False "clearBit" clearBit+ ++ genIntTest False "complementBit" complementBit+ ++ genIntTest True "shift" shift+ ++ genIntTest True "shiftL" shiftL+ ++ genIntTest True "shiftR" shiftR+ ++ genIntTest True "rotate" rotate+ ++ genIntTest True "rotateL" rotateL+ ++ genIntTest True "rotateR" rotateR+ ++ genShiftRotTest "shiftL_gen" sShiftLeft+ ++ genShiftRotTest "shiftR_gen" sShiftRight+ ++ genShiftRotTest "rotateL_gen" sRotateLeft+ ++ genShiftRotTest "rotateR_gen" sRotateRight+ ++ genShiftMixSize ++ genBlasts ++ genIntCasts @@ -101,34 +104,70 @@ where pair (x, a) b = (x, show (fromIntegral a `asTypeOf` b) == show b) mkTest (x, s) = testCase ("arithCF-" ++ nm ++ "." ++ x) (s `showsAs` "True") -genIntTest :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [TestTree]-genIntTest nm op = map mkTest $- zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- is] [x `op` y | x <- sw8s, y <- is]- ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is] [x `op` y | x <- sw16s, y <- is]- ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is] [x `op` y | x <- sw32s, y <- is]- ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is] [x `op` y | x <- sw64s, y <- is]- ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- is] [x `op` y | x <- si8s, y <- is]- ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is] [x `op` y | x <- si16s, y <- is]- ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is] [x `op` y | x <- si32s, y <- is]- ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is] [x `op` y | x <- si64s, y <- is]- ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- is] [x `op` y | x <- siUBs, y <- is]- where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)+genIntTest :: Bool -> String -> (forall a. (Num a, Bits a) => (a -> Int -> a)) -> [TestTree]+genIntTest overSized nm op = map mkTest $+ zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- is (intSizeOf x)] [x `op` y | x <- sw8s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is (intSizeOf x)] [x `op` y | x <- sw16s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is (intSizeOf x)] [x `op` y | x <- sw32s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is (intSizeOf x)] [x `op` y | x <- sw64s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- is (intSizeOf x)] [x `op` y | x <- si8s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is (intSizeOf x)] [x `op` y | x <- si16s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is (intSizeOf x)] [x `op` y | x <- si32s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is (intSizeOf x)] [x `op` y | x <- si64s, y <- is (intSizeOf x)]+ ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0..10]] [x `op` y | x <- siUBs, y <- [0..10]]+ where is sz = [0 .. sz - 1] ++ extras+ where extras+ | overSized = map (sz +) ([0 .. 1] ++ [sz, sz+1])+ | True = []+ pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b) mkTest (t, x, y, a, b, s) = testCase ("arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b) (s `showsAs` "True")- is = [-10 .. 10] -genIntTestS :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [TestTree]-genIntTestS nm op = map mkTest $- zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (ghcBitSize x - 1)]]- ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]] [x `op` y | x <- siUBs, y <- [0 .. 10 ]]- where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)+genShiftRotTest :: String -> (forall a. (SIntegral a, SDivisible (SBV a)) => (SBV a -> SBV a -> SBV a)) -> [TestTree]+genShiftRotTest nm op = map mkTest $+ zipWith pair [("u8", show x, show y, literal x `op` y) | x <- w8s, y <- is (intSizeOf x)] [x `op` y | x <- sw8s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u16", show x, show y, literal x `op` y) | x <- w16s, y <- is (intSizeOf x)] [x `op` y | x <- sw16s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u32", show x, show y, literal x `op` y) | x <- w32s, y <- is (intSizeOf x)] [x `op` y | x <- sw32s, y <- is (intSizeOf x)]+ ++ zipWith pair [("u64", show x, show y, literal x `op` y) | x <- w64s, y <- is (intSizeOf x)] [x `op` y | x <- sw64s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s8", show x, show y, literal x `op` y) | x <- i8s, y <- is (intSizeOf x)] [x `op` y | x <- si8s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s16", show x, show y, literal x `op` y) | x <- i16s, y <- is (intSizeOf x)] [x `op` y | x <- si16s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s32", show x, show y, literal x `op` y) | x <- i32s, y <- is (intSizeOf x)] [x `op` y | x <- si32s, y <- is (intSizeOf x)]+ ++ zipWith pair [("s64", show x, show y, literal x `op` y) | x <- i64s, y <- is (intSizeOf x)] [x `op` y | x <- si64s, y <- is (intSizeOf x)]+ -- NB. No generic shift/rotate for SMTLib unbounded integers+ where is sz = let b :: Word32+ b = fromIntegral sz+ in map (sFromIntegral . literal) $ [0 .. b - 1] ++ [b, b+1, 2*b, 2*b+1]+ pair (t, x, y, a) b = (t, x, y, show a, show b, isJust (unliteral a) && isJust (unliteral b) && unliteral a == unliteral b) mkTest (t, x, y, a, b, s) = testCase ("arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b) (s `showsAs` "True")++-- A few tests for mixed-size shifts+genShiftMixSize :: [TestTree]+genShiftMixSize = map mkTest $+ map pair [(show x, show y, "shl_w8_w16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w8s, y <- yw16s]+ ++ map pair [(show x, show y, "shr_w8_w16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w8s, y <- yw16s]+ ++ map pair [(show x, show y, "shl_w16_w8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w16s, y <- w8s]+ ++ map pair [(show x, show y, "shr_w16_w8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w16s, y <- w8s]+ ++ map pair [(show x, show y, "shl_i8_i16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i8s, y <- yi16s]+ ++ map pair [(show x, show y, "shr_i8_i16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i8s, y <- yi16s]+ ++ map pair [(show x, show y, "shl_i16_i8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i16s, y <- i8s, y >= 0]+ ++ map pair [(show x, show y, "shr_i16_i8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i16s, y <- i8s, y >= 0]+ ++ map pair [(show x, show y, "shl_w8_i16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w8s, y <- yi16s]+ ++ map pair [(show x, show y, "shr_w8_i16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w8s, y <- yi16s]+ ++ map pair [(show x, show y, "shl_w16_i8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- w16s, y <- i8s, y >= 0]+ ++ map pair [(show x, show y, "shr_w16_i8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- w16s, y <- i8s, y >= 0]+ ++ map pair [(show x, show y, "shl_i8_w16", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i8s, y <- yw16s]+ ++ map pair [(show x, show y, "shr_i8_w16", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i8s, y <- yw16s]+ ++ map pair [(show x, show y, "shl_i16_w8", literal x `sShiftLeft` literal y, x `shiftL` fromIntegral y) | x <- i16s, y <- w8s]+ ++ map pair [(show x, show y, "shr_i16_w8", literal x `sShiftRight` literal y, x `shiftR` fromIntegral y) | x <- i16s, y <- w8s]+ where pair :: (SymWord a, Show a) => (String, String, String, SBV a, a) -> (String, Bool)+ pair (x, y, l, sr, lr) = (l ++ "." ++ x ++ "_" ++ y ++ "_" ++ show (unliteral sr) ++ "_" ++ show lr, isJust (unliteral sr) && unliteral sr == Just lr)+ mkTest (l, s) = testCase ("arithCF-genShiftMixSize" ++ l) (s `showsAs` "True")++ yi16s :: [Int16]+ yi16s = [0, 255, 256, 257, maxBound]++ yw16s :: [Word16]+ yw16s = [0, 255, 256, 257, maxBound]+ genBlasts :: [TestTree] genBlasts = map mkTest $
SBVTestSuite/TestSuite/Basics/ArithSolver.hs view
@@ -11,19 +11,16 @@ -- constant folding. ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleContexts #-} module TestSuite.Basics.ArithSolver(tests) where -import Data.Maybe (fromMaybe) import qualified Data.Binary.IEEE754 as DB (wordToFloat, wordToDouble, floatToWord, doubleToWord) import Data.SBV.Internals import Utils.SBVTestFramework -ghcBitSize :: Bits a => a -> Int-ghcBitSize x = fromMaybe (error "SBV.ghcBitSize: Unexpected non-finite usage!") (bitSizeMaybe x)- -- Test suite tests :: TestTree tests =@@ -33,33 +30,36 @@ ++ genDoubles ++ genFPConverts ++ genQRems- ++ genBinTest True "+" (+)- ++ genBinTest True "-" (-)- ++ genBinTest True "*" (*)- ++ genUnTest True "negate" negate- ++ genUnTest True "abs" abs- ++ genUnTest True "signum" signum- ++ genBinTest False ".&." (.&.)- ++ genBinTest False ".|." (.|.)- ++ genBoolTest "<" (<) (.<)- ++ genBoolTest "<=" (<=) (.<=)- ++ genBoolTest ">" (>) (.>)- ++ genBoolTest ">=" (>=) (.>=)- ++ genBoolTest "==" (==) (.==)- ++ genBoolTest "/=" (/=) (./=)- ++ genBinTest False "xor" xor- ++ genUnTest False "complement" complement- ++ genIntTest "shift" shift- ++ genIntTest "rotate" rotate- ++ genIntTestS False "setBit" setBit- ++ genIntTestS False "clearBit" clearBit- ++ genIntTestS False "complementBit" complementBit- ++ genIntTest "shift" shift- ++ genIntTestS True "shiftL" shiftL- ++ genIntTestS True "shiftR" shiftR- ++ genIntTest "rotate" rotate- ++ genIntTestS True "rotateL" rotateL- ++ genIntTestS True "rotateR" rotateR+ ++ genBinTest True "+" (+)+ ++ genBinTest True "-" (-)+ ++ genBinTest True "*" (*)+ ++ genUnTest True "negate" negate+ ++ genUnTest True "abs" abs+ ++ genUnTest True "signum" signum+ ++ genBinTest False ".&." (.&.)+ ++ genBinTest False ".|." (.|.)+ ++ genBoolTest "<" (<) (.<)+ ++ genBoolTest "<=" (<=) (.<=)+ ++ genBoolTest ">" (>) (.>)+ ++ genBoolTest ">=" (>=) (.>=)+ ++ genBoolTest "==" (==) (.==)+ ++ genBoolTest "/=" (/=) (./=)+ ++ genBinTest False "xor" xor+ ++ genUnTest False "complement" complement+ ++ genIntTest False "setBit" setBit+ ++ genIntTest False "clearBit" clearBit+ ++ genIntTest False "complementBit" complementBit+ ++ genIntTest True "shift" shift+ ++ genIntTest True "shiftL" shiftL+ ++ genIntTest True "shiftR" shiftR+ ++ genIntTest True "rotate" rotate+ ++ genIntTest True "rotateL" rotateL+ ++ genIntTest True "rotateR" rotateR+ ++ genShiftRotTest "shiftL_gen" sShiftLeft+ ++ genShiftRotTest "shiftR_gen" sShiftRight+ ++ genShiftRotTest "rotateL_gen" sRotateLeft+ ++ genShiftRotTest "rotateR_gen" sRotateRight+ ++ genShiftMixSize ++ genBlasts ++ genIntCasts) @@ -110,37 +110,82 @@ constrain $ a .== literal x return $ literal r .== op a -genIntTest :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [TestTree]-genIntTest nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is]- ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is]- ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is]- ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is]- ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- is]- ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is]- ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is]- ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is]- ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is]- where mkTest (l, x, y, t) = testCase ("genIntTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y) (assert t)- is = [-10 .. 10]+genIntTest :: Bool -> String -> (forall a. (Num a, Bits a) => (a -> Int -> a)) -> [TestTree]+genIntTest overSized nm op = map mkTest $+ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is (intSizeOf x)]+ ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is (intSizeOf x)]+ ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is (intSizeOf x)]+ ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is (intSizeOf x)]+ ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- is (intSizeOf x)]+ ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is (intSizeOf x)]+ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is (intSizeOf x)]+ ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is (intSizeOf x)]+ -- No size based tests for unbounded integers+ where is sz = [0 .. sz - 1] ++ extras+ where extras+ | overSized = map (sz +) ([0 .. 1] ++ [sz, sz+1])+ | True = []+ mkTest (l, x, y, t) = testCase ("genIntTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y) (assert t) mkThm2 x y r = isTheorem $ do a <- free "x" constrain $ a .== literal x return $ literal r .== a `op` y +genShiftRotTest :: String -> (forall a. (SIntegral a, SDivisible (SBV a)) => (SBV a -> SBV a -> SBV a)) -> [TestTree]+genShiftRotTest nm op = map mkTest $+ [("u8", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w8s, y <- is (intSizeOf x)]+ ++ [("u16", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w16s, y <- is (intSizeOf x)]+ ++ [("u32", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w32s, y <- is (intSizeOf x)]+ ++ [("u64", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- w64s, y <- is (intSizeOf x)]+ ++ [("s8", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i8s, y <- is (intSizeOf x)]+ ++ [("s16", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i16s, y <- is (intSizeOf x)]+ ++ [("s32", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i32s, y <- is (intSizeOf x)]+ ++ [("s64", show x, show y, mkThm2 x (fromIntegral y) (literal x `op` sFromIntegral (literal y))) | x <- i64s, y <- is (intSizeOf x)]+ -- NB. No generic shift/rotate for SMTLib unbounded integers+ where is sz = let b :: Word32+ b = fromIntegral sz+ in [0 .. b - 1] ++ [b, b+1, 2*b, 2*b+1]+ mkTest (l, x, y, t) = testCase ("genShiftRotTest.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y) (assert t)+ mkThm2 x y sr+ | Just r <- unliteral sr+ = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `op` b+ | True+ = return False -genIntTestS :: Bool -> String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [TestTree]-genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (ghcBitSize x - 1)]]- ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]]- where mkTest (l, x, y, t) = testCase ("genIntTestS.arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y) (assert t)- mkThm2 x y r = isTheorem $ do a <- free "x"- constrain $ a .== literal x- return $ literal r .== a `op` y+-- A few tests for mixed-size shifts+genShiftMixSize :: [TestTree]+genShiftMixSize = map mkTest $ [(show x, show y, "shl_w8_w16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w8s, y <- yw16s]+ ++ [(show x, show y, "shr_w8_w16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w8s, y <- yw16s]+ ++ [(show x, show y, "shl_w16_w8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w16s, y <- w8s]+ ++ [(show x, show y, "shr_w16_w8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w16s, y <- w8s]+ ++ [(show x, show y, "shl_i8_i16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i8s, y <- yi16s]+ ++ [(show x, show y, "shr_i8_i16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i8s, y <- yi16s]+ ++ [(show x, show y, "shl_i16_i8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i16s, y <- i8s, y >= 0]+ ++ [(show x, show y, "shr_i16_i8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i16s, y <- i8s, y >= 0]+ ++ [(show x, show y, "shl_w8_i16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w8s, y <- yi16s]+ ++ [(show x, show y, "shr_w8_i16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w8s, y <- yi16s]+ ++ [(show x, show y, "shl_w16_i8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- w16s, y <- i8s, y >= 0]+ ++ [(show x, show y, "shr_w16_i8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- w16s, y <- i8s, y >= 0]+ ++ [(show x, show y, "shl_i8_w16", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i8s, y <- yw16s]+ ++ [(show x, show y, "shr_i8_w16", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i8s, y <- yw16s]+ ++ [(show x, show y, "shl_i16_w8", mk sShiftLeft x y (x `shiftL` fromIntegral y)) | x <- i16s, y <- w8s]+ ++ [(show x, show y, "shr_i16_w8", mk sShiftRight x y (x `shiftR` fromIntegral y)) | x <- i16s, y <- w8s]+ where yi16s :: [Int16]+ yi16s = [0, 255, 256, 257, maxBound]++ yw16s :: [Word16]+ yw16s = [0, 255, 256, 257, maxBound]++ mkTest (x, y, l, t) = testCase ("genShiftMixSize." ++ l ++ "." ++ x ++ "_" ++ y) (assert t)+ mk :: (SymWord a, SymWord b) => (SBV a -> SBV b -> SBV a) -> a -> b -> a -> IO Bool+ mk o x y r+ = isTheorem $ do a <- free "x"+ b <- free "y"+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `o` b genBlasts :: [TestTree] genBlasts = map mkTest $ [(show x, mkThm fromBitsLE blastLE x) | x <- w8s ]
+ SBVTestSuite/TestSuite/Basics/SmallShifts.hs view
@@ -0,0 +1,60 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.SmallShift+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Testing small-shift amounts using the dynamic interface. See+-- https://github.com/LeventErkok/sbv/issues/323 for the genesis.+-----------------------------------------------------------------------------++module TestSuite.Basics.SmallShifts(tests) where++import Utils.SBVTestFramework hiding (proveWith)++import Control.Monad.Reader (ask)+import Control.Monad.Trans (liftIO)+import Data.SBV.Dynamic++k1, k32, k33 :: Kind+k1 = KBounded False 1+k32 = KBounded False 32+k33 = KBounded False 33+type SW32 = SVal+type SW33 = SVal+type SW1 = SVal++b0 :: SW1+b0 = svInteger k1 0++b1 :: SW1+b1 = svInteger k1 1++average33 :: SW32 -> SW32 -> SW32+average33 x y = svExtract 31 0 (z' `svDivide` svInteger k33 2)+ where z' :: SW33+ z' = (b0 `svJoin` x) `svPlus` (b0 `svJoin` y)++average4 :: SW32 -> SW32 -> SW32+average4 x y = ((x `svShiftRight` b1) `svPlus` (y `svShiftRight` b1))+ `svPlus` (x `svAnd` (y `svAnd` svInteger k32 1))++prop :: Symbolic SVal+prop = do x <- ask >>= liftIO . svMkSymVar Nothing k32 (Just "x")+ y <- ask >>= liftIO . svMkSymVar Nothing k32 (Just "y")+ return $ average33 x y `svEqual` average4 x y++checkThm :: ThmResult -> Assertion+checkThm r = assert isThm+ where isThm = case r of+ ThmResult Unsatisfiable{} -> return True :: IO Bool+ ThmResult Satisfiable{} -> return False+ _ -> error "checkThm: Unexpected result!"++-- Test suite+tests :: TestTree+tests = testGroup "Basics.SmallShifts"+ [ testCase "smallShift" $ checkThm =<< proveWith z3 prop+ ]
+ SBVTestSuite/TestSuite/Optimization/Quantified.hs view
@@ -0,0 +1,81 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Optimization.Quantified+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for optimization iwth quantifiers+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module TestSuite.Optimization.Quantified(tests) where++import Data.List (isPrefixOf)++import Utils.SBVTestFramework+import qualified Control.Exception as C++-- Test suite+tests :: TestTree+tests =+ testGroup "Optimization.Reals"+ [ goldenString "optQuant1" $ optE q1+ , goldenVsStringShow "optQuant2" $ opt q2+ , goldenVsStringShow "optQuant3" $ opt q3+ , goldenVsStringShow "optQuant4" $ opt q4+ , goldenString "optQuant5" $ optE q5+ ]+ where opt = optimize Lexicographic+ optE q = (show <$> optimize Lexicographic q) `C.catch` (\(e::C.SomeException) -> return (pick (show e)))+ pick s = unlines [l | l <- lines s, "***" `isPrefixOf` l]++q1 :: Goal+q1 = do a <- sInteger "a"+ [b1, b2] <- sIntegers ["b1", "b2"]+ x <- forall "x" :: Symbolic SInteger+ constrain $ 2 * (a * x + b1) .== 2+ constrain $ 4 * (a * x + b2) .== 4+ constrain $ a .>= 0+ minimize "goal" $ 2*x++q2 :: Goal+q2 = do a <- sInteger "a"+ [b1, b2] <- sIntegers ["b1", "b2"]+ x <- forall "x" :: Symbolic SInteger+ constrain $ 2 * (a * x + b1) .== 2+ constrain $ 4 * (a * x + b2) .== 4+ constrain $ a .>= 0+ minimize "goal" a++q3 :: Goal+q3 = do a <- sInteger "a"+ [b1, b2] <- sIntegers ["b1", "b2"]+ minimize "goal" a+ x <- forall "x" :: Symbolic SInteger+ constrain $ 2 * (a * x + b1) .== 2+ constrain $ 4 * (a * x + b2) .== 4+ constrain $ a .>= 0++q4 :: Goal+q4 = do a <- sInteger "a"+ [b1, b2] <- sIntegers ["b1", "b2"]+ minimize "goal" $ 2*a+ x <- forall "x" :: Symbolic SInteger+ constrain $ 2 * (a * x + b1) .== 2+ constrain $ 4 * (a * x + b2) .== 4+ constrain $ a .>= 0++q5 :: Goal+q5 = do a <- sInteger "a"+ x <- forall "x" :: Symbolic SInteger+ y <- forall "y" :: Symbolic SInteger+ b <- sInteger "b"+ constrain $ a .>= 0+ constrain $ b .>= 0+ constrain $ x+y .>= 0+ minimize "goal" $ a+b++{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
SBVTestSuite/TestSuite/Queries/BasicQuery.hs view
@@ -21,7 +21,7 @@ tests :: TestTree tests = testGroup "Basics.Query"- [ goldenCapturedIO "noTravis_query1" testQuery+ [ goldenCapturedIO "query1" testQuery ] testQuery :: FilePath -> IO ()@@ -116,10 +116,10 @@ namedConstraint "bey" $ a .> literal (av + bv) namedConstraint "hey" $ a .< literal (av + bv) _ <- checkSat- _ <- timeout 4000 getUnsatCore+ _ <- timeout 80000 getUnsatCore _ <- getProof- _ <- timeout 6000 getAssertions+ _ <- timeout 90000 getAssertions echo "there we go"
SBVTestSuite/TestSuite/Queries/Int_ABC.hs view
@@ -22,7 +22,7 @@ tests :: TestTree tests = testGroup "Basics.QueryIndividual"- [ goldenCapturedIO "noTravis_query_abc" $ \rf -> runSMTWith abc{verbose=True, redirectVerbose=Just rf} q+ [ goldenCapturedIO "query_abc" $ \rf -> runSMTWith abc{verbose=True, redirectVerbose=Just rf} q ] q :: Symbolic ()
SBVTestSuite/TestSuite/Queries/Int_Boolector.hs view
@@ -22,7 +22,7 @@ tests :: TestTree tests = testGroup "Basics.QueryIndividual"- [ goldenCapturedIO "noTravis_query_boolector" $ \rf -> runSMTWith boolector{verbose=True, redirectVerbose=Just rf} q+ [ goldenCapturedIO "query_boolector" $ \rf -> runSMTWith boolector{verbose=True, redirectVerbose=Just rf} q ] q :: Symbolic ()
SBVTestSuite/TestSuite/Queries/Int_CVC4.hs view
@@ -22,7 +22,7 @@ tests :: TestTree tests = testGroup "Basics.QueryIndividual"- [ goldenCapturedIO "noTravis_query_cvc4" $ \rf -> runSMTWith cvc4{verbose=True, redirectVerbose=Just rf} q+ [ goldenCapturedIO "query_cvc4" $ \rf -> runSMTWith cvc4{verbose=True, redirectVerbose=Just rf} q ] q :: Symbolic ()
SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs view
@@ -22,7 +22,7 @@ tests :: TestTree tests = testGroup "Basics.QueryIndividual"- [ goldenCapturedIO "noTravis_query_mathsat" $ \rf -> runSMTWith mathSAT{verbose=True, redirectVerbose=Just rf} q+ [ goldenCapturedIO "query_mathsat" $ \rf -> runSMTWith mathSAT{verbose=True, redirectVerbose=Just rf} q ] q :: Symbolic ()
SBVTestSuite/TestSuite/Queries/Int_Yices.hs view
@@ -22,7 +22,7 @@ tests :: TestTree tests = testGroup "Basics.QueryIndividual"- [ goldenCapturedIO "noTravis_query_yices" $ \rf -> runSMTWith yices{verbose=True, redirectVerbose=Just rf} q+ [ goldenCapturedIO "query_yices" $ \rf -> runSMTWith yices{verbose=True, redirectVerbose=Just rf} q ] q :: Symbolic ()
SBVTestSuite/Utils/SBVTestFramework.hs view
@@ -19,7 +19,7 @@ , goldenString , goldenVsStringShow , goldenCapturedIO- , TravisOS(..), TestEnvironment(..), getTestEnvironment+ , CIOS(..), TestEnvironment(..), getTestEnvironment , pickTests -- module exports to simplify life , module Test.Tasty@@ -30,19 +30,24 @@ import qualified Control.Exception as C import qualified Data.ByteString.Lazy.Char8 as LBC+import qualified Data.ByteString as BS import System.Directory (removeFile) import System.Environment (lookupEnv) import Test.Tasty (testGroup, TestTree, TestName)-import Test.Tasty.Golden (goldenVsString, goldenVsFile) import Test.Tasty.HUnit (assert, Assertion, testCase) +import Test.Tasty.Golden (goldenVsString)+import Test.Tasty.Golden.Advanced (goldenTest)+ import Test.Tasty.Runners hiding (Result) import System.Random (randomRIO) import Data.SBV +import Data.Char (chr, ord, isDigit)+ import Data.Maybe(fromMaybe, catMaybes) import System.FilePath ((</>), (<.>))@@ -50,29 +55,38 @@ import Data.SBV.Internals (runSymbolic, Symbolic, Result, SBVRunMode(..), IStage(..)) ------------------------------------------------------------------------------------------ Test environment-data TravisOS = TravisLinux- | TravisOSX- | TravisWindows -- Travis actually doesn't support windows yet. This is "reserved" for future- deriving Show+-- Test environment; continuous integration+data CIOS = CILinux+ | CIOSX+ | CIWindows+ deriving Show data TestEnvironment = TestEnvLocal- | TestEnvTravis TravisOS+ | TestEnvCI CIOS | TestEnvUnknown deriving Show -getTestEnvironment :: IO TestEnvironment-getTestEnvironment = do mbTestEnv <- lookupEnv "SBV_TEST_ENVIRONMENT"+getTestEnvironment :: IO (TestEnvironment, Int)+getTestEnvironment = do mbTestEnv <- lookupEnv "SBV_TEST_ENVIRONMENT"+ mbTestPerc <- lookupEnv "SBV_HEAVYTEST_PERCENTAGE" - case mbTestEnv of- Just "local" -> return TestEnvLocal- Just "linux" -> return $ TestEnvTravis TravisLinux- Just "osx" -> return $ TestEnvTravis TravisOSX- Just "win" -> return $ TestEnvTravis TravisWindows- Just other -> do putStrLn $ "Ignoring unexpected test env value: " ++ show other- return TestEnvUnknown- Nothing -> return TestEnvUnknown+ env <- case mbTestEnv of+ Just "local" -> return TestEnvLocal+ Just "linux" -> return $ TestEnvCI CILinux+ Just "osx" -> return $ TestEnvCI CIOSX+ Just "win" -> return $ TestEnvCI CIWindows+ Just other -> do putStrLn $ "Ignoring unexpected test env value: " ++ show other+ return TestEnvUnknown+ Nothing -> return TestEnvUnknown + perc <- case mbTestPerc of+ Just n | all isDigit n -> return (read n)+ Just n -> do putStrLn $ "Ignoring unexpected test percentage value: " ++ show n+ return 100+ Nothing -> return 100++ return (env, perc)+ -- | Checks that a particular result shows as @s@ showsAs :: Show a => a -> String -> Assertion showsAs r s = assert $ show r == s@@ -87,11 +101,34 @@ goldenVsStringShow n res = goldenVsString n (goldFile n) (fmap (LBC.pack . show) res) goldenCapturedIO :: TestName -> (FilePath -> IO ()) -> TestTree-goldenCapturedIO n res = goldenVsFile n gf gfTmp (rm gfTmp >> res gfTmp)+goldenCapturedIO n res = doTheDiff n gf gfTmp (rm gfTmp >> res gfTmp) where gf = goldFile n gfTmp = gf ++ "_temp" rm f = removeFile f `C.catch` (\(_ :: C.SomeException) -> return ())++-- | When comparing ignore \r's for windows's sake+doTheDiff :: TestName -> FilePath -> FilePath -> IO () -> TestTree+doTheDiff nm ref new act = goldenTest nm (BS.readFile ref) (act >> BS.readFile new) cmp upd+ where upd = BS.writeFile ref++ cmp :: BS.ByteString -> BS.ByteString -> IO (Maybe String)+ cmp x y+ | cleanUp x == cleanUp y = return Nothing+ | True = return $ Just $ unlines $ [ "Discrepancy found. Expected: " ++ ref+ , "============================================"+ ]+ ++ lines xs+ ++ [ "Got: " ++ new+ , "============================================"+ ]+ ++ lines ys+ where xs = map (chr . fromIntegral) $ BS.unpack x+ ys = map (chr . fromIntegral) $ BS.unpack y++ -- deal with insane Windows \r stuff+ cleanUp = BS.filter (/= slashr)+ slashr = fromIntegral (ord '\r') -- | Count the number of models numberOfModels :: Provable a => a -> IO Int
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 7.1+Version: 7.2 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@@ -178,6 +178,7 @@ , TestSuite.Basics.QRem , TestSuite.Basics.Quantifiers , TestSuite.Basics.Recursive+ , TestSuite.Basics.SmallShifts , TestSuite.Basics.SquashReals , TestSuite.Basics.TOut , TestSuite.BitPrecise.BitTricks@@ -205,6 +206,7 @@ , TestSuite.Optimization.Basics , TestSuite.Optimization.Combined , TestSuite.Optimization.ExtensionField+ , TestSuite.Optimization.Quantified , TestSuite.Optimization.Reals , TestSuite.Polynomials.Polynomials , TestSuite.Puzzles.Coins@@ -237,7 +239,7 @@ Test-Suite SBVDocTest Build-Depends: base, directory, filepath, random- , doctest >= 0.9+ , doctest >= 0.13 , Glob >= 0.7 , bytestring >= 0.9 , tasty >= 0.11.2.3