sbv 7.0 → 7.1
raw patch · 31 files changed
+786/−87 lines, 31 files
Files
- CHANGES.md +14/−1
- Data/SBV/Control.hs +10/−14
- Data/SBV/Control/Query.hs +75/−7
- Data/SBV/Control/Types.hs +3/−0
- Data/SBV/Core/Operations.hs +1/−1
- Data/SBV/Examples/Misc/Enumerate.hs +2/−0
- Data/SBV/Examples/Puzzles/Fish.hs +10/−0
- Data/SBV/Examples/Puzzles/U2Bridge.hs +4/−0
- Data/SBV/Examples/Queries/Enums.hs +2/−0
- Data/SBV/Examples/Queries/FourFours.hs +57/−27
- Data/SBV/Examples/Queries/Interpolants.hs +65/−0
- Data/SBV/SMT/SMT.hs +23/−3
- Data/SBV/Tools/STree.hs +2/−2
- README.md +11/−2
- SBVTestSuite/GoldFiles/noTravis_query1.gold +8/−5
- SBVTestSuite/GoldFiles/query_Interpolant1.gold +43/−0
- SBVTestSuite/GoldFiles/query_Interpolant2.gold +48/−0
- SBVTestSuite/GoldFiles/query_Interpolant3.gold +48/−0
- SBVTestSuite/GoldFiles/query_Interpolant4.gold +46/−0
- SBVTestSuite/GoldFiles/query_badOption.gold +46/−0
- SBVTestSuite/SBVDocTest.hs +14/−1
- SBVTestSuite/SBVHLint.hs +15/−2
- SBVTestSuite/SBVTest.hs +28/−9
- SBVTestSuite/TestSuite/Basics/TOut.hs +1/−1
- SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs +5/−5
- SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs +2/−3
- SBVTestSuite/TestSuite/Queries/BadOption.hs +32/−0
- SBVTestSuite/TestSuite/Queries/BasicQuery.hs +3/−1
- SBVTestSuite/TestSuite/Queries/Interpolants.hs +97/−0
- SBVTestSuite/Utils/SBVTestFramework.hs +50/−0
- sbv.cabal +21/−3
CHANGES.md view
@@ -1,7 +1,20 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* 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
Data/SBV/Control.hs view
@@ -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. -}
Data/SBV/Control/Query.hs view
@@ -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
Data/SBV/Control/Types.hs view
@@ -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]
Data/SBV/Core/Operations.hs view
@@ -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]
Data/SBV/Examples/Misc/Enumerate.hs view
@@ -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
Data/SBV/Examples/Puzzles/Fish.hs view
@@ -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:
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -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'
Data/SBV/Examples/Queries/Enums.hs view
@@ -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'
Data/SBV/Examples/Queries/FourFours.hs view
@@ -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]
+ Data/SBV/Examples/Queries/Interpolants.hs view
@@ -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!"
Data/SBV/SMT/SMT.hs view
@@ -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!"
Data/SBV/Tools/STree.hs view
@@ -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)
README.md view
@@ -1,6 +1,15 @@ ## SBV: SMT Based Verification in Haskell +Please see: http://leventerkok.github.io/sbv/+ [](http://hackage.haskell.org/package/sbv)-[](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
SBVTestSuite/GoldFiles/noTravis_query1.gold view
@@ -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!
+ SBVTestSuite/GoldFiles/query_Interpolant1.gold view
@@ -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)"]
+ SBVTestSuite/GoldFiles/query_Interpolant2.gold view
@@ -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)))"]
+ SBVTestSuite/GoldFiles/query_Interpolant3.gold view
@@ -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))"]
+ SBVTestSuite/GoldFiles/query_Interpolant4.gold view
@@ -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)"]
+ SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -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
SBVTestSuite/SBVDocTest.hs view
@@ -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
SBVTestSuite/SBVHLint.hs view
@@ -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
SBVTestSuite/SBVTest.hs view
@@ -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)
SBVTestSuite/TestSuite/Basics/TOut.hs view
@@ -19,5 +19,5 @@ tests :: TestTree tests = testGroup "Basics.timeout"- [ goldenVsStringShow "timeout1" (sat (setTimeOut 1000 >> euler185))+ [ goldenVsStringShow "timeout1" $ sat $ setTimeOut 1000 >> euler185 ]
SBVTestSuite/TestSuite/BitPrecise/BitTricks.hs view
@@ -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 ]
SBVTestSuite/TestSuite/BitPrecise/PrefixSum.hs view
@@ -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) ]
+ SBVTestSuite/TestSuite/Queries/BadOption.hs view
@@ -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 ()
SBVTestSuite/TestSuite/Queries/BasicQuery.hs view
@@ -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
+ SBVTestSuite/TestSuite/Queries/Interpolants.hs view
@@ -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) #-}
SBVTestSuite/Utils/SBVTestFramework.hs view
@@ -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
sbv.cabal view
@@ -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