{-# LANGUAGE OverloadedStrings #-}
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
testBackend ::
String ->
[Src.Source] ->
((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
ByteString
_ <- Solver -> Builder -> IO ByteString
command Solver
solver Builder
"(get-info :name)"
forall (m :: * -> *) a. Monad m => a -> m a
return ()