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