diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,20 @@ * Hackage: * GitHub: -* Latest Hackage released version: 7.0, 2017-07-19 +* Latest Hackage released version: 7.1, 2017-07-29 + +### Version 7.1, 2017-07-29 + + * Add support for 'getInterpolant' in Query mode. + + * Support for SMT-results that can contain multi-line strings, which + is rare but it does happen. Previously SBV incorrectly interpreted such + responses to be erroneous. + + * Many improvements to build infrastructure and code clean-up. + + * Fix a bug in the implementation of `svSetBit`. Thanks to Robert Dockins + for the report. ### Version 7.0, Released 2017-07-19 diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs --- a/Data/SBV/Control.hs +++ b/Data/SBV/Control.hs @@ -33,6 +33,9 @@ -- ** Extracting a proof , getProof + -- ** Extracting interpolants + , getInterpolant + -- ** Extracting assertions , getAssertions @@ -49,21 +52,18 @@ -- * Resetting the solver state , resetAssertions - -- * Communicating results back - -- ** Constructing assignments + -- * Constructing assignments , (|->) - -- ** Miscellaneous - , echo - - -- ** Terminating the query + -- * Terminating the query , mkSMTResult , exit -- * Controlling the solver behavior , ignoreExitCode, timeout - -- * Performing actions + -- * Miscellaneous + , echo , io -- * Solver options @@ -166,13 +166,8 @@ {- $queryIntro In certain cases, the user might want to take over the communication with the solver, programmatically -querying the engine and issuing commands accordingly. Even with human guidance, perhaps, where the user -can take a look at the engine state and issue commands to guide the proof. This is an advanced feature, -as the user is given full access to the underlying SMT solver, so the usual protections provided by -SBV are no longer there to prevent mistakes. - -Having said that, queries can be extremely powerful as they allow direct control of the solver. Here's a -simple example: +querying the engine and issuing commands accordingly. Queries can be extremely powerful as +they allow direct control of the solver. Here's a simple example: @ module Test where @@ -244,4 +239,5 @@ - "Data.SBV.Examples.Queries.FourFours": Solution to a fun arithmetic puzzle, coded using queries. - "Data.SBV.Examples.Queries.GuessNumber": The famous number guessing game. - "Data.SBV.Examples.Queries.UnsatCore": Extracting unsat-cores using queries. + - "Data.SBV.Examples.Queries.Interpolants": Extracting interpolants using queries. -} diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -19,7 +19,7 @@ module Data.SBV.Control.Query ( send, ask, retrieveResponse , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet - , getUnsatCore, getProof, getAssignment, getOption, freshVar, freshVar_, push, pop, getAssertionStackDepth + , getUnsatCore, getProof, getInterpolant, getAssignment, getOption, freshVar, freshVar_, push, pop, getAssertionStackDepth , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getValue, getUninterpretedValue, getModel, getSMTResult , getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason , SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo @@ -83,13 +83,19 @@ serialize :: Bool -> SExpr -> String serialize removeQuotes = go where go (ECon s) = if removeQuotes then unQuote s else s - go (ENum (i, _)) = show i - go (EReal r) = show r - go (EFloat f) = show f - go (EDouble d) = show d + go (ENum (i, _)) = shNN i + go (EReal r) = shNN r + go (EFloat f) = shNN f + go (EDouble d) = shNN d go (EApp [x]) = go x go (EApp ss) = "(" ++ unwords (map go ss) ++ ")" + -- be careful with negative number printing in SMT-Lib.. + shNN :: (Show a, Num a, Ord a) => a -> String + shNN i + | i < 0 = "(- " ++ show (-i) ++ ")" + | True = show i + -- | Ask solver for info. getInfo :: SMTInfoFlag -> Query SMTInfoResponse getInfo flag = do @@ -143,6 +149,7 @@ ProduceAssertions{} -> askFor "ProduceAssertions" ":produce-assertions" $ bool ProduceAssertions ProduceAssignments{} -> askFor "ProduceAssignments" ":produce-assignments" $ bool ProduceAssignments ProduceProofs{} -> askFor "ProduceProofs" ":produce-proofs" $ bool ProduceProofs + ProduceInterpolants{} -> askFor "ProduceInterpolants" ":produce-interpolants" $ bool ProduceInterpolants ProduceUnsatAssumptions{} -> askFor "ProduceUnsatAssumptions" ":produce-unsat-assumptions" $ bool ProduceUnsatAssumptions ProduceUnsatCores{} -> askFor "ProduceUnsatCores" ":produce-unsat-cores" $ bool ProduceUnsatCores RandomSeed{} -> askFor "RandomSeed" ":random-seed" $ integer RandomSeed @@ -569,7 +576,7 @@ , "" , " setOption $ ProduceProofs True" , "" - , "to make sure the solver is ready for producing proofs." + , "to make sure the solver is ready for producing proofs," , "and that there is a proof by first issuing a 'checkSat' call." ] @@ -580,6 +587,56 @@ -- result of parsing is ignored. parse r bad $ \_ -> return r +-- | Retrieve interpolants after an 'Unsat' result is obtained. Note you must have arranged for +-- interpolants to be produced first (/via/ @'setOption' $ 'ProduceInterpolants' 'True'@) +-- for this call to not error out! +-- +-- To get an interpolant for a pair of formulas @A@ and @B@, use a 'namedConstraint' to attach +-- names to @A@ and @B@. Then call 'getInterpolant' @[\"A\", \"B\"]@, assuming those are the names +-- you gave to the formulas. +-- +-- An interpolant for @A@ and @B@ is a formula @I@ such that: +-- +-- @ +-- A ==> I +-- and B ==> not I +-- @ +-- +-- That is, it's evidence that @A@ and @B@ cannot be true together +-- since @A@ implies @I@ but @B@ implies @not I@; establishing that @A@ and @B@ cannot +-- be satisfied at the same time. Furthermore, @I@ will have only the symbols that are common +-- to @A@ and @B@. +-- +-- Interpolants generalize to sequences: If you pass more than two formulas, then you will get +-- a sequence of interpolants. In general, for @N@ formulas that are not satisfiable together, you will be +-- returned @N-1@ interpolants. If formulas are @A1 .. An@, then interpolants will be @I1 .. I(N-1)@, such +-- that @A1 ==> I1@, @A2 /\\ I1 ==> I2@, @A3 /\\ I2 ==> I3@, ..., and finally @AN ===> not I(N-1)@. +-- +-- Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants. +-- If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the +-- interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can +-- suggest a better API. +getInterpolant :: [String] -> Query [String] +getInterpolant fs + | length fs < 2 + = error $ "SBV.getInterpolant requires at least two named constraints, received: " ++ show fs + | True + = do let bar s = '|' : s ++ "|" + cmd = "(get-interpolant " ++ unwords (map bar fs) ++ ")" + bad = unexpected "getInterpolant" cmd "a get-interpolant response" + $ Just [ "Make sure you use:" + , "" + , " setOption $ ProduceInterpolants True" + , "" + , "to make sure the solver is ready for producing interpolants," + , "and that you have named the formulas with calls to 'namedConstraint'." + ] + + r <- ask cmd + + parse r bad $ \case EApp (ECon "interpolants" : es) -> return $ map (serialize False) es + _ -> bad r Nothing + -- | Retrieve assertions. Note you must have arranged for -- assertions to be available first (/via/ @'setOption' $ 'ProduceAssertions' 'True'@) -- for this call to not error out! @@ -631,7 +688,18 @@ parse r bad $ \case EApp ps | Just vs <- mapM grab ps -> return vs _ -> bad r Nothing --- | Make an assignment. The type 'Assignment' is abstract, see 'success' for an example use case. +-- | Make an assignment. The type 'Assignment' is abstract, the result is typically passed +-- to 'mkSMTResult': +-- +-- @ mkSMTResult [ a |-> 332 +-- , b |-> 2.3 +-- , c |-> True +-- ] +-- @ +-- +-- End users should use 'getModel' for automatically constructing models from the current solver state. +-- However, an explicit 'Assignment' might be handy in complex scenarios where a model needs to be +-- created manually. infix 1 |-> (|->) :: SymWord a => SBV a -> a -> Assignment SBV a |-> v = case literal v of diff --git a/Data/SBV/Control/Types.hs b/Data/SBV/Control/Types.hs --- a/Data/SBV/Control/Types.hs +++ b/Data/SBV/Control/Types.hs @@ -93,6 +93,7 @@ | ProduceAssertions Bool | ProduceAssignments Bool | ProduceProofs Bool + | ProduceInterpolants Bool | ProduceUnsatAssumptions Bool | ProduceUnsatCores Bool | RandomSeed Integer @@ -111,6 +112,7 @@ isStartModeOption ProduceAssertions{} = True isStartModeOption ProduceAssignments{} = True isStartModeOption ProduceProofs{} = True +isStartModeOption ProduceInterpolants{} = True isStartModeOption ProduceUnsatAssumptions{} = True isStartModeOption ProduceUnsatCores{} = True isStartModeOption RandomSeed{} = True @@ -132,6 +134,7 @@ cvt (ProduceAssertions b) = opt [":produce-assertions", smtBool b] cvt (ProduceAssignments b) = opt [":produce-assignments", smtBool b] cvt (ProduceProofs b) = opt [":produce-proofs", smtBool b] + cvt (ProduceInterpolants b) = opt [":produce-interpolants", smtBool b] cvt (ProduceUnsatAssumptions b) = opt [":produce-unsat-assumptions", smtBool b] cvt (ProduceUnsatCores b) = opt [":produce-unsat-cores", smtBool b] cvt (RandomSeed i) = opt [":random-seed", show i] 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 @@ -171,7 +171,7 @@ -- | Set a given bit at index svSetBit :: SVal -> Int -> SVal -svSetBit x i = x `svXOr` svInteger (kindOf x) (bit i :: Integer) +svSetBit x i = x `svOr` svInteger (kindOf x) (bit i :: Integer) -- | Bit-blast: Big-endian. Assumes the input is a bit-vector. svBlastBE :: SVal -> [SVal] diff --git a/Data/SBV/Examples/Misc/Enumerate.hs b/Data/SBV/Examples/Misc/Enumerate.hs --- a/Data/SBV/Examples/Misc/Enumerate.hs +++ b/Data/SBV/Examples/Misc/Enumerate.hs @@ -30,6 +30,8 @@ -- @TemplateHaskell@, @StandaloneDeriving@, @DeriveDataTypeable@, @DeriveAnyClass@ for -- this to work. data E = A | B | C + +-- | Make 'E' a symbolic value. mkSymbolicEnumeration ''E -- | Give a name to the symbolic variants of 'E', for convenience diff --git a/Data/SBV/Examples/Puzzles/Fish.hs b/Data/SBV/Examples/Puzzles/Fish.hs --- a/Data/SBV/Examples/Puzzles/Fish.hs +++ b/Data/SBV/Examples/Puzzles/Fish.hs @@ -39,22 +39,32 @@ -- | Colors of houses data Color = Red | Green | White | Yellow | Blue + +-- | Make 'Color' a symbolic value. mkSymbolicEnumeration ''Color -- | Nationalities of the occupants data Nationality = Briton | Dane | Swede | Norwegian | German + +-- | Make 'Nationality' a symbolic value. mkSymbolicEnumeration ''Nationality -- | Beverage choices data Beverage = Tea | Coffee | Milk | Beer | Water + +-- | Make 'Beverage' a symbolic value. mkSymbolicEnumeration ''Beverage -- | Pets they keep data Pet = Dog | Horse | Cat | Bird | Fish + +-- | Make 'Pet' a symbolic value. mkSymbolicEnumeration ''Pet -- | Sports they engage in data Sport = Football | Baseball | Volleyball | Hockey | Tennis + +-- | Make 'Sport' a symbolic value. mkSymbolicEnumeration ''Sport -- | We have: diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -33,6 +33,8 @@ -- | U2 band members. We want to translate this to SMT-Lib as a data-type, and hence the -- call to mkSymbolicEnumeration. data U2Member = Bono | Edge | Adam | Larry + +-- | Make 'U2Member' a symbolic value. mkSymbolicEnumeration ''U2Member -- | Symbolic shorthand for a 'U2Member' @@ -64,6 +66,8 @@ -- | Location of the flash data Location = Here | There + +-- | Make 'Location' a symbolic value. mkSymbolicEnumeration ''Location -- | Symbolic variant of 'Location' diff --git a/Data/SBV/Examples/Queries/Enums.hs b/Data/SBV/Examples/Queries/Enums.hs --- a/Data/SBV/Examples/Queries/Enums.hs +++ b/Data/SBV/Examples/Queries/Enums.hs @@ -22,6 +22,8 @@ -- | Days of the week. We make it symbolic using the 'mkSymbolicEnumeration' splice. data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday + +-- | Make 'Day' a symbolic value. mkSymbolicEnumeration ''Day -- | The type synonym 'SDay' is the symbolic variant of 'Day'. (Similar to 'SInteger'/'Integer' diff --git a/Data/SBV/Examples/Queries/FourFours.hs b/Data/SBV/Examples/Queries/FourFours.hs --- a/Data/SBV/Examples/Queries/FourFours.hs +++ b/Data/SBV/Examples/Queries/FourFours.hs @@ -38,11 +38,15 @@ -- and exponentiation will only be to the power @0@. This does restrict the search space, but is sufficient to -- solve all the instances. data BinOp = Plus | Minus | Times | Divide | Expt + +-- | Make 'BinOp' a symbolic value. mkSymbolicEnumeration ''BinOp -- | Supported unary operators. Similar to 'BinOp' case, we will restrict square-root and factorial to -- be only applied to the value @4. data UnOp = Negate | Sqrt | Factorial + +-- | Make 'UnOp' a symbolic value. mkSymbolicEnumeration ''UnOp -- | Symbolic variant of 'BinOp'. @@ -153,36 +157,62 @@ -- | Given an integer, walk through all possible tree shapes (at most 640 of them), and find a -- filling that solves the puzzle. find :: Integer -> IO () -find i = go allPossibleTrees - where go [] = putStrLn $ show i ++ ": No solution found." - go (t:ts) = do chk <- generate i t +find target = go allPossibleTrees + where go [] = putStrLn $ show target ++ ": No solution found." + go (t:ts) = do chk <- generate target t case chk of Nothing -> go ts - Just r -> putStrLn $ show i ++ ": " ++ show r + Just r -> do let ok = concEval r == target + tag = if ok then " [OK]: " else " [BAD]: " + sh i | i < 10 = ' ' : show i + | True = show i --- | Solution to the puzzle. We have: + putStrLn $ sh target ++ tag ++ show r + + -- Make sure the result is correct! + concEval :: T BinOp UnOp -> Integer + concEval F = 4 + concEval (U u t) = uEval u (concEval t) + concEval (B b l r) = bEval b (concEval l) (concEval r) + + uEval :: UnOp -> Integer -> Integer + uEval Negate i = -i + uEval Sqrt i = if i == 4 then 2 else error $ "uEval: Found sqrt applied to value: " ++ show i + uEval Factorial i = if i == 4 then 24 else error $ "uEval: Found factorial applied to value: " ++ show i + + bEval :: BinOp -> Integer -> Integer -> Integer + bEval Plus i j = i + j + bEval Minus i j = i - j + bEval Times i j = i * j + bEval Divide i j = i `div` j + bEval Expt i j = i ^ j + +-- | Solution to the puzzle. When you run this puzzle, the solver can produce different results +-- than what's shown here, but the expressions should still be all valid! -- --- >>> puzzle --- 0: (4 + (4 - (4 + 4))) --- 1: (4 / (4 + (4 - 4))) --- 2: sqrt((4 + (4 * (4 - 4)))) --- 3: (4 - (4 ^ (4 - 4))) --- 4: (4 * (4 ^ (4 - 4))) --- 5: (4 + (4 ^ (4 - 4))) --- 6: (4 + sqrt((4 * (4 / 4)))) --- 7: (4 + (4 - (4 / 4))) --- 8: (4 - (4 - (4 + 4))) --- 9: (4 + (4 + (4 / 4))) --- 10: (4 + (4 + (4 - sqrt(4)))) --- 11: (4 + ((4 + 4!) / 4)) --- 12: (4 * (4 - (4 / 4))) --- 13: (4! + ((sqrt(4) - 4!) / sqrt(4))) --- 14: (4 + (4 + (4 + sqrt(4)))) --- 15: (4 + ((4! - sqrt(4)) / sqrt(4))) --- 16: (4 + (4 + (4 + 4))) --- 17: (4 + ((sqrt(4) + 4!) / sqrt(4))) --- 18: -(4 + (4 - (4! + sqrt(4)))) --- 19: -(4 - (4! - (4 / 4))) --- 20: (4 * (4 + (4 / 4))) +-- @ +-- ghci> puzzle +-- 0 [OK]: (4 - (4 + (4 - 4))) +-- 1 [OK]: (4 / (4 + (4 - 4))) +-- 2 [OK]: sqrt((4 + (4 * (4 - 4)))) +-- 3 [OK]: (4 - (4 ^ (4 - 4))) +-- 4 [OK]: (4 + (4 * (4 - 4))) +-- 5 [OK]: (4 + (4 ^ (4 - 4))) +-- 6 [OK]: (4 + sqrt((4 * (4 / 4)))) +-- 7 [OK]: (4 + (4 - (4 / 4))) +-- 8 [OK]: (4 - (4 - (4 + 4))) +-- 9 [OK]: (4 + (4 + (4 / 4))) +-- 10 [OK]: (4 + (4 + (4 - sqrt(4)))) +-- 11 [OK]: (4 + ((4 + 4!) / 4)) +-- 12 [OK]: (4 * (4 - (4 / 4))) +-- 13 [OK]: (4! + ((sqrt(4) - 4!) / sqrt(4))) +-- 14 [OK]: (4 + (4 + (4 + sqrt(4)))) +-- 15 [OK]: (4 + ((4! - sqrt(4)) / sqrt(4))) +-- 16 [OK]: (4 * (4 * (4 / 4))) +-- 17 [OK]: (4 + ((sqrt(4) + 4!) / sqrt(4))) +-- 18 [OK]: -(4 + (4 - (sqrt(4) + 4!))) +-- 19 [OK]: -(4 - (4! - (4 / 4))) +-- 20 [OK]: (4 * (4 + (4 / 4))) +-- @ puzzle :: IO () puzzle = mapM_ find [0 .. 20] diff --git a/Data/SBV/Examples/Queries/Interpolants.hs b/Data/SBV/Examples/Queries/Interpolants.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Queries/Interpolants.hs @@ -0,0 +1,65 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Queries.Interpolants +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates extraction of interpolants via queries. +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Queries.Interpolants where + +import Data.SBV +import Data.SBV.Control + +-- | Compute the interpolant for formulas @y = 2x@ and @y = 2z+1@. +-- These formulas are not satisfiable together since it would mean +-- @y@ is both even and odd at the same time. An interpolant for +-- this pair of formulas is a formula that's expressed only in terms +-- of @y@, which is the only common symbol among them. We have: +-- +-- >>> runSMT evenOdd +-- ["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"] +-- +-- This is a bit hard to read unfortunately, due to translation artifacts and use of strings. To analyze, +-- we need to know that @s1@ is @y@ through SBV's translation. Let's express it in +-- regular infix notation with @y@ for @s1@: +-- +-- @ 0 <= (y `div` 2) + ((-y) `div` 2)@ +-- +-- Notice that the only symbol is @y@, as required. To establish that this is +-- indeed an interpolant, we should establish that when @y@ is even, this formula +-- is @True@; and if @y@ is odd, then then it should be @False@. You can argue +-- mathematically that this indeed the case, but let's just use SBV to prove these: +-- +-- >>> prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger)) +-- Q.E.D. +-- +-- And: +-- +-- >>> prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger)) +-- Q.E.D. +-- +-- This establishes that we indeed have an interpolant! +evenOdd :: Symbolic [String] +evenOdd = do + x <- sInteger "x" + y <- sInteger "y" + z <- sInteger "z" + + -- tell the solver we want interpolants + setOption $ ProduceInterpolants True + + -- create named constraints, which will allow + -- computation of the interpolants for our formulas + namedConstraint "y is even" $ y .== 2*x + namedConstraint "y is odd" $ y .== 2*z + 1 + + -- To obtain the interpolant, we run a query + query $ do cs <- checkSat + case cs of + Unsat -> getInterpolant ["y is even", "y is odd"] + Sat -> error "Unexpected sat result!" + Unk -> error "Unexpected unknown result!" diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -582,13 +582,32 @@ | True = Just 5000000 timeOutMsg t | isFirst = "User specified timeout of " ++ showTimeoutValue t ++ " exceeded." | True = "A multiline complete response wasn't received before " ++ showTimeoutValue t ++ " exceeded." + + -- Like hGetLine, except it keeps getting lines if inside a string. + getFullLine :: IO String + getFullLine = intercalate "\n" . reverse <$> collect False [] + where collect inString sofar = do ln <- hGetLine h + + let walk inside [] = inside + walk inside ('"':cs) = walk (not inside) cs + walk inside (_:cs) = walk inside cs + + stillInside = walk inString ln + + sofar' = ln : sofar + + if stillInside + then collect True sofar' + else return sofar' + in case timeOutToUse of - Nothing -> SolverRegular <$> hGetLine h - Just t -> do r <- Timeout.timeout t (hGetLine h) + Nothing -> SolverRegular <$> getFullLine + Just t -> do r <- Timeout.timeout t getFullLine case r of Just l -> return $ SolverRegular l Nothing -> return $ SolverTimeout $ timeOutMsg t + go isFirst i sofar = do errln <- safeGetLine isFirst outh `C.catch` (\(e :: C.SomeException) -> return (SolverException (show e))) case errln of @@ -681,7 +700,8 @@ let isOption = "(set-option" `isPrefixOf` dropWhile isSpace l reason | isOption = [ "*** Backend solver reports it does not support this option." - , "*** Please report this as a bug/feature request with the solver!" + , "*** Check the spelling, and if correct please report this as a" + , "*** bug/feature request with the solver!" ] | True = [ "*** Failed to establish solver context. Running in debug mode might provide" , "*** more information. Please report this as an issue!" diff --git a/Data/SBV/Tools/STree.hs b/Data/SBV/Tools/STree.hs --- a/Data/SBV/Tools/STree.hs +++ b/Data/SBV/Tools/STree.hs @@ -36,7 +36,7 @@ | SBin (STreeInternal i e) (STreeInternal i e) deriving Show -instance (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) where +instance SymWord e => Mergeable (STree i e) where symbolicMerge f b (SLeaf i) (SLeaf j) = SLeaf (symbolicMerge f b i j) symbolicMerge f b (SBin l r) (SBin l' r') = SBin (symbolicMerge f b l l') (symbolicMerge f b r r') symbolicMerge _ _ _ _ = error "SBV.STree.symbolicMerge: Impossible happened while merging states" @@ -51,7 +51,7 @@ -- | Writing a value, similar to how reads are done. The important thing is that the tree -- representation keeps updates to a minimum. -writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e +writeSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e writeSTree s i j = walk (blastBE i) s where walk [] _ = SLeaf j walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,15 @@ ## SBV: SMT Based Verification in Haskell +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](http://img.shields.io/travis/LeventErkok/sbv.svg?label=Build)](http://travis-ci.org/LeventErkok/sbv) -Please see: http://leventerkok.github.io/sbv/ +| 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] | + +[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 diff --git a/SBVTestSuite/GoldFiles/noTravis_query1.gold b/SBVTestSuite/GoldFiles/noTravis_query1.gold --- a/SBVTestSuite/GoldFiles/noTravis_query1.gold +++ b/SBVTestSuite/GoldFiles/noTravis_query1.gold @@ -7,6 +7,7 @@ [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) @@ -54,17 +55,19 @@ [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: 42 position: 0 +[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: 45 position: 0 +[SKIP] ; :reproducible-resource-limit line: 47 position: 0 [RECV] 0 [SEND] (get-option :smt.mbqi) [RECV] true @@ -108,10 +111,10 @@ [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) -[SKIP] ; :memory line: 71 position: 0 +[SKIP] ; :memory line: 73 position: 0 [RECV] unsupported [SEND] (get-value (s0)) -[SKIP] ; :time line: 72 position: 0 +[SKIP] ; :time line: 74 position: 0 [RECV] ((s0 5)) [SEND] (get-value (s1)) [RECV] ((s1 1)) @@ -186,5 +189,5 @@ c = 2.3 :: Float d = True :: Bool e = 3.12 :: Real - s5 = 244 :: Word8 + s5 = -12 :: Int8 DONE! diff --git a/SBVTestSuite/GoldFiles/query_Interpolant1.gold b/SBVTestSuite/GoldFiles/query_Interpolant1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_Interpolant1.gold @@ -0,0 +1,43 @@ +** 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-interpolants true) +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[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 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Bool (= s0 s1)) +[GOOD] (define-fun s5 () Bool (= s0 s2)) +[GOOD] (define-fun s6 () Bool (and s4 s5)) +[GOOD] (define-fun s7 () Bool (= s1 s3)) +[GOOD] (define-fun s8 () Bool (= s2 s3)) +[GOOD] (define-fun s9 () Bool (not s8)) +[GOOD] (define-fun s10 () Bool (and s7 s9)) +[GOOD] (assert (! s6 :named |c1|)) +[GOOD] (assert (! s10 :named |c2|)) +[SEND] (check-sat) +[RECV] unsat +[SEND] (get-interpolant |c1| |c2|) +[RECV] (interpolants + (= s1 s2)) +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +["(= s1 s2)"] diff --git a/SBVTestSuite/GoldFiles/query_Interpolant2.gold b/SBVTestSuite/GoldFiles/query_Interpolant2.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_Interpolant2.gold @@ -0,0 +1,48 @@ +** 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-interpolants true) +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[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 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] (declare-fun f (Int) Int) +[GOOD] (declare-fun g (Int) Int) +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Int (f s0)) +[GOOD] (define-fun s5 () Bool (= s2 s4)) +[GOOD] (define-fun s6 () Int (f s1)) +[GOOD] (define-fun s7 () Bool (= s3 s6)) +[GOOD] (define-fun s8 () Bool (and s5 s7)) +[GOOD] (define-fun s9 () Bool (= s0 s1)) +[GOOD] (define-fun s10 () Int (g s2)) +[GOOD] (define-fun s11 () Int (g s3)) +[GOOD] (define-fun s12 () Bool (distinct s10 s11)) +[GOOD] (define-fun s13 () Bool (and s9 s12)) +[GOOD] (assert (! s8 :named |c1|)) +[GOOD] (assert (! s13 :named |c2|)) +[SEND] (check-sat) +[RECV] unsat +[SEND] (get-interpolant |c1| |c2|) +[RECV] (interpolants + (or (= s2 s3) (not (= s0 s1)))) +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +["(or (= s2 s3) (not (= s0 s1)))"] diff --git a/SBVTestSuite/GoldFiles/query_Interpolant3.gold b/SBVTestSuite/GoldFiles/query_Interpolant3.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_Interpolant3.gold @@ -0,0 +1,48 @@ +** 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-interpolants true) +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[GOOD] (define-fun s3 () Int 0) +[GOOD] (define-fun s7 () Int 1) +[GOOD] ; --- skolem constants --- +[GOOD] (declare-fun s0 () Int) ; tracks user variable "x" +[GOOD] (declare-fun s1 () Int) ; tracks user variable "y" +[GOOD] (declare-fun s2 () Int) ; tracks user variable "z" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] (declare-fun array_0 () (Array Int Int)) +[GOOD] (declare-fun array_1 () (Array Int Int)) +[GOOD] (declare-fun array_2 () (Array Int Int)) +[GOOD] (declare-fun array_3 () (Array Int Int)) +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s4 () Bool (= array_1 array_3)) +[GOOD] (define-fun s5 () Bool (= s0 s2)) +[GOOD] (define-fun s6 () Int (select array_1 s2)) +[GOOD] (define-fun s8 () Bool (= s6 s7)) +[GOOD] (define-fun s9 () Bool (and s5 s8)) +[GOOD] (assert (= array_2 (store array_0 s0 s3))) +[GOOD] (assert (= array_3 (store array_2 s1 s3))) +[GOOD] (assert (! s4 :named |c1|)) +[GOOD] (assert (! s9 :named |c2|)) +[SEND] (check-sat) +[RECV] unsat +[SEND] (get-interpolant |c1| |c2|) +[RECV] (interpolants + (= array_1 (store array_2 s1 0))) +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +["(= array_1 (store array_2 s1 0))"] diff --git a/SBVTestSuite/GoldFiles/query_Interpolant4.gold b/SBVTestSuite/GoldFiles/query_Interpolant4.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_Interpolant4.gold @@ -0,0 +1,46 @@ +** 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-interpolants true) +[GOOD] (set-option :produce-models true) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s_2 () Bool false) +[GOOD] (define-fun s_1 () Bool true) +[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 () Int) ; tracks user variable "c" +[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" +[GOOD] (declare-fun s4 () Int) ; tracks user variable "e" +[GOOD] ; --- constant tables --- +[GOOD] ; --- skolemized tables --- +[GOOD] ; --- arrays --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user given axioms --- +[GOOD] ; --- formula --- +[GOOD] (define-fun s5 () Bool (= s0 s1)) +[GOOD] (define-fun s6 () Bool (= s0 s2)) +[GOOD] (define-fun s7 () Bool (and s5 s6)) +[GOOD] (define-fun s8 () Bool (= s2 s3)) +[GOOD] (define-fun s9 () Bool (= s1 s4)) +[GOOD] (define-fun s10 () Bool (distinct s3 s4)) +[GOOD] (define-fun s11 () Bool (and s9 s10)) +[GOOD] (assert (! s7 :named |c1|)) +[GOOD] (assert (! s8 :named |c2|)) +[GOOD] (assert (! s11 :named |c3|)) +[SEND] (check-sat) +[RECV] unsat +[SEND] (get-interpolant |c1| |c2| |c3|) +[RECV] (interpolants + (= s1 s2) + (= s1 s3)) +*** Solver : Z3 +*** Exit code: ExitSuccess + +FINAL OUTPUT: +["(= s1 s2)","(= s1 s3)"] diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -0,0 +1,46 @@ +** 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") +[FAIL] (set-option :there-is-no-such-option bad argument) + + + +*** Data.SBV: Unexpected non-success response from Z3: +*** +*** Sent : (set-option :there-is-no-such-option bad argument) +*** Expected : success +*** Received : (error "line 5 column 37: unknown parameter 'there_is_no_such_option' +*** Legal parameters are: +*** auto_config (bool) (default: true) +*** debug_ref_count (bool) (default: false) +*** dump_models (bool) (default: false) +*** memory_high_watermark (unsigned int) (default: 0) +*** memory_max_alloc_count (unsigned int) (default: 0) +*** memory_max_size (unsigned int) (default: 0) +*** model (bool) (default: true) +*** model_validate (bool) (default: false) +*** proof (bool) (default: false) +*** rlimit (unsigned int) (default: 0) +*** smtlib2_compliant (bool) (default: false) +*** timeout (unsigned int) (default: 4294967295) +*** trace (bool) (default: false) +*** trace_file_name (string) (default: z3.log) +*** type_check (bool) (default: true) +*** unsat_core (bool) (default: false) +*** verbose (unsigned int) (default: 0) +*** warning (bool) (default: true) +*** well_sorted_check (bool) (default: false)") +*** Exit code : ExitFailure (-15) +*** +*** Executable: /usr/local/bin/z3 +*** Options : -nw -in -smt2 +*** +*** Backend solver reports it does not support this option. +*** Check the spelling, and if correct please report this as a +*** bug/feature request with the solver! + +CallStack (from HasCallStack): + error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.1-56ITrlqRjAjFzgs28xEVp3:Data.SBV.SMT.SMT diff --git a/SBVTestSuite/SBVDocTest.hs b/SBVTestSuite/SBVDocTest.hs --- a/SBVTestSuite/SBVDocTest.hs +++ b/SBVTestSuite/SBVDocTest.hs @@ -3,5 +3,18 @@ import System.FilePath.Glob (glob) import Test.DocTest (doctest) +import System.Exit (exitSuccess) + +import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..)) + main :: IO () -main = glob "Data/SBV/**/*.hs" >>= doctest +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 diff --git a/SBVTestSuite/SBVHLint.hs b/SBVTestSuite/SBVHLint.hs --- a/SBVTestSuite/SBVHLint.hs +++ b/SBVTestSuite/SBVHLint.hs @@ -1,5 +1,7 @@ module Main (main) where +import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..)) + import Language.Haskell.HLint (hlint) import System.Exit (exitFailure, exitSuccess) @@ -12,5 +14,16 @@ main :: IO () main = do - hints <- hlint arguments - if null hints then exitSuccess else exitFailure + 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 + where runHLint = do hints <- hlint arguments + if null hints + then exitSuccess + else exitFailure diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -2,8 +2,11 @@ module Main(main) where import Test.Tasty -import System.Environment (lookupEnv) +import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), TravisOS(..), pickTests) + +import System.Exit (exitSuccess) + import qualified TestSuite.Arrays.Memory import qualified TestSuite.Basics.AllSat import qualified TestSuite.Basics.ArithNoSolver @@ -58,6 +61,7 @@ import qualified TestSuite.Puzzles.Temperature import qualified TestSuite.Puzzles.U2Bridge import qualified TestSuite.Queries.BasicQuery +import qualified TestSuite.Queries.BadOption import qualified TestSuite.Queries.Enums import qualified TestSuite.Queries.FreshVars import qualified TestSuite.Queries.Int_ABC @@ -66,6 +70,7 @@ import qualified TestSuite.Queries.Int_Mathsat import qualified TestSuite.Queries.Int_Yices import qualified TestSuite.Queries.Int_Z3 +import qualified TestSuite.Queries.Interpolants import qualified TestSuite.Queries.Uninterpreted import qualified TestSuite.Uninterpreted.AUF import qualified TestSuite.Uninterpreted.Axioms @@ -73,18 +78,30 @@ 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. + main :: IO () -main = do mbTravis <- lookupEnv "SBV_UNDER_TRAVIS" +main = do testEnv <- getTestEnvironment - isTravis <- case mbTravis of - Just "yes" -> do putStrLn "SBVTests: Running on Travis" - return True - _ -> do putStrLn "SBVTests: Not running on Travis" - return False + putStrLn $ "SBVTest: Test platform: " ++ show testEnv - let testCases = [tc | (canRunOnTravis, tc) <- allTests, not isTravis || canRunOnTravis] + let allTestCases = testGroup "Tests" [tc | (_, tc) <- allTests] + allTravisTestCases = testGroup "Tests" [tc | (True, tc) <- allTests] - defaultMain $ testGroup "Tests" testCases + 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)] @@ -142,6 +159,7 @@ , (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) @@ -150,6 +168,7 @@ , (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) diff --git a/SBVTestSuite/TestSuite/Basics/TOut.hs b/SBVTestSuite/TestSuite/Basics/TOut.hs --- a/SBVTestSuite/TestSuite/Basics/TOut.hs +++ b/SBVTestSuite/TestSuite/Basics/TOut.hs @@ -19,5 +19,5 @@ tests :: TestTree tests = testGroup "Basics.timeout" - [ goldenVsStringShow "timeout1" (sat (setTimeOut 1000 >> euler185)) + [ goldenVsStringShow "timeout1" $ sat $ setTimeOut 1000 >> euler185 ] diff --git a/SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs b/SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs --- a/SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs +++ b/SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs @@ -18,9 +18,9 @@ tests :: TestTree tests = testGroup "BitPrecise.BitTricks" - [ testCase "fast min" (assertIsThm fastMinCorrect) - , testCase "fast max" (assertIsThm fastMaxCorrect) - , testCase "opposite signs" (assertIsThm oppositeSignsCorrect) - , testCase "conditional set clear" (assertIsThm conditionalSetClearCorrect) - , testCase "power of two" (assertIsThm powerOfTwoCorrect) + [ testCase "fast min" $ assertIsThm fastMinCorrect + , testCase "fast max" $ assertIsThm fastMaxCorrect + , testCase "opposite signs" $ assertIsThm oppositeSignsCorrect + , testCase "conditional set clear" $ assertIsThm conditionalSetClearCorrect + , testCase "power of two" $ assertIsThm powerOfTwoCorrect ] diff --git a/SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs b/SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs --- a/SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs +++ b/SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs @@ -19,7 +19,6 @@ tests :: TestTree tests = testGroup "BitPrecise.PrefixSum" - [ - testCase "prefixSum1" (assertIsThm (flIsCorrect 8 (0, (+)))) - , testCase "prefixSum2" (assertIsThm (flIsCorrect 16 (0, smax))) + [ testCase "prefixSum1" $ assertIsThm $ flIsCorrect 8 (0, (+)) + , testCase "prefixSum2" $ assertIsThm $ flIsCorrect 16 (0, smax) ] diff --git a/SBVTestSuite/TestSuite/Queries/BadOption.hs b/SBVTestSuite/TestSuite/Queries/BadOption.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Queries/BadOption.hs @@ -0,0 +1,32 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Queries.BadOption +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Testing that a bad option setting is caught properly. +----------------------------------------------------------------------------- +{-# LANGUAGE ScopedTypeVariables #-} + +module TestSuite.Queries.BadOption (tests) where + +import Data.SBV.Control +import qualified Control.Exception as C + +import Utils.SBVTestFramework + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.QueryIndividual" + [ goldenCapturedIO "query_badOption" $ \rf -> runSMTWith z3{verbose=True, redirectVerbose=Just rf} q + `C.catch` + (\(e::C.SomeException) -> appendFile rf ("\n\n" ++ show e)) + ] + +q :: Symbolic () +q = do _ <- sInteger "x" + setOption $ OptionKeyword ":there-is-no-such-option" ["bad", "argument"] + query $ return () 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 @@ -38,7 +38,7 @@ e <- sReal "e" - (f :: SWord8) <- free_ + f :: SInt8 <- free_ namedConstraint "a > 0" $ a .> 0 constrain $ b .> 0 @@ -46,6 +46,7 @@ setOption $ ProduceUnsatCores True setOption $ ProduceUnsatAssumptions True setOption $ ProduceProofs True + setOption $ ProduceInterpolants True setOption $ RandomSeed 123 setOption $ ProduceAssertions True setOption $ OptionKeyword ":smt.mbqi" ["true"] @@ -61,6 +62,7 @@ _ <- getOption ProduceAssertions _ <- getOption ProduceAssignments _ <- getOption ProduceProofs + _ <- getOption ProduceInterpolants _ <- getOption ProduceUnsatAssumptions _ <- getOption ProduceUnsatCores _ <- getOption RandomSeed diff --git a/SBVTestSuite/TestSuite/Queries/Interpolants.hs b/SBVTestSuite/TestSuite/Queries/Interpolants.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Queries/Interpolants.hs @@ -0,0 +1,97 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Queries.Interpolants +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Testing a few interpolant computations. +----------------------------------------------------------------------------- +{-# LANGUAGE ScopedTypeVariables #-} + +module TestSuite.Queries.Interpolants (tests) where + +import Data.SBV.Control + +import Utils.SBVTestFramework + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.QueryIndividual" + [ goldenCapturedIO "query_Interpolant1" $ testQuery q1 + , goldenCapturedIO "query_Interpolant2" $ testQuery q2 + , goldenCapturedIO "query_Interpolant3" $ testQuery q3 + , goldenCapturedIO "query_Interpolant4" $ testQuery q4 + ] + +testQuery :: Show a => Symbolic a -> FilePath -> IO () +testQuery t rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t + appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n") + +q1 :: Symbolic [String] +q1 = do a <- sInteger "a" + b <- sInteger "b" + c <- sInteger "c" + d <- sInteger "d" + + setOption $ ProduceInterpolants True + + namedConstraint "c1" $ a .== b &&& a .== c + namedConstraint "c2" $ b .== d &&& bnot (c .== d) + + query $ do _ <- checkSat + getInterpolant ["c1", "c2"] + +q2 :: Symbolic [String] +q2 = do a <- sInteger "a" + b <- sInteger "b" + c <- sInteger "c" + d <- sInteger "d" + + let f, g :: SInteger -> SInteger + f = uninterpret "f" + g = uninterpret "g" + + setOption $ ProduceInterpolants True + + namedConstraint "c1" $ f a .== c &&& f b .== d + namedConstraint "c2" $ a .== b &&& g c ./= g d + + query $ do _ <- checkSat + getInterpolant ["c1", "c2"] + +q3 :: Symbolic [String] +q3 = do x <- sInteger "x" + y <- sInteger "y" + z <- sInteger "z" + + a :: SArray Integer Integer <- newArray "a" + b :: SArray Integer Integer <- newArray "b" + + namedConstraint "c1" $ b .== writeArray (writeArray a x 0) y (0::SInteger) + namedConstraint "c2" $ z .== x &&& readArray b z .== 1 + + setOption $ ProduceInterpolants True + + query $ do _ <- checkSat + getInterpolant ["c1", "c2"] + +q4 :: Symbolic [String] +q4 = do a <- sInteger "a" + b <- sInteger "b" + c <- sInteger "c" + d <- sInteger "d" + e <- sInteger "e" + + namedConstraint "c1" $ a .== b &&& a .== c + namedConstraint "c2" $ c .== d + namedConstraint "c3" $ b .== e &&& d ./= e + + setOption $ ProduceInterpolants True + + query $ do _ <- checkSat + getInterpolant ["c1", "c2", "c3"] + +{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-} diff --git a/SBVTestSuite/Utils/SBVTestFramework.hs b/SBVTestSuite/Utils/SBVTestFramework.hs --- a/SBVTestSuite/Utils/SBVTestFramework.hs +++ b/SBVTestSuite/Utils/SBVTestFramework.hs @@ -19,6 +19,8 @@ , goldenString , goldenVsStringShow , goldenCapturedIO + , TravisOS(..), TestEnvironment(..), getTestEnvironment + , pickTests -- module exports to simplify life , module Test.Tasty , module Test.Tasty.HUnit @@ -30,16 +32,47 @@ import qualified Data.ByteString.Lazy.Char8 as LBC 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.Runners hiding (Result) +import System.Random (randomRIO) + import Data.SBV +import Data.Maybe(fromMaybe, catMaybes) + import System.FilePath ((), (<.>)) 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 + +data TestEnvironment = TestEnvLocal + | TestEnvTravis TravisOS + | TestEnvUnknown + deriving Show + +getTestEnvironment :: IO TestEnvironment +getTestEnvironment = do mbTestEnv <- lookupEnv "SBV_TEST_ENVIRONMENT" + + 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 + -- | Checks that a particular result shows as @s@ showsAs :: Show a => a -> String -> Assertion showsAs r s = assert $ show r == s @@ -84,3 +117,20 @@ -- | Turn provable to a negative assertion, satisfiability case assertIsntSat :: Provable a => a -> Assertion assertIsntSat p = assert (fmap not (isSatisfiable p)) + +-- | Picking a certain percent of tests. +pickTests :: Int -> TestTree -> IO TestTree +pickTests d origTests = fromMaybe noTestsSelected <$> walk origTests + where noTestsSelected = TestGroup "pickTests.NoTestsSelected" [] + + walk PlusTestOptions{} = error "pickTests: Unexpected PlusTestOptions" + walk WithResource{} = error "pickTests: Unexpected WithResource" + walk AskOptions{} = error "pickTests: Unexpected AskOptions" + walk t@SingleTest{} = do c <- randomRIO (0, 99) + if c < d + then return $ Just t + else return Nothing + walk (TestGroup tn ts) = do cs <- catMaybes <$> mapM walk ts + case cs of + [] -> return Nothing + _ -> return $ Just $ TestGroup tn cs diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 7.0 +Version: 7.1 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 @@ -106,6 +106,7 @@ , Data.SBV.Examples.Queries.GuessNumber , Data.SBV.Examples.Queries.CaseSplit , Data.SBV.Examples.Queries.Enums + , Data.SBV.Examples.Queries.Interpolants , Data.SBV.Examples.Uninterpreted.AUF , Data.SBV.Examples.Uninterpreted.Deduce , Data.SBV.Examples.Uninterpreted.Function @@ -217,6 +218,7 @@ , TestSuite.Puzzles.Temperature , TestSuite.Puzzles.U2Bridge , TestSuite.Queries.BasicQuery + , TestSuite.Queries.BadOption , TestSuite.Queries.Enums , TestSuite.Queries.FreshVars , TestSuite.Queries.Int_ABC @@ -225,6 +227,7 @@ , TestSuite.Queries.Int_Mathsat , TestSuite.Queries.Int_Yices , TestSuite.Queries.Int_Z3 + , TestSuite.Queries.Interpolants , TestSuite.Queries.Uninterpreted , TestSuite.Uninterpreted.AUF , TestSuite.Uninterpreted.Axioms @@ -233,15 +236,30 @@ , TestSuite.Uninterpreted.Uninterpreted Test-Suite SBVDocTest - Build-Depends: base, doctest >= 0.9, Glob >= 0.7 + Build-Depends: base, directory, filepath, random + , doctest >= 0.9 + , Glob >= 0.7 + , bytestring >= 0.9 + , tasty >= 0.11.2.3 + , tasty-golden >= 2.3.1.1 + , tasty-hunit >= 0.9.2 + , sbv default-language: Haskell2010 Hs-Source-Dirs : SBVTestSuite main-is: SBVDocTest.hs + Other-modules : Utils.SBVTestFramework type: exitcode-stdio-1.0 Test-Suite SBVHLint - build-depends: base, hlint >= 2.0.9 + build-depends: base, directory, filepath, random + , hlint >= 2.0.9 + , bytestring >= 0.9 + , tasty >= 0.11.2.3 + , tasty-golden >= 2.3.1.1 + , tasty-hunit >= 0.9.2 + , sbv default-language: Haskell2010 hs-source-dirs: SBVTestSuite + Other-modules : Utils.SBVTestFramework main-is: SBVHLint.hs type: exitcode-stdio-1.0