File: SolverParserTest.hs

package info (click to toggle)
haskell-what4 1.5.1-4
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 2,240 kB
  • sloc: haskell: 34,630; makefile: 5
file content (69 lines) | stat: -rw-r--r-- 2,468 bytes parent folder | download
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)
    ]