{-# 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, QueuingFlag (..), 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 forall a b. (a -> b) -> a -> b
$ do
    QueuingFlag
queuing <- [QueuingFlag
NoQueuing, QueuingFlag
Queuing]
    forall (m :: * -> *) a. Monad m => a -> m a
return
      forall a b. (a -> b) -> a -> b
$ String -> [TestTree] -> TestTree
testGroup
        ( case QueuingFlag
queuing of
            QueuingFlag
Queuing -> String
"queuing"
            QueuingFlag
NoQueuing -> String
"no queuing"
        )
      forall a b. (a -> b) -> a -> b
$ do
        Source
source <- [Source]
sources
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
          String -> Assertion -> TestTree
testCase (Source -> String
Src.name Source
source) forall a b. (a -> b) -> a -> b
$
            (Backend -> Assertion) -> Assertion
with forall a b. (a -> b) -> a -> b
$ \Backend
backend -> do
              Solver
solver <- QueuingFlag -> Backend -> IO Solver
initSolver QueuingFlag
queuing Backend
backend
              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)"
              forall (m :: * -> *) a. Monad m => a -> m a
return ()