diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,31 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -98,6 +98,9 @@ -- -- * Z3 from Microsoft: -- +-- 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.) -- diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -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 = (">>", "<<") diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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 diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -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. -- diff --git a/Data/SBV/Core/Operations.hs b/Data/SBV/Core/Operations.hs --- a/Data/SBV/Core/Operations.hs +++ b/Data/SBV/Core/Operations.hs @@ -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) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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) diff --git a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs --- a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs +++ b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs @@ -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; -- --- return s40; +-- return s41; -- } -- == END: "popCount.c" ================== genPopCountInC :: IO () diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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 ++ "))" diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -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] diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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 diff --git a/Data/SBV/SMT/Utils.hs b/Data/SBV/SMT/Utils.hs --- a/Data/SBV/SMT/Utils.hs +++ b/Data/SBV/SMT/Utils.hs @@ -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.) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,15 +1,24 @@ ## SBV: SMT Based Verification in Haskell +[![Hackage version](http://img.shields.io/hackage/v/sbv.svg?label=Hackage)](http://hackage.haskell.org/package/sbv) + Please see: http://leventerkok.github.io/sbv/ -[![Hackage version](http://img.shields.io/hackage/v/sbv.svg?label=Hackage)](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 diff --git a/SBVTestSuite/GoldFiles/crcUSB5_2.gold b/SBVTestSuite/GoldFiles/crcUSB5_2.gold --- a/SBVTestSuite/GoldFiles/crcUSB5_2.gold +++ b/SBVTestSuite/GoldFiles/crcUSB5_2.gold @@ -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" ================== diff --git a/SBVTestSuite/GoldFiles/noTravis_query1.gold b/SBVTestSuite/GoldFiles/noTravis_query1.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query1.gold +++ /dev/null @@ -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! diff --git a/SBVTestSuite/GoldFiles/noTravis_query_abc.gold b/SBVTestSuite/GoldFiles/noTravis_query_abc.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query_abc.gold +++ /dev/null @@ -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 diff --git a/SBVTestSuite/GoldFiles/noTravis_query_boolector.gold b/SBVTestSuite/GoldFiles/noTravis_query_boolector.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query_boolector.gold +++ /dev/null @@ -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 diff --git a/SBVTestSuite/GoldFiles/noTravis_query_cvc4.gold b/SBVTestSuite/GoldFiles/noTravis_query_cvc4.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query_cvc4.gold +++ /dev/null @@ -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 : diff --git a/SBVTestSuite/GoldFiles/noTravis_query_mathsat.gold b/SBVTestSuite/GoldFiles/noTravis_query_mathsat.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query_mathsat.gold +++ /dev/null @@ -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 diff --git a/SBVTestSuite/GoldFiles/noTravis_query_yices.gold b/SBVTestSuite/GoldFiles/noTravis_query_yices.gold deleted file mode 100644 --- a/SBVTestSuite/GoldFiles/noTravis_query_yices.gold +++ /dev/null @@ -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 diff --git a/SBVTestSuite/GoldFiles/optQuant1.gold b/SBVTestSuite/GoldFiles/optQuant1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optQuant1.gold @@ -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. diff --git a/SBVTestSuite/GoldFiles/optQuant2.gold b/SBVTestSuite/GoldFiles/optQuant2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optQuant2.gold @@ -0,0 +1,5 @@ +Optimal model: + a = 0 :: Integer + b1 = 1 :: Integer + b2 = 1 :: Integer + goal = 0 :: Integer diff --git a/SBVTestSuite/GoldFiles/optQuant3.gold b/SBVTestSuite/GoldFiles/optQuant3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optQuant3.gold @@ -0,0 +1,5 @@ +Optimal model: + a = 0 :: Integer + b1 = 1 :: Integer + b2 = 1 :: Integer + goal = 0 :: Integer diff --git a/SBVTestSuite/GoldFiles/optQuant4.gold b/SBVTestSuite/GoldFiles/optQuant4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optQuant4.gold @@ -0,0 +1,5 @@ +Optimal model: + a = 0 :: Integer + b1 = 1 :: Integer + b2 = 1 :: Integer + goal = 0 :: Integer diff --git a/SBVTestSuite/GoldFiles/optQuant5.gold b/SBVTestSuite/GoldFiles/optQuant5.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optQuant5.gold @@ -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. diff --git a/SBVTestSuite/GoldFiles/popCount1.gold b/SBVTestSuite/GoldFiles/popCount1.gold --- a/SBVTestSuite/GoldFiles/popCount1.gold +++ b/SBVTestSuite/GoldFiles/popCount1.gold @@ -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" ================== diff --git a/SBVTestSuite/GoldFiles/popCount2.gold b/SBVTestSuite/GoldFiles/popCount2.gold --- a/SBVTestSuite/GoldFiles/popCount2.gold +++ b/SBVTestSuite/GoldFiles/popCount2.gold @@ -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" ================== diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -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! diff --git a/SBVTestSuite/GoldFiles/query_abc.gold b/SBVTestSuite/GoldFiles/query_abc.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_abc.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_boolector.gold b/SBVTestSuite/GoldFiles/query_boolector.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_boolector.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_cvc4.gold b/SBVTestSuite/GoldFiles/query_cvc4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_cvc4.gold @@ -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 : diff --git a/SBVTestSuite/GoldFiles/query_mathsat.gold b/SBVTestSuite/GoldFiles/query_mathsat.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_mathsat.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/query_yices.gold b/SBVTestSuite/GoldFiles/query_yices.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_yices.gold @@ -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 diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -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 + diff --git a/SBVTestSuite/SBVHLint.hs b/SBVTestSuite/SBVHLint.hs --- a/SBVTestSuite/SBVHLint.hs +++ b/SBVTestSuite/SBVHLint.hs @@ -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 diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -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 + ] diff --git a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs @@ -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 $ diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -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 ] diff --git a/SBVTestSuite/TestSuite/Basics/SmallShifts.hs b/SBVTestSuite/TestSuite/Basics/SmallShifts.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Basics/SmallShifts.hs @@ -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 + ] diff --git a/SBVTestSuite/TestSuite/Optimization/Quantified.hs b/SBVTestSuite/TestSuite/Optimization/Quantified.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Optimization/Quantified.hs @@ -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) #-} diff --git a/SBVTestSuite/TestSuite/Queries/BasicQuery.hs b/SBVTestSuite/TestSuite/Queries/BasicQuery.hs --- a/SBVTestSuite/TestSuite/Queries/BasicQuery.hs +++ b/SBVTestSuite/TestSuite/Queries/BasicQuery.hs @@ -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" diff --git a/SBVTestSuite/TestSuite/Queries/Int_ABC.hs b/SBVTestSuite/TestSuite/Queries/Int_ABC.hs --- a/SBVTestSuite/TestSuite/Queries/Int_ABC.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_ABC.hs @@ -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 () diff --git a/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs b/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Boolector.hs @@ -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 () diff --git a/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs b/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs --- a/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_CVC4.hs @@ -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 () diff --git a/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs b/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Mathsat.hs @@ -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 () diff --git a/SBVTestSuite/TestSuite/Queries/Int_Yices.hs b/SBVTestSuite/TestSuite/Queries/Int_Yices.hs --- a/SBVTestSuite/TestSuite/Queries/Int_Yices.hs +++ b/SBVTestSuite/TestSuite/Queries/Int_Yices.hs @@ -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 () diff --git a/SBVTestSuite/Utils/SBVTestFramework.hs b/SBVTestSuite/Utils/SBVTestFramework.hs --- a/SBVTestSuite/Utils/SBVTestFramework.hs +++ b/SBVTestSuite/Utils/SBVTestFramework.hs @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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