diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,15 @@ * Hackage: * GitHub: -* Latest Hackage released version: 10.3, 2024-01-05 +* Latest Hackage released version: 10.4, 2024-02-15 + +### Version 10.4, 2024-02-15 + + * Before issuing a get-value, make sure there are no outstanding assert calls. + See: https://github.com/LeventErkok/sbv/issues/682 for details. + + * crackNum mode now displays the surface form of NaNs more faithfully, if provided + with the input string. This functionality is used by the crackNum executable. ### Version 10.3, 2024-01-05 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -503,8 +503,8 @@ -- | Show a value in detailed (cracked) form, if possible. -- This makes most sense with numbers, and especially floating-point types. crack :: SBV a -> String -crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv = s -crack (SBV sv) = show sv +crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv Nothing = s +crack (SBV sv) = show sv -- Haddock section documentation {- $progIntro 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 @@ -273,23 +273,29 @@ queryDebug msgs = do QueryState{queryConfig} <- getQueryState io $ debug queryConfig msgs +-- | We need to track sent asserts/check-sat calls so we can issue an extra check-sat call if needed +trackAsserts :: (MonadIO m, MonadQuery m) => String -> m () +trackAsserts s + | isCheckSat || isAssert + = do State{rOutstandingAsserts} <- queryState + liftIO $ writeIORef rOutstandingAsserts isAssert + | True + = pure () + where trimmedS = dropWhile isSpace s + isCheckSat = "(check-sat" `isPrefixOf` trimmedS + isAssert = "(assert" `isPrefixOf` trimmedS + -- | Generalization of 'Data.SBV.Control.ask' ask :: (MonadIO m, MonadQuery m) => String -> m String -ask s = do QueryState{queryAsk, queryTimeOutValue} <- getQueryState - - case queryTimeOutValue of - Nothing -> queryDebug ["[SEND] " `alignPlain` s] - Just i -> queryDebug ["[SEND, TimeOut: " ++ showTimeoutValue i ++ "] " `alignPlain` s] - r <- io $ queryAsk queryTimeOutValue s - queryDebug ["[RECV] " `alignPlain` r] - - return r +ask s = askIgnoring s [] -- | Send a string to the solver, and return the response. Except, if the response -- is one of the "ignore" ones, keep querying. askIgnoring :: (MonadIO m, MonadQuery m) => String -> [String] -> m String askIgnoring s ignoreList = do + trackAsserts s + QueryState{queryAsk, queryRetrieveResponse, queryTimeOutValue} <- getQueryState case queryTimeOutValue of @@ -313,6 +319,8 @@ send :: (MonadIO m, MonadQuery m) => Bool -> String -> m () send requireSuccess s = do + trackAsserts s + QueryState{queryAsk, querySend, queryConfig, queryTimeOutValue} <- getQueryState if requireSuccess && supportsCustomQueries (capabilities (solver queryConfig)) @@ -365,10 +373,28 @@ -- | Generalization of 'Data.SBV.Control.getValue' getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a -getValue s = do sv <- inNewContext (`sbvToSV` s) - cv <- getValueCV Nothing sv - return $ fromCV cv +getValue s = do + sv <- inNewContext (`sbvToSV` s) + + -- If we're issuing get-value, we gotta make sure there are no outstanding asserts + -- This can happen if we sent some ourselves. See https://github.com/LeventErkok/sbv/issues/682 + outstandingAsserts <- do State{rOutstandingAsserts} <- queryState + liftIO $ readIORef rOutstandingAsserts + + when outstandingAsserts $ do + queryDebug ["[NOTE] getValue: There are outstanding asserts. Ensuring we're still sat."] + r <- checkSat + let bad = unexpected "checkSat" "check-sat" "one of sat/unsat/unknown" Nothing (show r) Nothing + case r of + Sat -> pure () + DSat{} -> pure () + Unk -> bad + Unsat -> bad + + cv <- getValueCV Nothing sv + return $ fromCV cv + -- | A class which allows for sexpr-conversion to functions class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where sexprToArg :: fun -> [SExpr] -> Maybe a @@ -1147,7 +1173,7 @@ cmd = "(get-value (" ++ nm ++ ")" ++ modelIndex ++ ")" - bad = unexpected "getModel" cmd ("a value binding for kind: " ++ show k) Nothing + bad = unexpected "get-value" cmd ("a value binding for kind: " ++ show k) Nothing r <- ask cmd diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -1224,40 +1224,41 @@ rnf (SMTLam fk frees params body) = rnf fk `seq` rnf frees `seq` rnf params `seq` rnf body -- | The state of the symbolic interpreter -data State = State { sbvContext :: SBVContext - , pathCond :: SVal -- ^ kind KBool - , stCfg :: SMTConfig - , startTime :: UTCTime - , rProgInfo :: IORef ProgInfo - , runMode :: IORef SBVRunMode - , rIncState :: IORef IncState - , rCInfo :: IORef [(String, CV)] - , rObservables :: IORef (S.Seq (Name, CV -> Bool, SV)) - , rctr :: IORef Int - , rLambdaLevel :: IORef Int - , rUsedKinds :: IORef KindSet - , rUsedLbls :: IORef (Set.Set String) - , rinps :: IORef Inputs - , rlambdaInps :: IORef LambdaInputs - , rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV)) - , rPartitionVars :: IORef [String] - , routs :: IORef [SV] - , rtblMap :: IORef TableMap - , spgm :: IORef SBVPgm - , rconstMap :: IORef CnstMap - , rexprMap :: IORef ExprMap - , rArrayMap :: IORef ArrayMap - , rUIMap :: IORef UIMap - , rUserFuncs :: IORef (Set.Set String) -- Functions that the user wanted explicit code generation for - , rCgMap :: IORef CgMap - , rDefns :: IORef [(SMTDef, SBVType)] - , rSMTOptions :: IORef [SMTOption] - , rOptGoals :: IORef [Objective (SV, SV)] - , rAsserts :: IORef [(String, Maybe CallStack, SV)] - , rSVCache :: IORef (Cache SV) - , rAICache :: IORef (Cache ArrayIndex) - , rQueryState :: IORef (Maybe QueryState) - , parentState :: Maybe State -- Pointer to our parent if we're in a sublevel +data State = State { sbvContext :: SBVContext + , pathCond :: SVal -- ^ kind KBool + , stCfg :: SMTConfig + , startTime :: UTCTime + , rProgInfo :: IORef ProgInfo + , runMode :: IORef SBVRunMode + , rIncState :: IORef IncState + , rCInfo :: IORef [(String, CV)] + , rObservables :: IORef (S.Seq (Name, CV -> Bool, SV)) + , rctr :: IORef Int + , rLambdaLevel :: IORef Int + , rUsedKinds :: IORef KindSet + , rUsedLbls :: IORef (Set.Set String) + , rinps :: IORef Inputs + , rlambdaInps :: IORef LambdaInputs + , rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV)) + , rPartitionVars :: IORef [String] + , routs :: IORef [SV] + , rtblMap :: IORef TableMap + , spgm :: IORef SBVPgm + , rconstMap :: IORef CnstMap + , rexprMap :: IORef ExprMap + , rArrayMap :: IORef ArrayMap + , rUIMap :: IORef UIMap + , rUserFuncs :: IORef (Set.Set String) -- Functions that the user wanted explicit code generation for + , rCgMap :: IORef CgMap + , rDefns :: IORef [(SMTDef, SBVType)] + , rSMTOptions :: IORef [SMTOption] + , rOptGoals :: IORef [Objective (SV, SV)] + , rAsserts :: IORef [(String, Maybe CallStack, SV)] + , rOutstandingAsserts :: IORef Bool -- Did we send an assert after the last check-sat call? + , rSVCache :: IORef (Cache SV) + , rAICache :: IORef (Cache ArrayIndex) + , rQueryState :: IORef (Maybe QueryState) + , parentState :: Maybe State -- Pointer to our parent if we're in a sublevel } -- | Chase to the root state. No infinite chains! @@ -1849,78 +1850,80 @@ -- | Create a new state mkNewState :: MonadIO m => SMTConfig -> SBVRunMode -> m State mkNewState cfg currentRunMode = liftIO $ do - currTime <- getCurrentTime - progInfo <- newIORef ProgInfo { hasQuants = False - , progSpecialRels = [] - , progTransClosures = [] - } - rm <- newIORef currentRunMode - ctr <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements - lambda <- newIORef $ case currentRunMode of - SMTMode{} -> 0 - CodeGen{} -> 0 - Concrete{} -> 0 - LambdaGen i -> i - cInfo <- newIORef [] - observes <- newIORef mempty - pgm <- newIORef (SBVPgm S.empty) - emap <- newIORef Map.empty - cmap <- newIORef Map.empty - inps <- newIORef mempty - lambdaInps <- newIORef mempty - outs <- newIORef [] - tables <- newIORef Map.empty - arrays <- newIORef IMap.empty - userFuncs <- newIORef Set.empty - uis <- newIORef Map.empty - cgs <- newIORef Map.empty - defns <- newIORef [] - swCache <- newIORef IMap.empty - aiCache <- newIORef IMap.empty - usedKinds <- newIORef Set.empty - usedLbls <- newIORef Set.empty - cstrs <- newIORef S.empty - pvs <- newIORef [] - smtOpts <- newIORef [] - optGoals <- newIORef [] - asserts <- newIORef [] - istate <- newIORef =<< newIncState - qstate <- newIORef Nothing - ctx <- genSBVContext - pure $ State { sbvContext = ctx - , runMode = rm - , stCfg = cfg - , startTime = currTime - , rProgInfo = progInfo - , pathCond = SVal KBool (Left trueCV) - , rIncState = istate - , rCInfo = cInfo - , rObservables = observes - , rctr = ctr - , rLambdaLevel = lambda - , rUsedKinds = usedKinds - , rUsedLbls = usedLbls - , rinps = inps - , rlambdaInps = lambdaInps - , routs = outs - , rtblMap = tables - , spgm = pgm - , rconstMap = cmap - , rArrayMap = arrays - , rexprMap = emap - , rUserFuncs = userFuncs - , rUIMap = uis - , rCgMap = cgs - , rDefns = defns - , rSVCache = swCache - , rAICache = aiCache - , rConstraints = cstrs - , rPartitionVars = pvs - , rSMTOptions = smtOpts - , rOptGoals = optGoals - , rAsserts = asserts - , rQueryState = qstate - , parentState = Nothing + currTime <- getCurrentTime + progInfo <- newIORef ProgInfo { hasQuants = False + , progSpecialRels = [] + , progTransClosures = [] + } + rm <- newIORef currentRunMode + ctr <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements + lambda <- newIORef $ case currentRunMode of + SMTMode{} -> 0 + CodeGen{} -> 0 + Concrete{} -> 0 + LambdaGen i -> i + cInfo <- newIORef [] + observes <- newIORef mempty + pgm <- newIORef (SBVPgm S.empty) + emap <- newIORef Map.empty + cmap <- newIORef Map.empty + inps <- newIORef mempty + lambdaInps <- newIORef mempty + outs <- newIORef [] + tables <- newIORef Map.empty + arrays <- newIORef IMap.empty + userFuncs <- newIORef Set.empty + uis <- newIORef Map.empty + cgs <- newIORef Map.empty + defns <- newIORef [] + swCache <- newIORef IMap.empty + aiCache <- newIORef IMap.empty + usedKinds <- newIORef Set.empty + usedLbls <- newIORef Set.empty + cstrs <- newIORef S.empty + pvs <- newIORef [] + smtOpts <- newIORef [] + optGoals <- newIORef [] + asserts <- newIORef [] + outstandingAsserts <- newIORef False + istate <- newIORef =<< newIncState + qstate <- newIORef Nothing + ctx <- genSBVContext + pure $ State { sbvContext = ctx + , runMode = rm + , stCfg = cfg + , startTime = currTime + , rProgInfo = progInfo + , pathCond = SVal KBool (Left trueCV) + , rIncState = istate + , rCInfo = cInfo + , rObservables = observes + , rctr = ctr + , rLambdaLevel = lambda + , rUsedKinds = usedKinds + , rUsedLbls = usedLbls + , rinps = inps + , rlambdaInps = lambdaInps + , routs = outs + , rtblMap = tables + , spgm = pgm + , rconstMap = cmap + , rArrayMap = arrays + , rexprMap = emap + , rUserFuncs = userFuncs + , rUIMap = uis + , rCgMap = cgs + , rDefns = defns + , rSVCache = swCache + , rAICache = aiCache + , rConstraints = cstrs + , rPartitionVars = pvs + , rSMTOptions = smtOpts + , rOptGoals = optGoals + , rAsserts = asserts + , rOutstandingAsserts = outstandingAsserts + , rQueryState = qstate + , parentState = Nothing } -- | Generalization of 'Data.SBV.runSymbolic' @@ -2280,27 +2283,28 @@ -- (i.e., SWord and SInt), but also with floats. It is particularly useful with floating-point numbers, as it shows you how they are laid out in -- memory following the IEEE754 rules. data SMTConfig = SMTConfig { - verbose :: Bool -- ^ Debug mode - , timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.) - , printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.) - , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) - , crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats. - , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. - , allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all. - , allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found. - , allSatTrackUFs :: Bool -- ^ In a 'Data.SBV.allSat' call, should we try to extract values of uninterpreted functions? - , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) - , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. - , optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints. - , transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly) - , smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool - , dsatPrecision :: Maybe Double -- ^ Delta-sat precision - , solver :: SMTSolver -- ^ The actual SMT solver. - , extraArgs :: [String] -- ^ Extra command line arguments to pass to the solver. - , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions - , solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver - , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess. - , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. + verbose :: Bool -- ^ Debug mode + , timing :: Timing -- ^ Print timing information on how long different phases took (construction, solving, etc.) + , printBase :: Int -- ^ Print integral literals in this base (2, 10, and 16 are supported.) + , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) + , crackNum :: Bool -- ^ For each numeric value, show it in detail in the model with its bits spliced out. Good for floats. + , crackNumSurfaceVals :: [(String, Integer)] -- ^ For crackNum: The surface representation of variables, if available + , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. + , allSatMaxModelCount :: Maybe Int -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all. + , allSatPrintAlong :: Bool -- ^ In a 'Data.SBV.allSat' call, print models as they are found. + , allSatTrackUFs :: Bool -- ^ In a 'Data.SBV.allSat' call, should we try to extract values of uninterpreted functions? + , isNonModelVar :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything) + , validateModel :: Bool -- ^ If set, SBV will attempt to validate the model it gets back from the solver. + , optimizeValidateConstraints :: Bool -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints. + , transcript :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly) + , smtLibVersion :: SMTLibVersion -- ^ What version of SMT-lib we use for the tool + , dsatPrecision :: Maybe Double -- ^ Delta-sat precision + , solver :: SMTSolver -- ^ The actual SMT solver. + , extraArgs :: [String] -- ^ Extra command line arguments to pass to the solver. + , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions + , solverSetOptions :: [SMTOption] -- ^ Options to set as we start the solver + , ignoreExitCode :: Bool -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess. + , redirectVerbose :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied. } -- | Ignore internal names and those the user told us to diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -70,46 +70,47 @@ -- don't really impact anything. comp State { -- These are not IORefs; so we share by copying the value; changes won't be copied back - sbvContext = share sbvContext - , pathCond = share pathCond - , startTime = share startTime + sbvContext = share sbvContext + , pathCond = share pathCond + , startTime = share startTime -- These are shared IORef's; and is shared, so they will be copied back to the parent state - , rProgInfo = share rProgInfo - , rIncState = share rIncState - , rCInfo = share rCInfo - , rUsedKinds = share rUsedKinds - , rUsedLbls = share rUsedLbls - , rUIMap = share rUIMap - , rUserFuncs = share rUserFuncs - , rCgMap = share rCgMap - , rDefns = share rDefns - , rSMTOptions = share rSMTOptions - , rOptGoals = share rOptGoals - , rAsserts = share rAsserts - , rPartitionVars = share rPartitionVars + , rProgInfo = share rProgInfo + , rIncState = share rIncState + , rCInfo = share rCInfo + , rUsedKinds = share rUsedKinds + , rUsedLbls = share rUsedLbls + , rUIMap = share rUIMap + , rUserFuncs = share rUserFuncs + , rCgMap = share rCgMap + , rDefns = share rDefns + , rSMTOptions = share rSMTOptions + , rOptGoals = share rOptGoals + , rAsserts = share rAsserts + , rOutstandingAsserts = share rOutstandingAsserts + , rPartitionVars = share rPartitionVars -- Everything else is fresh in the substate; i.e., will not copy back - , stCfg = fresh stCfg - , runMode = fresh runMode - , rctr = fresh rctr - , rLambdaLevel = fresh rLambdaLevel - , rtblMap = fresh rtblMap - , rArrayMap = fresh rArrayMap - , rAICache = fresh rAICache - , rinps = fresh rinps - , rlambdaInps = fresh rlambdaInps - , rConstraints = fresh rConstraints - , rObservables = fresh rObservables - , routs = fresh routs - , spgm = fresh spgm - , rconstMap = fresh rconstMap - , rexprMap = fresh rexprMap - , rSVCache = fresh rSVCache - , rQueryState = fresh rQueryState + , stCfg = fresh stCfg + , runMode = fresh runMode + , rctr = fresh rctr + , rLambdaLevel = fresh rLambdaLevel + , rtblMap = fresh rtblMap + , rArrayMap = fresh rArrayMap + , rAICache = fresh rAICache + , rinps = fresh rinps + , rlambdaInps = fresh rlambdaInps + , rConstraints = fresh rConstraints + , rObservables = fresh rObservables + , routs = fresh routs + , spgm = fresh spgm + , rconstMap = fresh rconstMap + , rexprMap = fresh rexprMap + , rSVCache = fresh rSVCache + , rQueryState = fresh rQueryState -- keep track of our parent - , parentState = Just inState + , parentState = Just inState } -- In this case, we expect just one group of parameters, with universal quantification 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 @@ -87,6 +87,7 @@ , printBase = 10 , printRealPrec = 16 , crackNum = False + , crackNumSurfaceVals = [] , transcript = Nothing , solver = s , smtLibVersion = smtVersion diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -560,8 +560,8 @@ | includeEverything = False | True = mustIgnoreVar cfg (T.unpack s) - shM (s, RegularCV v) = let vs = shCV cfg v in ((length s, s), (vlength vs, vs)) - shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs)) + shM (s, RegularCV v) = let vs = shCV cfg s v in ((length s, s), (vlength vs, vs)) + shM (s, other) = let vs = show other in ((length s, s), (vlength vs, vs)) display svs = map line svs where line ((_, s), (_, v)) = " " ++ right (nameWidth - length s) s ++ " = " ++ left (valWidth - lTrimRight (valPart v)) v @@ -633,8 +633,8 @@ paren _ x = x -- | Show a constant value, in the user-specified base -shCV :: SMTConfig -> CV -> String -shCV SMTConfig{printBase, crackNum} cv = cracked (sh printBase cv) +shCV :: SMTConfig -> String -> CV -> String +shCV SMTConfig{printBase, crackNum, crackNumSurfaceVals} nm cv = cracked (sh printBase cv) where sh 2 = binS sh 10 = show sh 16 = hexS @@ -642,7 +642,7 @@ cracked def | not crackNum = def - | True = case CN.crackNum cv of + | True = case CN.crackNum cv (nm `lookup` crackNumSurfaceVals) of Nothing -> def Just cs -> def ++ "\n" ++ cs diff --git a/Data/SBV/Utils/CrackNum.hs b/Data/SBV/Utils/CrackNum.hs --- a/Data/SBV/Utils/CrackNum.hs +++ b/Data/SBV/Utils/CrackNum.hs @@ -35,31 +35,31 @@ -- | A class for cracking things deeper, if we know how. class CrackNum a where -- | Convert an item to possibly bit-level description, if possible. - crackNum :: a -> Maybe String + crackNum :: a -> Maybe Integer -> Maybe String -- | CVs are easy to crack instance CrackNum CV where - crackNum cv = case kindOf cv of - -- Maybe one day we'll have a use for these, currently cracking them - -- any further seems overkill - KBool {} -> Nothing - KUnbounded {} -> Nothing - KReal {} -> Nothing - KUserSort {} -> Nothing - KChar {} -> Nothing - KString {} -> Nothing - KList {} -> Nothing - KSet {} -> Nothing - KTuple {} -> Nothing - KMaybe {} -> Nothing - KEither {} -> Nothing - KRational {} -> Nothing + crackNum cv mbIV = case kindOf cv of + -- Maybe one day we'll have a use for these, currently cracking them + -- any further seems overkill + KBool {} -> Nothing + KUnbounded {} -> Nothing + KReal {} -> Nothing + KUserSort {} -> Nothing + KChar {} -> Nothing + KString {} -> Nothing + KList {} -> Nothing + KSet {} -> Nothing + KTuple {} -> Nothing + KMaybe {} -> Nothing + KEither {} -> Nothing + KRational {} -> Nothing - -- Actual crackables - KFloat{} -> Just $ let CFloat f = cvVal cv in float f - KDouble{} -> Just $ let CDouble d = cvVal cv in float d - KFP{} -> Just $ let CFP f = cvVal cv in float f - KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i + -- Actual crackables + KFloat{} -> Just $ let CFloat f = cvVal cv in float mbIV f + KDouble{} -> Just $ let CDouble d = cvVal cv in float mbIV d + KFP{} -> Just $ let CFP f = cvVal cv in float mbIV f + KBounded sg sz -> Just $ let CInteger i = cvVal cv in int sg sz i -- How far off the screen we want displayed? Somewhat experimentally found. tab :: String @@ -227,11 +227,31 @@ | bfIsSubnormal opts f = Subnormal | True = Normal --- | Show a float in detail -float :: HasFloatData a => a -> String -float f = intercalate "\n" $ ruler ++ legend : info - where fd@FloatData{prec, eb, sb, bits, fpKind, fpVals} = getFloatData f +-- | Show a float in detail. mbSurface is the integer equivalent if this is a NaN; so we +-- can represent it faithfully to the original given. Used by crackNum executable. +float :: HasFloatData a => Maybe Integer -> a -> String +float mbSurface f = intercalate "\n" $ ruler ++ legend : info + where fd@FloatData{prec, eb, sb, bits = bitsAsStored, fpKind, fpVals} = getFloatData f + nanKind = case fpKind of + Zero{} -> False + Infty{} -> False + NaN -> True + Subnormal -> False + Normal -> False + + (nanClassifier, bits) + | nanKind, Just i <- mbSurface = (extraClassifier i, i) + | True = ("", bitsAsStored) + + -- Is this surface representation a signaling NaN or a quiet nan? + -- The test is that the tip bit of the significand is high: If so, quiet. If top bit is low, then signaling. + extraClassifier :: Integer -> String + extraClassifier i + | sb < 2 = "" -- I don't think this can happen, but just in case + | i `testBit` (sb - 2) = " (Quiet)" + | True = " (Signaling)" + splits = [1, eb, sb] ruler = map (tab ++) $ mkRuler (eb + sb) splits @@ -260,7 +280,7 @@ ] ++ [ " Exponent: " ++ show exponentVal ++ " (Subnormal, with fixed exponent value. " ++ esInfo ++ ")" | isSubNormal ] ++ [ " Exponent: " ++ show exponentVal ++ " (" ++ esInfo ++ ")" | not isSubNormal] - ++ [ " Classification: " ++ show fpKind] + ++ [ " Classification: " ++ show fpKind ++ nanClassifier] ++ (case fpVals of Left val -> [ " Value: " ++ val] Right (bval, oval, dval, hval) -> [ " Binary: " ++ bval diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -61,4 +61,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1634:57 in sbv-10.3-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.4-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/arrayGetValTest1.gold b/SBVTestSuite/GoldFiles/arrayGetValTest1.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/arrayGetValTest1.gold @@ -0,0 +1,44 @@ +** 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 unbounded values, using catch-all. +[GOOD] ; --- uninterpreted sorts --- +[GOOD] ; --- tuples --- +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] ; --- top level inputs --- +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- arrays --- +[GOOD] (declare-fun array_0 () (Array Int Int)) +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] ; --- arrayDelayeds --- +[GOOD] ; --- arraySetups --- +[GOOD] (define-fun array_0_initializer () Bool true) ; no initialization needed +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[SEND] (check-sat) +[RECV] sat +[GOOD] (define-fun s0 () Int 1) +[GOOD] (define-fun s1 () Int 2) +[GOOD] (declare-fun array_1 () (Array Int Int)) +[GOOD] (define-fun array_1_initializer_0 () Bool (= array_1 (store array_0 s0 s1))) +[GOOD] (define-fun s2 () Int (select array_1 s0)) +[GOOD] (define-fun array_1_initializer () Bool array_1_initializer_0) +[GOOD] (assert array_1_initializer) +[NOTE] getValue: There are outstanding asserts. Ensuring we're still sat. +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s2)) +[RECV] ((s2 2)) +*** Solver : Z3 +*** Exit code: ExitSuccess + + FINAL:2 +DONE! diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1934:48 in sbv-10.3-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1934:48 in sbv-10.3-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1934:48 in sbv-10.3-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1934:48 in sbv-10.3-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.4-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -77,7 +77,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.12.5") +[RECV] (:version "4.12.6") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -108,7 +108,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.12.5") +[RECV] (:version "4.12.6") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SBVTestSuite/SBVTest.hs b/SBVTestSuite/SBVTest.hs --- a/SBVTestSuite/SBVTest.hs +++ b/SBVTestSuite/SBVTest.hs @@ -98,6 +98,7 @@ import qualified TestSuite.Puzzles.Sudoku import qualified TestSuite.Puzzles.Temperature import qualified TestSuite.Puzzles.U2Bridge +import qualified TestSuite.Queries.ArrayGetVal import qualified TestSuite.Queries.BasicQuery import qualified TestSuite.Queries.BadOption import qualified TestSuite.Queries.DSat @@ -212,6 +213,7 @@ , TestSuite.Puzzles.Temperature.tests , TestSuite.Puzzles.U2Bridge.tests , TestSuite.Queries.BadOption.tests + , TestSuite.Queries.ArrayGetVal.tests , TestSuite.Queries.BasicQuery.tests , TestSuite.Queries.DSat.tests , TestSuite.Queries.Interpolants.tests diff --git a/SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs b/SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs new file mode 100644 --- /dev/null +++ b/SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs @@ -0,0 +1,37 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Queries.ArrayGetVal +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Making sure array get-value works, since we might send extra asserts after +-- check-sat. +----------------------------------------------------------------------------- + +{-# LANGUAGE ScopedTypeVariables #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module TestSuite.Queries.ArrayGetVal (tests) where + +import Data.SBV.Control + +import Utils.SBVTestFramework + +-- Test suite +tests :: TestTree +tests = + testGroup "Basics.ArrayGetVal" + [ goldenCapturedIO "arrayGetValTest1" testQuery + ] + +testQuery :: FilePath -> IO () +testQuery rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t1 + appendFile rf ("\n FINAL:" ++ show r ++ "\nDONE!\n") + +t1 :: Symbolic Integer +t1 = do a :: SArray Integer Integer <- newArray "a" Nothing + query $ do ensureSat + getValue (readArray (writeArray a 1 2) 1) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 10.3 +Version : 10.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 @@ -357,6 +357,7 @@ , TestSuite.Puzzles.Temperature , TestSuite.Puzzles.U2Bridge , TestSuite.Queries.BasicQuery + , TestSuite.Queries.ArrayGetVal , TestSuite.Queries.BadOption , TestSuite.Queries.DSat , TestSuite.Queries.Enums