diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,23 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV/Control.hs b/Data/SBV/Control.hs --- a/Data/SBV/Control.hs +++ b/Data/SBV/Control.hs @@ -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) diff --git a/Data/SBV/Control/Query.hs b/Data/SBV/Control/Query.hs --- a/Data/SBV/Control/Query.hs +++ b/Data/SBV/Control/Query.hs @@ -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 diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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. diff --git a/Data/SBV/Examples/BitPrecise/MultMask.hs b/Data/SBV/Examples/BitPrecise/MultMask.hs --- a/Data/SBV/Examples/BitPrecise/MultMask.hs +++ b/Data/SBV/Examples/BitPrecise/MultMask.hs @@ -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 diff --git a/Data/SBV/Examples/Puzzles/U2Bridge.hs b/Data/SBV/Examples/Puzzles/U2Bridge.hs --- a/Data/SBV/Examples/Puzzles/U2Bridge.hs +++ b/Data/SBV/Examples/Puzzles/U2Bridge.hs @@ -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. diff --git a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs --- a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs +++ b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -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 diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -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 diff --git a/Data/SBV/Utils/SExpr.hs b/Data/SBV/Utils/SExpr.hs --- a/Data/SBV/Utils/SExpr.hs +++ b/Data/SBV/Utils/SExpr.hs @@ -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 diff --git a/SBVTestSuite/GoldFiles/U2Bridge.gold b/SBVTestSuite/GoldFiles/U2Bridge.gold --- a/SBVTestSuite/GoldFiles/U2Bridge.gold +++ b/SBVTestSuite/GoldFiles/U2Bridge.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 127 :: Int8 + m = 127 :: Int8 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = -128 :: Int8 + m = -128 :: Int8 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 255 :: Word8 + m = 255 :: Word8 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_08_unsigned_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 0 :: Word8 + m = 0 :: Word8 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 32767 :: Int16 + m = 32767 :: Int16 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = -32768 :: Int16 + m = -32768 :: Int16 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 65535 :: Word16 + m = 65535 :: Word16 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_16_unsigned_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 0 :: Word16 + m = 0 :: Word16 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 2147483647 :: Int32 + m = 2147483647 :: Int32 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = -2147483648 :: Int32 + m = -2147483648 :: Int32 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 4294967295 :: Word32 + m = 4294967295 :: Word32 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_32_unsigned_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 0 :: Word32 + m = 0 :: Word32 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 9223372036854775807 :: Int64 + m = 9223372036854775807 :: Int64 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = -9223372036854775808 :: Int64 + m = -9223372036854775808 :: Int64 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_max.gold b/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_max.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_max.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 18446744073709551615 :: Word64 + m = 18446744073709551615 :: Word64 diff --git a/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_min.gold b/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_min.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/optBasicsRange_64_unsigned_min.gold @@ -0,0 +1,3 @@ +Optimal model: + x = 0 :: Word64 + m = 0 :: Word64 diff --git a/SBVTestSuite/GoldFiles/pareto1.gold b/SBVTestSuite/GoldFiles/pareto1.gold --- a/SBVTestSuite/GoldFiles/pareto1.gold +++ b/SBVTestSuite/GoldFiles/pareto1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/pareto2.gold b/SBVTestSuite/GoldFiles/pareto2.gold --- a/SBVTestSuite/GoldFiles/pareto2.gold +++ b/SBVTestSuite/GoldFiles/pareto2.gold @@ -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. diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -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|) diff --git a/SBVTestSuite/GoldFiles/query_Interpolant2.gold b/SBVTestSuite/GoldFiles/query_Interpolant2.gold --- a/SBVTestSuite/GoldFiles/query_Interpolant2.gold +++ b/SBVTestSuite/GoldFiles/query_Interpolant2.gold @@ -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)))"] diff --git a/SBVTestSuite/GoldFiles/query_Interpolant3.gold b/SBVTestSuite/GoldFiles/query_Interpolant3.gold --- a/SBVTestSuite/GoldFiles/query_Interpolant3.gold +++ b/SBVTestSuite/GoldFiles/query_Interpolant3.gold @@ -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))))"] diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/temperature.gold b/SBVTestSuite/GoldFiles/temperature.gold --- a/SBVTestSuite/GoldFiles/temperature.gold +++ b/SBVTestSuite/GoldFiles/temperature.gold @@ -1,5 +1,5 @@ Solution #1: - s0 = 28 :: Integer -Solution #2: s0 = 16 :: Integer +Solution #2: + s0 = 28 :: Integer Found 2 different solutions. diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -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 () diff --git a/SBVTestSuite/TestSuite/Optimization/Basics.hs b/SBVTestSuite/TestSuite/Optimization/Basics.hs --- a/SBVTestSuite/TestSuite/Optimization/Basics.hs +++ b/SBVTestSuite/TestSuite/Optimization/Basics.hs @@ -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" diff --git a/SBVTestSuite/TestSuite/Puzzles/PowerSet.hs b/SBVTestSuite/TestSuite/Puzzles/PowerSet.hs --- a/SBVTestSuite/TestSuite/Puzzles/PowerSet.hs +++ b/SBVTestSuite/TestSuite/Puzzles/PowerSet.hs @@ -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) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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