sbv-7.10: SBVTestSuite/TestSuite/Uninterpreted/AUF.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  TestSuite.Uninterpreted.AUF
-- Copyright   :  (c) Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Test suite for Documentation.SBV.Examples.Uninterpreted.AUF
-----------------------------------------------------------------------------

module TestSuite.Uninterpreted.AUF where

import Documentation.SBV.Examples.Uninterpreted.AUF

import Utils.SBVTestFramework

-- Test suite
tests :: TestTree
tests =
  testGroup "Uninterpreted.AUF"
    [ goldenVsStringShow "auf-0" $ runSAT      $ newArray "a" Nothing >>= \a -> free "x" >>= \x -> free "y" >>= \y -> output (thm x y (a :: SFunArray  Word32 Word32))
    , goldenVsStringShow "auf-1" $ runSAT      $ newArray "a" Nothing >>= \a -> free "x" >>= \x -> free "y" >>= \y -> output (thm x y (a :: SArray     Word32 Word32))
    , testCase "tc_auf-0"        $ assertIsThm $ newArray "a" Nothing >>= \a -> free "x" >>= \x -> free "y" >>= \y -> return (thm x y (a :: SArray     Word32 Word32))
    , testCase "tc_auf-1"        $ assertIsThm $ newArray "a" Nothing >>= \a -> free "x" >>= \x -> free "y" >>= \y -> return (thm x y (a :: SFunArray  Word32 Word32))
    ]