sbv 10.3 → 10.4
raw patch · 18 files changed
+360/−216 lines, 18 files
Files
- CHANGES.md +9/−1
- Data/SBV.hs +2/−2
- Data/SBV/Control/Utils.hs +39/−13
- Data/SBV/Core/Symbolic.hs +131/−127
- Data/SBV/Lambda.hs +35/−34
- Data/SBV/Provers/Prover.hs +1/−0
- Data/SBV/SMT/SMT.hs +5/−5
- Data/SBV/Utils/CrackNum.hs +46/−26
- SBVTestSuite/GoldFiles/allSat8.gold +1/−1
- SBVTestSuite/GoldFiles/arrayGetValTest1.gold +44/−0
- SBVTestSuite/GoldFiles/nested1.gold +1/−1
- SBVTestSuite/GoldFiles/nested2.gold +1/−1
- SBVTestSuite/GoldFiles/nested3.gold +1/−1
- SBVTestSuite/GoldFiles/nested4.gold +1/−1
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- SBVTestSuite/SBVTest.hs +2/−0
- SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs +37/−0
- sbv.cabal +2/−1
CHANGES.md view
@@ -1,7 +1,15 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.io/sbv/> -* 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
Data/SBV.hs view
@@ -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
Data/SBV/Control/Utils.hs view
@@ -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
Data/SBV/Core/Symbolic.hs view
@@ -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
Data/SBV/Lambda.hs view
@@ -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
Data/SBV/Provers/Prover.hs view
@@ -87,6 +87,7 @@ , printBase = 10 , printRealPrec = 16 , crackNum = False+ , crackNumSurfaceVals = [] , transcript = Nothing , solver = s , smtLibVersion = smtVersion
Data/SBV/SMT/SMT.hs view
@@ -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
Data/SBV/Utils/CrackNum.hs view
@@ -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
SBVTestSuite/GoldFiles/allSat8.gold view
@@ -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
+ SBVTestSuite/GoldFiles/arrayGetValTest1.gold view
@@ -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!
SBVTestSuite/GoldFiles/nested1.gold view
@@ -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
SBVTestSuite/GoldFiles/nested2.gold view
@@ -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
SBVTestSuite/GoldFiles/nested3.gold view
@@ -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
SBVTestSuite/GoldFiles/nested4.gold view
@@ -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
SBVTestSuite/GoldFiles/query1.gold view
@@ -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)
SBVTestSuite/SBVTest.hs view
@@ -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
+ SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs view
@@ -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)
sbv.cabal view
@@ -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