1-----------------------------------------------------------------------------
2-- |
3-- Module    : TestSuite.Transformers.SymbolicEval
4-- Copyright : (c) Brian Schroeder
5-- License   : BSD3
6-- Maintainer: erkokl@gmail.com
7-- Stability : experimental
8--
9-- Test suite for Documentation.SBV.Examples.Transformers.SymbolicEval
10-----------------------------------------------------------------------------
11
12{-# OPTIONS_GHC -Wall -Werror #-}
13
14module TestSuite.Transformers.SymbolicEval(tests) where
15
16import Control.Monad.Except (ExceptT, runExceptT, throwError)
17import Data.Either          (isLeft)
18
19import Data.SBV.Trans         (runSMT, sat)
20import Data.SBV.Trans.Control (query)
21
22import Documentation.SBV.Examples.Transformers.SymbolicEval
23import Utils.SBVTestFramework                               hiding (runSMT, sat)
24
25isSat :: SatResult -> Bool
26isSat (SatResult Unsatisfiable{}) = False
27isSat (SatResult Satisfiable{})   = True
28isSat _                           = error "isSat: Unexpected result!"
29
30-- Test suite
31tests :: TestTree
32tests = testGroup "Transformers.SymbolicEval"
33    [ testCase "alloc success" $ assert $
34          (== Right True) . fmap isSat <$>
35            runExceptT (sat $ (.< 5) <$> runAlloc (alloc "x") :: ExceptT String IO SatResult)
36
37    , testCase "alloc failure" $ assert $
38          (== Left "tried to allocate unnamed value") <$>
39              runExceptT (runSMT (runAlloc (alloc "")))
40
41    , testCase "query success" $ assert $
42          (== Right (Just True)) . fmap unliteral <$>
43              runExceptT (runSMT (query (runQ (pure $ (5 :: SInt8) .< 6))))
44
45    , testCase "query failure" $ assert $
46          isLeft <$>
47              runExceptT (runSMT (query (runQ $ throwError "oops")))
48
49    , testCase "combined success" $ assert $
50          (== Right (Counterexample 0 9)) <$>
51              check (Program  $ Var "x" `Plus` Lit 1 `Plus` Var "y")
52                    (Property $ Var "result" `LessThan` Lit 10)
53
54    , testCase "combined failure" $ assert $
55          (== Left "unknown variable") <$>
56              check (Program  $ Var "notAValidVar")
57                    (Property $ Var "result" `LessThan` Lit 10)
58    ]
59