1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Basics.Exceptions
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test the exception mechanism
-----------------------------------------------------------------------------
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Basics.Exceptions(testsLocal, testsRemote) where
import Data.SBV.Control
import Utils.SBVTestFramework
import qualified Control.Exception as C
-- Test suite
testsLocal :: TestTree
testsLocal =
testGroup "Basics.exceptions.local"
[ goldenCapturedIO "exceptionLocal1" yicesExc
, goldenCapturedIO "exceptionLocal2" z3Exc1
]
-- Yices throws an exception for this since exponent is too large
yicesExc :: FilePath -> IO ()
yicesExc rf = runSMTWith yices{verbose=True, redirectVerbose=Just rf} exc
`C.catch` \(e :: SBVException) -> do appendFile rf "CAUGHT SMT EXCEPTION"
appendFile rf (show e)
where exc = do x <- sWord32 "x"
constrain $ lsb x .=> (x * (x .^ (-1::SWord32))) .== 1
query $ do cs <- checkSat
cs `seq` return ()
testsRemote :: TestTree
testsRemote =
testGroup "Basics.exceptions.remote"
[ goldenCapturedIO "exceptionRemote1" z3Exc2
]
-- Create the case where we ask for integer-logic, but use reals
z3Exc1 :: FilePath -> IO ()
z3Exc1 rf = runSMTWith z3{verbose=True, redirectVerbose=Just rf} exc
`C.catch` \(e :: SBVException) -> do appendFile rf "CAUGHT SMT EXCEPTION"
appendFile rf (show e)
where exc = do setLogic QF_LIA
x <- sReal "x"
constrain $ x .== 2
query $ do cs <- checkSat
cs `seq` return ()
-- Similar to above, except linear logic, but use non-linear constructs
z3Exc2 :: FilePath -> IO ()
z3Exc2 rf = do r <- runSMT z3ExcCatch `C.catch` \(e :: SBVException) -> return ("OK, we got: " ++ sbvExceptionDescription e)
appendFile rf ("\nFINAL: " ++ show r ++ "\nDONE!\n")
where z3ExcCatch = do setLogic QF_LIA
x <- sInteger "x"
y <- sInteger "y"
query $ do constrain $ x*y .== x*x
show <$> checkSat
{- HLint ignore module "Reduce duplication" -}
|
