sbv 7.7 → 7.8
raw patch · 34 files changed
+680/−180 lines, 34 files
Files
- CHANGES.md +38/−3
- Data/SBV.hs +7/−6
- Data/SBV/Compilers/C.hs +34/−19
- Data/SBV/Compilers/CodeGen.hs +62/−46
- Data/SBV/Control/Query.hs +37/−1
- Data/SBV/Control/Utils.hs +10/−4
- Data/SBV/Core/Data.hs +8/−1
- Data/SBV/Core/Model.hs +0/−7
- Data/SBV/Core/Operations.hs +61/−7
- Data/SBV/Core/Symbolic.hs +22/−12
- Data/SBV/SMT/SMT.hs +1/−0
- Data/SBV/SMT/SMTLib.hs +4/−4
- Data/SBV/SMT/SMTLib2.hs +59/−17
- Data/SBV/SMT/Utils.hs +1/−0
- Data/SBV/Tools/CodeGen.hs +1/−1
- Data/SBV/Tools/GenTest.hs +1/−1
- Data/SBV/Utils/PrettyNum.hs +28/−1
- Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +141/−0
- SBVTestSuite/GoldFiles/queryArrays6.gold +79/−0
- SBVTestSuite/GoldFiles/tgen_c.gold +10/−10
- SBVTestSuite/TestSuite/Arrays/Query.hs +17/−0
- SBVTestSuite/TestSuite/BitPrecise/Legato.hs +2/−2
- SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs +2/−2
- SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs +2/−2
- SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs +2/−2
- SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs +4/−4
- SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs +4/−4
- SBVTestSuite/TestSuite/CodeGeneration/Floats.hs +1/−1
- SBVTestSuite/TestSuite/CodeGeneration/GCD.hs +2/−2
- SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs +2/−2
- SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs +3/−4
- SBVTestSuite/TestSuite/Crypto/AES.hs +3/−3
- SBVTestSuite/Utils/SBVTestFramework.hs +29/−10
- sbv.cabal +3/−2
CHANGES.md view
@@ -1,8 +1,44 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.7, 2018-04-29+* Latest Hackage released version: 7.8, 2018-05-18 +### Version 7.8, Released 2018-05-18++ * Fix printing of min-bounds for signed 32/64 bit numbers: These+ are tricky since C does not allow -min_value as a valid literal!+ Instead we use the macros provided in stdint.h. Thanks to Matt+ Peddie for reporting this corner case.++ * Fix translation of the "abs" function, to make sure we use+ the correct variant. Thanks to Matt Peddie for reporting.++ * Fix handling of tables and arrays in pushed-contexts. Previously,+ we used initializers to get table/array values stored properly.+ However, this trick does not work if we are in a pushed-context;+ since a pop can forget the corresponding assignments. SBV now+ handles this corner case properly, by using tracker assertions+ to keep track of what array values must be restored at each pop.+ Thanks to Martin Brain on the SMTLib mailing list for the+ suggestion. (See https://github.com/LeventErkok/sbv/issues/374+ for details.)++ * Fix corner case in ite branch equality with float/double arguments,+ where we were previously confusing +/-0 as equal to each other.+ Thanks to Matt Peddie for reporting.++ * Add a call 'cgOverwriteFiles', which suppresses code-generation+ prompts for overwriting files and quiets the prompts during+ code generation. Thanks to Matt Peddie for the suggestion.++ * Add support for uninterpreted function introductions in the query+ mode. Previously, this was only allowed before the query started,+ now we fully support uninterpreted functions in all modes.++ * New example: Documentation/SBV/Examples/Puzzles/HexPuzzle.hs,+ showing how to code cover properties using SBV, using a form+ of bounded model checking.+ ### Version 7.7, Released 2018-04-29 * Add support for Symbolic characters ('SChar') and strings ('SString'.)@@ -1183,8 +1219,7 @@ ### Version 2.9, 2013-01-02 - * Add support for the CVC4 SMT solver from New York University and- the University of Iowa. <http://cvc4.cs.nyu.edu/>.+ * Add support for the CVC4 SMT solver from Stanford: <http://cvc4.cs.stanford.edu/web/> NB. Z3 remains the default solver for SBV. To use CVC4, use the *With variants of the interface (i.e., proveWith, satWith, ..) by passing cvc4 as the solver argument. (Similarly, use 'yices'
Data/SBV.hs view
@@ -90,7 +90,7 @@ -- -- * ABC from University of Berkeley: <http://www.eecs.berkeley.edu/~alanmi/abc/> ----- * CVC4 from New York University and University of Iowa: <http://cvc4.cs.nyu.edu/>+-- * CVC4 from Stanford: <http://cvc4.cs.stanford.edu/web/> -- -- * Boolector from Johannes Kepler University: <http://fmv.jku.at/boolector/> --@@ -142,9 +142,9 @@ -- ** Algebraic reals -- $algReals , SReal, AlgReal, sRealToSInteger- -- ** Strings and Regular Expressions+ -- ** Characters, Strings and Regular Expressions -- $strings- , SString, SChar, (.++), (.!!)+ , SChar, SString, (.++), (.!!) -- * Arrays of symbolic values , SymArray(..), SArray, SFunArray, mkSFunArray @@ -702,9 +702,10 @@ -} {- $strings-Support for strings (intial version contributed by Joel Burget) adds support for QF_S logic,-described here: <https://rise4fun.com/z3/tutorialcontent/sequences>. Note that this logic-is still not part of official SMTLib (as of March 2018), so it should be considered+Support for characters, strings, and regular expressions (intial version contributed by Joel Burget)+adds support for QF_S logic, described here: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>+and here: <https://rise4fun.com/z3/tutorialcontent/sequences>. Note+that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental. See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for further related functions.
Data/SBV/Compilers/C.hs view
@@ -30,7 +30,7 @@ import Data.SBV.Core.Data import Data.SBV.Compilers.CodeGen -import Data.SBV.Utils.PrettyNum (shex, showCFloat, showCDouble)+import Data.SBV.Utils.PrettyNum (chex, showCFloat, showCDouble) import GHC.Stack @@ -53,7 +53,7 @@ compileToC mbDirName nm f = compileToC' nm f >>= renderCgPgmBundle mbDirName -- | Lower level version of 'compileToC', producing a 'CgPgmBundle'-compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle+compileToC' :: String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle) compileToC' nm f = do rands <- randoms `fmap` newStdGen codeGen SBVToC (defaultCgConfig { cgDriverVals = rands }) nm f @@ -71,7 +71,7 @@ compileToCLib mbDirName libName comps = compileToCLib' libName comps >>= renderCgPgmBundle mbDirName -- | Lower level version of 'compileToCLib', producing a 'CgPgmBundle'-compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle+compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO (CgConfig, CgPgmBundle) compileToCLib' libName comps = mergeToLib libName `fmap` mapM (uncurry compileToC') comps ---------------------------------------------------------------------------@@ -223,12 +223,12 @@ showSizedConst i (False, 1) = text (if i == 0 then "false" else "true") showSizedConst i (False, 8) = integer i showSizedConst i (True, 8) = integer i-showSizedConst i t@(False, 16) = text (shex False True t i) P.<> text "U"-showSizedConst i t@(True, 16) = text (shex False True t i)-showSizedConst i t@(False, 32) = text (shex False True t i) P.<> text "UL"-showSizedConst i t@(True, 32) = text (shex False True t i) P.<> text "L"-showSizedConst i t@(False, 64) = text (shex False True t i) P.<> text "ULL"-showSizedConst i t@(True, 64) = text (shex False True t i) P.<> text "LL"+showSizedConst i t@(False, 16) = text $ chex False True t i+showSizedConst i t@(True, 16) = text $ chex False True t i+showSizedConst i t@(False, 32) = text $ chex False True t i+showSizedConst i t@(True, 32) = text $ chex False True t i+showSizedConst i t@(False, 64) = text $ chex False True t i+showSizedConst i t@(True, 64) = text $ chex False True t i showSizedConst i (True, 1) = die $ "Signed 1-bit value " ++ show i showSizedConst i (s, sz) = die $ "Constant " ++ show i ++ " at type " ++ (if s then "SInt" else "SWord") ++ show sz @@ -735,11 +735,21 @@ in protectDiv0 k "/" z a b p Rem [a, b] = protectDiv0 (kindOf (head opArgs)) "%" a a b p UNeg [a] = parens (text "-" <+> a)- p Abs [a] = let f = case kindOf (head opArgs) of- KFloat -> text "fabsf"- KDouble -> text "fabs"- _ -> text "abs"- in f P.<> parens a+ p Abs [a] = let f KFloat = text "fabsf" P.<> parens a+ f KDouble = text "fabs" P.<> parens a+ f (KBounded False _) = text "/* unsigned, skipping call to abs */" <+> a+ f (KBounded True 32) = text "labs" P.<> parens a+ f (KBounded True 64) = text "llabs" P.<> parens a+ f KUnbounded = case cgInteger cfg of+ Nothing -> f $ KBounded True 32 -- won't matter, it'll be rejected later+ Just i -> f $ KBounded True i+ f KReal = case cgReal cfg of+ Nothing -> f KDouble -- won't matter, it'll be rejected later+ Just CgFloat -> f KFloat+ Just CgDouble -> f KDouble+ Just CgLongDouble -> text "fabsl" P.<> parens a+ f _ = text "abs" P.<> parens a+ in f (kindOf (head opArgs)) -- for And/Or, translate to boolean versions if on boolean kind p And [a, b] | kindOf (head opArgs) == KBool = a <+> text "&&" <+> b p Or [a, b] | kindOf (head opArgs) == KBool = a <+> text "||" <+> b@@ -837,15 +847,17 @@ l = maximum (0 : map length ss) pad s = replicate (l - length s) ' ' ++ s --- | Merge a bunch of bundles to generate code for a library-mergeToLib :: String -> [CgPgmBundle] -> CgPgmBundle-mergeToLib libName bundles+-- | Merge a bunch of bundles to generate code for a library. For the final+-- config, we simply return the first config we receive, or the default if none.+mergeToLib :: String -> [(CgConfig, CgPgmBundle)] -> (CgConfig, CgPgmBundle)+mergeToLib libName cfgBundles | length nubKinds /= 1 = error $ "Cannot merge programs with differing SInteger/SReal mappings. Received the following kinds:\n" ++ unlines (map show nubKinds) | True- = CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake]- where kinds = [k | CgPgmBundle k _ <- bundles]+ = (finalCfg, CgPgmBundle bundleKind $ sources ++ libHeader : [libDriver | anyDriver] ++ [libMake | anyMake])+ where bundles = map snd cfgBundles+ kinds = [k | CgPgmBundle k _ <- bundles] nubKinds = nub kinds bundleKind = head nubKinds files = concat [fs | CgPgmBundle _ fs <- bundles]@@ -860,6 +872,9 @@ libHInclude = text "#include" <+> text (show (libName ++ ".h")) libMake = ("Makefile", (CgMakefile mkFlags, [genLibMake anyDriver libName sourceNms mkFlags])) libDriver = (libName ++ "_driver.c", (CgDriver, mergeDrivers libName libHInclude (zip (map takeBaseName sourceNms) drivers)))+ finalCfg = case cfgBundles of+ [] -> defaultCgConfig+ ((c, _):_) -> c -- | Create a Makefile for the library genLibMake :: Bool -> String -> [String] -> [String] -> Doc
Data/SBV/Compilers/CodeGen.hs view
@@ -28,7 +28,7 @@ -- * Settings , cgPerformRTCs, cgSetDriverValues- , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert+ , cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert, cgOverwriteFiles , cgIntegerSize, cgSRealType, CgSRealType(..) -- * Infrastructure@@ -62,24 +62,26 @@ -- | Options for code-generation. data CgConfig = CgConfig {- cgRTC :: Bool -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.- , cgInteger :: Maybe Int -- ^ Bit-size to use for representing SInteger (if any)- , cgReal :: Maybe CgSRealType -- ^ Type to use for representing SReal (if any)- , cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers.- , cgGenDriver :: Bool -- ^ If 'True', will generate a driver program- , cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile- , cgIgnoreAsserts :: Bool -- ^ If 'True', will ignore 'sAssert' calls+ cgRTC :: Bool -- ^ If 'True', perform run-time-checks for index-out-of-bounds or shifting-by-large values etc.+ , cgInteger :: Maybe Int -- ^ Bit-size to use for representing SInteger (if any)+ , cgReal :: Maybe CgSRealType -- ^ Type to use for representing SReal (if any)+ , cgDriverVals :: [Integer] -- ^ Values to use for the driver program generated, useful for generating non-random drivers.+ , cgGenDriver :: Bool -- ^ If 'True', will generate a driver program+ , cgGenMakefile :: Bool -- ^ If 'True', will generate a makefile+ , cgIgnoreAsserts :: Bool -- ^ If 'True', will ignore 'sAssert' calls+ , cgOverwriteGenerated :: Bool -- ^ If 'True', will overwrite the generated files without prompting. } -- | Default options for code generation. The run-time checks are turned-off, and the driver values are completely random. defaultCgConfig :: CgConfig-defaultCgConfig = CgConfig { cgRTC = False- , cgInteger = Nothing- , cgReal = Nothing- , cgDriverVals = []- , cgGenDriver = True- , cgGenMakefile = True- , cgIgnoreAsserts = False+defaultCgConfig = CgConfig { cgRTC = False+ , cgInteger = Nothing+ , cgReal = Nothing+ , cgDriverVals = []+ , cgGenDriver = True+ , cgGenMakefile = True+ , cgIgnoreAsserts = False+ , cgOverwriteGenerated = False } -- | Abstraction of target language values@@ -88,25 +90,25 @@ -- | Code-generation state data CgState = CgState {- cgInputs :: [(String, CgVal)]- , cgOutputs :: [(String, CgVal)]- , cgReturns :: [CgVal]- , cgPrototypes :: [String] -- extra stuff that goes into the header- , cgDecls :: [String] -- extra stuff that goes into the top of the file- , cgLDFlags :: [String] -- extra options that go to the linker- , cgFinalConfig :: CgConfig+ cgInputs :: [(String, CgVal)]+ , cgOutputs :: [(String, CgVal)]+ , cgReturns :: [CgVal]+ , cgPrototypes :: [String] -- extra stuff that goes into the header+ , cgDecls :: [String] -- extra stuff that goes into the top of the file+ , cgLDFlags :: [String] -- extra options that go to the linker+ , cgFinalConfig :: CgConfig } -- | Initial configuration for code-generation initCgState :: CgState initCgState = CgState {- cgInputs = []- , cgOutputs = []- , cgReturns = []- , cgPrototypes = []- , cgDecls = []- , cgLDFlags = []- , cgFinalConfig = defaultCgConfig+ cgInputs = []+ , cgOutputs = []+ , cgReturns = []+ , cgPrototypes = []+ , cgDecls = []+ , cgLDFlags = []+ , cgFinalConfig = defaultCgConfig } -- | The code-generation monad. Allows for precise layout of input values@@ -184,6 +186,11 @@ new = if null old then ss else old ++ [""] ++ ss in s { cgPrototypes = new }) +-- | If passed 'True', then we will not ask the user if we're overwriting files as we generate+-- the C code. Otherwise, we'll prompt.+cgOverwriteFiles :: Bool -> SBVCodeGen ()+cgOverwriteFiles b = modify' (\s -> s { cgFinalConfig = (cgFinalConfig s) { cgOverwriteGenerated = b } })+ -- | Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions. cgAddDecl :: [String] -> SBVCodeGen () cgAddDecl ss = modify' (\s -> s { cgDecls = cgDecls s ++ ss })@@ -313,7 +320,7 @@ -- | Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection -- of makefiles, source code, headers, etc.-codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle+codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO (CgConfig, CgPgmBundle) codeGen l cgConfig nm (SBVCodeGen comp) = do (((), st'), res) <- runSymbolic CodeGen $ runStateT comp initCgState { cgFinalConfig = cgConfig } let st = st' { cgInputs = reverse (cgInputs st')@@ -323,29 +330,38 @@ dupNames = allNamedVars \\ nub allNamedVars unless (null dupNames) $ error $ "SBV.codeGen: " ++ show nm ++ " has following argument names duplicated: " ++ unwords dupNames- return $ translate l (cgFinalConfig st) nm st res + return (cgFinalConfig st, translate l (cgFinalConfig st) nm st res)+ -- | Render a code-gen bundle to a directory or to stdout-renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()-renderCgPgmBundle Nothing bundle = print bundle-renderCgPgmBundle (Just dirName) (CgPgmBundle _ files) = do+renderCgPgmBundle :: Maybe FilePath -> (CgConfig, CgPgmBundle) -> IO ()+renderCgPgmBundle Nothing (_ , bundle) = print bundle+renderCgPgmBundle (Just dirName) (cfg, CgPgmBundle _ files) = do+ b <- doesDirectoryExist dirName- unless b $ do putStrLn $ "Creating directory " ++ show dirName ++ ".."+ unless b $ do unless overWrite $ putStrLn $ "Creating directory " ++ show dirName ++ ".." createDirectoryIfMissing True dirName+ dups <- filterM (\fn -> doesFileExist (dirName </> fn)) (map fst files)- goOn <- case dups of- [] -> return True- _ -> do putStrLn $ "Code generation would override the following " ++ (if length dups == 1 then "file:" else "files:")- mapM_ (\fn -> putStrLn ('\t' : fn)) dups- putStr "Continue? [yn] "- hFlush stdout- resp <- getLine- return $ map toLower resp `isPrefixOf` "yes"++ goOn <- case (overWrite, dups) of+ (True, _) -> return True+ (_, []) -> return True+ _ -> do putStrLn $ "Code generation would overwrite the following " ++ (if length dups == 1 then "file:" else "files:")+ mapM_ (\fn -> putStrLn ('\t' : fn)) dups+ putStr "Continue? [yn] "+ hFlush stdout+ resp <- getLine+ return $ map toLower resp `isPrefixOf` "yes"+ if goOn then do mapM_ renderFile files- putStrLn "Done."+ unless overWrite $ putStrLn "Done." else putStrLn "Aborting."- where renderFile (f, (_, ds)) = do let fn = dirName </> f- putStrLn $ "Generating: " ++ show fn ++ ".."++ where overWrite = cgOverwriteGenerated cfg++ renderFile (f, (_, ds)) = do let fn = dirName </> f+ unless overWrite $ putStrLn $ "Generating: " ++ show fn ++ ".." writeFile fn (render' (vcat ds)) -- | An alternative to Pretty's 'render', which might have "leading" white-space in empty lines. This version
Data/SBV/Control/Query.hs view
@@ -33,8 +33,11 @@ import Control.Monad (unless, when, zipWithM) import Control.Monad.State.Lazy (get) -import Data.IORef (readIORef)+import Data.IORef (readIORef) +import qualified Data.Map as M+import qualified Data.IntMap as IM+ import Data.List (unzip3, intercalate, nubBy, sortBy) import Data.Maybe (listToMaybe, catMaybes) import Data.Function (on)@@ -438,6 +441,37 @@ getAssertionStackDepth :: Query Int getAssertionStackDepth = queryAssertionStackDepth <$> getQueryState +-- | Upon a pop, we need to restore all arrays and tables. See: https://github.com/LeventErkok/sbv/issues/374+restoreTablesAndArrays :: Query ()+restoreTablesAndArrays = do st <- get+ qs <- getQueryState++ case queryTblArrPreserveIndex qs of+ Nothing -> return ()+ Just (tc, ac) -> do tCount <- M.size <$> (io . readIORef) (rtblMap st)+ aCount <- IM.size <$> (io . readIORef) (rArrayMap st)++ let tInits = [ "table" ++ show i ++ "_initializer" | i <- [tc .. tCount - 1]]+ aInits = [ "array_" ++ show i ++ "_initializer" | i <- [ac .. aCount - 1]]+ inits = tInits ++ aInits++ case inits of+ [] -> return () -- Nothing to do+ [x] -> send True $ "(assert " ++ x ++ ")"+ xs -> send True $ "(assert (and " ++ unwords xs ++ "))"++-- | Upon a push, record the cut-off point for table and array restoration, if we haven't already+recordTablesAndArrayCutOff :: Query ()+recordTablesAndArrayCutOff = do st <- get+ qs <- getQueryState++ case queryTblArrPreserveIndex qs of+ Just _ -> return () -- already recorded, nothing to do+ Nothing -> do tCount <- M.size <$> (io . readIORef) (rtblMap st)+ aCount <- IM.size <$> (io . readIORef) (rArrayMap st)++ modifyQueryState $ \s -> s {queryTblArrPreserveIndex = Just (tCount, aCount)}+ -- | Run the query in a new assertion stack. That is, we push the context, run the query -- commands, and pop it back. inNewAssertionStack :: Query a -> Query a@@ -452,6 +486,7 @@ | i <= 0 = error $ "Data.SBV: push requires a strictly positive level argument, received: " ++ show i | True = do depth <- getAssertionStackDepth send True $ "(push " ++ show i ++ ")"+ recordTablesAndArrayCutOff modifyQueryState $ \s -> s{queryAssertionStackDepth = depth + i} -- | Pop the context, exiting a new one. Pops multiple levels if /n/ > 1. It's an error to pop levels that don't exist.@@ -470,6 +505,7 @@ , "*** Request this as a feature for the underlying solver!" ] else do send True $ "(pop " ++ show i ++ ")"+ restoreTablesAndArrays modifyQueryState $ \s -> s{queryAssertionStackDepth = depth - i} where shl 1 = "one level" shl n = show n ++ " levels"
Data/SBV/Control/Utils.hs view
@@ -34,6 +34,7 @@ , runProofOn ) where +import Data.Maybe (isJust) import Data.List (sortBy, elemIndex, partition, groupBy, tails) import Data.Char (isPunctuation, isSpace, chr)@@ -126,8 +127,8 @@ io = liftIO -- | Sync-up the external solver with new context we have generated-syncUpSolver :: IncState -> Query ()-syncUpSolver is = do+syncUpSolver :: Bool -> IncState -> Query ()+syncUpSolver afterAPush is = do cfg <- getConfig ls <- io $ do let swap (a, b) = (b, a) swapc ((_, a), b) = (b, a)@@ -138,8 +139,9 @@ cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is) arrs <- IMap.toAscList <$> readIORef (rNewArrs is) tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is)+ uis <- Map.toAscList <$> readIORef (rNewUIs is) as <- readIORef (rNewAsgns is)- return $ toIncSMTLib cfg inps ks cnsts arrs tbls as cfg+ return $ toIncSMTLib afterAPush cfg inps ks cnsts arrs tbls uis as cfg mapM_ (send True) $ mergeSExpr ls -- | Retrieve the query context@@ -169,7 +171,11 @@ inNewContext :: (State -> IO a) -> Query a inNewContext act = do st <- get (is, r) <- io $ withNewIncState st act- syncUpSolver is+ mbQS <- io . readIORef . queryState $ st+ let afterAPush = case mbQS of+ Nothing -> False+ Just qs -> isJust (queryTblArrPreserveIndex qs)+ syncUpSolver afterAPush is return r -- | Similar to 'freshVar', except creates unnamed variable.
Data/SBV/Core/Data.hs view
@@ -477,7 +477,7 @@ -- -- * Internally handled by the library and not mapped to SMT-Lib ----- * Reading an uninitialized value is considered an error (will throw exception)+-- * Reading an uninitialized value is considered an error (will throw exception). See `mkSFunArray` on how to avoid this. -- -- * Cannot check for equality (internally represented as functions) --@@ -491,6 +491,13 @@ show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">" -- | Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use `newArray`.)+-- A simple way to create an array such that reading an unintialized value is assigned a free variable is+-- to simply use an uninterpreted function. That is, use:+--+-- @ mkSFunArray (uninterpret "initial") @+--+-- Note that this will ensure all uninitialized reads to the same location will return the same value,+-- without constraining them otherwise; with different indexes containing different values. mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b mkSFunArray = SFunArray
Data/SBV/Core/Model.hs view
@@ -71,12 +71,6 @@ import Data.SBV.Utils.Boolean -mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW-mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b)--mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW-mkSymOp = mkSymOpSC (const (const Nothing))- -- Symbolic-Word class instances -- | Generate a finite symbolic bitvector, named@@ -1313,7 +1307,6 @@ -- Default implementation for 'symbolicMerge' if the type is 'Generic' default symbolicMerge :: (G.Generic a, GMergeable (G.Rep a)) => Bool -> SBool -> a -> a -> a symbolicMerge = symbolicMergeDefault- -- | If-then-else. This is by definition 'symbolicMerge' with both -- branches forced. This is typically the desired behavior, but also
Data/SBV/Core/Operations.hs view
@@ -37,6 +37,8 @@ , svRotateLeft, svRotateRight , svBlastLE, svBlastBE , svAddConstant, svIncrement, svDecrement+ -- Utils+ , mkSymOp ) where @@ -47,6 +49,7 @@ import Data.SBV.Core.Kind import Data.SBV.Core.Concrete import Data.SBV.Core.Symbolic+import Data.SBV.Utils.Numeric (fpIsEqualObjectH) import Data.Ratio @@ -480,11 +483,19 @@ svSymbolicMerge k force t a b | Just r <- svAsBool t = if r then a else b- | force, rationalSBVCheck a b, areConcretelyEqual a b+ | force, rationalSBVCheck a b, sameResult a b = a | True = SVal k $ Right $ cache c- where c st = do swt <- svToSW st t+ where+ -- Be careful with +/-0 here! See https://github.com/LeventErkok/sbv/issues/382+ sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2 && floatCheck (cwVal c1) (cwVal c2)+ sameResult _ _ = False+ floatCheck (CWFloat f1) (CWFloat f2) = f1 `fpIsEqualObjectH` f2+ floatCheck (CWDouble d1) (CWDouble d2) = d1 `fpIsEqualObjectH` d2+ floatCheck _ _ = True++ c st = do swt <- svToSW st t case () of () | swt == trueSW -> svToSW st a -- these two cases should never be needed as we expect symbolicMerge to be () | swt == falseSW -> svToSW st b -- called with symbolic tests, but just in case..@@ -819,6 +830,52 @@ where c st = do swa <- svToSW st a opS st k swa +{- A note on constant folding.++There are cases where we miss out on certain constant foldings. On May 8 2018, Matt Peddie pointed this+out, as the C code he was getting had redundancies. I was aware that could be missing constant foldings+due to missed out optimizations, or some other code snafu, but till Matt pointed it out I haven't realized+that we could be hiding constants inside an if-then-else. The example is:++ proveWith z3{verbose=True} $ \x -> 0 .< ite (x .== (x::SWord8)) 1 (2::SWord8)++If you try this, you'll see that it generates (shortened):++ (define-fun s1 () (_ BitVec 8) #x00)+ (define-fun s2 () (_ BitVec 8) #x01)+ (define-fun s3 () Bool (bvult s1 s2))++But clearly we have all the info for s3 to be computed! The issue here is that the reduction of @x .== x@ to @true@+happens after we start computing the if-then-else, hence we are already committed to an SW at that point. The call+to ite eventually recognizes this, but at that point it picks up the now constants from SW's, missing the constant+folding opportunity.++We can fix this, by looking up the constants table in liftSW2, like this:+++ liftSW2 :: (CW -> CW -> Bool) -> (CW -> CW -> CW) -> (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SVal -> SVal -> Cached SW+ liftSW2 okCW opCW opS k a b = cache c+ where c st = do sw1 <- svToSW st a+ sw2 <- svToSW st b+ cmap <- readIORef (rconstMap st)+ let cw1 = [cw | ((_, cw), sw) <- M.toList cmap, sw == sw1]+ cw2 = [cw | ((_, cw), sw) <- M.toList cmap, sw == sw2]+ case (cw1, cw2) of+ ([x], [y]) | okCW x y -> newConst st $ opCW x y+ _ -> opS st k sw1 sw2++(with obvious modifications to call sites to get the proper arguments.)++But this means that we have to grab the constant list for every symbolicly lifted operation, also do the+same for other places, etc.; for the rare opportunity of catching a @x .== x@ optimization. Even then, the+constants for the branches would still be generated. (i.e., in the above example we would still generate+@s1@ and @s2@, but would skip @s3@.)++It seems to me that the price to pay is rather high, as this is hardly the most common case; so we're opting+here to ignore these cases.++See https://github.com/LeventErkok/sbv/issues/379 for some further discussion.+-} liftSW2 :: (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SVal -> SVal -> Cached SW liftSW2 opS k a b = cache c where c st = do sw1 <- svToSW st a@@ -833,9 +890,11 @@ liftSym2B _ okCW opCR opCI opCF opCD opCC opCS opUI (SVal _ (Left a)) (SVal _ (Left b)) | okCW a b = svBool (liftCW2 opCR opCI opCF opCD opCC opCS opUI a b) liftSym2B opS _ _ _ _ _ _ _ _ a b = SVal KBool $ Right $ liftSW2 opS KBool a b +-- | Create a symbolic two argument operation; with shortcut optimizations mkSymOpSC :: (SW -> SW -> Maybe SW) -> Op -> State -> Kind -> SW -> SW -> IO SW mkSymOpSC shortCut op st k a b = maybe (newExpr st k (SBVApp op [a, b])) return (shortCut a b) +-- | Create a symbolic two argument operation; no shortcut optimizations mkSymOp :: Op -> State -> Kind -> SW -> SW -> IO SW mkSymOp = mkSymOpSC (const (const Nothing)) @@ -892,11 +951,6 @@ isConcreteMin (SVal _ (Left (CW (KBounded True w) (CWInteger n)))) = n == - bit (w - 1) isConcreteMin (SVal _ (Left (CW KBool (CWInteger n)))) = n == 0 isConcreteMin _ = False---- | Predicate for optimizing conditionals.-areConcretelyEqual :: SVal -> SVal -> Bool-areConcretelyEqual (SVal _ (Left a)) (SVal _ (Left b)) = a == b-areConcretelyEqual _ _ = False -- | Most operations on concrete rationals require a compatibility check to avoid faulting -- on algebraic reals.
Data/SBV/Core/Symbolic.hs view
@@ -439,6 +439,7 @@ , queryTerminate :: IO () , queryTimeOutValue :: Maybe Int , queryAssertionStackDepth :: Int+ , queryTblArrPreserveIndex :: Maybe (Int, Int) } -- | A query is a user-guided mechanism to directly communicate and extract results from the solver.@@ -619,6 +620,7 @@ , rNewConsts :: IORef CnstMap , rNewArrs :: IORef ArrayMap , rNewTbls :: IORef TableMap+ , rNewUIs :: IORef UIMap , rNewAsgns :: IORef SBVPgm } @@ -630,12 +632,14 @@ nc <- newIORef Map.empty am <- newIORef IMap.empty tm <- newIORef Map.empty+ ui <- newIORef Map.empty pgm <- newIORef (SBVPgm S.empty) return IncState { rNewInps = is , rNewKinds = ks , rNewConsts = nc , rNewArrs = am , rNewTbls = tm+ , rNewUIs = ui , rNewAsgns = pgm } @@ -764,18 +768,24 @@ newUninterpreted st nm t mbCode | null nm || not enclosed && (not (isAlpha (head nm)) || not (all validChar (tail nm))) = error $ "Bad uninterpreted constant name: " ++ show nm ++ ". Must be a valid identifier."- | True = do- uiMap <- readIORef (rUIMap st)- case nm `Map.lookup` uiMap of- Just t' -> when (t /= t') $ error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"- ++ " Current type : " ++ show t ++ "\n"- ++ " Previously used at: " ++ show t'- Nothing -> do modifyState st rUIMap (Map.insert nm t) $ noInteractive [ "Uninterpreted function introduction:"- , " Named: " ++ nm- , " Type : " ++ show t- ]- when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ())- where validChar x = isAlphaNum x || x `elem` "_"+ | True = do uiMap <- readIORef (rUIMap st)+ case nm `Map.lookup` uiMap of+ Just t' -> checkType t' (return ())+ Nothing -> do modifyState st rUIMap (Map.insert nm t)+ $ modifyIncState st rNewUIs (\newUIs -> case nm `Map.lookup` newUIs of+ Just t' -> checkType t' newUIs+ Nothing -> Map.insert nm t newUIs)++ -- No need to record the code in interactive mode: CodeGen doesn't use interactive+ when (isJust mbCode) $ modifyState st rCgMap (Map.insert nm (fromJust mbCode)) (return ())+ where checkType t' cont+ | t /= t' = error $ "Uninterpreted constant " ++ show nm ++ " used at incompatible types\n"+ ++ " Current type : " ++ show t ++ "\n"+ ++ " Previously used at: " ++ show t'+ | True = cont+++ validChar x = isAlphaNum x || x `elem` "_" enclosed = head nm == '|' && last nm == '|' && length nm > 2 && not (any (`elem` "|\\") (tail (init nm))) -- | Add a new sAssert based constraint
Data/SBV/SMT/SMT.hs view
@@ -784,6 +784,7 @@ , queryTerminate = cleanUp , queryTimeOutValue = Nothing , queryAssertionStackDepth = 0+ , queryTblArrPreserveIndex = Nothing } qsp = queryState ctx
Data/SBV/SMT/SMTLib.hs view
@@ -30,9 +30,9 @@ SMTLib2 -> toSMTLib2 -- | Convert to SMT-Lib, in an incremental query context.-toIncSMTLib :: SMTConfig -> SMTLibIncConverter [String]-toIncSMTLib SMTConfig{smtLibVersion} = case smtLibVersion of- SMTLib2 -> toIncSMTLib2+toIncSMTLib :: Bool -> SMTConfig -> SMTLibIncConverter [String]+toIncSMTLib afterAPush SMTConfig{smtLibVersion} = case smtLibVersion of+ SMTLib2 -> toIncSMTLib2 afterAPush -- | Convert to SMTLib-2 format toSMTLib2 :: SMTLibConverter SMTLibPgm@@ -67,6 +67,6 @@ where quantifiers = map fst (fst qinps) -- | Convert to SMTLib-2 format-toIncSMTLib2 :: SMTLibIncConverter [String]+toIncSMTLib2 :: Bool -> SMTLibIncConverter [String] toIncSMTLib2 = cvt SMTLib2 where cvt SMTLib2 = SMT2.cvtInc
Data/SBV/SMT/SMTLib2.hs view
@@ -13,7 +13,7 @@ module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where import Data.Bits (bit)-import Data.List (intercalate, partition)+import Data.List (intercalate, partition, unzip3) import qualified Data.Foldable as F (toList) import qualified Data.Map as M@@ -110,7 +110,7 @@ ++ [ "; --- optimization tracker variables ---" | not (null trackerVars) ] ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType [] s ++ ") ; tracks " ++ nm | (s, nm) <- trackerVars] ++ [ "; --- constant tables ---" ]- ++ concatMap constTable constTables+ ++ concatMap (constTable False) constTables ++ [ "; --- skolemized tables ---" ] ++ map (skolemTable (unwords (map swType foralls))) skolemTables ++ [ "; --- arrays ---" ]@@ -128,6 +128,10 @@ ] ++ map mkAssign postQuantifierAssigns + ++ concat arrayDelayeds++ ++ concat arraySetups+ ++ delayedAsserts delayedEqualities ++ finalAssert@@ -152,8 +156,8 @@ (constTables, skolemTables) = ([(t, d) | (t, Left d) <- allTables], [(t, d) | (t, Right d) <- allTables]) allTables = [(t, genTableData rm skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls]- (arrayConstants, allArrayDelayeds) = unzip $ map (declArray (not (null foralls)) (map fst consts) skolemMap) arrs- delayedEqualities = concatMap snd skolemTables ++ concat allArrayDelayeds+ (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray False (not (null foralls)) (map fst consts) skolemMap) arrs+ delayedEqualities = concatMap snd skolemTables delayedAsserts [] = [] delayedAsserts ds@(deH : deTs)@@ -249,8 +253,8 @@ body (c:cs) i = "(ite (= x " ++ c ++ ") " ++ show i ++ " " ++ body cs (i+1) ++ ")" -- | Convert in a query context-cvtInc :: SMTLibIncConverter [String]-cvtInc inps ks consts arrs tbls (SBVPgm asgnsSeq) cfg =+cvtInc :: Bool -> SMTLibIncConverter [String]+cvtInc afterAPush inps ks consts arrs tbls uis (SBVPgm asgnsSeq) cfg = -- sorts concatMap declSort [(s, dt) | KUserSort s dt <- Set.toList ks] -- constants@@ -259,12 +263,16 @@ ++ map declInp inps -- arrays ++ concat arrayConstants+ -- uninterpreteds+ ++ concatMap declUI uis -- tables- ++ concatMap constTable allTables+ ++ concatMap (constTable afterAPush) allTables -- expressions ++ map (declDef cfg skolemMap tableMap) (F.toList asgnsSeq) -- delayed equalities- ++ concatMap asrt arrayDelayeds+ ++ concat arrayDelayeds+ -- array setups+ ++ concat arraySetups where -- NB. The below setting of skolemMap to empty is OK, since we do -- not support queries in the context of skolemized variables skolemMap = M.empty@@ -273,14 +281,12 @@ declInp (s, _) = "(declare-fun " ++ show s ++ " () " ++ swType s ++ ")" - (arrayConstants, arrayDelayeds) = unzip $ map (declArray False (map fst consts) skolemMap) arrs+ (arrayConstants, arrayDelayeds, arraySetups) = unzip3 $ map (declArray afterAPush False (map fst consts) skolemMap) arrs allTables = [(t, either id id (genTableData rm skolemMap (False, []) (map fst consts) t)) | t <- tbls] tableMap = IM.fromList $ map mkTable allTables where mkTable (((t, _, _), _), _) = (t, "table" ++ show t) - asrt = map (\s -> "(assert " ++ s ++ ")")- declDef :: SMTConfig -> SkolemMap -> TableMap -> (SW, SBVExpr) -> String declDef cfg skolemMap tableMap (s, expr) = case expr of@@ -304,12 +310,30 @@ declAx :: (String, [String]) -> String declAx (nm, ls) = (";; -- user given axiom: " ++ nm ++ "\n") ++ intercalate "\n" ls -constTable :: (((Int, Kind, Kind), [SW]), [String]) -> [String]-constTable (((i, ak, rk), _elts), is) = decl : map wrap is+constTable :: Bool -> (((Int, Kind, Kind), [SW]), [String]) -> [String]+constTable afterAPush (((i, ak, rk), _elts), is) = decl : zipWith wrap [(0::Int)..] is ++ setup where t = "table" ++ show i decl = "(declare-fun " ++ t ++ " (" ++ smtType ak ++ ") " ++ smtType rk ++ ")"- wrap s = "(assert " ++ s ++ ")" + -- Arrange for initializers+ mkInit idx = "table" ++ show i ++ "_initializer_" ++ show (idx :: Int)+ initializer = "table" ++ show i ++ "_initializer"+ wrap index s+ | afterAPush = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")"+ | True = "(assert " ++ s ++ ")"+ lis = length is+ setup+ | not afterAPush = []+ | lis == 0 = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed"+ ]+ | lis == 1 = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")"+ , "(assert " ++ initializer ++ ")"+ ]+ | True = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lis - 1]) ++ "))"+ , "(assert " ++ initializer ++ ")"+ ]++ skolemTable :: String -> (((Int, Kind, Kind), [SW]), [String]) -> String skolemTable qsIn (((i, ak, rk), _elts), _) = decl where qs = if null qsIn then "" else qsIn ++ " "@@ -335,8 +359,8 @@ -- we might have to skolemize those. Implement this properly. -- The difficulty is with the Mutate/Merge: We have to postpone an init if -- the components are themselves postponed, so this cannot be implemented as a simple map.-declArray :: Bool -> [SW] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String])-declArray quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : map (wrap . snd) pre, map snd post)+declArray :: Bool -> Bool -> [SW] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])+declArray afterAPush quantified consts skolemMap (i, (_, (aKnd, bKnd), ctx)) = (adecl : zipWith wrap [(0::Int)..] (map snd pre), zipWith wrap [lpre..] (map snd post), setup) where topLevel = not quantified || case ctx of ArrayFree -> True ArrayMutate _ a b -> all (`elem` consts) [a, b]@@ -353,7 +377,25 @@ ArrayFree -> [] ArrayMutate j a b -> [(all (`elem` consts) [a, b], "(= " ++ nm ++ " (store array_" ++ show j ++ " " ++ ssw a ++ " " ++ ssw b ++ "))")] ArrayMerge t j k -> [(t `elem` consts, "(= " ++ nm ++ " (ite " ++ ssw t ++ " array_" ++ show j ++ " array_" ++ show k ++ "))")]- wrap s = "(assert " ++ s ++ ")"++ -- Arrange for initializers+ mkInit idx = "array_" ++ show i ++ "_initializer_" ++ show (idx :: Int)+ initializer = "array_" ++ show i ++ "_initializer"+ wrap index s+ | afterAPush = "(define-fun " ++ mkInit index ++ " () Bool " ++ s ++ ")"+ | True = "(assert " ++ s ++ ")"+ lpre = length pre+ lAll = lpre + length post+ setup+ | not afterAPush = []+ | lAll == 0 = [ "(define-fun " ++ initializer ++ " () Bool true) ; no initializiation needed"+ ]+ | lAll == 1 = [ "(define-fun " ++ initializer ++ " () Bool " ++ mkInit 0 ++ ")"+ , "(assert " ++ initializer ++ ")"+ ]+ | True = [ "(define-fun " ++ initializer ++ " () Bool (and " ++ unwords (map mkInit [0..lAll - 1]) ++ "))"+ , "(assert " ++ initializer ++ ")"+ ] swType :: SW -> String swType s = smtType (kindOf s)
Data/SBV/SMT/Utils.hs view
@@ -57,6 +57,7 @@ -> [(SW, CW)] -- ^ constants -> [(Int, ArrayInfo)] -- ^ newly created arrays -> [((Int, Kind, Kind), [SW])] -- ^ newly created tables+ -> [(String, SBVType)] -- ^ newly created uninterpreted functions/constants -> SBVPgm -- ^ assignments -> SMTConfig -- ^ configuration -> a
Data/SBV/Tools/CodeGen.hs view
@@ -16,7 +16,7 @@ SBVCodeGen -- ** Setting code-generation options- , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile+ , cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile, cgOverwriteFiles -- ** Designating inputs , cgInput, cgInputArr
Data/SBV/Tools/GenTest.hs view
@@ -225,7 +225,7 @@ mkLine (is, os) = "{{" ++ intercalate ", " (map v is) ++ "}, {" ++ intercalate ", " (map v os) ++ "}}" v cw = case kindOf cw of KBool -> if cwToBool cw then "true " else "false"- KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w+ KBounded sgn sz -> let CWInteger w = cwVal cw in chex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w KFloat -> let CWFloat w = cwVal cw in showCFloat w KDouble -> let CWDouble w = cwVal cw in showCDouble w
Data/SBV/Utils/PrettyNum.hs view
@@ -14,7 +14,7 @@ {-# LANGUAGE TypeSynonymInstances #-} module Data.SBV.Utils.PrettyNum (- PrettyNum(..), readBin, shex, shexI, sbin, sbinI+ PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI , showCFloat, showCDouble, showHFloat, showHDouble , showSMTFloat, showSMTDouble, smtRoundingMode, cwToSMTLib, mkSkolemZero ) where@@ -129,6 +129,33 @@ pre | shPre = "0x" | True = "" l = (size + 3) `div` 4++-- | Show as hexadecimal, but for C programs. We have to be careful about+-- printing min-bounds, since C does some funky casting, possibly losing+-- the sign bit. In those cases, we use the defined constants in <stdint.h>.+-- We also properly append the necessary suffixes as needed.+chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String+chex shType shPre (signed, size) a+ | Just s <- (signed, size, fromIntegral a) `lookup` specials+ = s+ | True+ = shex shType shPre (signed, size) a ++ suffix+ where specials :: [((Bool, Int, Integer), String)]+ specials = [ ((True, 8, fromIntegral (minBound :: Int8)), "INT8_MIN" )+ , ((True, 16, fromIntegral (minBound :: Int16)), "INT16_MIN")+ , ((True, 32, fromIntegral (minBound :: Int32)), "INT32_MIN")+ , ((True, 64, fromIntegral (minBound :: Int64)), "INT64_MIN")+ ]+ suffix = case (signed, size) of+ (False, 16) -> "U"++ (False, 32) -> "UL"+ (True, 32) -> "L"++ (False, 64) -> "ULL"+ (True, 64) -> "LL"++ _ -> "" -- | Show as a hexadecimal value, integer version. Almost the same as shex above -- except we don't have a bit-length so the length of the string will depend
+ Documentation/SBV/Examples/Puzzles/HexPuzzle.hs view
@@ -0,0 +1,141 @@+-----------------------------------------------------------------------------+-- |+-- Module : Documentation.SBV.Examples.Puzzles.HexPuzzle+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- A solution to the hexagon solver puzzle: <http://www5.cadence.com/2018ClubVQuiz_LP.html>+-- In case the above URL goes dead, here's an ASCII rendering of the problem.+--+-- We're given a board, with 19 hexagon cells. The cells are arranged as follows:+--+-- @+-- 01 02 03+-- 04 05 06 07+-- 08 09 10 11 12+-- 13 14 15 16+-- 17 18 19+-- @+--+-- - Each cell has a color, one of @BLACK@, @BLUE@, @GREEN@, or @RED@.+--+-- - At each step, you get to press one of the center buttons. That is,+-- one of 5, 6, 9, 10, 11, 14, or 15.+--+-- - Pressing a button that is currently colored @BLACK@ has no effect.+--+-- - Otherwise (i.e., if the pressed button is not @BLACK@), then colors+-- rotate clockwise around that button. For instance if you press 15+-- when it is not colored @BLACK@, then 11 moves to 16, 16 moves to 19,+-- 19 moves to 18, 18 moves to 14, 14 moves to 10, and 10 moves to 11.+--+-- - Note that by "move," we mean the colors move: We still refer to the buttons+-- with the same number after a move.+--+-- You are given an initial board coloring, and a final one. Your goal is+-- to find a minimal sequence of button presses that will turn the original board+-- to the final one.+-----------------------------------------------------------------------------++{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Documentation.SBV.Examples.Puzzles.HexPuzzle where++import Data.SBV+import Data.SBV.Control++-- | Colors we're allowed+data Color = Black | Blue | Green | Red++-- | Make 'Color' a symbolic value.+mkSymbolicEnumeration ''Color++-- | Give symbolic colors a name for convenience.+type SColor = SBV Color++-- | Use 8-bit words for button numners, even though we only have 1 to 19.+type Button = Word8++-- | Symbolic version of button.+type SButton = SBV Button++-- | The grid is an array mapping each button to its color.+type Grid = SFunArray Button Color++-- | Given a button press, and the current grid, compute the next grid.+-- If the button is "unpressable", i.e., if it is not one of the center+-- buttons or it is currently colored black, we return the grid unchanged.+next :: SButton -> Grid -> Grid+next b g = ite (readArray g b .== literal Black) g+ $ ite (b .== 5) (rot [ 1, 2, 6, 10, 9, 4])+ $ ite (b .== 6) (rot [ 2, 3, 7, 11, 10, 5])+ $ ite (b .== 9) (rot [ 4, 5, 10, 14, 13, 8])+ $ ite (b .== 10) (rot [ 5, 6, 11, 15, 14, 9])+ $ ite (b .== 11) (rot [ 6, 7, 12, 16, 15, 10])+ $ ite (b .== 14) (rot [ 9, 10, 15, 18, 17, 13])+ $ ite (b .== 15) (rot [10, 11, 16, 19, 18, 14]) g+ where rot xs = foldr (\(i, c) a -> writeArray a (literal i) c) g (zip new cur)+ where cur = map (readArray g . literal) xs+ new = tail xs ++ [head xs]++-- | Iteratively search at increasing depths of button-presses to see if we can+-- transform from the initial board position to a final board position.+search :: [Color] -> [Color] -> IO ()+search initial final = runSMT $ do setLogic Logic_ALL+ query $ loop (0 :: Int) initGrid []++ where initGrid = foldr (\(i, c) a -> writeArray a (literal i) (literal c)) (mkSFunArray (uninterpret "initGrid")) (zip [1..] initial)++ loop i g sofar = do io $ putStrLn $ "Searching at depth: " ++ show i++ -- Go into a new context, and see if we've reached a solution:+ push 1+ constrain $ map (readArray g . literal) [1..19] .== map literal final+ cs <- checkSat++ case cs of+ Unk -> error $ "Solver said Unknown, depth: " ++ show i++ Unsat -> do -- It didn't work out. Pop and try again with one more move:+ pop 1+ b <- freshVar ("press_" ++ show i)+ constrain $ b `sElem` map literal [5, 6, 9, 10, 11, 14, 15]+ loop (i+1) (next b g) (sofar ++ [b])++ Sat -> do vs <- mapM getValue sofar+ io $ putStrLn $ "Found: " ++ show vs+ findOthers sofar vs++ findOthers vs = go+ where go curVals = do constrain $ bOr $ zipWith (\v c -> v ./= literal c) vs curVals+ cs <- checkSat+ case cs of+ Unk -> error $ "Unknown!"+ Unsat -> io $ putStrLn $ "There are no more solutions."+ Sat -> do newVals <- mapM getValue vs+ io $ putStrLn $ "Found: " ++ show newVals+ go newVals++-- | A particular example run. We have:+--+-- >>> example+-- Searching at depth: 0+-- Searching at depth: 1+-- Searching at depth: 2+-- Searching at depth: 3+-- Searching at depth: 4+-- Searching at depth: 5+-- Searching at depth: 6+-- Found: [10,10,9,11,14,6]+-- Found: [10,10,11,9,14,6]+-- There are no more solutions.+example :: IO ()+example = search initBoard finalBoard+ where initBoard = [Black, Black, Black, Red, Blue, Green, Red, Black, Green, Green, Green, Black, Red, Green, Green, Red, Black, Black, Black]+ finalBoard = [Black, Red, Black, Black, Green, Green, Black, Red, Green, Blue, Green, Red, Black, Green, Green, Black, Black, Red, Black]
+ SBVTestSuite/GoldFiles/queryArrays6.gold view
@@ -0,0 +1,79 @@+** Calling: z3 -nw -in -smt2+[GOOD] ; Automatically generated by SBV. Do not edit.+[GOOD] (set-option :print-success true)+[GOOD] (set-option :global-declarations true)+[GOOD] (set-option :smtlib2_compliant true)+[GOOD] (set-option :diagnostic-output-channel "stdout")+[GOOD] (set-option :produce-models true)+[GOOD] (set-logic ALL) ; has non-bitvector arrays, 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] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] (declare-fun array_0 () (Array Int Int))+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (assert s_1)+[GOOD] (push 1)+[GOOD] (define-fun s0 () Int 1)+[GOOD] (define-fun s2 () Int 5)+[GOOD] (declare-fun array_1 () (Array Int Int))+[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s0)))+[GOOD] (define-fun s1 () Int (select array_1 s0))+[GOOD] (define-fun s3 () Bool (= s1 s2))+[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0)+[GOOD] (assert array_1_initializer)+[GOOD] (assert s3)+[SEND] (check-sat)+[RECV] unsat+[GOOD] (pop 1)+[GOOD] (assert array_1_initializer)+[GOOD] (declare-fun s4 () Int)+[GOOD] (define-fun s6 () Int 3)+[GOOD] (define-fun s5 () Bool (>= s4 s0))+[GOOD] (define-fun s7 () Bool (< s4 s6))+[GOOD] (define-fun s8 () Bool (and s5 s7))+[GOOD] (assert s8)+[GOOD] (push 1)+[GOOD] (declare-fun array_2 () (Array Int Int))+[GOOD] (define-fun s9 () Int (+ s1 s4))+[GOOD] (define-fun s10 () Int (select array_2 s0))+[GOOD] (define-fun s11 () Bool (= s2 s10))+[GOOD] (define-fun array_2_initializer_0 () Bool (= array_2 (store array_1 s0 s9)))+[GOOD] (define-fun array_2_initializer () Bool array_2_initializer_0)+[GOOD] (assert array_2_initializer)+[GOOD] (assert s11)+[SEND] (check-sat)+[RECV] unsat+[GOOD] (pop 1)+[GOOD] (assert (and array_1_initializer array_2_initializer))+[GOOD] (declare-fun s12 () Int)+[GOOD] (define-fun s13 () Bool (>= s12 s0))+[GOOD] (define-fun s14 () Bool (< s12 s6))+[GOOD] (define-fun s15 () Bool (and s13 s14))+[GOOD] (assert s15)+[GOOD] (push 1)+[GOOD] (declare-fun array_3 () (Array Int Int))+[GOOD] (define-fun s16 () Int (+ s10 s12))+[GOOD] (define-fun s17 () Int (select array_3 s0))+[GOOD] (define-fun s18 () Bool (= s2 s17))+[GOOD] (define-fun array_3_initializer_0 () Bool (= array_3 (store array_2 s0 s16)))+[GOOD] (define-fun array_3_initializer () Bool array_3_initializer_0)+[GOOD] (assert array_3_initializer)+[GOOD] (assert s18)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s4))+[RECV] ((s4 2))+[SEND] (get-value (s12))+[RECV] ((s12 2))+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL:[2,2]+DONE!
SBVTestSuite/GoldFiles/tgen_c.gold view
@@ -41,16 +41,16 @@ } CTestTestVector; CTestTestVector CTest[] = {- {{0xfcbe0fdb, 0xd321df04}, {0xcfdfeedf, 0x299c30d7, 0x0f03046c}}- , {{0x7e037b43, 0xf66d083b}, {0x7470837e, 0x87967308, 0x042e8071}}- , {{0xce482a70, 0x66b7c768}, {0x34fff1d8, 0x67906308, 0xdc5e4d80}}- , {{0xec1eda04, 0x465a32a9}, {0x32790cad, 0xa5c4a75b, 0xa45ab4a4}}- , {{0x61f89467, 0x00d8fb06}, {0x62d18f6d, 0x611f9961, 0x3c3c776a}}- , {{0x30e2d88c, 0x10ea31cd}, {0x41cd0a59, 0x1ff8a6bf, 0x4112341c}}- , {{0x4bf1b3fd, 0x2124dc8b}, {0x6d169088, 0x2accd772, 0xdf7e265f}}- , {{0x96885656, 0x60a8c5ca}, {0xf7311c20, 0x35df908c, 0x9a744ddc}}- , {{0xc2bac856, 0xe5a9367c}, {0xa863fed2, 0xdd1191da, 0xe7812da8}}- , {{0x8b10b4f2, 0xf010d50f}, {0x7b218a01, 0x9affdfe3, 0x3ba7f42e}}+ {{0xfcbe0fdbUL, 0xd321df04UL}, {0xcfdfeedfUL, 0x299c30d7UL, 0x0f03046cUL}}+ , {{0x7e037b43UL, 0xf66d083bUL}, {0x7470837eUL, 0x87967308UL, 0x042e8071UL}}+ , {{0xce482a70UL, 0x66b7c768UL}, {0x34fff1d8UL, 0x67906308UL, 0xdc5e4d80UL}}+ , {{0xec1eda04UL, 0x465a32a9UL}, {0x32790cadUL, 0xa5c4a75bUL, 0xa45ab4a4UL}}+ , {{0x61f89467UL, 0x00d8fb06UL}, {0x62d18f6dUL, 0x611f9961UL, 0x3c3c776aUL}}+ , {{0x30e2d88cUL, 0x10ea31cdUL}, {0x41cd0a59UL, 0x1ff8a6bfUL, 0x4112341cUL}}+ , {{0x4bf1b3fdUL, 0x2124dc8bUL}, {0x6d169088UL, 0x2accd772UL, 0xdf7e265fUL}}+ , {{0x96885656UL, 0x60a8c5caUL}, {0xf7311c20UL, 0x35df908cUL, 0x9a744ddcUL}}+ , {{0xc2bac856UL, 0xe5a9367cUL}, {0xa863fed2UL, 0xdd1191daUL, 0xe7812da8UL}}+ , {{0x8b10b4f2UL, 0xf010d50fUL}, {0x7b218a01UL, 0x9affdfe3UL, 0x3ba7f42eUL}} }; int CTestLength = 10;
SBVTestSuite/TestSuite/Arrays/Query.hs view
@@ -26,6 +26,7 @@ , goldenCapturedIO "queryArrays3" $ t q3 , goldenCapturedIO "queryArrays4" $ t q4 , goldenCapturedIO "queryArrays5" $ t q5+ , goldenCapturedIO "queryArrays6" $ t q6 ] where t tc goldFile = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just goldFile} tc appendFile goldFile ("\n FINAL:" ++ show r ++ "\nDONE!\n")@@ -99,5 +100,21 @@ Sat -> do av <- getValue a vv <- getValue v return $ Just (av, vv)++q6 :: Symbolic [Integer]+q6 = do (a :: SArray Integer Integer) <- newArray "a"++ query $ loop (writeArray a 1 1) []++ where loop a sofar = do push 1+ constrain $ readArray a 1 .== 5+ cs <- checkSat+ case cs of+ Unk -> error "Unknown"+ Unsat -> do pop 1+ d <- freshVar $ "d" ++ show (length sofar)+ constrain $ d .>= 1 &&& d .< 3+ loop (writeArray a 1 (readArray a 1 + d)) (sofar ++ [d])+ Sat -> mapM getValue sofar {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
SBVTestSuite/TestSuite/BitPrecise/Legato.hs view
@@ -33,11 +33,11 @@ flagC <- free "flagC" flagZ <- free "flagZ" output $ legatoIsCorrect (mkSFunArray (const 0)) (addrX, x) (addrY, y) addrLow (regX, regA, flagC, flagZ)- legatoC = compileToC' "legatoMult" $ do+ legatoC = snd <$> compileToC' "legatoMult" (do cgSetDriverValues [87, 92] cgPerformRTCs True x <- cgInput "x" y <- cgInput "y" let (hi, lo) = runLegato (0, x) (1, y) 2 (initMachine (mkSFunArray (const 0)) (0, 0, false, false)) cgOutput "hi" hi- cgOutput "lo" lo+ cgOutput "lo" lo)
SBVTestSuite/TestSuite/BitPrecise/MergeSort.hs view
@@ -21,7 +21,7 @@ tests = testGroup "BitPrecise.MergeSort" [ goldenVsStringShow "merge" mergeC ]- where mergeC = compileToC' "merge" $ do+ where mergeC = snd <$> compileToC' "merge" (do cgSetDriverValues [10, 6, 4, 82, 71] xs <- cgInputArr 5 "xs"- cgOutputArr "ys" (mergeSort xs)+ cgOutputArr "ys" (mergeSort xs))
SBVTestSuite/TestSuite/CodeGeneration/AddSub.hs view
@@ -21,11 +21,11 @@ tests = testGroup "CodeGen.addSub" [ goldenVsStringShow "addSub" code ]- where code = compileToC' "addSub" $ do+ where code = snd <$> compileToC' "addSub" (do cgSetDriverValues [76, 92] cgPerformRTCs True x <- cgInput "x" y <- cgInput "y" let (s, d) = addSub x y cgOutput "sum" s- cgOutput "dif" d+ cgOutput "dif" d)
SBVTestSuite/TestSuite/CodeGeneration/CRC_USB5.hs view
@@ -22,7 +22,7 @@ goldenVsStringShow "crcUSB5_1" $ genC crcUSB , goldenVsStringShow "crcUSB5_2" $ genC crcUSB' ]- where genC f = compileToC' "crcUSB5" $ do+ where genC f = snd <$> compileToC' "crcUSB5" (do cgSetDriverValues [0xFEDC] msg <- cgInput "msg"- cgReturn $ f msg+ cgReturn $ f msg)
SBVTestSuite/TestSuite/CodeGeneration/CgTests.hs view
@@ -24,18 +24,18 @@ , goldenVsStringShow "selUnchecked" $ genSelect False "selUnChecked" , goldenVsStringShow "codeGen1" foo ]- where genSelect b n = compileToC' n $ do+ where genSelect b n = snd <$> compileToC' n (do cgSetDriverValues [65] cgPerformRTCs b let sel :: SWord8 -> SWord8 sel x = select [1, x+2] 3 x x <- cgInput "x"- cgReturn $ sel x- foo = compileToC' "foo" $ do+ cgReturn $ sel x)+ foo = snd <$> compileToC' "foo" (do cgSetDriverValues $ repeat 0 (x::SInt16) <- cgInput "x" (ys::[SInt64]) <- cgInputArr 45 "xArr" cgOutput "z" (5 :: SWord16) cgOutputArr "zArr" (replicate 7 (x+1)) cgOutputArr "yArr" ys- cgReturn (x*2)+ cgReturn (x*2))
SBVTestSuite/TestSuite/CodeGeneration/Fibonacci.hs view
@@ -22,7 +22,7 @@ goldenVsStringShow "fib1" $ tst [12] "fib1" (fib1 64) , goldenVsStringShow "fib2" $ tst [20] "fib2" (fib2 64) ]- where tst vs nm f = compileToC' nm $ do cgPerformRTCs True- cgSetDriverValues vs- n <- cgInput "n"- cgReturn $ f n+ where tst vs nm f = snd <$> compileToC' nm (do cgPerformRTCs True+ cgSetDriverValues vs+ n <- cgInput "n"+ cgReturn $ f n)
SBVTestSuite/TestSuite/CodeGeneration/Floats.hs view
@@ -20,7 +20,7 @@ tests = testGroup "CodeGeneration.Floats" [ goldenVsStringShow "floats_cgen" code ]- where code = compileToCLib' "floatCodeGen" cases+ where code = snd <$> compileToCLib' "floatCodeGen" cases setup = do cgSRealType CgLongDouble cgIntegerSize 64
SBVTestSuite/TestSuite/CodeGeneration/GCD.hs view
@@ -21,8 +21,8 @@ tests = testGroup "CodeGeneration.GCD" [ goldenVsStringShow "gcd" gcdC ]- where gcdC = compileToC' "sgcd" $ do+ where gcdC = snd <$> compileToC' "sgcd" (do cgSetDriverValues [55,154] x <- cgInput "x" y <- cgInput "y"- cgReturn $ sgcd x y+ cgReturn $ sgcd x y)
SBVTestSuite/TestSuite/CodeGeneration/PopulationCount.hs view
@@ -19,8 +19,8 @@ -- Test suite tests :: TestTree tests = testGroup "CodeGeneration.PopulationCount" [- goldenVsStringShow "popCount1" $ genC False- , goldenVsStringShow "popCount2" $ genC True+ goldenVsStringShow "popCount1" $ snd <$> genC False+ , goldenVsStringShow "popCount2" $ snd <$> genC True ] where genC b = compileToC' "popCount" $ do cgSetDriverValues [0x0123456789ABCDEF]
SBVTestSuite/TestSuite/CodeGeneration/Uninterpreted.hs view
@@ -21,7 +21,6 @@ tests = testGroup "CodeGeneration.Uninterpreted" [ goldenVsStringShow "cgUninterpret" genC ]- where genC = compileToC' "tstShiftLeft" $ do- cgSetDriverValues [1, 2, 3]- [x, y, z] <- cgInputArr 3 "vs"- cgReturn $ tstShiftLeft x y z+ where genC = snd <$> compileToC' "tstShiftLeft" (do cgSetDriverValues [1, 2, 3]+ [x, y, z] <- cgInputArr 3 "vs"+ cgReturn $ tstShiftLeft x y z)
SBVTestSuite/TestSuite/Crypto/AES.hs view
@@ -19,9 +19,9 @@ -- Test suite tests :: TestTree tests = testGroup "Crypto.AES" [- goldenVsStringShow "aes128Enc" $ compileToC' "aes128Enc" (aes128EncDec True)- , goldenVsStringShow "aes128Dec" $ compileToC' "aes128Dec" (aes128EncDec False)- , goldenVsStringShow "aes128Lib" $ compileToCLib' "aes128Lib" aes128Comps+ goldenVsStringShow "aes128Enc" $ snd <$> compileToC' "aes128Enc" (aes128EncDec True)+ , goldenVsStringShow "aes128Dec" $ snd <$> compileToC' "aes128Dec" (aes128EncDec False)+ , goldenVsStringShow "aes128Lib" $ snd <$> compileToCLib' "aes128Lib" aes128Comps ] where aes128EncDec d = do pt <- cgInputArr 4 "pt" key <- cgInputArr 4 "key"
SBVTestSuite/Utils/SBVTestFramework.hs view
@@ -53,9 +53,9 @@ import Data.SBV import Data.SBV.Control -import Data.Char (chr, ord, isDigit)--import Data.Maybe(fromMaybe, catMaybes)+import Data.Char (chr, ord, isDigit)+import Data.List (zip3)+import Data.Maybe (fromMaybe, catMaybes) import System.FilePath ((</>), (<.>)) @@ -127,15 +127,34 @@ cmp x y | cleanUp x == cleanUp y = return Nothing | True = return $ Just $ unlines $ [ "Discrepancy found. Expected: " ++ ref- , "============================================"- ]- ++ lines xs- ++ [ "Got: " ++ new- , "============================================"- ]- ++ lines ys+ , "============================================"+ ]+ ++ lxs+ ++ [ "Got: " ++ new+ , "============================================"+ ]+ ++ lys+ ++ [ "Diff: "+ , "============================================"+ ]+ ++ diff where xs = map (chr . fromIntegral) $ BS.unpack x ys = map (chr . fromIntegral) $ BS.unpack y++ lxs = lines xs+ lys = lines ys++ diffLen = length lxs `max` length lys+ diff = concatMap pick $ zip3 [1..diffLen] (lxs ++ repeat "") (lys ++ repeat "")++ pick (i, expected, got)+ | expected == got+ = []+ | True+ = [ "== Line " ++ show i ++ " =="+ , " Expected: " ++ show expected+ , " Got : " ++ show got+ ] -- deal with insane Windows \r stuff cleanUp = BS.filter (/= slashr)
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 7.7+Version: 7.8 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@@ -16,7 +16,7 @@ Bug-reports: http://github.com/LeventErkok/sbv/issues Maintainer: Levent Erkok (erkokl@gmail.com) Build-Type: Simple-Cabal-Version: >= 1.14+Cabal-Version: 1.14 Data-Files: SBVTestSuite/GoldFiles/*.gold Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md @@ -95,6 +95,7 @@ , Documentation.SBV.Examples.Puzzles.DogCatMouse , Documentation.SBV.Examples.Puzzles.Euler185 , Documentation.SBV.Examples.Puzzles.Fish+ , Documentation.SBV.Examples.Puzzles.HexPuzzle , Documentation.SBV.Examples.Puzzles.MagicSquare , Documentation.SBV.Examples.Puzzles.NQueens , Documentation.SBV.Examples.Puzzles.SendMoreMoney