content: {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TemplateHaskell #-}
  module Test.Smtlib (smtlibTestGroup) where
  
  import Control.DeepSeq
  import Control.Monad
  import qualified Data.Set as Set
  
  import Test.Tasty
  import Test.Tasty.QuickCheck hiding (Success)
  import Test.Tasty.HUnit
  import Test.Tasty.TH
  
  import Smtlib.Syntax.Syntax
  import Smtlib.Syntax.ShowSL
  import Smtlib.Parsers.CommonParsers
  import Smtlib.Parsers.CommandsParsers
  import Smtlib.Parsers.ResponseParsers
  import Text.Parsec (parse)
  
  
  prop_parseTerm :: Property
  prop_parseTerm = forAll arbitrary $ \(t :: Term) ->
    parse parseTerm "" (showSL t) == Right t
  
  prop_parseAttribute :: Property
  prop_parseAttribute = forAll arbitrary $ \a ->
    parse parseAttribute "" (showSL a) == Right a
  
  prop_parseSort :: Property
  prop_parseSort = forAll arbitrary $ \s ->
    parse parseSort "" (showSL s) == Right s
  
  prop_parseIdentifier :: Property
  prop_parseIdentifier = forAll arbitrary $ \a ->
    parse parseIdentifier "" (showSL a) == Right a
  
  prop_parseSexpr :: Property
  prop_parseSexpr = forAll arbitrary $ \a ->
    parse parseSexpr "" (showSL a) == Right a
  
  prop_parseSpecConstant :: Property
  prop_parseSpecConstant = forAll arbitrary $ \a ->
    parse parseSpecConstant "" (showSL a) == Right a
  
  prop_parseSource :: Property
  prop_parseSource = forAll arbitrary $ \a ->
    parse parseSource "" (joinA a) == Right a
  
  prop_parseCommand :: Property
  prop_parseCommand = forAll arbitrary $ \a ->
    parse parseCommand "" (showSL a) == Right a
  
  prop_parseOption :: Property
  prop_parseOption = forAll arbitrary $ \a ->
    parse parseOption "" (showSL a) == Right a
  
  prop_parseInfoFlags :: Property
  prop_parseInfoFlags = forAll arbitrary $ \a ->
    parse parseOption "" (showSL a) == Right a
  
  prop_parseCmdResult :: Property
  prop_parseCmdResult = forAll arbitrary $ \(a :: CmdResponse) ->
    case parse parseCmdResult "" (showSL a) of
      Left err -> error (show err)
      Right a' -> parse parseCmdResult "" (showSL a') == Right a'
  
  prop_parseGenResponse :: Property
  prop_parseGenResponse = forAll arbitrary $ \a ->
    parse parseGenResponse "" (showSL a) == Right a
  
  prop_parseGetInfoResponse :: Property
  prop_parseGetInfoResponse = forAll arbitrary $ \a ->
    parse parseGetInfoResponse "" ("(" ++ joinA a ++ ")") == Right a
  
  prop_parseCheckSatResponse :: Property
  prop_parseCheckSatResponse = forAll arbitrary $ \a ->
    parse parseCheckSatResponse "" (showSL a) == Right a
  
  prop_parseGetAssertionsResponse :: Property
  prop_parseGetAssertionsResponse = forAll genGetAssertionsResponse $ \a ->
    parse parseGetAssertionsResponse "" ("(" ++ joinA a ++ ")") == Right a
  
  prop_parseGetAssignmentResp :: Property
  prop_parseGetAssignmentResp = forAll arbitrary $ \a ->
    parse parseGetAssignmentResp "" ("(" ++ joinA a ++ ")") == Right a
  
  prop_parseGetProofResponse :: Property
  prop_parseGetProofResponse = forAll arbitrary $ \a ->
    parse parseGetProofResponse "" (showSL a) == Right a
  
  prop_parseGetUnsatCoreResp :: Property
  prop_parseGetUnsatCoreResp = forAll genGetUnsatCoreResponse $ \a ->
    parse parseGetUnsatCoreResp "" ("(" ++ unwords (fmap showSymbol a) ++ ")") == Right a
  
  prop_parseGetUnsatAssumptionsResp :: Property
  prop_parseGetUnsatAssumptionsResp = forAll (listOf' genSymbol) $ \a ->
    parse parseGetUnsatCoreResp "" ("(" ++ unwords (fmap showSymbol a) ++ ")") == Right a
  
  prop_parseGetValueResponse :: Property
  prop_parseGetValueResponse = forAll genGetValueResponse $ \a ->
    parse parseGetValueResponse "" ("(" ++ joinA a ++ ")") == Right a
  
  prop_parseGetModelResponse :: Property
  prop_parseGetModelResponse = forAll genGetModelResponse $ \a ->
    parse parseGetModelResponse "" ("(" ++ joinA a ++ ")") == Right a
  
  prop_parseGetOptionResponse :: Property
  prop_parseGetOptionResponse = forAll arbitrary $ \a ->
    parse parseGetOptionResponse "" (showSL a) == Right a
  
  prop_parseEchoResponse :: Property
  prop_parseEchoResponse = forAll genEchoResponse $ \a ->
    parse parseEchoResponse "" a == Right a
  
  case_bug_1 :: Assertion
  case_bug_1 = do
    parse parseSort "" "(_a b)" @?= Right (SortIdentifiers (ISymbol "_a") [SortId (ISymbol "b")])
    parse parseTerm "" "(_a b)" @?= Right (TermQualIdentifierT (QIdentifier (ISymbol "_a")) [TermQualIdentifier (QIdentifier (ISymbol "b"))])
  
  case_bug_2 :: Assertion
  case_bug_2 = do
    parse parseTerm "" "(asX b)" @?= Right (TermQualIdentifierT (QIdentifier (ISymbol "asX")) [TermQualIdentifier (QIdentifier (ISymbol "b"))])
  
  case_parse_string_literal_ascii :: Assertion
  case_parse_string_literal_ascii = parse str "" s @?= Right s
    where
      s = showStringLiteral $ ['\t','\n','\r'] ++ [toEnum 32 .. toEnum 126]
  
  prop_parse_string_literal :: Property
  prop_parse_string_literal =
    forAll genStringLiteral $  \s ->
      parse str "" s == Right s
  
  case_parseSexprKeyword_bug :: Assertion
  case_parseSexprKeyword_bug =
    parse parseSexprKeyword "" ":keyword" @?= Right (SexprKeyword ":keyword")
  
  case_parseHexadecimal :: Assertion
  case_parseHexadecimal = parse parseHexadecimal "" (showSL s) @?= Right s
    where
      s = SpecConstantHexadecimal "afbf00"
  
  case_parseBinary :: Assertion
  case_parseBinary = parse parseBinary "" (showSL s) @?= Right s
    where
      s = SpecConstantBinary "011001"
  
  case_comment :: Assertion
  case_comment = do
    parse parseTerm "" "(f ; hogehoge\na;bbb\n)" @?=
      Right (TermQualIdentifierT (QIdentifier (ISymbol "f")) [TermQualIdentifier (QIdentifier (ISymbol "a"))])
  
  -- ---------------------------------------------------------------------
  
  prop_Command_show :: Property
  prop_Command_show = forAll arbitrary $ \(a :: Command) ->
    show a `deepseq` True
  
  prop_Option_show :: Property
  prop_Option_show = forAll arbitrary $ \(a :: Option) ->
    show a `deepseq` True
  
  prop_InfoFlags_show :: Property
  prop_InfoFlags_show = forAll arbitrary $ \(a :: InfoFlags) ->
    show a `deepseq` True
  
  prop_Term_show :: Property
  prop_Term_show = forAll arbitrary $ \(a :: Term) ->
    show a `deepseq` True
  
  prop_VarBinding_show :: Property
  prop_VarBinding_show = forAll arbitrary $ \(a :: VarBinding) ->
    show a `deepseq` True
  
  prop_SortedVar_show :: Property
  prop_SortedVar_show = forAll arbitrary $ \(a :: VarBinding) ->
    show a `deepseq` True
  
  prop_QualIdentifier_show :: Property
  prop_QualIdentifier_show = forAll arbitrary $ \(a :: QualIdentifier) ->
    show a `deepseq` True
  
  prop_FunDec_show :: Property
  prop_FunDec_show = forAll arbitrary $ \(a :: FunDec) ->
    show a `deepseq` True
  
  prop_AttrValue_show :: Property
  prop_AttrValue_show = forAll arbitrary $ \(a :: AttrValue) ->
    show a `deepseq` True
  
  prop_Attribute_show :: Property
  prop_Attribute_show = forAll arbitrary $ \(a :: Attribute) ->
    show a `deepseq` True
  
  prop_Index_show :: Property
  prop_Index_show = forAll arbitrary $ \(a :: Index) ->
    show a `deepseq` True
  
  prop_Identifier_show :: Property
  prop_Identifier_show = forAll arbitrary $ \(a :: Identifier) ->
    show a `deepseq` True
  
  prop_Sort_show :: Property
  prop_Sort_show = forAll arbitrary $ \(a :: Sort) ->
    show a `deepseq` True
  
  prop_SpecConstant_show :: Property
  prop_SpecConstant_show = forAll arbitrary $ \(a :: SpecConstant) ->
    show a `deepseq` True
  
  prop_Sexpr_show :: Property
  prop_Sexpr_show = forAll arbitrary $ \(a :: Sexpr) ->
    show a `deepseq` True
  
  prop_CmdResponse_show :: Property
  prop_CmdResponse_show = forAll arbitrary $ \(a :: CmdResponse) ->
    show a `deepseq` True
  
  prop_GenResponse_show :: Property
  prop_GenResponse_show = forAll arbitrary $ \(a :: GenResponse) ->
    show a `deepseq` True
  
  prop_ErrorBehavior_show :: Property
  prop_ErrorBehavior_show = forAll arbitrary $ \(a :: ErrorBehavior) ->
    show a `deepseq` True
  
  prop_ReasonUnknown_show :: Property
  prop_ReasonUnknown_show = forAll arbitrary $ \(a :: ReasonUnknown) ->
    show a `deepseq` True
  
  prop_CheckSatResponse_show :: Property
  prop_CheckSatResponse_show = forAll arbitrary $ \(a :: CheckSatResponse) ->
    show a `deepseq` True
  
  prop_InfoResponse_show :: Property
  prop_InfoResponse_show = forAll arbitrary $ \(a :: InfoResponse) ->
    show a `deepseq` True
  
  prop_ValuationPair_show :: Property
  prop_ValuationPair_show = forAll arbitrary $ \(a :: ValuationPair) ->
    show a `deepseq` True
  
  prop_TValuationPair_show :: Property
  prop_TValuationPair_show = forAll arbitrary $ \(a :: TValuationPair) ->
    show a `deepseq` True
  
  -- ---------------------------------------------------------------------
  
  instance Arbitrary Term where
    arbitrary = sized $ \n -> oneof $
      [ TermSpecConstant <$> arbitrary
      , TermQualIdentifier <$> arbitrary
      ] ++ (if n > 0 then gs else [])
      where
        gs =
          [ liftM2 TermQualIdentifierT arbitrary (listOf1' arbitrary')
          , liftM2 TermLet (listOf1' arbitrary) arbitrary'
          , liftM2 TermForall (listOf1' arbitrary) arbitrary'
          , liftM2 TermExists (listOf1' arbitrary) arbitrary'
          , liftM2 TermAnnot arbitrary' (listOf1' arbitrary)
          ]
  
  instance Arbitrary VarBinding where
    arbitrary = liftM2 VB genSymbol arbitrary'
  
  instance Arbitrary SortedVar where
    arbitrary = liftM2 SV genSymbol arbitrary
  
  instance Arbitrary AttrValue where
    arbitrary = oneof
      [ AttrValueConstant <$> arbitrary
      , AttrValueSymbol <$> genSymbol
      , AttrValueSexpr <$> listOf' arbitrary
      ]
  
  instance Arbitrary Attribute where
    arbitrary = oneof
      [ Attribute <$> genKeyword
      , liftM2 AttributeVal genKeyword arbitrary
      ]
  
  instance Arbitrary QualIdentifier where
    arbitrary = oneof
      [ QIdentifier <$> arbitrary
      , liftM2 QIdentifierAs arbitrary arbitrary
      ]
  
  instance Arbitrary Index where
    arbitrary = oneof
      [ IndexNumeral <$> abs <$> arbitrary
      , IndexSymbol <$> genSymbol
      ]
  
  instance Arbitrary Identifier where
    arbitrary = oneof
      [ ISymbol <$> genSymbol
      , liftM2 I_Symbol genSymbol (listOf1' arbitrary)
      ]
  
  instance Arbitrary Sort where
    arbitrary = oneof
      [ SortId <$> arbitrary
      , liftM2 SortIdentifiers arbitrary (listOf1' arbitrary')
      ]
  
  instance Arbitrary SpecConstant where
    arbitrary = oneof
      [ SpecConstantNumeral <$> abs <$> arbitrary
      , liftM SpecConstantDecimal $ do
          a <- show <$> abs <$> (arbitrary :: Gen Int)
          b <- listOf $ return '0'
          c <- show <$> abs <$> (arbitrary :: Gen Int)
          return $ a ++ "." ++ b ++ c
      , SpecConstantHexadecimal <$> listOf1 (elements (['0'..'9'] ++ ['a'..'f'] ++ ['A'..'F']))
      , SpecConstantBinary <$> listOf1 (elements ['0','1'])
      , liftM SpecConstantString $ do
          let p c = c `elem` ['\t','\n','\r'] || (32 <= fromEnum c && fromEnum c <= 126) || 128 <= fromEnum c
          s <- listOf $ arbitrary `suchThat` p
          return $ "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- s] ++ "\""
      ]
  
  instance Arbitrary Sexpr where
    arbitrary = sized $ \n -> oneof $
      [ SexprSpecConstant <$> arbitrary
      , SexprSymbol <$> genSymbol
      , SexprKeyword <$> genKeyword
      ] ++
      [ liftM SexprSxp $ listOf' arbitrary' | n > 0 ]
  
  halve :: Gen a -> Gen a
  halve g = sized (\n -> resize (n `div` 2) g)
  
  arbitrary' :: Arbitrary a => Gen a
  arbitrary' = halve arbitrary
  
  listOf' :: Gen a -> Gen [a]
  listOf' g = do
    n <- frequency [(6, return 0), (3, return 1), (1, return 2)]
    replicateM n g
  
  listOf1' :: Gen a -> Gen [a]
  listOf1' g = do
    n <- frequency [(10, return 1), (4, return 2), (1, return 3)]
    replicateM n g
  
  -- ---------------------------------------------------------------------
  
  type Symbol = String
  
  genSymbol :: Gen Symbol
  genSymbol = oneof [genSimpleSymbol, genQuotedSymbol]
  
  genSimpleSymbol :: Gen Symbol
  genSimpleSymbol = g `suchThat` (`Set.notMember` reserved)
    where
      xs = ['a'..'z']++['A'..'Z']++"~!@$%^&*_-+=<>.?/"
      g = liftM2 (:) (elements xs) (listOf1 $ elements $ ['0'..'9'] ++ xs)
      reserved = Set.fromList $
        ["BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "par"] ++
        ["set-logic", "set-option", "set-info", "declare-sort", "define-sort", "declare-const", "declare-fun", "declare-fun-rec", "declare-funs-rec", "push", "pop", "reset", "reset-assertions", "assert", "check-sat", "check-sat-assuming", "get-assertions", "get-model", "get-proof", "get-unsat-core", "get-unsat-assumptions", "get-value", "get-assignment", "get-option", "get-info", "echo", "exit"]
  
  genQuotedSymbol :: Gen Symbol
  genQuotedSymbol = listOf1 g
    where
      g :: Gen Char
      g = oneof [elements (Set.toList xs), choose (toEnum 128, maxBound)]
      xs = Set.fromList (['\t','\n','\r'] ++ [' ' .. toEnum 126]) `Set.difference` Set.fromList ['\\', '|']
  
  genKeyword :: Gen String
  genKeyword = oneof
    [ (':':) <$> genSimpleSymbol
    , elements
        [ ":print-success"
        , ":expand-definitions"
        , ":interactive-mode"
        , ":produce-proofs"
        , ":produce-unsat-cores"
        , ":produce-unsat-assumptions"
        , ":produce-models"
        , ":produce-assignments"
        , ":produce-assertions"
        , ":global-declarations"
        , ":regular-output-channel"
        , ":diagnostic-output-channel"
        , ":random-seed"
        , ":verbosity"
        , ":reproducible-resource-limit"
  
        , ":error-behavior"
        , ":name"
        , ":authors"
        , ":version"
        , ":status"
        , ":reason-unknown"
        , ":all-statistics"
        , ":assertion-stack-levels"
        ]
    ]
  
  genStringLiteral :: Gen String
  genStringLiteral = showStringLiteral <$> listOf genStringChar
  
  showStringLiteral :: String -> String
  showStringLiteral s = "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- s] ++ "\""
  
  genStringChar :: Gen Char
  genStringChar = arbitrary `suchThat` p
     where
      p c = c `elem` ['\t','\n','\r'] || (32 <= fromEnum c && fromEnum c <= 126) || 128 <= fromEnum c
  
  -- ---------------------------------------------------------------------
  
  instance Arbitrary Command where
    arbitrary = oneof
      [ SetLogic <$> genSymbol
      , SetOption <$> arbitrary
      , SetInfo <$> arbitrary
      , DeclareSort <$> genSymbol <*> (abs <$> arbitrary)
      , DefineSort <$> genSymbol <*> listOf' genSymbol <*> arbitrary
      , DeclareConst <$> genSymbol <*> arbitrary
      , DeclareFun <$> genSymbol <*> listOf' arbitrary <*> arbitrary
      , DefineFun <$> genSymbol <*> listOf' arbitrary <*> arbitrary <*> arbitrary
      , DefineFunRec <$> genSymbol <*> listOf' arbitrary <*> arbitrary <*> arbitrary
      , DefineFunsRec <$> listOf1' arbitrary <*> listOf1' arbitrary
      , Push <$> (abs <$> arbitrary)
      , Pop <$> (abs <$> arbitrary)
      , return Reset
      , return ResetAssertions
      , Assert <$> arbitrary
      , return CheckSat
      , CheckSatAssuming <$> listOf' arbitrary
      , return GetAssertions
      , return GetModel
      , return GetProof
      , return GetUnsatCore
      , return GetUnsatAssumptions
      , GetValue <$> listOf1' arbitrary
      , return GetAssignment
      , GetOption <$> genKeyword
      , GetInfo <$> arbitrary
      , Echo <$> genStringLiteral
      , return Exit
      ]
  
  instance Arbitrary Option where
    arbitrary = oneof
      [ PrintSuccess <$> arbitrary
      , ExpandDefinitions <$> arbitrary
      , InteractiveMode <$> arbitrary
      , ProduceProofs <$> arbitrary
      , ProduceUnsatCores <$> arbitrary
      , ProduceUnsatAssumptions <$> arbitrary
      , ProduceModels <$> arbitrary
      , ProduceAssignments <$> arbitrary
      , ProduceAssertions <$> arbitrary
      , GlobalDeclarations <$> arbitrary
      , RegularOutputChannel <$> genStringLiteral
      , DiagnosticOutputChannel <$> genStringLiteral
      , RandomSeed <$> (abs <$> arbitrary)
      , Verbosity <$> abs <$> arbitrary
      , ReproducibleResourceLimit <$> abs <$> arbitrary
      , OptionAttr <$> (arbitrary `suchThat` p)
      ]
      where
        p (Attribute kw) = kw `Set.notMember` reserved
        p (AttributeVal kw _) = kw `Set.notMember` reserved
        reserved = Set.fromList
          [ ":print-success"
          , ":expand-definitions"
          , ":interactive-mode"
          , ":produce-proofs"
          , ":produce-unsat-cores"
          , ":produce-unsat-assumptions"
          , ":produce-models"
          , ":produce-assignments"
          , ":produce-assertions"
          , ":global-declarations"
          , ":regular-output-channel"
          , ":diagnostic-output-channel"
          , ":random-seed"
          , ":verbosity"
          , ":reproducible-resource-limit"
          ]
  
  instance Arbitrary InfoFlags where
    arbitrary = oneof
      [ return ErrorBehavior
      , return Name
      , return Authors
      , return Version
      , return Status
      , return ReasonUnknown
      , return AllStatistics
      , return AssertionStackLevels
      , InfoFlags <$> (genKeyword `suchThat` (`Set.notMember` reserved))
      ]
      where
        reserved = Set.fromList
          [ ":error-behavior"
          , ":name"
          , ":authors"
          , ":version"
          , ":status"
          , ":reason-unknown"
          , ":all-statistics"
          , ":assertion-stack-levels"
          ]
  
  instance Arbitrary FunDec where
    arbitrary = FunDec <$> genSymbol <*> listOf' arbitrary <*> arbitrary
  
  -- ---------------------------------------------------------------------
  
  instance Arbitrary CmdResponse where
    arbitrary = oneof
      [ CmdGenResponse <$> arbitrary
      , CmdGetInfoResponse <$> genGetInfoResponse
      , CmdCheckSatResponse <$> arbitrary
      , CmdGetAssertionsResponse <$> genGetAssertionsResponse
      , CmdGetAssignmentResponse <$> arbitrary
      , CmdGetProofResponse <$> arbitrary
      , CmdGetUnsatCoreResponse <$> genGetUnsatCoreResponse
      , CmdGetUnsatAssumptionsResponse <$> arbitrary
      , CmdGetValueResponse <$> genGetValueResponse
      , CmdGetModelResponse <$> arbitrary
      , CmdGetOptionResponse <$> arbitrary
      , CmdEchoResponse <$> genEchoResponse
      ]
  
  instance Arbitrary GenResponse where
    arbitrary = oneof
      [ return Unsupported
      , return Success
      , Error <$> genStringLiteral
      ]
  
  instance Arbitrary ErrorBehavior where
    arbitrary = elements [ImmediateExit, ContinuedExecution]
  
  instance Arbitrary ReasonUnknown where
    arbitrary = elements [Memout, Incomplete]
  
  instance Arbitrary CheckSatResponse where
    arbitrary = elements [Sat, Unsat, Unknown]
  
  instance Arbitrary InfoResponse where
    arbitrary = oneof
      [ ResponseErrorBehavior <$> arbitrary
      , ResponseName <$> genStringLiteral
      , ResponseAuthors <$> genStringLiteral
      , ResponseVersion <$> genStringLiteral
      , ResponseReasonUnknown <$> arbitrary
      , ResponseAssertionStackLevels <$> abs <$> arbitrary
      , ResponseAttribute <$> (arbitrary `suchThat` p)
      ]
      where
        p (Attribute kw) = kw `Set.notMember` reserved
        p (AttributeVal kw _) = kw `Set.notMember` reserved
        reserved = Set.fromList
          [ ":error-behavior"
          , ":name"
          , ":authors"
          , ":version"
          , ":status"
          , ":reason-unknown"
          , ":all-statistics"
          , ":assertion-stack-levels"
          ]
  
  genGetInfoResponse :: Gen [InfoResponse]
  genGetInfoResponse = listOf' arbitrary
  
  genGetAssertionsResponse :: Gen [Term]
  genGetAssertionsResponse = listOf' arbitrary
  
  genGetUnsatCoreResponse :: Gen [Symbol]
  genGetUnsatCoreResponse = listOf' genSymbol
  
  genGetValueResponse :: Gen [ValuationPair]
  genGetValueResponse = listOf' arbitrary
  
  genGetModelResponse :: Gen [Command]
  genGetModelResponse = listOf1' $ oneof
    [ DefineFun <$> genSymbol <*> listOf' arbitrary <*> arbitrary <*> arbitrary
    , DefineFunRec <$> genSymbol <*> listOf' arbitrary <*> arbitrary <*> arbitrary
    , DefineFunsRec <$> listOf1' arbitrary <*> listOf1' arbitrary
    ]
  
  genEchoResponse :: Gen String
  genEchoResponse = genStringLiteral
  
  instance Arbitrary ValuationPair where
    arbitrary = ValuationPair <$> arbitrary <*> arbitrary
  
  instance Arbitrary TValuationPair where
    arbitrary = TValuationPair <$> genSymbol <*> arbitrary
  
  -- ---------------------------------------------------------------------
  -- Test harness
  
  smtlibTestGroup :: TestTree
  smtlibTestGroup = $(testGroupGenerator)
  