sbv 7.8 → 7.9
raw patch · 45 files changed
+1619/−642 lines, 45 files
Files
- CHANGES.md +48/−1
- Data/SBV.hs +21/−9
- Data/SBV/Compilers/C.hs +41/−4
- Data/SBV/Compilers/CodeGen.hs +1/−1
- Data/SBV/Control.hs +6/−8
- Data/SBV/Control/Query.hs +34/−33
- Data/SBV/Control/Types.hs +9/−1
- Data/SBV/Control/Utils.hs +30/−34
- Data/SBV/Core/Concrete.hs +12/−10
- Data/SBV/Core/Data.hs +2/−0
- Data/SBV/Core/Floating.hs +2/−2
- Data/SBV/Core/Model.hs +5/−3
- Data/SBV/Core/Operations.hs +12/−8
- Data/SBV/Core/Symbolic.hs +79/−45
- Data/SBV/Provers/Prover.hs +2/−2
- Data/SBV/SMT/SMT.hs +4/−4
- Data/SBV/SMT/SMTLib2.hs +12/−12
- Data/SBV/SMT/Utils.hs +8/−6
- Data/SBV/String.hs +1/−1
- Data/SBV/Tools/Overflow.hs +399/−0
- Data/SBV/Utils/Numeric.hs +14/−0
- Documentation/SBV/Examples/Existentials/Diophantine.hs +0/−1
- Documentation/SBV/Examples/Misc/Floating.hs +14/−14
- Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +1/−1
- Documentation/SBV/Examples/Queries/Interpolants.hs +37/−24
- SBVTestSuite/GoldFiles/floats_cgen.gold +2/−1
- SBVTestSuite/GoldFiles/pareto1.gold +94/−94
- SBVTestSuite/GoldFiles/pareto2.gold +146/−146
- SBVTestSuite/GoldFiles/pareto3.gold +8/−0
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- SBVTestSuite/GoldFiles/query_Interpolant1.gold +9/−10
- SBVTestSuite/GoldFiles/query_Interpolant2.gold +9/−10
- SBVTestSuite/GoldFiles/query_Interpolant3.gold +0/−49
- SBVTestSuite/GoldFiles/query_Interpolant4.gold +0/−46
- SBVTestSuite/GoldFiles/safe1.gold +39/−0
- SBVTestSuite/GoldFiles/safe2.gold +38/−0
- SBVTestSuite/GoldFiles/timeout1.gold +1/−1
- SBVTestSuite/SBVDocTest.hs +36/−12
- SBVTestSuite/SBVTest.hs +9/−2
- SBVTestSuite/TestSuite/Basics/Assert.hs +23/−0
- SBVTestSuite/TestSuite/Optimization/Combined.hs +10/−0
- SBVTestSuite/TestSuite/Overflows/Arithmetic.hs +246/−0
- SBVTestSuite/TestSuite/Overflows/Casts.hs +134/−0
- SBVTestSuite/TestSuite/Queries/Interpolants.hs +13/−43
- sbv.cabal +6/−2
CHANGES.md view
@@ -1,7 +1,54 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 7.8, 2018-05-18+* Latest Hackage released version: 7.9, 2018-06-15++### Version 7.9, 2018-06-15+ + * Add support for bit-vector arithmetic underflow/overflow detection. The new+ 'ArithmeticOverflow' class captures conditions under which addition, subtraction,+ multiplication, division, and negation can underflow/overflow for+ both signed and unsigned bit-vector values. The implementation is based on+ http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf,+ and can be used to detect overflow caused bugs in machine arithmetic.+ See "Data.SBV.Tools.Overflow" for details.++ * Add 'sFromIntegralO', which is the overflow/underflow detecting variant+ of 'sFromIntegral'. This function returns (along with the converted+ result), a pair of booleans showing whether the conversion underflowed+ or overflowed.++ * Change the function 'getUnknownReason' to return a proper data-type+ ('SMTReasonUnknown') as opposed to a mere string. This is at the+ query level. Similarly, change `Unknown` result to return the same+ data-type at the sat/prove level.++ * Interpolants: With Z3 4.8.0 release, Z3 folks have dropped support+ for producing interpolants. If you need interpolants, you will have+ to use the MathSAT backend now. Also, the MathSAT API is slightly+ different from how Z3 supported interpolants as well, which means+ your old code will need some modifications. See the example in+ Documentation.SBV.Examples.Queries.Interpolants for the new usage.++ * Add 'constrainWithAttribute' call, which can be used to attach + arbitrary attribute to a constraint. Main use case is in interpolant+ generation with MathSAT.++ * C code generation: SBV now spits out linker flag -lm if needed.+ Thanks to Matt Peddie for reporting.++ * Code reorg: Simplify constant mapping table, by properly accounting+ for negative-zero floats.+ + * Export 'sexprToVal' for the class SMTValue, which allows for custom+ definitions of value extractions. Thanks to Brian Schroeder for the+ patch.+ + * Export 'Logic' directly from Data.SBV. (Previously was from Control.)++ * Fix a long standing issue (ever since we introduced queries) where+ 'sAssert' calls were run in the context of the final output boolean,+ which is simply the wrong thing to do. ### Version 7.8, Released 2018-05-18
Data/SBV.hs view
@@ -209,9 +209,9 @@ -- ** Constraint Vacuity -- $constraintVacuity - -- ** Named constraints+ -- ** Named constraints and attributes -- $namedConstraints- , namedConstraint+ , namedConstraint, constrainWithAttribute -- ** Unsat cores -- $unsatCores@@ -247,7 +247,7 @@ -- ** Inspecting proof results -- $resultTypes- , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)+ , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..), SMTReasonUnknown(..) -- ** Observing expressions -- $observeInternal@@ -267,7 +267,7 @@ , boolector, cvc4, yices, z3, mathSAT, abc -- ** Configurations , defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, sbvAvailableSolvers- , setLogic, setOption, setInfo, setTimeOut+ , setLogic, Logic(..), setOption, setInfo, setTimeOut -- ** Solver exceptions , SMTException(..) @@ -309,7 +309,8 @@ import Data.Generics import Data.SBV.SMT.Utils (SMTException(..))-import Data.SBV.Control.Utils (SMTValue)+import Data.SBV.Control.Utils (SMTValue (..))+import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..)) -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing -- problems with constraints, like the following:@@ -591,11 +592,16 @@ * ['Pareto']. Finally, the user can query for pareto-fronts. A pareto front is an model such that no goal can be made "better" without making some other goal "worse." + Pareto fronts only make sense when the objectives are bounded. If there are unbounded objective values, then the+ backend solver can loop infinitely. (This is what z3 does currently.) If you are not sure the objectives are+ bounded, you should first use 'Independent' mode to ensure the objectives are bounded, and then switch to+ pareto-mode to extract them further.+ The optional number argument to 'Pareto' specifies the maximum number of pareto-fronts the user is asking- to get. If 'Nothing', SBV will query for all pareto-fronts. Note that pareto-fronts can be infinite- in number, so if 'Nothing' is used, there is a potential for infinitely waiting for the SBV-solver interaction- to finish. (If you suspect this might be the case, run in 'verbose' mode to see the interaction and- put a limiting factor appropriately.)+ to get. If 'Nothing', SBV will query for all pareto-fronts. Note that pareto-fronts can be really large,+ so if 'Nothing' is used, there is a potential for waiting indefinitely for the SBV-solver interaction to finish. (If+ you suspect this might be the case, run in 'verbose' mode to see the interaction and put a limiting factor+ appropriately.) -} {- $softAssertions@@ -826,6 +832,12 @@ Constraints can be given names: @ 'namedConstraint' "a is at least 5" $ a .>= 5@++Similarly, arbitrary term attributes can also be associated:++ @ 'constrainWithAttribute' [(":solver-specific-attribute", "value")] $ a .>= 5@++Note that a 'namedConstraint' is equivalent to a 'constrainWithAttribute' call, setting the `":named"' attribute. -} {- $unsatCores
Data/SBV/Compilers/C.hs view
@@ -104,13 +104,18 @@ , (nmd ++ ".c", (CgDriver, genDriver cfg randVals nm ins outs mbRet)) , (nm ++ ".c", (CgSource, body)) ]- body = genCProg cfg nm sig sbvProg ins outs mbRet extDecls++ (body, flagsNeeded) = genCProg cfg nm sig sbvProg ins outs mbRet extDecls+ bundleKind = (cgInteger cfg, cgReal cfg)+ randVals = cgDriverVals cfg+ filt xs = [c | c@(_, (k, _)) <- xs, need k] where need k | isCgDriver k = cgGenDriver cfg | isCgMakefile k = cgGenMakefile cfg | True = True+ nmd = nm ++ "_driver" sig = pprCFunHeader nm ins outs mbRet ins = cgInputs st@@ -126,7 +131,7 @@ extDecls = case cgDecls st of [] -> empty xs -> vcat $ text "/* User given declarations: */" : map text xs- flags = cgLDFlags st+ flags = flagsNeeded ++ cgLDFlags st -- | Pretty print a functions type. If there is only one output, we compile it -- as a function that returns that value. Otherwise, we compile it as a void function@@ -411,7 +416,7 @@ spec = specifier cfg sw -- | Generate the C program-genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc]+genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> ([Doc], [String]) genCProg cfg fn proto (Result kindInfo _tvals _ovals cgs ins preConsts tbls arrs _uis _axioms (SBVPgm asgns) cstrs origAsserts _) inVars outVars mbRet extDecls | isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo = error $ "SBV->C: Unbounded integers are not supported by the C compiler."@@ -432,7 +437,7 @@ | needsExistentials (map fst (fst ins)) = error "SBV->C: Cannot compile functions with existentially quantified variables." | True- = [pre, header, post]+ = ([pre, header, post], flagsNeeded) where asserts | cgIgnoreAsserts cfg = [] | True = origAsserts @@ -462,6 +467,10 @@ assignments = F.toList asgns + -- Do we need any linker flags for C?+ flagsNeeded = nub $ concatMap (getLDFlag . opRes) assignments+ where opRes (sw, SBVApp o _) = (o, kindOf sw)+ codeSeg (fnm, ls) = text "/* User specified custom code for" <+> doubleQuotes (text fnm) <+> text "*/" $$ vcat (map text ls) $$ text ""@@ -687,6 +696,7 @@ p (Label s) [a] = a <+> text "/*" <+> text s <+> text "*/" p (IEEEFP w) as = handleIEEE w consts (zip opArgs as) var p (PseudoBoolean pb) as = handlePB pb as+ p (OverflowOp o) _ = tbd $ "Overflow operations" ++ show o p (KindCast _ to) [a] = parens (text (show to)) <+> a p (Uninterpreted s) [] = text "/* Uninterpreted constant */" <+> text s p (Uninterpreted s) as = text "/* Uninterpreted function */" <+> text s P.<> parens (fsep (punctuate comma as))@@ -949,5 +959,32 @@ ptag = "printf(\"" ++ tag ++ "\\n\");" lsep = replicate (length tag) '=' psep = "printf(\"" ++ lsep ++ "\\n\");"++-- Does this operation with this result kind require an LD flag?+getLDFlag :: (Op, Kind) -> [String]+getLDFlag (o, k) = flag o+ where math = ["-lm"]++ flag (IEEEFP FP_Cast{}) = math+ flag (IEEEFP fop) | fop `elem` requiresMath = math+ flag Abs | k `elem` [KFloat, KDouble, KReal] = math+ flag _ = []++ requiresMath = [ FP_Abs+ , FP_FMA+ , FP_Sqrt+ , FP_Rem+ , FP_Min+ , FP_Max+ , FP_RoundToIntegral+ , FP_ObjEqual+ , FP_IsSubnormal+ , FP_IsInfinite+ , FP_IsNaN+ , FP_IsNegative+ , FP_IsPositive+ , FP_IsNormal+ , FP_IsZero+ ] {-# ANN module ("HLint: ignore Redundant lambda" :: String) #-}
Data/SBV/Compilers/CodeGen.hs view
@@ -295,7 +295,7 @@ data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] -- | Different kinds of "files" we can produce. Currently this is quite "C" specific.-data CgPgmKind = CgMakefile [String]+data CgPgmKind = CgMakefile [String] -- list of flags to pass to linker | CgHeader [Doc] | CgSource | CgDriver
Data/SBV/Control.hs view
@@ -40,7 +40,7 @@ , getAssertions -- * Getting solver information- , SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..)+ , SMTInfoFlag(..), SMTErrorBehavior(..), SMTInfoResponse(..) , getInfo, getOption -- * Entering and exiting assertion stack@@ -69,15 +69,11 @@ -- * Solver options , SMTOption(..)-- -- * Logics supported- , Logic(..)- ) where import Data.SBV.Core.Data (SMTProblem(..), SMTSolver(..), SMTConfig(..)) import Data.SBV.Core.Symbolic ( Query, IStage(..), SBVRunMode(..), Symbolic, Query(..), rSMTOptions- , extractSymbolicSimulationState, solverSetOptions, runMode+ , extractSymbolicSimulationState, solverSetOptions, runMode, isRunIStage ) import Data.SBV.Control.Query@@ -96,12 +92,14 @@ rm <- liftIO $ readIORef (runMode st) case rm of -- Transitioning from setup- SMTMode ISetup isSAT cfg -> liftIO $ do let backend = engine (solver cfg)+ SMTMode stage isSAT cfg | not (isRunIStage stage) -> liftIO $ do + let backend = engine (solver cfg)+ res <- extractSymbolicSimulationState st setOpts <- reverse <$> readIORef (rSMTOptions st) - let SMTProblem{smtLibPgm} = runProofOn cfg isSAT [] res+ let SMTProblem{smtLibPgm} = runProofOn rm [] res cfg' = cfg { solverSetOptions = solverSetOptions cfg ++ setOpts } pgm = smtLibPgm cfg'
Data/SBV/Control/Query.hs view
@@ -38,6 +38,7 @@ import qualified Data.Map as M import qualified Data.IntMap as IM +import Data.Char (toLower) import Data.List (unzip3, intercalate, nubBy, sortBy) import Data.Maybe (listToMaybe, catMaybes) import Data.Function (on)@@ -110,8 +111,6 @@ isAllStat = isAllStatistics flag - render = serialize True- grabAllStat k v = (render k, render v) -- we're trying to do our best to get key-value pairs here, but this@@ -134,13 +133,25 @@ EApp [ECon ":error-behavior", ECon "immediate-exit"] -> return $ Resp_Error ErrorImmediateExit EApp [ECon ":error-behavior", ECon "continued-execution"] -> return $ Resp_Error ErrorContinuedExecution EApp (ECon ":name" : o) -> return $ Resp_Name (render (EApp o))- EApp [ECon ":reason-unknown", ECon "memout"] -> return $ Resp_ReasonUnknown UnknownMemOut- EApp [ECon ":reason-unknown", ECon "incomplete"] -> return $ Resp_ReasonUnknown UnknownIncomplete- EApp (ECon ":reason-unknown" : o) -> return $ Resp_ReasonUnknown (UnknownOther (render (EApp o)))+ EApp (ECon ":reason-unknown" : o) -> return $ Resp_ReasonUnknown (unk o) EApp (ECon ":version" : o) -> return $ Resp_Version (render (EApp o)) EApp (ECon s : o) -> return $ Resp_InfoKeyword s (map render o) _ -> bad r Nothing + where render = serialize True++ unk [ECon s] | Just d <- getUR s = d+ unk o = UnknownOther (render (EApp o))++ getUR s = map toLower (unQuote s) `lookup` [(map toLower k, d) | (k, d) <- unknownReasons]++ -- As specified in Section 4.1 of the SMTLib document. Note that we're adding the+ -- extra timeout as it is useful in this context.+ unknownReasons = [ ("memout", UnknownMemOut)+ , ("incomplete", UnknownIncomplete)+ , ("timeout", UnknownTimeOut)+ ]+ -- | Retrieve the value of an 'SMTOption.' The curious function argument is on purpose here, -- simply pass the constructor name. Example: the call @'getOption' 'ProduceUnsatCores'@ will return -- either @Nothing@ or @Just (ProduceUnsatCores True)@ or @Just (ProduceUnsatCores False)@.@@ -186,16 +197,13 @@ stringList c e _ = return $ Just $ c $ stringsOf e -- | Get the reason unknown. Only internally used.-getUnknownReason :: Query String+getUnknownReason :: Query SMTReasonUnknown getUnknownReason = do ru <- getInfo ReasonUnknown case ru of- Resp_Unsupported -> return "No reason provided."- Resp_ReasonUnknown r -> return $ case r of- UnknownMemOut -> "Out of memory."- UnknownIncomplete -> "Incomplete."- UnknownOther s -> s+ Resp_Unsupported -> return $ UnknownOther "Solver responded: Unsupported."+ Resp_ReasonUnknown r -> return r -- Shouldn't happen, but just in case:- _ -> return $ "Unexpected reason value received: " ++ show ru+ _ -> error $ "Unexpected reason value received: " ++ show ru -- | Issue check-sat and get an SMT Result out. getSMTResult :: Query SMTResult@@ -254,7 +262,7 @@ Unsat -> return (False, []) Sat -> continue (classifyModel cfg) Unk -> do ur <- getUnknownReason- return (False, [ProofError cfg [ur]])+ return (False, [ProofError cfg [show ur]]) where continue classify = do m <- getModel (limReached, fronts) <- getParetoFronts (subtract 1 <$> mbN) [m]@@ -623,13 +631,13 @@ -- result of parsing is ignored. parse r bad $ \_ -> return r --- | Retrieve interpolants after an 'Unsat' result is obtained. Note you must have arranged for+-- | Retrieve an interpolant after an 'Unsat' result is obtained. Note you must have arranged for -- interpolants to be produced first (/via/ @'setOption' $ 'ProduceInterpolants' 'True'@) -- for this call to not error out! ----- To get an interpolant for a pair of formulas @A@ and @B@, use a 'namedConstraint' to attach--- names to @A@ and @B@. Then call 'getInterpolant' @[\"A\", \"B\"]@, assuming those are the names--- you gave to the formulas.+-- To get an interpolant for a pair of formulas @A@ and @B@, use a 'constrainWithAttribute' call to attach+-- interplation groups to @A@ and @B@. Then call 'getInterpolant' @[\"A\"]@, assuming those are the names+-- you gave to the formulas in the @A@ group. -- -- An interpolant for @A@ and @B@ is a formula @I@ such that: --@@ -643,35 +651,28 @@ -- be satisfied at the same time. Furthermore, @I@ will have only the symbols that are common -- to @A@ and @B@. ----- Interpolants generalize to sequences: If you pass more than two formulas, then you will get--- a sequence of interpolants. In general, for @N@ formulas that are not satisfiable together, you will be--- returned @N-1@ interpolants. If formulas are @A1 .. An@, then interpolants will be @I1 .. I(N-1)@, such--- that @A1 ==> I1@, @A2 /\\ I1 ==> I2@, @A3 /\\ I2 ==> I3@, ..., and finally @AN ===> not I(N-1)@.------ Currently, SBV only returns simple and sequence interpolants, and does not support tree-interpolants.--- If you need these, please get in touch. Furthermore, the result will be a list of mere strings representing the--- interpolating formulas, as opposed to a more structured type. Please get in touch if you use this function and can--- suggest a better API.-getInterpolant :: [String] -> Query [String]+-- N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. Use the MathSAT backend for extracting+-- interpolants. See 'Documentation.SBV.Examples.Queries.Interpolants' for an example.+getInterpolant :: [String] -> Query String getInterpolant fs- | length fs < 2- = error $ "SBV.getInterpolant requires at least two named constraints, received: " ++ show fs+ | null fs+ = error "SBV.getInterpolant requires at least one marked constraint, received none!" | True = do let bar s = '|' : s ++ "|"- cmd = "(get-interpolant " ++ unwords (map bar fs) ++ ")"+ cmd = "(get-interpolant (" ++ unwords (map bar fs) ++ "))" bad = unexpected "getInterpolant" cmd "a get-interpolant response" $ Just [ "Make sure you use:" , "" , " setOption $ ProduceInterpolants True" , "" , "to make sure the solver is ready for producing interpolants,"- , "and that you have named the formulas with calls to 'namedConstraint'."+ , "and that you have used the proper attributes using the"+ , "constrainWithAttribute function." ] r <- ask cmd - parse r bad $ \case EApp (ECon "interpolants" : es) -> return $ map (serialize False) es- _ -> bad r Nothing+ parse r bad $ \e -> return $ serialize False e -- | Retrieve assertions. Note you must have arranged for -- assertions to be available first (/via/ @'setOption' $ 'ProduceAssertions' 'True'@)
Data/SBV/Control/Types.hs view
@@ -51,8 +51,16 @@ -- | Reason for reporting unknown. data SMTReasonUnknown = UnknownMemOut | UnknownIncomplete+ | UnknownTimeOut | UnknownOther String- deriving Show+ deriving (Generic, NFData)++-- | Show instance for unknown+instance Show SMTReasonUnknown where+ show UnknownMemOut = "memout"+ show UnknownIncomplete = "incomplete"+ show UnknownTimeOut = "timeout"+ show (UnknownOther s) = s -- | Collectable information from the solver. data SMTInfoResponse = Resp_Unsupported
Data/SBV/Control/Utils.hs view
@@ -60,15 +60,15 @@ , QueryState(..), SVal(..), Quantifier(..), cache , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..) , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities- , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..), SMTSolver(..)+ , Result(..), SMTProblem(..), trueSW, SymWord(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..) )-import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar)+import Data.SBV.Core.Symbolic (IncState(..), withNewIncState, State(..), svToSW, registerLabel, svMkSymVar, isSafetyCheckingIStage, isSetupIStage) import Data.SBV.Core.AlgReals (mergeAlgReals) import Data.SBV.Core.Operations (svNot, svNotEqual, svOr) import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib)-import Data.SBV.SMT.Utils (showTimeoutValue, annotateWithName, alignPlain, debug, mergeSExpr, SMTException(..))+import Data.SBV.SMT.Utils (showTimeoutValue, addAnnotations, alignPlain, debug, mergeSExpr, SMTException(..)) import Data.SBV.Utils.Lib (qfsToString) @@ -83,8 +83,9 @@ -- | 'Query' as a 'SolverContext'. instance SolverContext Query where- constrain = addQueryConstraint Nothing- namedConstraint nm = addQueryConstraint (Just nm)+ constrain = addQueryConstraint []+ namedConstraint nm = addQueryConstraint [(":named", nm)]+ constrainWithAttribute = addQueryConstraint setOption o | isStartModeOption o = error $ unlines [ ""@@ -93,15 +94,12 @@ ] | True = send True $ setSMTOption o --- | Adding a constraint, possibly named. Only used internally.+-- | Adding a constraint, possibly with attributes. Only used internally. -- Use 'constrain' and 'namedConstraint' from user programs.-addQueryConstraint :: Maybe String -> SBool -> Query ()-addQueryConstraint mbNm b = do sw <- inNewContext (\st -> do maybe (return ()) (registerLabel st) mbNm+addQueryConstraint :: [(String, String)] -> SBool -> Query ()+addQueryConstraint atts b = do sw <- inNewContext (\st -> do mapM_ (registerLabel st) [nm | (":named", nm) <- atts] sbvToSW st b)- send True $ "(assert " ++ mkNamed mbNm (show sw) ++ ")"- where mkNamed Nothing s = s- mkNamed (Just nm) s = annotateWithName nm s-+ send True $ "(assert " ++ addAnnotations atts (show sw) ++ ")" -- | Get the current configuration getConfig :: Query SMTConfig@@ -131,12 +129,11 @@ syncUpSolver afterAPush is = do cfg <- getConfig ls <- io $ do let swap (a, b) = (b, a)- swapc ((_, a), b) = (b, a) cmp (a, _) (b, _) = a `compare` b arrange (i, (at, rt, es)) = ((i, at, rt), es) inps <- reverse <$> readIORef (rNewInps is) ks <- readIORef (rNewKinds is)- cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rNewConsts is)+ cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rNewConsts is) arrs <- IMap.toAscList <$> readIORef (rNewArrs is) tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is) uis <- Map.toAscList <$> readIORef (rNewUIs is)@@ -680,9 +677,13 @@ io $ C.throwIO exc -- | Convert a query result to an SMT Problem-runProofOn :: SMTConfig -> Bool -> [String] -> Result -> SMTProblem-runProofOn config isSat comments res@(Result ki _qcInfo _observables _codeSegs is consts tbls arrs uis axs pgm cstrs _assertions outputs) =- let flipQ (ALL, x) = (EX, x)+runProofOn :: SBVRunMode -> [String] -> Result -> SMTProblem+runProofOn rm comments res@(Result ki _qcInfo _observables _codeSegs is consts tbls arrs uis axs pgm cstrs _assertions outputs) =+ let (config, isSat, isSafe, isSetup) = case rm of+ SMTMode stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)+ _ -> error $ "runProofOn: Unexpected run mode: " ++ show rm++ flipQ (ALL, x) = (EX, x) flipQ (EX, x) = (ALL, x) skolemize :: [(Quantifier, NamedSymVar)] -> [Either SW (SW, [SW])]@@ -694,23 +695,18 @@ qinps = if isSat then fst is else map flipQ (fst is) skolemMap = skolemize qinps - o = case outputs of- [] -> trueSW- [so] -> case so of- SW KBool _ -> so- _ -> trueSW- {-- -- TODO: We used to error out here, but "safeWith" might have a non-bool out- -- I wish we can get rid of this and still check for it. Perhaps this entire- -- runProofOn might disappear.- error $ unlines [ "Impossible happened, non-boolean output: " ++ show so- , "Detected while generating the trace:\n" ++ show res- ]- -}- os -> error $ unlines [ "User error: Multiple output values detected: " ++ show os- , "Detected while generating the trace:\n" ++ show res- , "*** Check calls to \"output\", they are typically not needed!"- ]+ o | isSafe = trueSW+ | True = case outputs of+ [] | isSetup -> trueSW+ [so] -> case so of+ SW KBool _ -> so+ _ -> error $ unlines [ "Impossible happened, non-boolean output: " ++ show so+ , "Detected while generating the trace:\n" ++ show res+ ]+ os -> error $ unlines [ "User error: Multiple output values detected: " ++ show os+ , "Detected while generating the trace:\n" ++ show res+ , "*** Check calls to \"output\", they are typically not needed!"+ ] in SMTProblem { smtLibPgm = toSMTLib config ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o }
Data/SBV/Core/Concrete.hs view
@@ -24,6 +24,8 @@ import Data.SBV.Core.Kind import Data.SBV.Core.AlgReals +import Data.SBV.Utils.Numeric (fpIsEqualObjectH, fpCompareObjectH)+ -- | A constant value data CWVal = CWAlgReal !AlgReal -- ^ algebraic real | CWInteger !Integer -- ^ bit-vector/unbounded integer@@ -37,14 +39,14 @@ -- instances for these when values are infinitely precise reals. However, we do -- need a structural eq/ord for Map indexes; so define custom ones here: instance Eq CWVal where- CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b- CWInteger a == CWInteger b = a == b- CWUserSort a == CWUserSort b = a == b- CWFloat a == CWFloat b = a == b- CWDouble a == CWDouble b = a == b- CWChar a == CWChar b = a == b- CWString a == CWString b = a == b- _ == _ = False+ CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b+ CWInteger a == CWInteger b = a == b+ CWUserSort a == CWUserSort b = a == b+ CWFloat a == CWFloat b = a `fpIsEqualObjectH` b -- We don't want +0/-0 to be confused; and also we want NaN = NaN here!+ CWDouble a == CWDouble b = a `fpIsEqualObjectH` b -- ditto+ CWChar a == CWChar b = a == b+ CWString a == CWString b = a == b+ _ == _ = False -- | Ord instance for CWVal. Same comments as the 'Eq' instance why this cannot be derived. instance Ord CWVal where@@ -66,7 +68,7 @@ CWFloat _ `compare` CWAlgReal _ = GT CWFloat _ `compare` CWInteger _ = GT- CWFloat a `compare` CWFloat b = a `compare` b+ CWFloat a `compare` CWFloat b = a `fpCompareObjectH` b CWFloat _ `compare` CWDouble _ = LT CWFloat _ `compare` CWChar _ = LT CWFloat _ `compare` CWString _ = LT@@ -75,7 +77,7 @@ CWDouble _ `compare` CWAlgReal _ = GT CWDouble _ `compare` CWInteger _ = GT CWDouble _ `compare` CWFloat _ = GT- CWDouble a `compare` CWDouble b = a `compare` b+ CWDouble a `compare` CWDouble b = a `fpCompareObjectH` b CWDouble _ `compare` CWChar _ = LT CWDouble _ `compare` CWString _ = LT CWDouble _ `compare` CWUserSort _ = LT
Data/SBV/Core/Data.hs view
@@ -264,6 +264,8 @@ constrain :: SBool -> m () -- | Add a named constraint. The name is used in unsat-core extraction. namedConstraint :: String -> SBool -> m ()+ -- | Add a constraint, with arbitrary attributes. Used in interpolant generation.+ constrainWithAttribute :: [(String, String)] -> SBool -> m () -- | Set info. Example: @setInfo ":status" ["unsat"]@. setInfo :: String -> [String] -> m () -- | Set an option.
Data/SBV/Core/Floating.hs view
@@ -389,7 +389,7 @@ newExpr st w32 (SBVApp (IEEEFP (FP_Reinterpret KFloat w32)) [f]) else do n <- internalVariable st w32 ysw <- newExpr st KFloat (SBVApp (IEEEFP (FP_Reinterpret w32 KFloat)) [n])- internalConstraint st Nothing $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KFloat (Right (cache (\_ -> return ysw))))+ internalConstraint st [] $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KFloat (Right (cache (\_ -> return ysw)))) return n -- | Convert an 'SDouble' to an 'SWord64', preserving the bit-correspondence. Note that since the@@ -410,7 +410,7 @@ newExpr st w64 (SBVApp (IEEEFP (FP_Reinterpret KDouble w64)) [f]) else do n <- internalVariable st w64 ysw <- newExpr st KDouble (SBVApp (IEEEFP (FP_Reinterpret w64 KDouble)) [n])- internalConstraint st Nothing $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KDouble (Right (cache (\_ -> return ysw))))+ internalConstraint st [] $ unSBV $ fVal `fpIsEqualObject` SBV (SVal KDouble (Right (cache (\_ -> return ysw)))) return n -- | Extract the sign\/exponent\/mantissa of a single-precision float. The output will have
Data/SBV/Core/Model.hs view
@@ -1779,9 +1779,11 @@ -- | Symbolic computations provide a context for writing symbolic programs. instance SolverContext Symbolic where- constrain (SBV c) = imposeConstraint Nothing c- namedConstraint nm (SBV c) = imposeConstraint (Just nm) c- setOption o = addNewSMTOption o+ constrain (SBV c) = imposeConstraint [] c+ namedConstraint nm (SBV c) = imposeConstraint [(":named", nm)] c+ constrainWithAttribute atts (SBV c) = imposeConstraint atts c++ setOption o = addNewSMTOption o -- | Introduce a soft assertion, with an optional penalty assertSoft :: String -> SBool -> Penalty -> Symbolic ()
Data/SBV/Core/Operations.hs view
@@ -31,6 +31,8 @@ , svSelect , svSign, svUnsign, svSetBit, svWordFromBE, svWordFromLE , svExp, svFromIntegral+ -- ** Overflows+ , svMkOverflow -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight@@ -49,7 +51,6 @@ import Data.SBV.Core.Kind import Data.SBV.Core.Concrete import Data.SBV.Core.Symbolic-import Data.SBV.Utils.Numeric (fpIsEqualObjectH) import Data.Ratio @@ -487,13 +488,8 @@ = a | True = SVal k $ Right $ cache c- where- -- Be careful with +/-0 here! See https://github.com/LeventErkok/sbv/issues/382- sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2 && floatCheck (cwVal c1) (cwVal c2)- sameResult _ _ = False- floatCheck (CWFloat f1) (CWFloat f2) = f1 `fpIsEqualObjectH` f2- floatCheck (CWDouble d1) (CWDouble d2) = d1 `fpIsEqualObjectH` d2- floatCheck _ _ = True+ where sameResult (SVal _ (Left c1)) (SVal _ (Left c2)) = c1 == c2+ sameResult _ _ = False c st = do swt <- svToSW st t case () of@@ -802,6 +798,14 @@ z = svInteger (kindOf x) 0 zi = svInteger (kindOf i) 0 n = svInteger (kindOf i) (toInteger sx)++--------------------------------------------------------------------------------+-- | Overflow detection.+svMkOverflow :: OvOp -> SVal -> SVal -> SVal+svMkOverflow o x y = SVal KBool (Right (cache r))+ where r st = do sx <- svToSW st x+ sy <- svToSW st y+ newExpr st KBool $ SBVApp (OverflowOp o) [sx, sy] -------------------------------------------------------------------------------- -- Utility functions
Data/SBV/Core/Symbolic.hs view
@@ -27,7 +27,7 @@ module Data.SBV.Core.Symbolic ( NodeId(..) , SW(..), swKind, trueSW, falseSW- , Op(..), PBOp(..), FPOp(..), StrOp(..), RegExp(..)+ , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), RegExp(..) , Quantifier(..), needsExistentials , RoundingMode(..) , SBVType(..), newUninterpreted, addAxiom@@ -35,7 +35,7 @@ , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_ , ArrayContext(..), ArrayInfo , svToSW, svToSymSW, forceSWArg- , SBVExpr(..), newExpr, isCodeGenMode+ , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage , Cached, cache, uncache , ArrayIndex, uncacheAI , NamedSymVar@@ -64,7 +64,7 @@ import Data.Char (isAlpha, isAlphaNum, toLower) import Data.IORef (IORef, newIORef, readIORef) import Data.List (intercalate, sortBy)-import Data.Maybe (isJust, fromJust, fromMaybe)+import Data.Maybe (isJust, fromJust, fromMaybe, listToMaybe) import Data.String (IsString(fromString)) import Data.Time (getCurrentTime, UTCTime)@@ -154,6 +154,7 @@ | Label String -- Essentially no-op; useful for code generation to emit comments. | IEEEFP FPOp -- Floating-point ops, categorized separately | PseudoBoolean PBOp -- Pseudo-boolean ops, categorized separately+ | OverflowOp OvOp -- Overflow-ops, categorized separately | StrOp StrOp -- String ops, categorized separately deriving (Eq, Ord) @@ -221,6 +222,18 @@ | PB_Eq [Int] Int -- ^ Exactly k, with coefficients given. Generalized PB_Exactly deriving (Eq, Ord, Show) +-- | Overflow operations+data OvOp = Overflow_SMul_OVFL -- ^ Signed multiplication overflow+ | Overflow_SMul_UDFL -- ^ Signed multiplication underflow+ | Overflow_UMul_OVFL -- ^ Unsigned multiplication overflow+ deriving (Eq, Ord)++-- | Show instance. It's important that these follow the internal z3 names+instance Show OvOp where+ show Overflow_SMul_OVFL = "bvsmul_noovfl"+ show Overflow_SMul_UDFL = "bvsmul_noudfl"+ show Overflow_UMul_OVFL = "bvumul_noovfl"+ -- | String operations. Note that we do not define `StrAt` as it translates to `StrSubStr` trivially. data StrOp = StrConcat -- ^ Concatenation of one or more strings | StrLen -- ^ String length@@ -339,6 +352,7 @@ show (Label s) = "[label] " ++ s show (IEEEFP w) = show w show (PseudoBoolean p) = show p+ show (OverflowOp o) = show o show (StrOp s) = show s show op | Just s <- op `lookup` syms = s@@ -392,6 +406,7 @@ show (SBVApp (Rol i) [a]) = unwords [show a, "<<<", show i] show (SBVApp (Ror i) [a]) = unwords [show a, ">>>", show i] show (SBVApp (PseudoBoolean pb) args) = unwords (show pb : map show args)+ show (SBVApp (OverflowOp op) args) = unwords (show op : map show args) show (SBVApp op [a, b]) = unwords [show a, show op, show b] show (SBVApp op args) = unwords (show op : map show args) @@ -406,7 +421,7 @@ -- potentially be an infinite number of them and there is no way to know exactly -- how many ahead of time. If 'Nothing' is given, SBV will possibly loop forever -- if the number is really infinite.-data OptimizeStyle = Lexicographic -- ^ Objectives are optimized in the order given, earlier objectives have higher priority. This is the default.+data OptimizeStyle = Lexicographic -- ^ Objectives are optimized in the order given, earlier objectives have higher priority. | Independent -- ^ Each objective is optimized independently. | Pareto (Maybe Int) -- ^ Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. deriving (Eq, Show)@@ -470,7 +485,7 @@ , resUIConsts :: [(String, SBVType)] -- ^ uninterpreted constants , resAxioms :: [(String, [String])] -- ^ axioms , resAsgns :: SBVPgm -- ^ assignments- , resConstraints :: [(Maybe String, SW)] -- ^ additional constraints (boolean)+ , resConstraints :: [([(String, String)], SW)] -- ^ additional constraints (boolean) , resAssertions :: [(String, Maybe CallStack, SW)] -- ^ assertions , resOutputs :: [SW] -- ^ outputs }@@ -540,8 +555,9 @@ shax (nm, ss) = " -- user defined axiom: " ++ nm ++ "\n " ++ intercalate "\n " ss - shCstr (Nothing, c) = show c- shCstr (Just nm, c) = nm ++ ": " ++ show c+ shCstr ([], c) = show c+ shCstr ([(":named", nm)], c) = nm ++ ": " ++ show c+ shCstr (attrs, c) = show c ++ " (attributes: " ++ show attrs ++ ")" shAssert (nm, stk, p) = " -- assertion: " ++ nm ++ " " ++ maybe "[No location]" #if MIN_VERSION_base(4,9,0)@@ -562,16 +578,16 @@ show (ArrayMerge s i j) = " merged arrays " ++ show i ++ " and " ++ show j ++ " on condition " ++ show s -- | Expression map, used for hash-consing-type ExprMap = Map.Map SBVExpr SW+type ExprMap = Map.Map SBVExpr SW --- | Constants are stored in a map, for hash-consing. The bool is needed to tell -0 from +0, sigh-type CnstMap = Map.Map (Bool, CW) SW+-- | Constants are stored in a map, for hash-consing.+type CnstMap = Map.Map CW SW -- | Kinds used in the program; used for determining the final SMT-Lib logic to pick type KindSet = Set.Set Kind -- | Tables generated during a symbolic run-type TableMap = Map.Map (Kind, Kind, [SW]) Int+type TableMap = Map.Map (Kind, Kind, [SW]) Int -- | Representation for symbolic arrays type ArrayInfo = (String, (Kind, Kind), ArrayContext)@@ -589,9 +605,31 @@ type Cache a = IMap.IntMap [(StableName (State -> IO a), a)] -- | Stage of an interactive run-data IStage = ISetup -- Before we initiate contact- | IRun -- After the contact is started+data IStage = ISetup -- Before we initiate contact.+ | ISafe -- In the context of a safe/safeWith call+ | IRun -- After the contact is started +-- | Are we cecking safety+isSafetyCheckingIStage :: IStage -> Bool+isSafetyCheckingIStage s = case s of+ ISetup -> False+ ISafe -> True+ IRun -> False++-- | Are we in setup?+isSetupIStage :: IStage -> Bool+isSetupIStage s = case s of+ ISetup -> True+ ISafe -> False+ IRun -> True++-- | Are we in a run?+isRunIStage :: IStage -> Bool+isRunIStage s = case s of+ ISetup -> False+ ISafe -> False+ IRun -> True+ -- | Different means of running a symbolic piece of code data SBVRunMode = SMTMode IStage Bool SMTConfig -- ^ In regular mode, with a stage. Bool is True if this is SAT. | CodeGen -- ^ Code generation mode.@@ -600,8 +638,10 @@ -- Show instance for SBVRunMode; debugging purposes only instance Show SBVRunMode where show (SMTMode ISetup True _) = "Satisfiability setup"+ show (SMTMode ISafe True _) = "Safety setup" show (SMTMode IRun True _) = "Satisfiability" show (SMTMode ISetup False _) = "Proof setup"+ show (SMTMode ISafe False _) = error "ISafe-False is not an expected/supported combination for SBVRunMode!" show (SMTMode IRun False _) = "Proof" show CodeGen = "Code generation" show Concrete = "Concrete evaluation"@@ -665,7 +705,7 @@ , rUsedKinds :: IORef KindSet , rUsedLbls :: IORef (Set.Set String) , rinps :: IORef ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- User defined, and internal existential- , rConstraints :: IORef [(Maybe String, SW)]+ , rConstraints :: IORef [([(String, String)], SW)] , routs :: IORef [SW] , rtblMap :: IORef TableMap , spgm :: IORef SBVPgm@@ -856,24 +896,16 @@ else modifyState st rUsedLbls (Set.insert nm) (return ()) -- | Create a new constant; hash-cons as necessary--- NB. For each constant, we also store weather it's negative-0 or not,--- as otherwise +0 == -0 and thus we'd confuse those entries. That's a--- bummer as we incur an extra boolean for this rare case, but it's simple--- and hopefully we don't generate a ton of constants in general. newConst :: State -> CW -> IO SW newConst st c = do constMap <- readIORef (rconstMap st)- let key = (isNeg0 (cwVal c), c)- case key `Map.lookup` constMap of+ case c `Map.lookup` constMap of Just sw -> return sw Nothing -> do let k = kindOf c (sw, _) <- newSW st k- let ins = Map.insert key sw+ let ins = Map.insert c sw modifyState st rconstMap ins $ modifyIncState st rNewConsts ins return sw- where isNeg0 (CWFloat f) = isNegativeZero f- isNeg0 (CWDouble d) = isNegativeZero d- isNeg0 _ = False {-# INLINE newConst #-} -- | Create a new table; hash-cons as necessary@@ -1102,21 +1134,24 @@ SBVPgm rpgm <- readIORef pgm inpsO <- (reverse *** reverse) <$> readIORef inps outsO <- reverse <$> readIORef outs+ let swap (a, b) = (b, a)- swapc ((_, a), b) = (b, a) cmp (a, _) (b, _) = a `compare` b arrange (i, (at, rt, es)) = ((i, at, rt), es)- cnsts <- sortBy cmp . map swapc . Map.toList <$> readIORef (rconstMap st)++ cnsts <- sortBy cmp . map swap . Map.toList <$> readIORef (rconstMap st) tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef tables arrs <- IMap.toAscList <$> readIORef arrays unint <- Map.toList <$> readIORef uis axs <- reverse <$> readIORef axioms knds <- readIORef usedKinds cgMap <- Map.toList <$> readIORef cgs- traceVals <- reverse <$> readIORef cInfo++ traceVals <- reverse <$> readIORef cInfo observables <- reverse <$> readIORef observes- extraCstrs <- reverse <$> readIORef cstrs- assertions <- reverse <$> readIORef asserts+ extraCstrs <- reverse <$> readIORef cstrs+ assertions <- reverse <$> readIORef asserts+ return $ Result knds traceVals observables cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs assertions outsO -- | Add a new option@@ -1125,23 +1160,21 @@ liftIO $ modifyState st rSMTOptions (o:) (return ()) -- | Handling constraints-imposeConstraint :: Maybe String -> SVal -> Symbolic ()-imposeConstraint mbNm c = do st <- ask- rm <- liftIO $ readIORef (runMode st)- case rm of- CodeGen -> error "SBV: constraints are not allowed in code-generation"- _ -> do () <- case mbNm of- Nothing -> return ()- Just nm -> liftIO $ registerLabel st nm- liftIO $ internalConstraint st mbNm c+imposeConstraint :: [(String, String)] -> SVal -> Symbolic ()+imposeConstraint attrs c = do st <- ask+ rm <- liftIO $ readIORef (runMode st)+ case rm of+ CodeGen -> error "SBV: constraints are not allowed in code-generation"+ _ -> liftIO $ do mapM_ (registerLabel st) [nm | (":named", nm) <- attrs]+ internalConstraint st attrs c -- | Require a boolean condition to be true in the state. Only used for internal purposes.-internalConstraint :: State -> Maybe String -> SVal -> IO ()-internalConstraint st mbNm b = do v <- svToSW st b- modifyState st rConstraints ((mbNm, v):)- $ noInteractive [ "Adding an internal constraint:"- , " Named: " ++ fromMaybe "<unnamed>" mbNm- ]+internalConstraint :: State -> [(String, String)] -> SVal -> IO ()+internalConstraint st attrs b = do v <- svToSW st b+ modifyState st rConstraints ((attrs, v):)+ $ noInteractive [ "Adding an internal constraint:"+ , " Named: " ++ fromMaybe "<unnamed>" (listToMaybe [nm | (":named", nm) <- attrs])+ ] -- | Add an optimization goal addSValOptGoal :: Objective SVal -> Symbolic ()@@ -1439,7 +1472,7 @@ data SMTResult = Unsatisfiable SMTConfig (Maybe [String]) -- ^ Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter. | Satisfiable SMTConfig SMTModel -- ^ Satisfiable with model | SatExtField SMTConfig SMTModel -- ^ Prover returned a model, but in an extension field containing Infinite/epsilon- | Unknown SMTConfig String -- ^ Prover returned unknown, with the given reason+ | Unknown SMTConfig SMTReasonUnknown -- ^ Prover returned unknown, with the given reason | ProofError SMTConfig [String] -- ^ Prover errored out -- | A script, to be passed to the solver.@@ -1476,3 +1509,4 @@ {-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-} {-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}+{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}
Data/SBV/Provers/Prover.hs view
@@ -378,7 +378,7 @@ (_, res) <- runSymbolic (SMTMode ISetup isSat cfg) $ (if isSat then forSome_ else forAll_) a >>= output - let SMTProblem{smtLibPgm} = Control.runProofOn cfg isSat comments res+ let SMTProblem{smtLibPgm} = Control.runProofOn (SMTMode IRun isSat cfg) comments res out = show (smtLibPgm cfg) return $ out ++ "\n(check-sat)\n"@@ -559,7 +559,7 @@ let mkRelative path | cwd `isPrefixOf` path = drop (length cwd) path | True = path- fst <$> runSymbolic (SMTMode ISetup True cfg) (sName_ a >> check mkRelative)+ fst <$> runSymbolic (SMTMode ISafe True cfg) (sName_ a >> check mkRelative) where check mkRelative = Control.query $ Control.getSBVAssertions >>= mapM (verify mkRelative) -- check that the cond is unsatisfiable. If satisfiable, that would
Data/SBV/SMT/SMT.hs view
@@ -156,8 +156,8 @@ ParetoResult (False, [r]) -> sh (\s -> "Unique pareto front: " ++ s) r ParetoResult (False, rs) -> multi "pareto optimal values" (zipWith shP [(1::Int)..] rs) ParetoResult (True, rs) -> multi "pareto optimal values" (zipWith shP [(1::Int)..] rs)- ++ "\n*** Note: Pareto-front extraction was terminated before stream was ended as requested by the user."- ++ "\n*** There might be other (potentially infinitely more) results."+ ++ "\n*** Note: Pareto-front extraction was terminated as requested by the user."+ ++ "\n*** There might be many other results!" where multi w [] = "There are no " ++ w ++ " to display models for." multi _ xs = intercalate "\n" xs@@ -385,7 +385,7 @@ getModelAssignment (Unsatisfiable _ _) = Left "SBV.getModelAssignment: Unsatisfiable result" getModelAssignment (Satisfiable _ m) = Right (False, parseModelOut m) getModelAssignment (SatExtField _ _) = Left "SBV.getModelAssignment: The model is in an extension field"- getModelAssignment (Unknown _ m) = Left $ "SBV.getModelAssignment: Solver state is unknown: " ++ m+ getModelAssignment (Unknown _ m) = Left $ "SBV.getModelAssignment: Solver state is unknown: " ++ show m getModelAssignment (ProofError _ s) = error $ unlines $ "Backend solver complains: " : s modelExists Satisfiable{} = True@@ -428,7 +428,7 @@ Satisfiable _ (SMTModel _ []) -> satMsg Satisfiable _ m -> satMsgModel ++ showModel cfg m SatExtField _ (SMTModel b _) -> satExtMsg ++ showModelDictionary cfg b- Unknown _ r -> unkMsg ++ ".\n" ++ " Reason: " `alignPlain` r+ Unknown _ r -> unkMsg ++ ".\n" ++ " Reason: " `alignPlain` show r ProofError _ [] -> "*** An error occurred. No additional information available. Try running in verbose mode" ProofError _ ls -> "*** An error occurred.\n" ++ intercalate "\n" (map ("*** " ++) ls) where cfg = resultConfig result
Data/SBV/SMT/SMTLib2.hs view
@@ -14,6 +14,7 @@ import Data.Bits (bit) import Data.List (intercalate, partition, unzip3)+import Data.Maybe (listToMaybe, fromMaybe) import qualified Data.Foldable as F (toList) import qualified Data.Map as M@@ -168,15 +169,16 @@ finalAssert | null foralls- = map (\a -> "(assert " ++ named a ++ ")") assertions+ = map (\a -> "(assert " ++ uncurry addAnnotations a ++ ")") assertions | not (null namedAsserts)- = error $ intercalate "\n" [ "SBV: Named constraints and quantifiers cannot be mixed!"+ = error $ intercalate "\n" [ "SBV: Constraints with attributes and quantifiers cannot be mixed!" , " Quantified variables: " ++ unwords (map show foralls) , " Named constraints : " ++ intercalate ", " (map show namedAsserts) ] | True = [impAlign (letShift combined) ++ replicate noOfCloseParens ')']- where namedAsserts = [n | (Just n, _) <- assertions]+ where namedAsserts = [findName attrs | (attrs, _) <- assertions, not (null attrs)]+ where findName attrs = fromMaybe "<anonymous>" (listToMaybe [nm | (":named", nm) <- attrs]) combined = case map snd assertions of [x] -> x@@ -202,12 +204,12 @@ -- -- negation of the output in a prove -- -- output itself in a sat assertions- | null finals = [(Nothing, cvtSW skolemMap trueSW)]+ | null finals = [([], cvtSW skolemMap trueSW)] | True = finals - where finals = cstrs' ++ maybe [] (\r -> [(Nothing, r)]) mbO+ where finals = cstrs' ++ maybe [] (\r -> [([], r)]) mbO - cstrs' = [(mbNm, c') | (mbNm, c) <- cstrs, Just c' <- [pos c]]+ cstrs' = [(attrs, c') | (attrs, c) <- cstrs, Just c' <- [pos c]] mbO | isSat = pos out | True = neg out@@ -606,7 +608,7 @@ , (Join, lift2 "concat") ] - sh (SBVApp (Label m) [a]) = curry named (Just m) $ cvtSW skolemMap a -- This won't be reached; but just in case!+ sh (SBVApp (Label _) [a]) = cvtSW skolemMap a -- This won't be reached; but just in case! sh (SBVApp (IEEEFP (FP_Cast kFrom kTo m)) args) = handleFPCast kFrom kTo (ssw m) (unwords (map ssw args)) sh (SBVApp (IEEEFP w ) args) = "(" ++ show w ++ " " ++ unwords (map ssw args) ++ ")"@@ -616,6 +618,9 @@ | True = reducePB pb args' where args' = map ssw args + -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not.+ sh (SBVApp (OverflowOp op) args) = "(not (" ++ show op ++ " " ++ unwords (map ssw args) ++ "))"+ -- Note the unfortunate reversal in StrInRe.. sh (SBVApp (StrOp (StrInRe r)) args) = "(str.in.re " ++ unwords (map ssw args) ++ " " ++ show r ++ ")" sh (SBVApp (StrOp op) args) = "(" ++ show op ++ " " ++ unwords (map ssw args) ++ ")"@@ -865,8 +870,3 @@ where addIf :: [Int] -> String addIf cs = "(+ " ++ unwords ["(ite " ++ a ++ " " ++ show c ++ " 0)" | (a, c) <- zip args cs] ++ ")"---- Add a named annotation-named :: (Maybe String, String) -> String-named (Nothing, x) = x-named (Just nm, x) = annotateWithName nm x
Data/SBV/SMT/Utils.hs view
@@ -14,7 +14,7 @@ module Data.SBV.SMT.Utils ( SMTLibConverter , SMTLibIncConverter- , annotateWithName+ , addAnnotations , showTimeoutValue , alignDiagnostic , alignPlain@@ -46,7 +46,7 @@ -> [(String, SBVType)] -- ^ uninterpreted functions/constants -> [(String, [String])] -- ^ user given axioms -> SBVPgm -- ^ assignments- -> [(Maybe String, SW)] -- ^ extra constraints+ -> [([(String, String)], SW)] -- ^ extra constraints -> SW -- ^ output variable -> SMTConfig -- ^ configuration -> a@@ -62,10 +62,12 @@ -> SMTConfig -- ^ configuration -> a --- | Create an annotated term with the given name-annotateWithName :: String -> String -> String-annotateWithName nm x = "(! " ++ x ++ " :named |" ++ concatMap sanitize nm ++ "|)"- where sanitize '|' = "_bar_"+-- | Create an annotated term+addAnnotations :: [(String, String)] -> String -> String+addAnnotations [] x = x+addAnnotations atts x = "(! " ++ x ++ " " ++ unwords (map mkAttr atts) ++ ")"+ where mkAttr (a, v) = a ++ " |" ++ concatMap sanitize v ++ "|"+ sanitize '|' = "_bar_" sanitize '\\' = "_backslash_" sanitize c = [c]
Data/SBV/String.hs view
@@ -138,7 +138,7 @@ y si st = do c <- internalVariable st w8 cs <- newExpr st KString (SBVApp (StrOp StrUnit) [c]) let csSBV = SBV (SVal KString (Right (cache (\_ -> return cs))))- internalConstraint st Nothing $ unSBV $ csSBV .== si+ internalConstraint st [] $ unSBV $ csSBV .== si return c -- | Short cut for 'strToCharAt'
+ Data/SBV/Tools/Overflow.hs view
@@ -0,0 +1,399 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Tools.Overflow+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Implementation of overflow detection functions.+-- Based on: <http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf>+-----------------------------------------------------------------------------++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Data.SBV.Tools.Overflow (++ -- * Arithmetic overflows+ ArithOverflow(..)++ -- * Cast overflows+ , sFromIntegralO++ ) where++import Data.SBV.Core.Data+import Data.SBV.Core.Symbolic+import Data.SBV.Core.Model+import Data.SBV.Core.Operations+import Data.SBV.Utils.Boolean++-- Doctest only+-- $setup+-- >>> import Data.SBV.Provers.Prover (prove, allSat)+-- >>> import Data.SBV.Utils.Boolean ((<=>))++-- | Detecting underflow/overflow conditions. For each function,+-- the first result is the condition under which the computation+-- underflows, and the second is the condition under which it+-- overflows.+class ArithOverflow a where+ -- | Bit-vector addition. Unsigned addition can only overflow. Signed addition can underflow and overflow.+ --+ -- A tell tale sign of unsigned addition overflow is when the sum is less than minumum of the arguments.+ --+ -- >>> prove $ \x y -> snd (bvAddO x (y::SWord16)) <=> x + y .< x `smin` y+ -- Q.E.D.+ bvAddO :: a -> a -> (SBool, SBool)++ -- | Bit-vector subtraction. Unsigned subtraction can only underflow. Signed subtraction can underflow and overflow.+ bvSubO :: a -> a -> (SBool, SBool)++ -- | Bit-vector multiplication. Unsigned multiplication can only overflow. Signed multiplication can underflow and overflow.+ bvMulO :: a -> a -> (SBool, SBool)++ -- | Same as 'bvMulO', except instead of doing the computation internally, it simply sends it off to z3 as a primitive.+ -- Obviously, only use if you have the z3 backend! Note that z3 provides this operation only when no logic is set,+ -- so make sure to call @setLogic Logic_NONE@ in your program!+ bvMulOFast :: a -> a -> (SBool, SBool)++ -- | Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each+ -- signed bitvector type, there's precisely one pair that overflows, when @x@ is @minBound@ and @y@ is @-1@:+ --+ -- >>> allSat $ \x y -> snd (x `bvDivO` (y::SInt8))+ -- Solution #1:+ -- s0 = -128 :: Int8+ -- s1 = -1 :: Int8+ -- This is the only solution.++ bvDivO :: a -> a -> (SBool, SBool)++ -- | Bit-vector negation. Unsigned negation neither underflows nor overflows. Signed negation can only overflow, when the argument is+ -- @minBound@:+ --+ -- >>> prove $ \x -> x .== minBound <=> snd (bvNegO (x::SInt16))+ -- Q.E.D.+ bvNegO :: a -> (SBool, SBool)++instance ArithOverflow SWord8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SWord16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SWord32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SWord64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SInt8 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SInt16 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SInt32 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}+instance ArithOverflow SInt64 where {bvAddO = l2 bvAddO; bvSubO = l2 bvSubO; bvMulO = l2 bvMulO; bvMulOFast = l2 bvMulOFast; bvDivO = l2 bvDivO; bvNegO = l1 bvNegO}++instance ArithOverflow SVal where+ bvAddO = signPick2 bvuaddo bvsaddo+ bvSubO = signPick2 bvusubo bvssubo+ bvMulO = signPick2 bvumulo bvsmulo+ bvMulOFast = signPick2 bvumuloFast bvsmuloFast+ bvDivO = signPick2 bvudivo bvsdivo+ bvNegO = signPick1 bvunego bvsnego++-- | Zero-extend to given bits+zx :: Int -> SVal -> SVal+zx n a+ | n < sa = error $ "Data.SBV: Unexpected zero extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n+ | True = p `svJoin` a+ where sa = intSizeOf a+ s = hasSign a+ p = svInteger (KBounded s (n - sa)) 0++-- | Sign-extend to given bits. Note that we keep the signedness of the argument.+sx :: Int -> SVal -> SVal+sx n a+ | n < sa = error $ "Data.SBV: Unexpected sign extension: from: " ++ show (intSizeOf a) ++ " to: " ++ show n+ | True = p `svJoin` a+ where sa = intSizeOf a+ mk = svInteger $ KBounded (hasSign a) (n - sa)+ p = svIte (pos a) (mk 0) (mk (-1))++-- | Get the sign-bit+signBit :: SVal -> SVal+signBit x = x `svTestBit` (intSizeOf x - 1)++-- | Is the sign-bit high?+neg :: SVal -> SVal+neg x = signBit x `svEqual` svTrue++-- | Is the sign-bit low?+pos :: SVal -> SVal+pos x = signBit x `svEqual` svFalse++-- | Do these have the same sign?+sameSign :: SVal -> SVal -> SVal+sameSign x y = (pos x `svAnd` pos y) `svOr` (neg x `svAnd` neg y)++-- | Do these have opposing signs?+diffSign :: SVal -> SVal -> SVal+diffSign x y = svNot (sameSign x y)++-- | Check all true+svAll :: [SVal] -> SVal+svAll = foldr svAnd svTrue++-- | Are all the bits between a b (inclusive) zero?+allZero :: Int -> Int -> SBV a -> SVal+allZero m n (SBV x)+ | m >= sz || n < 0 || m < n+ = error $ "Data.SBV.Tools.Overflow.allZero: Received unexpected parameters: " ++ show (m, n, sz)+ | True+ = svAll [svTestBit x i `svEqual` svFalse | i <- [m, m-1 .. n]]+ where sz = intSizeOf x++-- | Are all the bits between a b (inclusive) one?+allOne :: Int -> Int -> SBV a -> SVal+allOne m n (SBV x)+ | m >= sz || n < 0 || m < n+ = error $ "Data.SBV.Tools.Overflow.allOne: Received unexpected parameters: " ++ show (m, n, sz)+ | True+ = svAll [svTestBit x i `svEqual` svTrue | i <- [m, m-1 .. n]]+ where sz = intSizeOf x++-- | Unsigned addition. Can only overflow.+bvuaddo :: Int -> SVal -> SVal -> (SVal, SVal)+bvuaddo n x y = (underflow, overflow)+ where underflow = svFalse++ n' = n+1+ overflow = neg $ zx n' x `svPlus` zx n' y++-- | Signed addition.+bvsaddo :: Int -> SVal -> SVal -> (SVal, SVal)+bvsaddo _n x y = (underflow, overflow)+ where underflow = svAll [neg x, neg y, pos (x `svPlus` y)]+ overflow = svAll [pos x, pos y, neg (x `svPlus` y)]++-- | Unsigned subtraction. Can only underflow.+bvusubo :: Int -> SVal -> SVal -> (SVal, SVal)+bvusubo _n x y = (underflow, overflow)+ where underflow = y `svGreaterThan` x+ overflow = svFalse++-- | Signed subtraction.+bvssubo :: Int -> SVal -> SVal -> (SVal, SVal)+bvssubo _n x y = (underflow, overflow)+ where underflow = svAll [neg x, pos y, pos (x `svMinus` y)]+ overflow = svAll [pos x, neg y, neg (x `svMinus` y)]++-- | Unsigned multiplication. Can only overflow.+bvumulo :: Int -> SVal -> SVal -> (SVal, SVal)+bvumulo 0 _ _ = (svFalse, svFalse)+bvumulo n x y = (underflow, overflow)+ where underflow = svFalse++ n1 = n+1+ overflow1 = signBit $ zx n1 x `svTimes` zx n1 y++ -- From Z3 sources:+ --+ -- expr_ref ovf(m()), v(m()), tmp(m());+ -- ovf = m().mk_false();+ -- v = m().mk_false();+ -- for (unsigned i = 1; i < sz; ++i) {+ -- mk_or(ovf, a_bits[sz-i], ovf);+ -- mk_and(ovf, b_bits[i], tmp);+ -- mk_or(tmp, v, v);+ -- }+ -- overflow2 = v;+ --+ overflow2 = go 1 svFalse svFalse+ where go i ovf v+ | i >= n = v+ | True = go (i+1) ovf' v'+ where ovf' = ovf `svOr` (x `svTestBit` (n-i))+ tmp = ovf' `svAnd` (y `svTestBit` i)+ v' = tmp `svOr` v++ overflow = overflow1 `svOr` overflow2++-- | Signed multiplication.+bvsmulo :: Int -> SVal -> SVal -> (SVal, SVal)+bvsmulo 0 _ _ = (svFalse, svFalse)+bvsmulo n x y = (underflow, overflow)+ where underflow = diffSign x y `svAnd` overflowPossible+ overflow = sameSign x y `svAnd` overflowPossible++ n1 = n+1+ overflow1 = (xy1 `svTestBit` n) `svXOr` (xy1 `svTestBit` (n-1))+ where xy1 = sx n1 x `svTimes` sx n1 y++ -- From Z3 sources:+ -- expr_ref v(m()), tmp(m()), a(m()), b(m()), a_acc(m()), sign(m());+ -- a_acc = m().mk_false();+ -- v = m().mk_false();+ -- for (unsigned i = 1; i + 1 < sz; ++i) {+ -- mk_xor(b_bits[sz-1], b_bits[i], b);+ -- mk_xor(a_bits[sz-1], a_bits[sz-1-i], a);+ -- mk_or(a, a_acc, a_acc);+ -- mk_and(a_acc, b, tmp);+ -- mk_or(tmp, v, v);+ -- }+ -- overflow2 = v;+ overflow2 = go 1 svFalse svFalse+ where sY = signBit y+ sX = signBit x+ go i v a_acc+ | i + 1 >= n = v+ | True = go (i+1) v' a_acc'+ where b = sY `svXOr` (y `svTestBit` i)+ a = sX `svXOr` (x `svTestBit` (n-1-i))+ a_acc' = a `svOr` a_acc+ tmp = a_acc' `svAnd` b+ v' = tmp `svOr` v++ overflowPossible = overflow1 `svOr` overflow2++-- | Is this a concrete value?+known :: SVal -> Bool+known (SVal _ (Left _)) = True+known _ = False++-- | Unsigned multiplication, fast version using z3 primitives.+bvumuloFast :: Int -> SVal -> SVal -> (SVal, SVal)+bvumuloFast n x y+ | known x && known y -- Not particularly fast, but avoids shipping of to the solver+ = bvumulo n x y+ | True+ = (underflow, overflow)+ where underflow = fst $ bvumulo n x y -- No internal version for underflow exists (because it can't underflow)+ overflow = svMkOverflow Overflow_UMul_OVFL x y++-- | Signed multiplication, fast version using z3 primitives.+bvsmuloFast :: Int -> SVal -> SVal -> (SVal, SVal)+bvsmuloFast n x y+ | known x && known y -- Not particularly fast, but avoids shipping of to the solver+ = bvsmulo n x y+ | True+ = (underflow, overflow)+ where underflow = svMkOverflow Overflow_SMul_UDFL x y+ overflow = svMkOverflow Overflow_SMul_OVFL x y++-- | Unsigned division. Neither underflows, nor overflows.+bvudivo :: Int -> SVal -> SVal -> (SVal, SVal)+bvudivo _ _ _ = (underflow, overflow)+ where underflow = svFalse+ overflow = svFalse++-- | Signed division. Can only overflow.+bvsdivo :: Int -> SVal -> SVal -> (SVal, SVal)+bvsdivo n x y = (underflow, overflow)+ where underflow = svFalse++ ones = svInteger (KBounded True n) (-1)+ topSet = svInteger (KBounded True n) (2^(n-1))++ overflow = svAll [x `svEqual` topSet, y `svEqual` ones]++-- | Unsigned negation. Neither underflows, nor overflows.+bvunego :: Int -> SVal -> (SVal, SVal)+bvunego _ _ = (underflow, overflow)+ where underflow = svFalse+ overflow = svFalse++-- | Signed negation. Can only overflow.+bvsnego :: Int -> SVal -> (SVal, SVal)+bvsnego n x = (underflow, overflow)+ where underflow = svFalse++ topSet = svInteger (KBounded True n) (2^(n-1))+ overflow = x `svEqual` topSet++-- | Detecting underflow/overflow conditions for casting between bit-vectors. The first output is the result,+-- the second component itself is a pair with the first boolean indicating underflow and the second indicating overflow.+--+-- >>> sFromIntegralO (256 :: SInt16) :: (SWord8, (SBool, SBool))+-- (0 :: SWord8,(False,True))+-- >>> sFromIntegralO (-2 :: SInt16) :: (SWord8, (SBool, SBool))+-- (254 :: SWord8,(True,False))+-- >>> sFromIntegralO (2 :: SInt16) :: (SWord8, (SBool, SBool))+-- (2 :: SWord8,(False,False))+-- >>> prove $ \x -> sFromIntegralO (x::SInt32) .== (sFromIntegral x :: SInteger, (false, false))+-- Q.E.D.+--+-- As the last example shows, converting to `sInteger` never underflows or overflows for any value.+sFromIntegralO :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> (SBV b, (SBool, SBool))+sFromIntegralO x = case (kindOf x, kindOf (undefined :: b)) of+ (KBounded False n, KBounded False m) -> (res, u2u n m)+ (KBounded False n, KBounded True m) -> (res, u2s n m)+ (KBounded True n, KBounded False m) -> (res, s2u n m)+ (KBounded True n, KBounded True m) -> (res, s2s n m)+ (KUnbounded, KBounded s m) -> (res, checkBounds s m)+ (KBounded{}, KUnbounded) -> (res, (false, false))+ (KUnbounded, KUnbounded) -> (res, (false, false))+ (kFrom, kTo) -> error $ "sFromIntegralO: Expected bounded-BV types, received: " ++ show (kFrom, kTo)++ where res :: SBV b+ res = sFromIntegral x++ checkBounds :: Bool -> Int -> (SBool, SBool)+ checkBounds signed sz = (ix .< literal lb, ix .> literal ub)+ where ix :: SInteger+ ix = sFromIntegral x++ s :: Integer+ s = fromIntegral sz++ ub :: Integer+ ub | signed = 2^(s - 1) - 1+ | True = 2^s - 1++ lb :: Integer+ lb | signed = -ub-1+ | True = 0++ u2u :: Int -> Int -> (SBool, SBool)+ u2u n m = (underflow, overflow)+ where underflow = false+ overflow+ | n <= m = false+ | True = SBV $ svNot $ allZero (n-1) m x++ u2s :: Int -> Int -> (SBool, SBool)+ u2s n m = (underflow, overflow)+ where underflow = false+ overflow+ | m > n = false+ | True = SBV $ svNot $ allZero (n-1) (m-1) x++ s2u :: Int -> Int -> (SBool, SBool)+ s2u n m = (underflow, overflow)+ where underflow = SBV $ (unSBV x `svTestBit` (n-1)) `svEqual` svTrue++ overflow+ | m >= n - 1 = false+ | True = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svFalse, svNot $ allZero (n-1) m x]++ s2s :: Int -> Int -> (SBool, SBool)+ s2s n m = (underflow, overflow)+ where underflow+ | m > n = false+ | True = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svTrue, svNot $ allOne (n-1) (m-1) x]++ overflow+ | m > n = false+ | True = SBV $ svAll [(unSBV x `svTestBit` (n-1)) `svEqual` svFalse, svNot $ allZero (n-1) (m-1) x]++-- Helpers+l2 :: (SVal -> SVal -> (SBool, SBool)) -> SBV a -> SBV a -> (SBool, SBool)+l2 f (SBV a) (SBV b) = f a b++l1 :: (SVal -> (SBool, SBool)) -> SBV a -> (SBool, SBool)+l1 f (SBV a) = f a++signPick2 :: (Int -> SVal -> SVal -> (SVal, SVal)) -> (Int -> SVal -> SVal -> (SVal, SVal)) -> (SVal -> SVal -> (SBool, SBool))+signPick2 fu fs a b+ | hasSign a = let (u, o) = fs n a b in (SBV u, SBV o)+ | True = let (u, o) = fu n a b in (SBV u, SBV o)+ where n = intSizeOf a++signPick1 :: (Int -> SVal -> (SVal, SVal)) -> (Int -> SVal -> (SVal, SVal)) -> (SVal -> (SBool, SBool))+signPick1 fu fs a+ | hasSign a = let (u, o) = fs n a in (SBV u, SBV o)+ | True = let (u, o) = fu n a in (SBV u, SBV o)+ where n = intSizeOf a
Data/SBV/Utils/Numeric.hs view
@@ -102,6 +102,20 @@ | isNegativeZero b = isNegativeZero a | True = a == b +-- | Ordering for floats, avoiding the +0/-0/NaN issues. Note that this is+-- essentially used for indexing into a map, so we need to be total. Thus,+-- the order we pick is:+-- NaN -oo -0 +0 +oo+-- The placement of NaN here is questionable, but immaterial.+fpCompareObjectH :: RealFloat a => a -> a -> Ordering+fpCompareObjectH a b+ | a `fpIsEqualObjectH` b = EQ+ | isNaN a = LT+ | isNaN b = GT+ | isNegativeZero a, b == 0 = LT+ | isNegativeZero b, a == 0 = GT+ | True = a `compare` b+ -- | Check if a number is "normal." Note that +0/-0 is not considered a normal-number -- and also this is not simply the negation of isDenormalized! fpIsNormalizedH :: RealFloat a => a -> Bool
Documentation/SBV/Examples/Existentials/Diophantine.hs view
@@ -12,7 +12,6 @@ module Documentation.SBV.Examples.Existentials.Diophantine where import Data.SBV-import Data.SBV.Control -------------------------------------------------------------------------------------------------- -- * Representing solutions
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -56,16 +56,16 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example:--- x = 1.9259302e-34 :: Float--- y = -1.9259117e-34 :: Float--- z = -1.814176e-39 :: Float+-- x = -1.844675e19 :: Float+-- y = 8.7960925e12 :: Float+-- z = -2.4178333e24 :: Float -- -- Indeed, we have: ----- >>> ((1.9259302e-34) + ((-1.9259117e-34) + (-1.814176e-39))) :: Float--- 3.4438e-41--- >>> (((1.9259302e-34) + ((-1.9259117e-34))) + (-1.814176e-39)) :: Float--- 3.4014e-41+-- >>> (-1.844675e19) + ((8.7960925e12) + (-2.4178333e24)):: Float+-- -2.417852e24+-- >>> ((-1.844675e19) + (8.7960925e12)) + (-2.4178333e24) :: Float+-- -2.4178516e24 -- -- Note the difference between two additions! assocPlusRegular :: IO ThmResult@@ -87,17 +87,17 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example:--- a = 2.424457e-38 :: Float--- b = -1.0e-45 :: Float+-- a = -2.524355e-29 :: Float+-- b = 9.403955e-38 :: Float -- -- Indeed, we have: ----- >>> (2.424457e-38 + (-1.0e-45)) == (2.424457e-38 :: Float)+-- >>> (-2.524355e-29 + 9.403955e-38) == (-2.524355e-29 :: Float) -- True -- -- But: ----- >>> -1.0e-45 == (0 :: Float)+-- >>> 9.403955e-38 == (0 :: Float) -- False -- nonZeroAddition :: IO ThmResult@@ -118,13 +118,13 @@ -- -- >>> multInverse -- Falsifiable. Counter-example:--- a = 1.119056263978578e-308 :: Double+-- a = 8.988465678497178e307 :: Double -- -- Indeed, we have: ----- >>> let a = 1.119056263978578e-308 :: Double+-- >>> let a = 8.988465678497178e307 :: Double -- >>> a * (1/a)--- 0.9999999999999999+-- 1.0000000000000002 multInverse :: IO ThmResult multInverse = prove $ do a <- sDouble "a" constrain $ fpIsPoint a
Documentation/SBV/Examples/Puzzles/HexPuzzle.hs view
@@ -59,7 +59,7 @@ -- | Give symbolic colors a name for convenience. type SColor = SBV Color --- | Use 8-bit words for button numners, even though we only have 1 to 19.+-- | Use 8-bit words for button numbers, even though we only have 1 to 19. type Button = Word8 -- | Symbolic version of button.
Documentation/SBV/Examples/Queries/Interpolants.hs view
@@ -7,6 +7,9 @@ -- Stability : experimental -- -- Demonstrates extraction of interpolants via queries.+--+-- N.B. As of Z3 version 4.8.0; Z3 no longer supports interpolants. You need+-- to use the MathSAT backend for this example to work. ----------------------------------------------------------------------------- module Documentation.SBV.Examples.Queries.Interpolants where@@ -14,37 +17,45 @@ import Data.SBV import Data.SBV.Control --- | Compute the interpolant for formulas @y = 2x@ and @y = 2z+1@.--- These formulas are not satisfiable together since it would mean--- @y@ is both even and odd at the same time. An interpolant for--- this pair of formulas is a formula that's expressed only in terms--- of @y@, which is the only common symbol among them. We have:+-- | Compute the interpolant for the following sets of formulas: ----- >>> runSMT evenOdd--- ["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"]+-- @{x - 3y >= -1, x + y >= 0}@ ----- This is a bit hard to read unfortunately, due to translation artifacts and use of strings. To analyze,--- we need to know that @s1@ is @y@ through SBV's translation. Let's express it in--- regular infix notation with @y@ for @s1@:+-- AND ----- @ 0 <= (y `div` 2) + ((-y) `div` 2)@+-- @{z - 2x >= 3, 2z <= 1}@ ----- Notice that the only symbol is @y@, as required. To establish that this is--- indeed an interpolant, we should establish that when @y@ is even, this formula--- is @True@; and if @y@ is odd, then then it should be @False@. You can argue--- mathematically that this indeed the case, but let's just use SBV to prove these:+-- where the variables are integers. Note that these sets of+-- formulas are themselves satisfiable, but not taken all together.+-- The pair @(x, y) = (0, 0)@ satisfies the first set. The pair @(x, z) = (-2, 0)@+-- satisfies the second. However, there's no triple @(x, y, z)@ that satisfies all+-- these four formulas together. We can use SBV to check this fact: ----- >>> prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))+-- >>> sat $ \x y z -> bAnd [x - 3*y .>= -1, x + y .>= 0, z - 2*x .>= 3, 2 * z .<= (1::SInteger)]+-- Unsatisfiable+--+-- An interpolant for these sets would only talk about the variable @x@ that is common+-- to both. We have:+--+-- >>> runSMTWith mathSAT example+-- "(<= 0 s0)"+--+-- Notice that we get a string back, not a term; so there's some back-translation we need to do. We+-- know that @s0@ is @x@ through our translation mechanism, so the interpolant is saying that @x >= 0@+-- is entailed by the first set of formulas, and is inconsistent with the second. Let's use SBV+-- to indeed show that this is the case:+--+-- >>> prove $ \x y -> (x - 3*y .>= -1 &&& x + y .>= 0) ==> (x .>= (0::SInteger)) -- Q.E.D. -- -- And: ----- >>> prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))+-- >>> prove $ \x z -> (z - 2*x .>= 3 &&& 2 * z .<= 1) ==> bnot (x .>= (0::SInteger)) -- Q.E.D. -- -- This establishes that we indeed have an interpolant!-evenOdd :: Symbolic [String]-evenOdd = do+example :: Symbolic String+example = do x <- sInteger "x" y <- sInteger "y" z <- sInteger "z"@@ -52,14 +63,16 @@ -- tell the solver we want interpolants setOption $ ProduceInterpolants True - -- create named constraints, which will allow- -- computation of the interpolants for our formulas- namedConstraint "y is even" $ y .== 2*x- namedConstraint "y is odd" $ y .== 2*z + 1+ -- create interpolation constraints. MathSAT requires the relevant formulas+ -- to be marked with the attribute :interpolation-group+ constrainWithAttribute [(":interpolation-group", "A")] $ x - 3*y .>= -1+ constrainWithAttribute [(":interpolation-group", "A")] $ x + y .>= 0+ constrainWithAttribute [(":interpolation-group", "B")] $ z - 2*x .>= 3+ constrainWithAttribute [(":interpolation-group", "B")] $ 2*z .<= 1 -- To obtain the interpolant, we run a query query $ do cs <- checkSat case cs of- Unsat -> getInterpolant ["y is even", "y is odd"]+ Unsat -> getInterpolant ["A"] Sat -> error "Unexpected sat result!" Unk -> error "Unexpected unknown result!"
SBVTestSuite/GoldFiles/floats_cgen.gold view
@@ -2574,6 +2574,7 @@ CC?=gcc CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer+LDFLAGS?=-lm AR?=ar ARFLAGS?=cr @@ -2583,7 +2584,7 @@ ${AR} ${ARFLAGS} $@ $^ floatCodeGen_driver: floatCodeGen_driver.c floatCodeGen.h- ${CC} ${CCFLAGS} $< -o $@ floatCodeGen.a+ ${CC} ${CCFLAGS} $< -o $@ floatCodeGen.a ${LDFLAGS} toFP_Int8_ToFloat.o: toFP_Int8_ToFloat.c floatCodeGen.h ${CC} ${CCFLAGS} -c $< -o $@
SBVTestSuite/GoldFiles/pareto1.gold view
@@ -5,89 +5,89 @@ max_x_plus_y = 0 :: Integer min_y = 0 :: Integer Pareto front #2: Optimal model:- x = 0 :: Integer- y = 1 :: Integer- min_x = 0 :: Integer- max_x_plus_y = 1 :: Integer- min_y = 1 :: Integer-Pareto front #3: Optimal model:- x = 4 :: Integer+ x = 1 :: Integer y = 0 :: Integer- min_x = 4 :: Integer- max_x_plus_y = 4 :: Integer+ min_x = 1 :: Integer+ max_x_plus_y = 1 :: Integer min_y = 0 :: Integer-Pareto front #4: Optimal model:- 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:+Pareto front #3: Optimal model: x = 0 :: Integer y = 2 :: Integer min_x = 0 :: Integer max_x_plus_y = 2 :: Integer min_y = 2 :: Integer-Pareto front #6: Optimal model:- x = 2 :: Integer- y = 2 :: Integer- min_x = 2 :: Integer- max_x_plus_y = 4 :: Integer- min_y = 2 :: Integer-Pareto front #7: Optimal model:+Pareto front #4: Optimal model: x = 1 :: Integer- y = 0 :: Integer+ y = 1 :: Integer min_x = 1 :: Integer+ max_x_plus_y = 2 :: Integer+ min_y = 1 :: Integer+Pareto front #5: Optimal model:+ x = 0 :: Integer+ y = 1 :: Integer+ min_x = 0 :: Integer max_x_plus_y = 1 :: Integer- min_y = 0 :: Integer-Pareto front #8: Optimal model:- x = 5 :: Integer- y = 0 :: 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:+ min_y = 1 :: Integer+Pareto front #6: Optimal model: x = 1 :: Integer y = 2 :: Integer min_x = 1 :: Integer max_x_plus_y = 3 :: Integer min_y = 2 :: Integer-Pareto front #11: Optimal model:- x = 4 :: Integer- y = 2 :: Integer- min_x = 4 :: Integer- max_x_plus_y = 6 :: Integer- min_y = 2 :: Integer-Pareto front #12: Optimal model:+Pareto front #7: 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:+Pareto front #8: Optimal model:+ x = 2 :: Integer+ y = 1 :: Integer+ min_x = 2 :: Integer+ max_x_plus_y = 3 :: Integer+ min_y = 1 :: Integer+Pareto front #9: Optimal model: x = 3 :: Integer y = 0 :: Integer min_x = 3 :: Integer max_x_plus_y = 3 :: Integer min_y = 0 :: Integer-Pareto front #14: Optimal model:+Pareto front #10: Optimal model: x = 3 :: Integer- y = 2 :: Integer+ y = 1 :: Integer min_x = 3 :: Integer+ max_x_plus_y = 4 :: Integer+ min_y = 1 :: Integer+Pareto front #11: Optimal model:+ x = 4 :: Integer+ y = 0 :: Integer+ min_x = 4 :: Integer+ max_x_plus_y = 4 :: Integer+ min_y = 0 :: Integer+Pareto front #12: Optimal model:+ x = 4 :: Integer+ y = 1 :: Integer+ min_x = 4 :: Integer max_x_plus_y = 5 :: Integer- min_y = 2 :: Integer-Pareto front #15: Optimal model:- x = 1 :: Integer+ min_y = 1 :: Integer+Pareto front #13: Optimal model:+ x = 5 :: Integer+ y = 0 :: Integer+ min_x = 5 :: Integer+ max_x_plus_y = 5 :: Integer+ min_y = 0 :: Integer+Pareto front #14: Optimal model:+ x = 5 :: Integer y = 1 :: Integer- min_x = 1 :: Integer- max_x_plus_y = 2 :: Integer+ min_x = 5 :: Integer+ max_x_plus_y = 6 :: Integer min_y = 1 :: Integer+Pareto front #15: Optimal model:+ x = 2 :: Integer+ y = 2 :: Integer+ min_x = 2 :: Integer+ max_x_plus_y = 4 :: Integer+ min_y = 2 :: Integer Pareto front #16: Optimal model: x = 0 :: Integer y = 3 :: Integer@@ -113,68 +113,68 @@ 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+ x = 2 :: Integer+ y = 3 :: Integer+ min_x = 2 :: Integer max_x_plus_y = 5 :: Integer- min_y = 1 :: Integer+ min_y = 3 :: Integer Pareto front #21: Optimal model:- x = 5 :: Integer- y = 1 :: Integer- min_x = 5 :: Integer+ x = 2 :: Integer+ y = 4 :: Integer+ min_x = 2 :: Integer max_x_plus_y = 6 :: Integer- min_y = 1 :: Integer+ min_y = 4 :: Integer Pareto front #22: Optimal model:- x = 4 :: Integer- y = 3 :: Integer- min_x = 4 :: Integer- max_x_plus_y = 7 :: Integer- min_y = 3 :: Integer+ x = 3 :: Integer+ y = 2 :: Integer+ min_x = 3 :: Integer+ max_x_plus_y = 5 :: Integer+ min_y = 2 :: Integer Pareto front #23: Optimal model:- x = 5 :: Integer+ x = 3 :: Integer y = 3 :: Integer- min_x = 5 :: Integer- max_x_plus_y = 8 :: Integer+ min_x = 3 :: Integer+ max_x_plus_y = 6 :: Integer min_y = 3 :: Integer Pareto front #24: Optimal model:- x = 5 :: Integer+ x = 3 :: Integer y = 4 :: Integer- min_x = 5 :: Integer- max_x_plus_y = 9 :: Integer+ min_x = 3 :: Integer+ max_x_plus_y = 7 :: Integer min_y = 4 :: Integer Pareto front #25: Optimal model:- x = 2 :: Integer- y = 1 :: Integer- min_x = 2 :: Integer- max_x_plus_y = 3 :: Integer- min_y = 1 :: Integer+ x = 4 :: Integer+ y = 2 :: Integer+ min_x = 4 :: Integer+ max_x_plus_y = 6 :: Integer+ min_y = 2 :: Integer Pareto front #26: Optimal model:- x = 3 :: Integer- y = 1 :: Integer- min_x = 3 :: Integer- max_x_plus_y = 4 :: Integer- min_y = 1 :: Integer+ x = 5 :: Integer+ y = 2 :: Integer+ min_x = 5 :: Integer+ max_x_plus_y = 7 :: Integer+ min_y = 2 :: Integer Pareto front #27: Optimal model:- x = 2 :: Integer+ x = 4 :: Integer y = 3 :: Integer- min_x = 2 :: Integer- max_x_plus_y = 5 :: Integer+ min_x = 4 :: Integer+ max_x_plus_y = 7 :: Integer min_y = 3 :: Integer Pareto front #28: Optimal model:- x = 3 :: Integer+ x = 5 :: Integer y = 3 :: Integer- min_x = 3 :: Integer- max_x_plus_y = 6 :: Integer+ min_x = 5 :: Integer+ max_x_plus_y = 8 :: Integer min_y = 3 :: Integer Pareto front #29: Optimal model:- x = 2 :: Integer+ x = 4 :: Integer y = 4 :: Integer- min_x = 2 :: Integer- max_x_plus_y = 6 :: Integer+ min_x = 4 :: Integer+ max_x_plus_y = 8 :: Integer min_y = 4 :: Integer Pareto front #30: Optimal model:- x = 3 :: Integer+ x = 5 :: Integer y = 4 :: Integer- min_x = 3 :: Integer- max_x_plus_y = 7 :: Integer+ min_x = 5 :: Integer+ max_x_plus_y = 9 :: Integer min_y = 4 :: Integer
SBVTestSuite/GoldFiles/pareto2.gold view
@@ -1,182 +1,182 @@ Pareto front #1: Optimal model:- x = 0 :: Integer- y = 4 :: Integer- min_x = 0 :: Integer- max_y = 4 :: Integer- max_x_plus_y = 4 :: Integer+ x = 0 :: Integer+ y = -1 :: Integer+ min_x = 0 :: Integer+ max_y = -1 :: Integer+ max_x_plus_y = -1 :: Integer Pareto front #2: Optimal model:- x = 0 :: Integer- y = 5 :: Integer- min_x = 0 :: Integer- max_y = 5 :: Integer- max_x_plus_y = 5 :: Integer+ x = 0 :: Integer+ y = -2 :: Integer+ min_x = 0 :: Integer+ max_y = -2 :: Integer+ max_x_plus_y = -2 :: Integer Pareto front #3: Optimal model:- x = 0 :: Integer- y = 6 :: Integer- min_x = 0 :: Integer- max_y = 6 :: Integer- max_x_plus_y = 6 :: Integer+ x = 0 :: Integer+ y = -3 :: Integer+ min_x = 0 :: Integer+ max_y = -3 :: Integer+ max_x_plus_y = -3 :: Integer Pareto front #4: Optimal model:- x = 0 :: Integer- y = 7 :: Integer- min_x = 0 :: Integer- max_y = 7 :: Integer- max_x_plus_y = 7 :: Integer+ x = 0 :: Integer+ y = -4 :: Integer+ min_x = 0 :: Integer+ max_y = -4 :: Integer+ max_x_plus_y = -4 :: Integer Pareto front #5: Optimal model:- x = 0 :: Integer- y = 8 :: Integer- min_x = 0 :: Integer- max_y = 8 :: Integer- max_x_plus_y = 8 :: Integer+ x = 0 :: Integer+ y = -5 :: Integer+ min_x = 0 :: Integer+ max_y = -5 :: Integer+ max_x_plus_y = -5 :: Integer Pareto front #6: Optimal model:- x = 0 :: Integer- y = 9 :: Integer- min_x = 0 :: Integer- max_y = 9 :: Integer- max_x_plus_y = 9 :: Integer+ x = 0 :: Integer+ y = -6 :: Integer+ min_x = 0 :: Integer+ max_y = -6 :: Integer+ max_x_plus_y = -6 :: Integer Pareto front #7: Optimal model: x = 0 :: Integer- y = 10 :: Integer+ y = -7 :: Integer min_x = 0 :: Integer- max_y = 10 :: Integer- max_x_plus_y = 10 :: Integer+ max_y = -7 :: Integer+ max_x_plus_y = -7 :: Integer Pareto front #8: Optimal model: x = 0 :: Integer- y = 11 :: Integer+ y = -8 :: Integer min_x = 0 :: Integer- max_y = 11 :: Integer- max_x_plus_y = 11 :: Integer+ max_y = -8 :: Integer+ max_x_plus_y = -8 :: Integer Pareto front #9: Optimal model: x = 0 :: Integer- y = 12 :: Integer+ y = -9 :: Integer min_x = 0 :: Integer- max_y = 12 :: Integer- max_x_plus_y = 12 :: Integer+ max_y = -9 :: Integer+ max_x_plus_y = -9 :: Integer Pareto front #10: Optimal model:- x = 0 :: Integer- y = 13 :: Integer- min_x = 0 :: Integer- max_y = 13 :: Integer- max_x_plus_y = 13 :: Integer+ x = 0 :: Integer+ y = -10 :: Integer+ min_x = 0 :: Integer+ max_y = -10 :: Integer+ max_x_plus_y = -10 :: Integer Pareto front #11: Optimal model:- x = 0 :: Integer- y = 14 :: Integer- min_x = 0 :: Integer- max_y = 14 :: Integer- max_x_plus_y = 14 :: Integer+ x = 0 :: Integer+ y = -11 :: Integer+ min_x = 0 :: Integer+ max_y = -11 :: Integer+ max_x_plus_y = -11 :: Integer Pareto front #12: Optimal model:- x = 0 :: Integer- y = 15 :: Integer- min_x = 0 :: Integer- max_y = 15 :: Integer- max_x_plus_y = 15 :: Integer+ x = 0 :: Integer+ y = -12 :: Integer+ min_x = 0 :: Integer+ max_y = -12 :: Integer+ max_x_plus_y = -12 :: Integer Pareto front #13: Optimal model:- x = 0 :: Integer- y = 16 :: Integer- min_x = 0 :: Integer- max_y = 16 :: Integer- max_x_plus_y = 16 :: Integer+ x = 0 :: Integer+ y = -13 :: Integer+ min_x = 0 :: Integer+ max_y = -13 :: Integer+ max_x_plus_y = -13 :: Integer Pareto front #14: Optimal model:- x = 0 :: Integer- y = 17 :: Integer- min_x = 0 :: Integer- max_y = 17 :: Integer- max_x_plus_y = 17 :: Integer+ x = 0 :: Integer+ y = -14 :: Integer+ min_x = 0 :: Integer+ max_y = -14 :: Integer+ max_x_plus_y = -14 :: Integer Pareto front #15: Optimal model:- x = 0 :: Integer- y = 18 :: Integer- min_x = 0 :: Integer- max_y = 18 :: Integer- max_x_plus_y = 18 :: Integer+ x = 0 :: Integer+ y = -15 :: Integer+ min_x = 0 :: Integer+ max_y = -15 :: Integer+ max_x_plus_y = -15 :: Integer Pareto front #16: Optimal model:- x = 0 :: Integer- y = 19 :: Integer- min_x = 0 :: Integer- max_y = 19 :: Integer- max_x_plus_y = 19 :: Integer+ x = 0 :: Integer+ y = -16 :: Integer+ min_x = 0 :: Integer+ max_y = -16 :: Integer+ max_x_plus_y = -16 :: Integer Pareto front #17: Optimal model:- x = 0 :: Integer- y = 20 :: Integer- min_x = 0 :: Integer- max_y = 20 :: Integer- max_x_plus_y = 20 :: Integer+ x = 0 :: Integer+ y = -17 :: Integer+ min_x = 0 :: Integer+ max_y = -17 :: Integer+ max_x_plus_y = -17 :: Integer Pareto front #18: Optimal model:- x = 0 :: Integer- y = 21 :: Integer- min_x = 0 :: Integer- max_y = 21 :: Integer- max_x_plus_y = 21 :: Integer+ x = 0 :: Integer+ y = -18 :: Integer+ min_x = 0 :: Integer+ max_y = -18 :: Integer+ max_x_plus_y = -18 :: Integer Pareto front #19: Optimal model:- x = 0 :: Integer- y = 22 :: Integer- min_x = 0 :: Integer- max_y = 22 :: Integer- max_x_plus_y = 22 :: Integer+ x = 0 :: Integer+ y = -19 :: Integer+ min_x = 0 :: Integer+ max_y = -19 :: Integer+ max_x_plus_y = -19 :: Integer Pareto front #20: Optimal model:- x = 0 :: Integer- y = 23 :: Integer- min_x = 0 :: Integer- max_y = 23 :: Integer- max_x_plus_y = 23 :: Integer+ x = 0 :: Integer+ y = -20 :: Integer+ min_x = 0 :: Integer+ max_y = -20 :: Integer+ max_x_plus_y = -20 :: Integer Pareto front #21: Optimal model:- x = 0 :: Integer- y = 24 :: Integer- min_x = 0 :: Integer- max_y = 24 :: Integer- max_x_plus_y = 24 :: Integer+ x = 0 :: Integer+ y = -21 :: Integer+ min_x = 0 :: Integer+ max_y = -21 :: Integer+ max_x_plus_y = -21 :: Integer Pareto front #22: Optimal model:- x = 0 :: Integer- y = 25 :: Integer- min_x = 0 :: Integer- max_y = 25 :: Integer- max_x_plus_y = 25 :: Integer+ x = 0 :: Integer+ y = -22 :: Integer+ min_x = 0 :: Integer+ max_y = -22 :: Integer+ max_x_plus_y = -22 :: Integer Pareto front #23: Optimal model:- x = 0 :: Integer- y = 26 :: Integer- min_x = 0 :: Integer- max_y = 26 :: Integer- max_x_plus_y = 26 :: Integer+ x = 0 :: Integer+ y = -23 :: Integer+ min_x = 0 :: Integer+ max_y = -23 :: Integer+ max_x_plus_y = -23 :: Integer Pareto front #24: Optimal model:- x = 0 :: Integer- y = 27 :: Integer- min_x = 0 :: Integer- max_y = 27 :: Integer- max_x_plus_y = 27 :: Integer+ x = 0 :: Integer+ y = -24 :: Integer+ min_x = 0 :: Integer+ max_y = -24 :: Integer+ max_x_plus_y = -24 :: Integer Pareto front #25: Optimal model:- x = 0 :: Integer- y = 3 :: Integer- min_x = 0 :: Integer- max_y = 3 :: Integer- max_x_plus_y = 3 :: Integer+ x = 0 :: Integer+ y = -25 :: Integer+ min_x = 0 :: Integer+ max_y = -25 :: Integer+ max_x_plus_y = -25 :: Integer Pareto front #26: Optimal model:- x = 0 :: Integer- y = 2 :: Integer- min_x = 0 :: Integer- max_y = 2 :: Integer- max_x_plus_y = 2 :: Integer+ x = 0 :: Integer+ y = -26 :: Integer+ min_x = 0 :: Integer+ max_y = -26 :: Integer+ max_x_plus_y = -26 :: Integer Pareto front #27: Optimal model:- x = 0 :: Integer- y = 1 :: Integer- min_x = 0 :: Integer- max_y = 1 :: Integer- max_x_plus_y = 1 :: Integer+ x = 0 :: Integer+ y = -27 :: Integer+ min_x = 0 :: Integer+ max_y = -27 :: Integer+ max_x_plus_y = -27 :: Integer Pareto front #28: Optimal model:- x = 0 :: Integer- y = 0 :: Integer- min_x = 0 :: Integer- max_y = 0 :: Integer- max_x_plus_y = 0 :: Integer+ x = 0 :: Integer+ y = -28 :: Integer+ min_x = 0 :: Integer+ max_y = -28 :: Integer+ max_x_plus_y = -28 :: Integer Pareto front #29: Optimal model:- x = 0 :: Integer- y = -1 :: Integer- min_x = 0 :: Integer- max_y = -1 :: Integer- max_x_plus_y = -1 :: Integer+ x = 0 :: Integer+ y = -29 :: Integer+ min_x = 0 :: Integer+ max_y = -29 :: Integer+ max_x_plus_y = -29 :: Integer Pareto front #30: Optimal model:- x = 0 :: Integer- y = -2 :: Integer- min_x = 0 :: 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.+ x = 0 :: Integer+ y = -30 :: Integer+ min_x = 0 :: Integer+ max_y = -30 :: Integer+ max_x_plus_y = -30 :: Integer+*** Note: Pareto-front extraction was terminated as requested by the user.+*** There might be many other results!
+ SBVTestSuite/GoldFiles/pareto3.gold view
@@ -0,0 +1,8 @@+Pareto front #1: Optimal model:+ x = 0 :: Integer+ min_x = 0 :: Integer+ max_x_plus_x = 0 :: Integer+Pareto front #2: Optimal model:+ x = 1 :: Integer+ min_x = 1 :: Integer+ max_x_plus_x = 2 :: Integer
SBVTestSuite/GoldFiles/query1.gold view
@@ -76,7 +76,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.7.0")+[RECV] (:version "4.8.0") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -107,7 +107,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.7.0")+[RECV] (:version "4.8.0") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)
SBVTestSuite/GoldFiles/query_Interpolant1.gold view
@@ -1,8 +1,8 @@-** Calling: z3 -nw -in -smt2+** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4 [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)+** Backend solver MathSAT does not support global decls.+** Some incremental calls, such as pop, will be limited. [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-interpolants true) [GOOD] (set-option :produce-models true)@@ -29,15 +29,14 @@ [GOOD] (define-fun s8 () Bool (= s2 s3)) [GOOD] (define-fun s9 () Bool (not s8)) [GOOD] (define-fun s10 () Bool (and s7 s9))-[GOOD] (assert (! s6 :named |c1|))-[GOOD] (assert (! s10 :named |c2|))+[GOOD] (assert (! s6 :interpolation-group |c1|))+[GOOD] (assert (! s10 :interpolation-group |c2|)) [SEND] (check-sat) [RECV] unsat-[SEND] (get-interpolant |c1| |c2|)-[RECV] (interpolants- (= s1 s2))-*** Solver : Z3+[SEND] (get-interpolant (|c1|))+[RECV] (= s1 s2)+*** Solver : MathSAT *** Exit code: ExitSuccess FINAL OUTPUT:-["(= s1 s2)"]+"(= s1 s2)"
SBVTestSuite/GoldFiles/query_Interpolant2.gold view
@@ -1,8 +1,8 @@-** Calling: z3 -nw -in -smt2+** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4 [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)+** Backend solver MathSAT does not support global decls.+** Some incremental calls, such as pop, will be limited. [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-interpolants true) [GOOD] (set-option :produce-models true)@@ -34,15 +34,14 @@ [GOOD] (define-fun s11 () Int (g s3)) [GOOD] (define-fun s12 () Bool (distinct s10 s11)) [GOOD] (define-fun s13 () Bool (and s9 s12))-[GOOD] (assert (! s8 :named |c1|))-[GOOD] (assert (! s13 :named |c2|))+[GOOD] (assert (! s8 :interpolation-group |c1|))+[GOOD] (assert (! s13 :interpolation-group |c2|)) [SEND] (check-sat) [RECV] unsat-[SEND] (get-interpolant |c1| |c2|)-[RECV] (interpolants- (or (= s2 s3) (not (= s1 s0))))-*** Solver : Z3+[SEND] (get-interpolant (|c1|))+[RECV] (not (and (= s0 s1) (not (= s2 s3))))+*** Solver : MathSAT *** Exit code: ExitSuccess FINAL OUTPUT:-["(or (= s2 s3) (not (= s1 s0)))"]+"(not (and (= s0 s1) (not (= s2 s3))))"
− SBVTestSuite/GoldFiles/query_Interpolant3.gold
@@ -1,49 +0,0 @@-** 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-interpolants true)-[GOOD] (set-option :produce-models true)-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s_2 () Bool false)-[GOOD] (define-fun s_1 () Bool true)-[GOOD] (define-fun s3 () Int 0)-[GOOD] (define-fun s7 () Int 1)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () Int) ; tracks user variable "x"-[GOOD] (declare-fun s1 () Int) ; tracks user variable "y"-[GOOD] (declare-fun s2 () Int) ; tracks user variable "z"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] (declare-fun array_0 () (Array Int Int))-[GOOD] (declare-fun array_1 () (Array Int Int))-[GOOD] (declare-fun array_2 () (Array Int Int))-[GOOD] (declare-fun array_3 () (Array Int Int))-[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s4 () Bool (= array_1 array_3))-[GOOD] (define-fun s5 () Bool (= s0 s2))-[GOOD] (define-fun s6 () Int (select array_1 s2))-[GOOD] (define-fun s8 () Bool (= s6 s7))-[GOOD] (define-fun s9 () Bool (and s5 s8))-[GOOD] (assert (= array_2 (store array_0 s0 s3)))-[GOOD] (assert (= array_3 (store array_2 s1 s3)))-[GOOD] (assert (! s4 :named |c1|))-[GOOD] (assert (! s9 :named |c2|))-[SEND] (check-sat)-[RECV] unsat-[SEND] (get-interpolant |c1| |c2|)-[RECV] (interpolants- (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:-["(and (= (select array_1 s0) (select (store array_2 s1 0) s0)) (or (= 0 (select array_1 s0)) (not (= s0 s1))))"]
− SBVTestSuite/GoldFiles/query_Interpolant4.gold
@@ -1,46 +0,0 @@-** 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-interpolants true)-[GOOD] (set-option :produce-models true)-[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.-[GOOD] ; --- uninterpreted sorts ----[GOOD] ; --- literal constants ----[GOOD] (define-fun s_2 () Bool false)-[GOOD] (define-fun s_1 () Bool true)-[GOOD] ; --- skolem constants ----[GOOD] (declare-fun s0 () Int) ; tracks user variable "a"-[GOOD] (declare-fun s1 () Int) ; tracks user variable "b"-[GOOD] (declare-fun s2 () Int) ; tracks user variable "c"-[GOOD] (declare-fun s3 () Int) ; tracks user variable "d"-[GOOD] (declare-fun s4 () Int) ; tracks user variable "e"-[GOOD] ; --- constant tables ----[GOOD] ; --- skolemized tables ----[GOOD] ; --- arrays ----[GOOD] ; --- uninterpreted constants ----[GOOD] ; --- user given axioms ----[GOOD] ; --- formula ----[GOOD] (define-fun s5 () Bool (= s0 s1))-[GOOD] (define-fun s6 () Bool (= s0 s2))-[GOOD] (define-fun s7 () Bool (and s5 s6))-[GOOD] (define-fun s8 () Bool (= s2 s3))-[GOOD] (define-fun s9 () Bool (= s1 s4))-[GOOD] (define-fun s10 () Bool (distinct s3 s4))-[GOOD] (define-fun s11 () Bool (and s9 s10))-[GOOD] (assert (! s7 :named |c1|))-[GOOD] (assert (! s8 :named |c2|))-[GOOD] (assert (! s11 :named |c3|))-[SEND] (check-sat)-[RECV] unsat-[SEND] (get-interpolant |c1| |c2| |c3|)-[RECV] (interpolants- (= s1 s2)- (= s1 s3))-*** Solver : Z3-*** Exit code: ExitSuccess--FINAL OUTPUT:-["(= s1 s2)","(= s1 s3)"]
+ SBVTestSuite/GoldFiles/safe1.gold view
@@ -0,0 +1,39 @@+** 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] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] (define-fun s1 () Int 12)+[GOOD] (define-fun s3 () Int 2)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () Int)+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s2 () Bool (= s0 s1))+[GOOD] (define-fun s4 () Bool (> s0 s3))+[GOOD] (define-fun s5 () Bool (not s4))+[GOOD] (assert s_1)+[GOOD] (push 1)+[GOOD] (assert s5)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 0))+[GOOD] (pop 1)+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL: [safe1: Violated. Model:+ s0 = 0 :: Integer]+DONE!
+ SBVTestSuite/GoldFiles/safe2.gold view
@@ -0,0 +1,38 @@+** 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] ; --- literal constants ---+[GOOD] (define-fun s_2 () Bool false)+[GOOD] (define-fun s_1 () Bool true)+[GOOD] (define-fun s1 () Int 12)+[GOOD] (define-fun s2 () Int 2)+[GOOD] ; --- skolem constants ---+[GOOD] (declare-fun s0 () Int)+[GOOD] ; --- constant tables ---+[GOOD] ; --- skolemized tables ---+[GOOD] ; --- arrays ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user given axioms ---+[GOOD] ; --- formula ---+[GOOD] (define-fun s3 () Bool (> s0 s2))+[GOOD] (define-fun s4 () Bool (not s3))+[GOOD] (assert s_1)+[GOOD] (push 1)+[GOOD] (assert s4)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 0))+[GOOD] (pop 1)+*** Solver : Z3+*** Exit code: ExitSuccess++ FINAL: [safe2: Violated. Model:+ s0 = 0 :: Integer]+DONE!
SBVTestSuite/GoldFiles/timeout1.gold view
@@ -1,2 +1,2 @@ Unknown.- Reason: canceled+ Reason: timeout
SBVTestSuite/SBVDocTest.hs view
@@ -10,28 +10,52 @@ import Utils.SBVTestFramework (getTestEnvironment, TestEnvironment(..), CIOS(..)) +import System.Random (randomRIO)+ main :: IO () main = do (testEnv, testPercentage) <- getTestEnvironment putStrLn $ "SBVDocTest: Test platform: " ++ show testEnv case testEnv of- TestEnvLocal -> runDocTest False+ TestEnvLocal -> runDocTest False False 100 TestEnvCI env -> if testPercentage < 50 then do putStrLn $ "Test percentage below tresheold, skipping doctest: " ++ show testPercentage exitSuccess- else runDocTest (env == CIWindows)+ else runDocTest (env == CIWindows) True testPercentage TestEnvUnknown -> do putStrLn "Unknown test environment, skipping doctests" exitSuccess- where runDocTest windowsSkip = do srcFiles <- glob "Data/SBV/**/*.hs"- docFiles <- glob "Documentation/SBV/**/*.hs"- let allFiles = srcFiles ++ docFiles- testFiles- | windowsSkip = filter (not . bad) allFiles- | True = allFiles- doctest testFiles - -- The following test has a path encoded in its output, and hence fails on Windows- -- since it has the c:\blah\blah format. Skip it:- bad fn = "nodiv0.hs" `isSuffixOf` map toLower fn+ where runDocTest onWindows onRemote tp = do srcFiles <- glob "Data/SBV/**/*.hs"+ docFiles <- glob "Documentation/SBV/**/*.hs" + let allFiles = srcFiles ++ docFiles+ testFiles = filter (\nm -> not (skipWindows nm || skipRemote nm)) allFiles++ args = ["--fast", "--no-magic"]++ tfs <- pickPercentage tp testFiles++ doctest $ args ++ tfs++ where skipWindows nm+ | not onWindows = False+ | True = -- The following test has a path encoded in its output, and hence fails on Windows+ -- since it has the c:\blah\blah format. Skip it:+ "nodiv0.hs" `isSuffixOf` map toLower nm++ skipRemote nm+ | not onRemote = False+ | True = any (`isSuffixOf` map toLower nm) $ map (map toLower) skipList+ where skipList = [ "Interpolants.hs" -- The following test requires mathSAT, so can't run on remote+ , "HexPuzzle.hs" -- Doctest is way too slow on this with ghci loading, sigh+ , "MultMask.hs" -- Also, quite slow+ ]++-- Pick (about) the given percentage of files+pickPercentage :: Int -> [String] -> IO [String]+pickPercentage 100 xs = return xs+pickPercentage 0 _ = return []+pickPercentage p xs = concat <$> mapM pick xs+ where pick f = do c <- randomRIO (0, 100)+ return [f | c >= p]
SBVTestSuite/SBVTest.hs view
@@ -12,6 +12,7 @@ import qualified TestSuite.Basics.AllSat import qualified TestSuite.Basics.ArithNoSolver import qualified TestSuite.Basics.ArithSolver+import qualified TestSuite.Basics.Assert import qualified TestSuite.Basics.BasicTests import qualified TestSuite.Basics.Exceptions import qualified TestSuite.Basics.GenBenchmark@@ -54,6 +55,8 @@ import qualified TestSuite.Optimization.ExtensionField import qualified TestSuite.Optimization.Quantified import qualified TestSuite.Optimization.Reals+import qualified TestSuite.Overflows.Arithmetic+import qualified TestSuite.Overflows.Casts import qualified TestSuite.Polynomials.Polynomials import qualified TestSuite.Puzzles.Coins import qualified TestSuite.Puzzles.Counts@@ -125,8 +128,10 @@ , TestSuite.Queries.Int_CVC4.tests , TestSuite.Queries.Int_Mathsat.tests , TestSuite.Queries.Int_Yices.tests- -- quick-check tests take a long time, so just run them locally.+ -- quick-check tests take a long time, so just run them locally: , TestSuite.QuickCheck.QC.tests+ -- interpolant tests require MathSAT, run locally:+ , TestSuite.Queries.Interpolants.tests ] -- | Remaining tests@@ -136,6 +141,7 @@ , TestSuite.Arrays.Query.tests , TestSuite.Basics.AllSat.tests , TestSuite.Basics.ArithNoSolver.tests+ , TestSuite.Basics.Assert.tests , TestSuite.Basics.BasicTests.tests , TestSuite.Basics.Exceptions.testsRemote , TestSuite.Basics.GenBenchmark.tests@@ -178,6 +184,8 @@ , TestSuite.Optimization.ExtensionField.tests , TestSuite.Optimization.Quantified.tests , TestSuite.Optimization.Reals.tests+ , TestSuite.Overflows.Arithmetic.tests+ , TestSuite.Overflows.Casts.tests , TestSuite.Polynomials.Polynomials.tests , TestSuite.Puzzles.Coins.tests , TestSuite.Puzzles.Counts.tests@@ -192,7 +200,6 @@ , TestSuite.Queries.Enums.tests , TestSuite.Queries.FreshVars.tests , TestSuite.Queries.Int_Z3.tests- , TestSuite.Queries.Interpolants.tests , TestSuite.Queries.Strings.tests , TestSuite.Queries.Uninterpreted.tests , TestSuite.Uninterpreted.AUF.tests
+ SBVTestSuite/TestSuite/Basics/Assert.hs view
@@ -0,0 +1,23 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.Assert+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test the sAssert feature.+-----------------------------------------------------------------------------++module TestSuite.Basics.Assert(tests) where++import Utils.SBVTestFramework++-- Test suite+tests :: TestTree+tests = testGroup "Basics.Assert"+ [ goldenCapturedIO "safe1" $ t $ \x -> sAssert Nothing "safe1" (x .> (2::SInteger)) (x .== 12)+ , goldenCapturedIO "safe2" $ t $ \x -> sAssert Nothing "safe2" (x .> (2::SInteger)) (12::SInteger)+ ]+ where t tc goldFile = do r <- safeWith z3{verbose=True, redirectVerbose=Just goldFile} tc+ appendFile goldFile ("\n FINAL: " ++ show r ++ "\nDONE!")
SBVTestSuite/TestSuite/Optimization/Combined.hs view
@@ -21,6 +21,7 @@ , goldenVsStringShow "combined2" (optimize Lexicographic combined2) , goldenVsStringShow "pareto1" (optimize (Pareto Nothing) pareto1) , goldenVsStringShow "pareto2" (optimize (Pareto (Just 30)) pareto2)+ , goldenVsStringShow "pareto3" (optimize (Pareto Nothing) pareto3) , goldenVsStringShow "boxed1" (optimize Independent boxed1) ] @@ -72,6 +73,15 @@ minimize "min_x" x maximize "max_y" y minimize "max_x_plus_y" $ x + y++pareto3 :: Goal+pareto3 = do x <- sInteger "x"++ constrain $ 1 .>= x+ constrain $ 0 .<= x++ minimize "min_x" x+ maximize "max_x_plus_x" $ x + x boxed1 :: Goal boxed1 = do x <- sReal "x"
+ SBVTestSuite/TestSuite/Overflows/Arithmetic.hs view
@@ -0,0 +1,246 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Overflows.Arithmetic+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for overflow checking+-----------------------------------------------------------------------------++{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++module TestSuite.Overflows.Arithmetic(tests) where++import Data.SBV+import Data.SBV.Dynamic+import Data.SBV.Internals (unSBV, SBV(..))++import Data.SBV.Tools.Overflow++import Utils.SBVTestFramework++-- Test suite+tests :: TestTree+tests = testGroup "Overflows" [testGroup "Arithmetic" ts]+ where ts = [ testGroup "add-uf" [ testCase "w8" $ assertIsThm $ underflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ underflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ underflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ underflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ underflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ underflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ underflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ underflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "add-of" [ testCase "w8" $ assertIsThm $ overflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ overflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ overflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ overflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ overflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ overflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ overflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ overflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "sub-uf" [ testCase "w8" $ assertIsThm $ underflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ underflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ underflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ underflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ underflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ underflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ underflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ underflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "sub-of" [ testCase "w8" $ assertIsThm $ overflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ overflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ overflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ overflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ overflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ overflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ overflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ overflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "mul-uf" [ testCase "w8" $ assertIsThm $ underflow svTimes (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ underflow svTimes (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ underflow svTimes (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ underflow svTimes (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "mul-of" [ testCase "w8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "div-uf" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ never svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ never svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ never svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ never svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "div-of" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ divChk svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ divChk svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ divChk svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ divChk svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool))+ ]+ , testGroup "neg-uf" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool))+ ]+ , testGroup "neg-of" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool))+ , testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool))+ , testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool))+ , testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool))+ , testCase "i8" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool))+ , testCase "i16" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool))+ , testCase "i32" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool))+ , testCase "i64" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool))+ ]+ ]++-- 256 bits is large enough to do all these proofs+large :: Int+large = 256++type SLarge = SVal++svNeg0 :: SLarge -> SLarge+svNeg0 v = z `svMinus` v+ where z = svInteger (KBounded (hasSign v) large) 0++exactlyWhen :: SBool -> SVal -> SBool+exactlyWhen (SBV a) b = SBV $ (a `svAnd` b) `svOr` (svNot a `svAnd` svNot b)++-- Properly extend to a dynamic large vector+toLarge :: SBV a -> SLarge+toLarge v+ | extra < 0 = error $ "toLarge: Unexpected size: " ++ show (n, large)+ | hasSign v = p `svJoin` dv+ | True = z `svJoin` dv+ where n = intSizeOf v+ extra = large - n++ dv = unSBV v+ mk = svInteger (KBounded True extra)+ z = mk 0+ o = mk (-1)+ pos = (dv `svTestBit` (n-1)) `svEqual` svFalse+ p = svIte pos z o++-- Multiplication checks are expensive. For these, we simply check that the SBV encodings and the z3 versions are equivalent+mulChkO :: forall a. (SymWord a) => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+mulChkO fast slow = do setLogic Logic_NONE+ x <- free "x"+ y <- free "y"++ let (_, ov1) = x `fast` y+ (_, ov2) = x `slow` y++ return $ ov1 .== ov2++-- Underflow mults+mulChkU :: forall a. (SymWord a) => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+mulChkU fast slow = do setLogic Logic_NONE+ x <- free "x"+ y <- free "y"++ let (uf1, _) = x `fast` y+ (uf2, _) = x `slow` y++ return $ uf1 .== uf2++-- Signed division can only underflow under one condition, check that simply instead of trying to do an expensive embedding proof+divChk :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+divChk _op cond = do x <- free "x"+ y <- free "y"++ let (_, overflowHappens) = x `cond` y++ special = (unSBV x `svEqual` topSet) `svAnd` (unSBV y `svEqual` neg1)++ n = intSizeOf x+ neg1 = svInteger (KBounded True n) (-1)+ topSet = svInteger (KBounded True n) (2^(n-1))++ return $ overflowHappens `exactlyWhen` special++-- For a few cases, we expect them to "never" overflow. The "embedding proofs" are either too expensive (in case of division), or+-- not possible (in case of negation). We capture these here.+never :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+never _op cond = do x <- free "x"+ y <- free "y"++ let (underflowHappens, _) = x `cond` y++ return $ underflowHappens `exactlyWhen` svFalse++never1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate+never1 _op cond = do x <- free "x"++ let (underflowHappens, _) = cond x++ return $ underflowHappens `exactlyWhen` svFalse++underflow :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+underflow op cond = do x <- free "x"+ y <- free "y"++ let (underflowHappens, _) = x `cond` y++ extResult :: SLarge+ extResult = toLarge x `op` toLarge y+++ return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))++overflow :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate+overflow op cond = do x <- free "x"+ y <- free "y"++ let (_, overflowHappens) = x `cond` y++ extResult :: SLarge+ extResult = toLarge x `op` toLarge y++ return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))++underflow1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate+underflow1 op cond = do x <- free "x"++ let (underflowHappens, _) = cond x++ extResult :: SLarge+ extResult = op $ toLarge x++ return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))++overflow1 :: forall a. (Integral a, Bounded a, SymWord a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate+overflow1 op cond = do x <- free "x"++ let (_, overflowHappens) = cond x++ extResult :: SLarge+ extResult = op $ toLarge x++ return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))++{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
+ SBVTestSuite/TestSuite/Overflows/Casts.hs view
@@ -0,0 +1,134 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Overflows.Casts+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for overflow checking+-----------------------------------------------------------------------------++{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++module TestSuite.Overflows.Casts(tests) where++import Data.SBV+import Data.SBV.Tools.Overflow++import Utils.SBVTestFramework++type C a b = SBV a -> (SBV b, (SBool, SBool))++getBounds :: (Bounded a, Integral a) => a -> Maybe (Integer, Integer)+getBounds x = Just (fromIntegral (minBound `asTypeOf` x), fromIntegral (maxBound `asTypeOf` x))++-- Test suite+tests :: TestTree+tests = testGroup "Overflows" [testGroup "Casts" ts]+ where ts = [ testGroup "w8" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word8 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word8 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word8 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word8 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Word8 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word8 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word8 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word8 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Word8 Integer)+ ]+ , testGroup "w16" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word16 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word16 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word16 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word16 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Word16 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word16 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word16 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word16 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Word16 Integer)+ ]+ , testGroup "w32" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word32 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word32 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word32 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word32 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Word32 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word32 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word32 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word32 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Word32 Integer)+ ]+ , testGroup "w64" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Word64 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Word64 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Word64 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Word64 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Word64 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Word64 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Word64 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Word64 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Word64 Integer)+ ]+ , testGroup "i8" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int8 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int8 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int8 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int8 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Int8 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int8 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int8 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int8 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Int8 Integer)+ ]+ , testGroup "i16" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int16 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int16 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int16 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int16 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Int16 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int16 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int16 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int16 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Int16 Integer)+ ]+ , testGroup "i32" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int32 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int32 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int32 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int32 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Int32 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int32 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int32 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int32 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Int32 Integer)+ ]+ , testGroup "i64" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Int64 Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Int64 Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Int64 Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Int64 Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Int64 Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Int64 Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Int64 Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Int64 Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Int64 Integer)+ ]+ , testGroup "i" [ testCase "w8" $ assertIsThm $ chk (getBounds (undefined :: Word8 )) (sFromIntegralO :: C Integer Word8)+ , testCase "w16" $ assertIsThm $ chk (getBounds (undefined :: Word16)) (sFromIntegralO :: C Integer Word16)+ , testCase "w32" $ assertIsThm $ chk (getBounds (undefined :: Word32)) (sFromIntegralO :: C Integer Word32)+ , testCase "w64" $ assertIsThm $ chk (getBounds (undefined :: Word64)) (sFromIntegralO :: C Integer Word64)+ , testCase "i8" $ assertIsThm $ chk (getBounds (undefined :: Int8 )) (sFromIntegralO :: C Integer Int8)+ , testCase "i16" $ assertIsThm $ chk (getBounds (undefined :: Int16 )) (sFromIntegralO :: C Integer Int16)+ , testCase "i32" $ assertIsThm $ chk (getBounds (undefined :: Int32 )) (sFromIntegralO :: C Integer Int32)+ , testCase "i64" $ assertIsThm $ chk (getBounds (undefined :: Int64 )) (sFromIntegralO :: C Integer Int64)+ , testCase "i" $ assertIsThm $ chk Nothing (sFromIntegralO :: C Integer Integer)+ ]+ ]++chk :: forall a b. (SymWord a, SymWord b, Integral a, Integral b) => Maybe (Integer, Integer) -> (SBV a -> (SBV b, (SBool, SBool))) -> Predicate+chk mb cvt = do (x :: SBV a) <- free "x"++ let (_ :: SBV b, (uf, ov)) = cvt x++ ix :: SInteger+ ix = sFromIntegral x++ (ufCorrect, ovCorrect) = case mb of+ Nothing -> (uf .== false, ov .== false)+ Just (lb, ub) -> (uf <=> ix .< literal lb, ov <=> ix .> literal ub)++ return $ ufCorrect &&& ovCorrect
SBVTestSuite/TestSuite/Queries/Interpolants.hs view
@@ -7,6 +7,7 @@ -- Stability : experimental -- -- Testing a few interpolant computations.+-- ----------------------------------------------------------------------------- {-# LANGUAGE ScopedTypeVariables #-} @@ -22,15 +23,16 @@ testGroup "Basics.QueryInterpolants" [ goldenCapturedIO "query_Interpolant1" $ testQuery q1 , goldenCapturedIO "query_Interpolant2" $ testQuery q2- , goldenCapturedIO "query_Interpolant3" $ testQuery q3- , goldenCapturedIO "query_Interpolant4" $ testQuery q4 ] testQuery :: Show a => Symbolic a -> FilePath -> IO ()-testQuery t rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t+testQuery t rf = do r <- runSMTWith mathSAT{verbose=True, redirectVerbose=Just rf} t appendFile rf ("\nFINAL OUTPUT:\n" ++ show r ++ "\n") -q1 :: Symbolic [String]+iConstraint :: String -> SBool -> Symbolic ()+iConstraint g = constrainWithAttribute [(":interpolation-group", g)]++q1 :: Symbolic String q1 = do a <- sInteger "a" b <- sInteger "b" c <- sInteger "c"@@ -38,13 +40,13 @@ setOption $ ProduceInterpolants True - namedConstraint "c1" $ a .== b &&& a .== c- namedConstraint "c2" $ b .== d &&& bnot (c .== d)+ iConstraint "c1" $ a .== b &&& a .== c+ iConstraint "c2" $ b .== d &&& bnot (c .== d) query $ do _ <- checkSat- getInterpolant ["c1", "c2"]+ getInterpolant ["c1"] -q2 :: Symbolic [String]+q2 :: Symbolic String q2 = do a <- sInteger "a" b <- sInteger "b" c <- sInteger "c"@@ -56,42 +58,10 @@ setOption $ ProduceInterpolants True - namedConstraint "c1" $ f a .== c &&& f b .== d- namedConstraint "c2" $ a .== b &&& g c ./= g d-- query $ do _ <- checkSat- getInterpolant ["c1", "c2"]--q3 :: Symbolic [String]-q3 = do x <- sInteger "x"- y <- sInteger "y"- z <- sInteger "z"-- a :: SArray Integer Integer <- newArray "a"- b :: SArray Integer Integer <- newArray "b"-- namedConstraint "c1" $ b .== writeArray (writeArray a x 0) y (0::SInteger)- namedConstraint "c2" $ z .== x &&& readArray b z .== 1-- setOption $ ProduceInterpolants True-- query $ do _ <- checkSat- getInterpolant ["c1", "c2"]--q4 :: Symbolic [String]-q4 = do a <- sInteger "a"- b <- sInteger "b"- c <- sInteger "c"- d <- sInteger "d"- e <- sInteger "e"-- namedConstraint "c1" $ a .== b &&& a .== c- namedConstraint "c2" $ c .== d- namedConstraint "c3" $ b .== e &&& d ./= e-- setOption $ ProduceInterpolants True+ iConstraint "c1" $ f a .== c &&& f b .== d+ iConstraint "c2" $ a .== b &&& g c ./= g d query $ do _ <- checkSat- getInterpolant ["c1", "c2", "c3"]+ getInterpolant ["c1"] {-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 7.8+Version: 7.9 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@@ -61,6 +61,7 @@ , Data.SBV.RegExp , Data.SBV.Tools.CodeGen , Data.SBV.Tools.GenTest+ , Data.SBV.Tools.Overflow , Data.SBV.Tools.Polynomial , Data.SBV.Tools.STree , Documentation.SBV.Examples.BitPrecise.BitTricks@@ -168,6 +169,7 @@ , TestSuite.Basics.AllSat , TestSuite.Basics.ArithNoSolver , TestSuite.Basics.ArithSolver+ , TestSuite.Basics.Assert , TestSuite.Basics.BasicTests , TestSuite.Basics.Exceptions , TestSuite.Basics.GenBenchmark@@ -210,6 +212,8 @@ , TestSuite.Optimization.ExtensionField , TestSuite.Optimization.Quantified , TestSuite.Optimization.Reals+ , TestSuite.Overflows.Arithmetic+ , TestSuite.Overflows.Casts , TestSuite.Polynomials.Polynomials , TestSuite.Puzzles.Coins , TestSuite.Puzzles.Counts@@ -243,7 +247,7 @@ Test-Suite SBVDocTest Build-Depends: base, directory, filepath, random- , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck+ , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, random , sbv default-language: Haskell2010 Hs-Source-Dirs : SBVTestSuite