packages feed

sbv 7.3 → 7.4

raw patch · 38 files changed

+336/−237 lines, 38 files

Files

CHANGES.md view
@@ -1,7 +1,23 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.3, 2017-09-06+* Latest Hackage released version: 7.4, 2017-11-03++### Version 7.4, 2017-11-03++  * Export queryDebug from the Control module, allowing custom queries to print+    debugging messages with the verbose flag is set.++  * Relax value-parsing to allow for non-standard output from solvers. For+    instance, MathSAT/Yices prints reals as integers when they do not have a+    fraction. We now support such cases, relaxing the standard slightly. Thanks+    to Geoffrey Ramseyer for reporting.++  * Fix optimization routines when applied to signed-bitvector goals. Thanks+    to Anders Kaseorg for reporting. Since SMT-Lib does not distinguish between+    signed and unsigned bit-vectors, we have to be careful when expressing goals+    that are over signed values. See https://github.com/LeventErkok/sbv/issues/333+    for details.  ### Version 7.3, 2017-09-06
Data/SBV/Control.hs view
@@ -63,6 +63,7 @@      , ignoreExitCode, timeout       -- * Miscellaneous+     , queryDebug      , echo      , io @@ -80,7 +81,7 @@                               )  import Data.SBV.Control.Query-import Data.SBV.Control.Utils (runProofOn, SMTValue(..))+import Data.SBV.Control.Utils (runProofOn, SMTValue(..), queryDebug)  import Data.IORef (readIORef, writeIORef)
Data/SBV/Control/Query.hs view
@@ -35,7 +35,7 @@  import Data.IORef    (readIORef) -import Data.List     (unzip3, intercalate, nubBy, sortBy, elemIndex)+import Data.List     (unzip3, intercalate, nubBy, sortBy) import Data.Maybe    (listToMaybe, catMaybes) import Data.Function (on) @@ -317,40 +317,24 @@         getObjValue :: (forall a. Maybe [String] -> Query a) -> [NamedSymVar] -> SExpr -> Query (Maybe (String, GeneralizedCW))         getObjValue bailOut inputs expr =                 case expr of-                  EApp [_]          -> return Nothing  -- Happens when a soft-assertion has no associated group.-                  EApp [ECon nm, v] -> case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of-                                         Nothing               -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names-                                         Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, val)-                  _                 -> dontUnderstand (show expr)+                  EApp [_]                                       -> return Nothing            -- Happens when a soft-assertion has no associated group.+                  EApp [ECon nm, v]                              -> locate nm v               -- Regular case+                  EApp [EApp [ECon "bvadd", ECon nm, ENum _], v] -> locate nm v               -- Happens when we "adjust" a signed-bounded objective+                  _                                              -> dontUnderstand (show expr) -          where dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."+          where locate nm v = case listToMaybe [p | p@(sw, _) <- inputs, show sw == nm] of+                                Nothing               -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names+                                Just (sw, actualName) -> grab sw v >>= \val -> return $ Just (actualName, val)++                dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."                                                   , "While trying to process: " ++ s                                                   ]                  grab :: SW -> SExpr -> Query GeneralizedCW-                grab s topExpr = extract topExpr+                grab s topExpr+                  | Just v <- recoverKindedValue k topExpr = return $ RegularCW v+                  | True                                   = ExtendedCW <$> cvt (simplify topExpr)                   where k = kindOf s--                        -- things that can be printed as "integral" values-                        isFromInteger sw = or [f sw | f <- [isBoolean, isBounded, isInteger, isReal, isFloat, isDouble]]--                        getUIIndex (KUserSort  _ (Right xs)) i = i `elemIndex` xs-                        getUIIndex _                         _ = Nothing--                        guard True  v = return v-                        guard False _ = dontUnderstand (show topExpr)--                        extract (ENum    i) = guard (isFromInteger s) $ RegularCW  $ mkConstCW  k (fst i)-                        extract (EReal   i) = guard (isReal        s) $ RegularCW  $ CW KReal   (CWAlgReal i)-                        extract (EFloat  i) = guard (isFloat       s) $ RegularCW  $ CW KFloat  (CWFloat   i)-                        extract (EDouble i) = guard (isDouble      s) $ RegularCW  $ CW KDouble (CWDouble  i)--                        -- If we have an ECon, it could be uninterpted, or oo/epsilon-                        extract (ECon i)-                           | isUninterpreted s = return $ RegularCW  $ CW k (CWUserSort (getUIIndex k i, i))--                        -- Exhausted regular values, look for infinities and such:-                        extract val         = ExtendedCW <$> cvt (simplify val)                          -- Convert to an extended expression. Hopefully complete!                         cvt :: SExpr -> Query ExtCW
Data/SBV/Control/Utils.hs view
@@ -28,6 +28,7 @@      , timeout      , queryDebug      , retrieveResponse+     , recoverKindedValue      , runProofOn      ) where @@ -181,7 +182,9 @@ freshVar nm = inNewContext $ fmap SBV . svMkSymVar (Just EX) k (Just nm)   where k = kindOf (undefined :: a) --- | Internal diagnostic messages.+-- | If 'verbose' is 'True', print the message, useful for debugging messages+-- in custom queries. Note that 'redirectVerbose' will be respected: If a+-- file redirection is given, the output will go to the file. queryDebug :: [String] -> Query () queryDebug msgs = do QueryState{queryConfig} <- getQueryState                      io $ debug queryConfig msgs@@ -282,12 +285,14 @@ instance SMTValue Integer where sexprToVal = fromIntegralToVal  instance SMTValue Float where-   sexprToVal (EFloat f) = Just f-   sexprToVal _          = Nothing+   sexprToVal (EFloat f)    = Just f+   sexprToVal (ENum (v, _)) = Just (fromIntegral v)+   sexprToVal _             = Nothing  instance SMTValue Double where-   sexprToVal (EDouble f) = Just f-   sexprToVal _           = Nothing+   sexprToVal (EDouble f)   = Just f+   sexprToVal (ENum (v, _)) = Just (fromIntegral v)+   sexprToVal _             = Nothing  instance SMTValue Bool where    sexprToVal (ENum (1, _)) = Just True@@ -295,8 +300,9 @@    sexprToVal _             = Nothing  instance SMTValue AlgReal where-   sexprToVal (EReal a) = Just a-   sexprToVal _         = Nothing+   sexprToVal (EReal a)     = Just a+   sexprToVal (ENum (v, _)) = Just (fromIntegral v)+   sexprToVal _             = Nothing  -- | Get the value of a term. getValue :: SMTValue a => SBV a -> Query a@@ -348,22 +354,27 @@             bad = unexpected "getModel" cmd ("a value binding for kind: " ++ show k) Nothing -           getUIIndex (KUserSort  _ (Right xs)) i = i `elemIndex` xs-           getUIIndex _                         _ = Nothing-        r <- ask cmd -       let isIntegral sw = isBoolean sw || isBounded sw || isInteger sw+       parse r bad $ \case EApp [EApp [ECon v, val]] | v == nm -> case recoverKindedValue (kindOf s) val of+                                                                    Just cw -> return cw+                                                                    Nothing -> bad r Nothing+                           _                                   -> bad r Nothing -           extract (ENum    i) | isIntegral      s = return $ mkConstCW  k (fst i)-           extract (EReal   i) | isReal          s = return $ CW KReal   (CWAlgReal i)-           extract (EFloat  i) | isFloat         s = return $ CW KFloat  (CWFloat   i)-           extract (EDouble i) | isDouble        s = return $ CW KDouble (CWDouble  i)-           extract (ECon    i) | isUninterpreted s = return $ CW k       (CWUserSort (getUIIndex k i, i))-           extract _                               = bad r Nothing+-- | Recover a given solver-printed value with a possible interpretation+recoverKindedValue :: Kind -> SExpr -> Maybe CW+recoverKindedValue k e = case e of+                           ENum    i | isIntegralLike    -> Just $ mkConstCW k (fst i)+                           EReal   i | isReal          k -> Just $ CW KReal    (CWAlgReal i)+                           EFloat  i | isFloat         k -> Just $ CW KFloat   (CWFloat   i)+                           EDouble i | isDouble        k -> Just $ CW KDouble  (CWDouble  i)+                           ECon    i | isUninterpreted k -> Just $ CW k        (CWUserSort (getUIIndex k i, i))+                           _                             -> Nothing+  where isIntegralLike = or [f k | f <- [isBoolean, isBounded, isInteger, isReal, isFloat, isDouble]] -       parse r bad $ \case EApp [EApp [ECon v, val]] | v == nm -> extract val-                           _                                   -> bad r Nothing+        getUIIndex (KUserSort  _ (Right xs)) i = i `elemIndex` xs+        getUIIndex _                         _ = Nothing+  -- | Get the value of a term. If the kind is Real and solver supports decimal approximations, -- we will "squash" the representations.
Data/SBV/Examples/BitPrecise/MultMask.hs view
@@ -36,7 +36,7 @@ -- >>> maskAndMult -- Satisfiable. Model: --   mask = 0x8080808080808080 :: Word64---   mult = 0x0002040810204081 :: Word64+--   mult = 0xc202040810204081 :: Word64 -- -- That is, any 64 bit value masked by the first and multipled by the second -- value above will have its bits at positions @[7,15,23,31,39,47,55,63]@ moved
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -258,16 +258,16 @@ -- Checking for solutions with 5 moves. -- Solution #1: --  0 --> Edge, Bono---  2 <-- Edge---  4 --> Larry, Adam--- 14 <-- Bono+--  2 <-- Bono+--  3 --> Larry, Adam+-- 13 <-- Edge -- 15 --> Edge, Bono -- Total time: 17 -- Solution #2: --  0 --> Edge, Bono---  2 <-- Bono---  3 --> Larry, Adam--- 13 <-- Edge+--  2 <-- Edge+--  4 --> Larry, Adam+-- 14 <-- Bono -- 15 --> Edge, Bono -- Total time: 17 -- Found: 2 solutions with 5 moves.
Data/SBV/Examples/Uninterpreted/UISortAllSat.hs view
@@ -56,12 +56,12 @@ --   l1 = L!val!1 :: L --   l2 = L!val!2 :: L -- Solution #2:---   l  = L!val!2 :: L+--   l  = L!val!1 :: L --   l0 = L!val!0 :: L --   l1 = L!val!1 :: L --   l2 = L!val!2 :: L -- Solution #3:---   l  = L!val!1 :: L+--   l  = L!val!2 :: L --   l0 = L!val!0 :: L --   l1 = L!val!1 :: L --   l2 = L!val!2 :: L
Data/SBV/Provers/Prover.hs view
@@ -48,6 +48,7 @@ import Data.SBV.Core.Symbolic import Data.SBV.SMT.SMT import Data.SBV.Utils.TDiff+import Data.SBV.Utils.PrettyNum  import qualified Data.SBV.Control       as Control import qualified Data.SBV.Control.Query as Control@@ -262,9 +263,9 @@                     let optimizerDirectives = concatMap minmax objectives ++ priority style                          where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"-                               minmax (Minimize   _  xy@(_, v))     = [mkEq xy, "(minimize "    ++ show v ++ ")"]-                               minmax (Maximize   _  xy@(_, v))     = [mkEq xy, "(maximize "    ++ show v ++ ")"]-                               minmax (AssertSoft nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ show v ++ penalize mbp ++ ")"]+                               minmax (Minimize   _  xy@(_, v))     = [mkEq xy, "(minimize "    ++ signAdjust v (show v) ++ ")"]+                               minmax (Maximize   _  xy@(_, v))     = [mkEq xy, "(maximize "    ++ signAdjust v (show v) ++ ")"]+                               minmax (AssertSoft nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ signAdjust v (show v) ++ penalize mbp ++ ")"]                                  where penalize DefaultPenalty    = ""                                        penalize (Penalty w mbGrp)                                           | w <= 0         = error $ unlines [ "SBV.AssertSoft: Goal " ++ show nm ++ " is assigned a non-positive penalty: " ++ shw@@ -278,6 +279,21 @@                                priority Lexicographic = [] -- default, no option needed                                priority Independent   = ["(set-option :opt.priority box)"]                                priority (Pareto _)    = ["(set-option :opt.priority pareto)"]++                               -- if the goal is a signed-BV, then we need to add 2^{n-1} to the maximal value+                               -- is properly placed in the correct range. See http://github.com/Z3Prover/z3/issues/1339 for+                               -- details on why we have to do this:+                               signAdjust :: SW -> String -> String+                               signAdjust v o = case kindOf v of+                                                  -- NB. The order we spit out the addition here (i.e., "bvadd v constant")+                                                  -- is important as we parse it back in precisely that form when we+                                                  -- get the objective. Don't change it!+                                                  KBounded True sz -> "(bvadd " ++ o ++ " " ++ adjust sz ++ ")"+                                                  _                -> o+                                  where adjust :: Int -> String+                                        adjust sz = cwToSMTLib RoundNearestTiesToEven -- rounding mode doesn't matter here, just pick one+                                                              (mkConstCW (KBounded False sz)+                                                                         ((2::Integer)^(fromIntegral sz - (1::Integer))))                     mapM_ (Control.send True) optimizerDirectives
Data/SBV/Provers/Z3.hs view
@@ -18,7 +18,7 @@  -- | The description of the Z3 SMT solver. -- The default executable is @\"z3\"@, which must be in your path. You can use the @SBV_Z3@ environment variable to point to the executable on your system.--- The default options are @\"-nw -in -smt2\"@, which is valid for Z3 4.1. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options.+-- The default options are @\"-nw -in -smt2\"@. You can use the @SBV_Z3_OPTIONS@ environment variable to override the options. z3 :: SMTSolver z3 = SMTSolver {            name         = Z3
Data/SBV/Utils/SExpr.hs view
@@ -109,12 +109,13 @@         parseApp (tok:toks) sofar = do t <- pTok tok                                        parseApp toks (t : sofar) -        pTok "false"              = return $ ENum (0, Nothing)-        pTok "true"               = return $ ENum (1, Nothing)-        pTok ('0':'b':r)          = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r-        pTok ('b':'v':r)          = mkNum Nothing               $ readDec (takeWhile (/= '[') r)-        pTok ('#':'b':r)          = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r-        pTok ('#':'x':r)          = mkNum (Just (4 * length r)) $ readHex r+        pTok "false" = return $ ENum (0, Nothing)+        pTok "true"  = return $ ENum (1, Nothing)++        pTok ('0':'b':r)                                 = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+        pTok ('b':'v':r) | not (null r) && all isDigit r = mkNum Nothing               $ readDec (takeWhile (/= '[') r)+        pTok ('#':'b':r)                                 = mkNum (Just (length r))     $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r+        pTok ('#':'x':r)                                 = mkNum (Just (4 * length r)) $ readHex r         pTok n           | not (null n) && isDigit (head n)           = if '.' `elem` n then getReal n
SBVTestSuite/GoldFiles/U2Bridge.gold view
@@ -3,13 +3,13 @@   s1  =  Edge :: U2Member   s2  =  Bono :: U2Member   s3  =  True :: Bool-  s4  =  Edge :: U2Member+  s4  =  Bono :: U2Member   s5  =  Bono :: U2Member   s6  = False :: Bool   s7  = Larry :: U2Member   s8  =  Adam :: U2Member   s9  =  True :: Bool-  s10 =  Bono :: U2Member+  s10 =  Edge :: U2Member   s11 =  Bono :: U2Member   s12 = False :: Bool   s13 =  Edge :: U2Member
+ SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 127 :: Int8+  m = 127 :: Int8
+ SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = -128 :: Int8+  m = -128 :: Int8
+ SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 255 :: Word8+  m = 255 :: Word8
+ SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 0 :: Word8+  m = 0 :: Word8
+ SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 32767 :: Int16+  m = 32767 :: Int16
+ SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = -32768 :: Int16+  m = -32768 :: Int16
+ SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 65535 :: Word16+  m = 65535 :: Word16
+ SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 0 :: Word16+  m = 0 :: Word16
+ SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 2147483647 :: Int32+  m = 2147483647 :: Int32
+ SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = -2147483648 :: Int32+  m = -2147483648 :: Int32
+ SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 4294967295 :: Word32+  m = 4294967295 :: Word32
+ SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 0 :: Word32+  m = 0 :: Word32
+ SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 9223372036854775807 :: Int64+  m = 9223372036854775807 :: Int64
+ SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = -9223372036854775808 :: Int64+  m = -9223372036854775808 :: Int64
+ SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_max.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 18446744073709551615 :: Word64+  m = 18446744073709551615 :: Word64
+ SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_min.gold view
@@ -0,0 +1,3 @@+Optimal model:+  x = 0 :: Word64+  m = 0 :: Word64
SBVTestSuite/GoldFiles/pareto1.gold view
@@ -1,180 +1,180 @@ Pareto front #1: Optimal model:-  x            = 1 :: Integer+  x            = 0 :: Integer   y            = 0 :: Integer-  min_x        = 1 :: Integer-  max_x_plus_y = 1 :: Integer+  min_x        = 0 :: Integer+  max_x_plus_y = 0 :: Integer   min_y        = 0 :: Integer Pareto front #2: Optimal model:   x            = 0 :: Integer-  y            = 2 :: Integer+  y            = 1 :: Integer   min_x        = 0 :: Integer-  max_x_plus_y = 2 :: Integer-  min_y        = 2 :: Integer+  max_x_plus_y = 1 :: Integer+  min_y        = 1 :: Integer Pareto front #3: Optimal model:-  x            = 0 :: Integer+  x            = 4 :: Integer   y            = 0 :: Integer-  min_x        = 0 :: Integer-  max_x_plus_y = 0 :: Integer+  min_x        = 4 :: Integer+  max_x_plus_y = 4 :: Integer   min_y        = 0 :: Integer Pareto front #4: Optimal model:-  x            = 1 :: Integer-  y            = 2 :: Integer-  min_x        = 1 :: Integer-  max_x_plus_y = 3 :: Integer-  min_y        = 2 :: Integer+  x            = 4 :: Integer+  y            = 4 :: Integer+  min_x        = 4 :: Integer+  max_x_plus_y = 8 :: Integer+  min_y        = 4 :: Integer Pareto front #5: Optimal model:   x            = 0 :: Integer-  y            = 1 :: Integer+  y            = 2 :: Integer   min_x        = 0 :: Integer-  max_x_plus_y = 1 :: Integer-  min_y        = 1 :: Integer-Pareto front #6: Optimal model:-  x            = 1 :: Integer-  y            = 1 :: Integer-  min_x        = 1 :: Integer   max_x_plus_y = 2 :: Integer-  min_y        = 1 :: Integer-Pareto front #7: Optimal model:+  min_y        = 2 :: Integer+Pareto front #6: Optimal model:   x            = 2 :: Integer-  y            = 0 :: Integer+  y            = 2 :: Integer   min_x        = 2 :: Integer-  max_x_plus_y = 2 :: Integer+  max_x_plus_y = 4 :: Integer+  min_y        = 2 :: Integer+Pareto front #7: Optimal model:+  x            = 1 :: Integer+  y            = 0 :: Integer+  min_x        = 1 :: Integer+  max_x_plus_y = 1 :: Integer   min_y        = 0 :: Integer Pareto front #8: Optimal model:-  x            = 0 :: Integer-  y            = 4 :: Integer-  min_x        = 0 :: Integer-  max_x_plus_y = 4 :: Integer-  min_y        = 4 :: Integer-Pareto front #9: Optimal model:-  x            = 3 :: Integer+  x            = 5 :: Integer   y            = 0 :: Integer-  min_x        = 3 :: Integer-  max_x_plus_y = 3 :: Integer+  min_x        = 5 :: Integer+  max_x_plus_y = 5 :: Integer   min_y        = 0 :: Integer+Pareto front #9: Optimal model:+  x            = 5 :: Integer+  y            = 2 :: Integer+  min_x        = 5 :: Integer+  max_x_plus_y = 7 :: Integer+  min_y        = 2 :: Integer Pareto front #10: Optimal model:-  x            = 2 :: Integer-  y            = 1 :: Integer-  min_x        = 2 :: Integer+  x            = 1 :: Integer+  y            = 2 :: Integer+  min_x        = 1 :: Integer   max_x_plus_y = 3 :: Integer-  min_y        = 1 :: Integer+  min_y        = 2 :: Integer Pareto front #11: Optimal model:-  x            = 3 :: Integer-  y            = 1 :: Integer-  min_x        = 3 :: Integer-  max_x_plus_y = 4 :: Integer-  min_y        = 1 :: Integer-Pareto front #12: Optimal model:   x            = 4 :: Integer-  y            = 0 :: Integer+  y            = 2 :: Integer   min_x        = 4 :: Integer-  max_x_plus_y = 4 :: Integer+  max_x_plus_y = 6 :: Integer+  min_y        = 2 :: Integer+Pareto front #12: Optimal model:+  x            = 2 :: Integer+  y            = 0 :: Integer+  min_x        = 2 :: Integer+  max_x_plus_y = 2 :: Integer   min_y        = 0 :: Integer Pareto front #13: Optimal model:-  x            = 5 :: Integer+  x            = 3 :: Integer   y            = 0 :: Integer-  min_x        = 5 :: Integer-  max_x_plus_y = 5 :: Integer+  min_x        = 3 :: Integer+  max_x_plus_y = 3 :: Integer   min_y        = 0 :: Integer Pareto front #14: Optimal model:-  x            = 4 :: Integer-  y            = 1 :: Integer-  min_x        = 4 :: Integer+  x            = 3 :: Integer+  y            = 2 :: Integer+  min_x        = 3 :: Integer   max_x_plus_y = 5 :: Integer-  min_y        = 1 :: Integer+  min_y        = 2 :: Integer Pareto front #15: Optimal model:-  x            = 5 :: Integer+  x            = 1 :: Integer   y            = 1 :: Integer-  min_x        = 5 :: Integer-  max_x_plus_y = 6 :: Integer+  min_x        = 1 :: Integer+  max_x_plus_y = 2 :: Integer   min_y        = 1 :: Integer Pareto front #16: Optimal model:+  x            = 0 :: Integer+  y            = 3 :: Integer+  min_x        = 0 :: Integer+  max_x_plus_y = 3 :: Integer+  min_y        = 3 :: Integer+Pareto front #17: Optimal model:   x            = 1 :: Integer-  y            = 4 :: Integer+  y            = 3 :: Integer   min_x        = 1 :: Integer-  max_x_plus_y = 5 :: Integer-  min_y        = 4 :: Integer-Pareto front #17: Optimal model:-  x            = 2 :: Integer-  y            = 4 :: Integer-  min_x        = 2 :: Integer-  max_x_plus_y = 6 :: Integer-  min_y        = 4 :: Integer+  max_x_plus_y = 4 :: Integer+  min_y        = 3 :: Integer Pareto front #18: Optimal model:-  x            = 3 :: Integer+  x            = 0 :: Integer   y            = 4 :: Integer-  min_x        = 3 :: Integer-  max_x_plus_y = 7 :: Integer+  min_x        = 0 :: Integer+  max_x_plus_y = 4 :: Integer   min_y        = 4 :: Integer Pareto front #19: Optimal model:-  x            = 4 :: Integer+  x            = 1 :: Integer   y            = 4 :: Integer-  min_x        = 4 :: Integer-  max_x_plus_y = 8 :: Integer+  min_x        = 1 :: Integer+  max_x_plus_y = 5 :: Integer   min_y        = 4 :: Integer Pareto front #20: Optimal model:+  x            = 4 :: Integer+  y            = 1 :: Integer+  min_x        = 4 :: Integer+  max_x_plus_y = 5 :: Integer+  min_y        = 1 :: Integer+Pareto front #21: Optimal model:   x            = 5 :: Integer-  y            = 4 :: Integer+  y            = 1 :: Integer   min_x        = 5 :: Integer-  max_x_plus_y = 9 :: Integer-  min_y        = 4 :: Integer-Pareto front #21: Optimal model:-  x            = 0 :: Integer-  y            = 3 :: Integer-  min_x        = 0 :: Integer-  max_x_plus_y = 3 :: Integer-  min_y        = 3 :: Integer+  max_x_plus_y = 6 :: Integer+  min_y        = 1 :: Integer Pareto front #22: Optimal model:-  x            = 1 :: Integer+  x            = 4 :: Integer   y            = 3 :: Integer-  min_x        = 1 :: Integer-  max_x_plus_y = 4 :: Integer+  min_x        = 4 :: Integer+  max_x_plus_y = 7 :: Integer   min_y        = 3 :: Integer Pareto front #23: Optimal model:+  x            = 5 :: Integer+  y            = 3 :: Integer+  min_x        = 5 :: Integer+  max_x_plus_y = 8 :: Integer+  min_y        = 3 :: Integer+Pareto front #24: Optimal model:+  x            = 5 :: Integer+  y            = 4 :: Integer+  min_x        = 5 :: Integer+  max_x_plus_y = 9 :: Integer+  min_y        = 4 :: Integer+Pareto front #25: Optimal model:   x            = 2 :: Integer-  y            = 2 :: Integer+  y            = 1 :: Integer   min_x        = 2 :: Integer-  max_x_plus_y = 4 :: Integer-  min_y        = 2 :: Integer-Pareto front #24: Optimal model:+  max_x_plus_y = 3 :: Integer+  min_y        = 1 :: Integer+Pareto front #26: Optimal model:   x            = 3 :: Integer-  y            = 2 :: Integer+  y            = 1 :: Integer   min_x        = 3 :: Integer-  max_x_plus_y = 5 :: Integer-  min_y        = 2 :: Integer-Pareto front #25: Optimal model:+  max_x_plus_y = 4 :: Integer+  min_y        = 1 :: Integer+Pareto front #27: Optimal model:   x            = 2 :: Integer   y            = 3 :: Integer   min_x        = 2 :: Integer   max_x_plus_y = 5 :: Integer   min_y        = 3 :: Integer-Pareto front #26: Optimal model:+Pareto front #28: Optimal model:   x            = 3 :: Integer   y            = 3 :: Integer   min_x        = 3 :: Integer   max_x_plus_y = 6 :: Integer   min_y        = 3 :: Integer-Pareto front #27: Optimal model:-  x            = 4 :: Integer-  y            = 2 :: Integer-  min_x        = 4 :: Integer-  max_x_plus_y = 6 :: Integer-  min_y        = 2 :: Integer-Pareto front #28: Optimal model:-  x            = 5 :: Integer-  y            = 2 :: Integer-  min_x        = 5 :: Integer-  max_x_plus_y = 7 :: Integer-  min_y        = 2 :: Integer Pareto front #29: Optimal model:-  x            = 4 :: Integer-  y            = 3 :: Integer-  min_x        = 4 :: Integer-  max_x_plus_y = 7 :: Integer-  min_y        = 3 :: Integer+  x            = 2 :: Integer+  y            = 4 :: Integer+  min_x        = 2 :: Integer+  max_x_plus_y = 6 :: Integer+  min_y        = 4 :: Integer Pareto front #30: Optimal model:-  x            = 5 :: Integer-  y            = 3 :: Integer-  min_x        = 5 :: Integer-  max_x_plus_y = 8 :: Integer-  min_y        = 3 :: Integer+  x            = 3 :: Integer+  y            = 4 :: Integer+  min_x        = 3 :: Integer+  max_x_plus_y = 7 :: Integer+  min_y        = 4 :: Integer
SBVTestSuite/GoldFiles/pareto2.gold view
@@ -143,40 +143,40 @@   max_y        = 27 :: Integer   max_x_plus_y = 27 :: Integer Pareto front #25: Optimal model:-  x            =  0 :: Integer-  y            = 28 :: Integer-  min_x        =  0 :: Integer-  max_y        = 28 :: Integer-  max_x_plus_y = 28 :: Integer+  x            = 0 :: Integer+  y            = 3 :: Integer+  min_x        = 0 :: Integer+  max_y        = 3 :: Integer+  max_x_plus_y = 3 :: Integer Pareto front #26: Optimal model:-  x            =  0 :: Integer-  y            = 29 :: Integer-  min_x        =  0 :: Integer-  max_y        = 29 :: Integer-  max_x_plus_y = 29 :: Integer+  x            = 0 :: Integer+  y            = 2 :: Integer+  min_x        = 0 :: Integer+  max_y        = 2 :: Integer+  max_x_plus_y = 2 :: Integer Pareto front #27: Optimal model:-  x            =  0 :: Integer-  y            = 30 :: Integer-  min_x        =  0 :: Integer-  max_y        = 30 :: Integer-  max_x_plus_y = 30 :: Integer+  x            = 0 :: Integer+  y            = 1 :: Integer+  min_x        = 0 :: Integer+  max_y        = 1 :: Integer+  max_x_plus_y = 1 :: Integer Pareto front #28: Optimal model:-  x            =  0 :: Integer-  y            = 31 :: Integer-  min_x        =  0 :: Integer-  max_y        = 31 :: Integer-  max_x_plus_y = 31 :: Integer+  x            = 0 :: Integer+  y            = 0 :: Integer+  min_x        = 0 :: Integer+  max_y        = 0 :: Integer+  max_x_plus_y = 0 :: Integer Pareto front #29: Optimal model:   x            =  0 :: Integer-  y            = 32 :: Integer+  y            = -1 :: Integer   min_x        =  0 :: Integer-  max_y        = 32 :: Integer-  max_x_plus_y = 32 :: Integer+  max_y        = -1 :: Integer+  max_x_plus_y = -1 :: Integer Pareto front #30: Optimal model:   x            =  0 :: Integer-  y            = 33 :: Integer+  y            = -2 :: Integer   min_x        =  0 :: Integer-  max_y        = 33 :: Integer-  max_x_plus_y = 33 :: Integer+  max_y        = -2 :: Integer+  max_x_plus_y = -2 :: Integer *** Note: Pareto-front extraction was terminated before stream was ended as requested by the user. ***       There might be other (potentially infinitely more) results.
SBVTestSuite/GoldFiles/query1.gold view
@@ -152,19 +152,20 @@        (declare-fun bey () Bool)        (declare-fun hey () Bool)        (proof-       (let (($x232 (<= s0 6)))-       (let (($x233 (not $x232)))-       (let (($x236 (or (not bey) $x233)))-       (let ((@x238 (monotonicity (rewrite (= (> s0 6) $x233)) (= (or (not bey) (> s0 6)) $x236))))-       (let ((@x231 (rewrite (= (=> bey (> s0 6)) (or (not bey) (> s0 6))))))-       (let ((@x241 (mp (asserted (=> bey (> s0 6))) (trans @x231 @x238 (= (=> bey (> s0 6)) $x236)) $x236)))-       (let (($x252 (>= s0 6)))-       (let (($x250 (not $x252)))-       (let (($x254 (or (not hey) $x250)))-       (let ((@x256 (monotonicity (rewrite (= (< s0 6) $x250)) (= (or (not hey) (< s0 6)) $x254))))-       (let ((@x249 (rewrite (= (=> hey (< s0 6)) (or (not hey) (< s0 6))))))-       (let ((@x259 (mp (asserted (=> hey (< s0 6))) (trans @x249 @x256 (= (=> hey (< s0 6)) $x254)) $x254)))-       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x252 $x232)) (unit-resolution @x259 (asserted hey) $x250) (unit-resolution @x241 (asserted bey) $x233) false)))))))))))))))+       (let (($x215 (<= s0 6)))+       (let (($x216 (not $x215)))+       (let (($x223 (or (not bey) $x216)))+       (let ((@x221 (monotonicity (rewrite (= (> s0 6) $x216)) (= (=> bey (> s0 6)) (=> bey $x216)))))+       (let ((@x227 (trans @x221 (rewrite (= (=> bey $x216) $x223)) (= (=> bey (> s0 6)) $x223))))+       (let ((@x228 (mp (asserted (=> bey (> s0 6))) @x227 $x223)))+       (let (($x240 (>= s0 6)))+       (let (($x239 (not $x240)))+       (let (($x249 (or (not hey) $x239)))+       (let ((@x242 (monotonicity (rewrite (= (<= 6 s0) $x240)) (= (not (<= 6 s0)) $x239))))+       (let ((@x244 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) @x242 (= (< s0 6) $x239))))+       (let ((@x253 (trans (monotonicity @x244 (= (=> hey (< s0 6)) (=> hey $x239))) (rewrite (= (=> hey $x239) $x249)) (= (=> hey (< s0 6)) $x249))))+       (let ((@x254 (mp (asserted (=> hey (< s0 6))) @x253 $x249)))+       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x240 $x215)) (unit-resolution @x254 (asserted hey) $x239) (unit-resolution @x228 (asserted bey) $x216) false)))))))))))))))) [SEND, TimeOut: 90000ms] (get-assertions)  [RECV] ((! s7 :named |a > 0|)
SBVTestSuite/GoldFiles/query_Interpolant2.gold view
@@ -40,9 +40,9 @@ [RECV] unsat [SEND] (get-interpolant |c1| |c2|) [RECV] (interpolants-        (or (= s2 s3) (not (= s0 s1))))+        (or (= s2 s3) (not (= s1 s0)))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-["(or (= s2 s3) (not (= s0 s1)))"]+["(or (= s2 s3) (not (= s1 s0)))"]
SBVTestSuite/GoldFiles/query_Interpolant3.gold view
@@ -40,9 +40,10 @@ [RECV] unsat [SEND] (get-interpolant |c1| |c2|) [RECV] (interpolants-        (= array_1 (store array_2 s1 0)))+        (and (= (select array_1 s0) (select (store array_2 s1 0) s0))+            (or (= 0 (select array_1 s0)) (not (= s0 s1))))) *** Solver   : Z3 *** Exit code: ExitSuccess  FINAL OUTPUT:-["(= array_1 (store array_2 s1 0))"]+["(and (= (select array_1 s0) (select (store array_2 s1 0) s0)) (or (= 0 (select array_1 s0)) (not (= s0 s1))))"]
SBVTestSuite/GoldFiles/query_badOption.gold view
@@ -16,6 +16,7 @@ ***                Legal parameters are: ***                  auto_config (bool) (default: true) ***                  debug_ref_count (bool) (default: false)+***                  dot_proof_file (string) (default: proof.dot) ***                  dump_models (bool) (default: false) ***                  memory_high_watermark (unsigned int) (default: 0) ***                  memory_max_alloc_count (unsigned int) (default: 0)
SBVTestSuite/GoldFiles/temperature.gold view
@@ -1,5 +1,5 @@ Solution #1:-  s0 = 28 :: Integer-Solution #2:   s0 = 16 :: Integer+Solution #2:+  s0 = 28 :: Integer Found 2 different solutions.
SBVTestSuite/SBVTest.hs view
@@ -89,7 +89,7 @@ -- TODO: Would be nice to run them all on Windows/OSX on remote hosts as well. ciFilter :: CIOS -> Int -> TestTree -> IO TestTree ciFilter _  100 tt = return tt-ciFilter os   n tt = do putStrLn $ "OS: " ++ show os ++ ", Running only " ++ show n ++ "% of tests."+ciFilter os   n tt = do putStrLn $ "OS: " ++ show os ++ ", Running only " ++ show n ++ "% of arithmetic tests."                         pickTests n tt  main :: IO ()
SBVTestSuite/TestSuite/Optimization/Basics.hs view
@@ -16,10 +16,29 @@ -- Test suite tests :: TestTree tests =-  testGroup "Optimization.Basics"-    [ goldenVsStringShow "optBasics1" (optimize Lexicographic optBasics1)-    , goldenVsStringShow "optBasics2" (optimize Lexicographic optBasics2)-    ]+  testGroup "Optimization.Basics" $+       [ goldenVsStringShow "optBasics1" (optimize Lexicographic optBasics1)+       , goldenVsStringShow "optBasics2" (optimize Lexicographic optBasics2)+       ]+    ++ [ goldenVsStringShow ("optBasicsRange_" ++ n) (optimize Lexicographic f)+       | (n, f) <- [ ("08_unsigned_max", sWord8  "x" >>= maximize "m")+                   , ("08_unsigned_min", sWord8  "x" >>= minimize "m")+                   , ("16_unsigned_max", sWord16 "x" >>= maximize "m")+                   , ("16_unsigned_min", sWord16 "x" >>= minimize "m")+                   , ("32_unsigned_max", sWord32 "x" >>= maximize "m")+                   , ("32_unsigned_min", sWord32 "x" >>= minimize "m")+                   , ("64_unsigned_max", sWord64 "x" >>= maximize "m")+                   , ("64_unsigned_min", sWord64 "x" >>= minimize "m")+                   , ("08_signed_max",   sInt8   "x" >>= maximize "m")+                   , ("08_signed_min",   sInt8   "x" >>= minimize "m")+                   , ("16_signed_max",   sInt16  "x" >>= maximize "m")+                   , ("16_signed_min",   sInt16  "x" >>= minimize "m")+                   , ("32_signed_max",   sInt32  "x" >>= maximize "m")+                   , ("32_signed_min",   sInt32  "x" >>= minimize "m")+                   , ("64_signed_max",   sInt64  "x" >>= maximize "m")+                   , ("64_signed_min",   sInt64  "x" >>= minimize "m")+                   ]+       ]  optBasics1 :: Goal optBasics1 = do x <- sInteger "x"
SBVTestSuite/TestSuite/Puzzles/PowerSet.hs view
@@ -19,7 +19,7 @@     [ testCase ("powerSet " ++ show i) (assert (pSet i)) | i <- [0 .. 7] ]  pSet :: Int -> IO Bool-pSet n = do cnt <- numberOfModels $ do _ <- mapM (\i -> sBool ("e" ++ show i)) [1..n]+pSet n = do cnt <- numberOfModels $ do mapM_ (\i -> sBool ("e" ++ show i)) [1..n]                                        -- Look ma! No constraints!                                        return (true :: SBool)             return (cnt == 2^n)
sbv.cabal view
@@ -1,5 +1,5 @@ Name:          sbv-Version:       7.3+Version:       7.4 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