1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
|
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
import Control.Monad.Catch ( SomeException, try )
import qualified Data.Text.IO as TIO
import Numeric.Natural
import qualified System.IO.Streams as Streams
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.Ingredients
import Test.Tasty.Sugar
import What4.Expr.Builder ( emptySymbolVarBimap )
import What4.ProblemFeatures ( noFeatures )
import What4.Protocol.SMTLib2.Response ( SMTResponse, getLimitedSolverResponse )
import qualified What4.Protocol.SMTLib2.Syntax as SMT2
import What4.Protocol.SMTWriter
sugarCube :: CUBE
sugarCube = mkCUBE { inputDirs = [ "test/responses" ]
, rootName = "*.rsp"
, expectedSuffix = ".exp"
, validParams = [ ("parsing", Just ["strict", "lenient"])
]
}
ingredients :: [Ingredient]
ingredients = includingOptions sugarOptions :
sugarIngredients [sugarCube] <>
defaultIngredients
main :: IO ()
main = do testSweets <- findSugar sugarCube
defaultMainWithIngredients ingredients .
testGroup "solver response tests" =<<
withSugarGroups testSweets testGroup mkTest
mkTest :: Sweets -> Natural -> Expectation -> IO [TestTree]
mkTest s n e = do
expect <- readFile $ expectedFile e
let strictness =
let strictVal pmtch =
if paramMatchVal "strict" pmtch
then Strict
else if paramMatchVal "lenient" pmtch
then Lenient
else error "Invalid strictness specification"
in maybe Strict strictVal $ lookup "parsing" $ expParamsMatch e
return
[
testCase (rootMatchName s <> " #" <> show n) $ do
inpStrm <- Streams.makeInputStream $ Just <$> TIO.readFile (rootFile s)
outStrm <- Streams.makeOutputStream $ \_ -> error "output not supported for test"
w <- newWriterConn
outStrm
inpStrm
(AckAction $ undefined)
"test-solver"
strictness
noFeatures
emptySymbolVarBimap
()
actual <- try $ getLimitedSolverResponse "test resp" Just w (SMT2.Cmd "test cmd")
expect @=? show (actual :: Either SomeException SMTResponse)
]
|