{-# LANGUAGE OverloadedStrings #-}

-- | A module providing functions useful for testing a backend for SimpleSMT.
module SMTLIB.Backends.Tests
  ( testBackend,
    Src.Source (..),
    Src.sources,
  )
where

import SMTLIB.Backends (Backend, command, initSolver)
import qualified SMTLIB.Backends.Tests.Sources as Src
import Test.Tasty
import Test.Tasty.HUnit

-- | Test a backend by using it to run a list of examples.
testBackend ::
  -- | The name of the test group.
  String ->
  -- | A list of examples on which to run the backend.
  [Src.Source] ->
  -- | A function that should create a backend, run a given
  -- computation and release the backend's resources.
  ((Backend -> Assertion) -> Assertion) ->
  TestTree
testBackend :: String
-> [Source] -> ((Backend -> Assertion) -> Assertion) -> TestTree
testBackend String
name [Source]
sources (Backend -> Assertion) -> Assertion
with =
  String -> [TestTree] -> TestTree
testGroup String
name ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ do
    Bool
lazyMode <- [Bool
False, Bool
True]
    TestTree -> [TestTree]
forall (m :: * -> *) a. Monad m => a -> m a
return (TestTree -> [TestTree]) -> TestTree -> [TestTree]
forall a b. (a -> b) -> a -> b
$
      String -> [TestTree] -> TestTree
testGroup
        ( if Bool
lazyMode
            then String
"lazy"
            else String
"eager"
        )
        ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$ do
          Source
source <- [Source]
sources
          TestTree -> [TestTree]
forall (m :: * -> *) a. Monad m => a -> m a
return (TestTree -> [TestTree]) -> TestTree -> [TestTree]
forall a b. (a -> b) -> a -> b
$
            String -> Assertion -> TestTree
testCase (Source -> String
Src.name Source
source) (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
              (Backend -> Assertion) -> Assertion
with ((Backend -> Assertion) -> Assertion)
-> (Backend -> Assertion) -> Assertion
forall a b. (a -> b) -> a -> b
$ \Backend
backend -> do
                Solver
solver <- Backend -> Bool -> IO Solver
initSolver Backend
backend Bool
lazyMode
                Source -> Solver -> Assertion
Src.run Source
source Solver
solver
                -- ensure the sources consisting only of queued commands also run
                ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-info :name)"
                () -> Assertion
forall (m :: * -> *) a. Monad m => a -> m a
return ()