diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -4,3 +4,7 @@ Initial release. +## 0.1.0.1 + +Relax dependency constraints. + diff --git a/smt2-parser.cabal b/smt2-parser.cabal --- a/smt2-parser.cabal +++ b/smt2-parser.cabal @@ -1,20 +1,18 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0. +-- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack --- --- hash: 4f628659c75828fd69bbaa9653ea5cc2f1b03a1f2a64632313f69a9874e522fc name: smt2-parser -version: 0.1.0.0 +version: 0.1.0.1 synopsis: A Haskell parser for SMT-LIB version 2.6 description: Please see the README on GitHub at category: SMT, Formal Languages, Language homepage: https://github.com/crvdgc/smt2-parser#readme bug-reports: https://github.com/crvdgc/smt2-parser/issues author: crvdgc -maintainer: 2502project@gmail.com +maintainer: ubikium@gmail.com copyright: 2020 crvdgc license: BSD3 license-file: LICENSE @@ -36,9 +34,9 @@ hs-source-dirs: src build-depends: - base >=4.13.0 && <4.14 - , parsec >=3.1.14 && <3.2 - , text >=1.2.4 && <1.3 + base >=4.13.0 && <5 + , parsec >=3.1.14 + , text >=1.2.4 default-language: Haskell2010 test-suite smt2-parser-test @@ -50,9 +48,9 @@ test ghc-options: -threaded -rtsopts -with-rtsopts=-N build-depends: - HUnit >=1.6.0 && <1.7 - , base >=4.13.0 && <4.14 - , parsec >=3.1.14 && <3.2 + HUnit >=1.6.0 + , base >=4.13.0 && <5 + , parsec >=3.1.14 , smt2-parser - , text >=1.2.4 && <1.3 + , text >=1.2.4 default-language: Haskell2010 diff --git a/src/Language/SMT2/Parser.hs b/src/Language/SMT2/Parser.hs --- a/src/Language/SMT2/Parser.hs +++ b/src/Language/SMT2/Parser.hs @@ -1,107 +1,119 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} -{-| - - Module : Language.SMT2.Parser - - Description : SMT language parser - - Maintainer : yokis1997@pku.edu.cn - - Stability : experimental --} + +-- | +-- - Module : Language.SMT2.Parser +-- - Description : SMT language parser +-- - Maintainer : ubikium@gmail.com +-- - Stability : experimental module Language.SMT2.Parser ( -- * Utils -- $utils - parseString - , parseStringEof - , parseFileMsg - , parseCommentFreeFileMsg - , stripSpaces - , removeComment + parseString, + parseStringEof, + parseFileMsg, + parseCommentFreeFileMsg, + stripSpaces, + removeComment, + -- * Lexicons (Sec. 3.1) -- $lexicon - , numeral - , decimal - , hexadecimal - , binary - , stringLiteral - , reservedWord - , symbol - , keyword + numeral, + decimal, + hexadecimal, + binary, + stringLiteral, + reservedWord, + symbol, + keyword, + -- * S-expressions (Sec. 3.2) - , slist - , specConstant - , sexpr + slist, + specConstant, + sexpr, + -- * Identifiers (Sec 3.3) - , index - , identifier + index, + identifier, + -- * Attributes (Sec. 3.4) - , attributeValue - , attribute - -- * Sorts (Sec 3.5) - , sort + attributeValue, + attribute, + + -- * Sorts (Sec 3.5) + sort, + -- * Terms and Formulas (Sec 3.6) - , qualIdentifier - , varBinding - , sortedVar - , matchPattern - , matchCase - , term + qualIdentifier, + varBinding, + sortedVar, + matchPattern, + matchCase, + term, + -- * Theory declarations (Sec 3.7) - , sortSymbolDecl - , metaSpecConstant - , funSymbolDecl - , parFunSymbolDecl - , theoryAttribute - , theoryDecl + sortSymbolDecl, + metaSpecConstant, + funSymbolDecl, + parFunSymbolDecl, + theoryAttribute, + theoryDecl, + -- * Logic Declarations (Sec 3.8) - , logicAttribute - , logic + logicAttribute, + logic, + -- * Scripts (Sec 3.9) - , sortDec - , selectorDec - , constructorDec - , datatypeDec - , functionDec - , functionDef - , propLiteral - , command - , script - , bValue - , scriptOption - , infoFlag + sortDec, + selectorDec, + constructorDec, + datatypeDec, + functionDec, + functionDef, + propLiteral, + command, + script, + bValue, + scriptOption, + infoFlag, + -- ** Responses (Sec 3.9.1) + -- *** values - , resErrorBehaviour - , resReasonUnknown - , resModel - , resInfo - , valuationPair - , tValuationPair - , resCheckSat + resErrorBehaviour, + resReasonUnknown, + resModel, + resInfo, + valuationPair, + tValuationPair, + resCheckSat, + -- *** instances - , checkSatRes - , echoRes - , getAssertionsRes - , getAssignmentRes - , getInfoRes - , getModelRes - , getOptionRes - , getProofRes - , getUnsatAssumpRes - , getUnsatCoreRes - , getValueRes - ) where + checkSatRes, + echoRes, + getAssertionsRes, + getAssignmentRes, + getInfoRes, + getModelRes, + getOptionRes, + getProofRes, + getUnsatAssumpRes, + getUnsatCoreRes, + getValueRes, + ) +where -import Data.Bifunctor (bimap) -import Data.Char (toLower) -import Data.Functor (($>)) -import Data.List.NonEmpty (NonEmpty, fromList) -import qualified Data.Text as T -import Language.SMT2.Syntax -import Text.Parsec (ParseError, eof, parse, try) -import Text.Parsec.Char -import Text.Parsec.Combinator -import Text.Parsec.Error (messageString) -import Text.Parsec.Prim (many, unexpected, (), (<|>)) -import Text.Parsec.Text (GenParser, Parser) +import Data.Bifunctor (first) +import Data.Char (toLower) +import Data.Functor (($>)) +import Data.List.NonEmpty (NonEmpty, fromList) +import qualified Data.Text as T +import Language.SMT2.Syntax +import Text.Parsec (ParseError, parse, try) +import Text.Parsec.Char +import Text.Parsec.Combinator +import Text.Parsec.Prim (many, unexpected, (), (<|>)) +import Text.Parsec.Text (GenParser, Parser) parseString :: Parser a -> T.Text -> Either ParseError a parseString p = parse p "" @@ -109,16 +121,16 @@ parseStringEof :: Parser a -> T.Text -> Either ParseError a parseStringEof p = parse (p <* eof) "" - -- | parse from a file string, may have leading & trailing spaces and comments parseFileMsg :: Parser a -> T.Text -> Either T.Text a parseFileMsg p = parseCommentFreeFileMsg p . removeComment -- | parse from a comment-free file string parseCommentFreeFileMsg :: Parser a -> T.Text -> Either T.Text a -parseCommentFreeFileMsg p = bimap (T.pack . show) id . parseStringEof (stripSpaces p) +parseCommentFreeFileMsg p = first (T.pack . show) . parseStringEof (stripSpaces p) -- * Utils + -- $utils -- commonly used combinators @@ -126,7 +138,6 @@ text :: String -> GenParser st T.Text text = (T.pack <$>) . string - -- | skip one or more @spaces@ spaces1 :: GenParser st () spaces1 = skipMany1 space @@ -168,11 +179,11 @@ -- | like @tryStr@, but prefix with a @':'@ tryAttr :: String -> GenParser st () -tryAttr s = tryStr (':':s) +tryAttr s = tryStr (':' : s) -- | like @tryStr1@, but prefix with a @':'@ tryAttr1 :: String -> GenParser st () -tryAttr1 s = tryStr1 (':':s) +tryAttr1 s = tryStr1 (':' : s) -- | strip away the leading and trailing @spaces@ stripSpaces :: GenParser st a -> GenParser st a @@ -183,21 +194,25 @@ removeComment = rc T.empty where rc :: T.Text -> T.Text -> T.Text - rc acc rest = if T.null rest - then acc - else let (c, cs) = (T.head rest, T.tail rest) - f = case c of - '"' -> capture "\"" (T.cons '"') - '|' -> capture "|" (T.cons '|') - ';' -> capture "\n\r" (const $ T.singleton ' ') - x -> nextPos x - in f acc cs + rc acc rest = + if T.null rest + then acc + else + let (c, cs) = (T.head rest, T.tail rest) + f = case c of + '"' -> capture "\"" (T.cons '"') + '|' -> capture "|" (T.cons '|') + ';' -> capture "\n\r" (const $ T.singleton ' ') + x -> nextPos x + in f acc cs capture :: String -> (T.Text -> T.Text) -> T.Text -> T.Text -> T.Text - capture stops after acc cs = let (captured, rest) = T.break (`elem` stops) cs - in if T.null rest - then acc <> after captured - else let (s, ss) = (T.head rest, T.tail rest) - in rc (acc <> after captured <> T.singleton s) ss + capture stops after acc cs = + let (captured, rest) = T.break (`elem` stops) cs + in if T.null rest + then acc <> after captured + else + let (s, ss) = (T.head rest, T.tail rest) + in rc (acc <> after captured <> T.singleton s) ss -- 1. if the string is ill-formed, ignore; -- let the parser catch, for a better format -- 2. the double " escaping in a string literal is the same as capturing twice @@ -205,6 +220,7 @@ nextPos x acc = rc (acc `T.snoc` x) -- * Lexicons (Sec. 3.1) + -- $lexicon -- Parsers for lexicons. -- @@ -212,17 +228,20 @@ -- For a hexadecimal or a binary, the result is stripped with marks (@#x@ and @#b@). numeral :: GenParser st Numeral -numeral = text "0" - <|> do c <- oneOf "123456789" - cs <- many digit - return $ T.pack (c:cs) +numeral = + text "0" + <|> do + c <- oneOf "123456789" + cs <- many digit + return $ T.pack (c : cs) decimal :: GenParser st Decimal -decimal = do whole <- numeral - char '.' - zeros <- many (char '0') - restFractional <- option "" numeral - return $ whole <> T.singleton '.' <> T.pack zeros <> restFractional +decimal = do + whole <- numeral + char '.' + zeros <- many (char '0') + restFractional <- option "" numeral + return $ whole <> T.singleton '.' <> T.pack zeros <> restFractional hexadecimal :: GenParser st Hexadecimal hexadecimal = text "#x" >> T.pack . fmap toLower <$> many1 hexDigit @@ -231,23 +250,49 @@ binary = text "#b" >> T.pack <$> many1 (char '0' <|> char '1') stringLiteral :: GenParser st StringLiteral -stringLiteral = do char '"' - str <- many (nonEscaped <|> escaped) - char '"' - return $ T.pack str +stringLiteral = do + char '"' + str <- many (nonEscaped <|> escaped) + char '"' + return $ T.pack str where nonEscaped = noneOf "\"" escaped = try (string "\"\"") $> '"' reservedWords :: [String] -reservedWords = [ -- General - "!", "_" , "as", "DECIMAL", "exists", "forall", "let", "NUMERAL", "par", "STRING", - -- Command names - "assert", "check-sat", "declare-sort", "declare-fun", "define-sort", - "define-fun", "exit", "get-assertions", "get-assignment", "get-info", "get-option", - "get-proof", "get-unsat-core", "get-value", "pop", "push", "set-logic", "set-info", - "set-option" - ] +reservedWords = + [ -- General + "!", + "_", + "as", + "DECIMAL", + "exists", + "forall", + "let", + "NUMERAL", + "par", + "STRING", + -- Command names + "assert", + "check-sat", + "declare-sort", + "declare-fun", + "define-sort", + "define-fun", + "exit", + "get-assertions", + "get-assignment", + "get-info", + "get-option", + "get-proof", + "get-unsat-core", + "get-value", + "pop", + "push", + "set-logic", + "set-info", + "set-option" + ] -- | accept all reserved words, -- the exact content should be checked later in the parsing procedure @@ -257,27 +302,26 @@ parseWord :: String -> GenParser st ReservedWord parseWord w = try (text w) <* notFollowedBy anyChar - -- | characters allowed in a name nameChar :: GenParser st Char -nameChar = oneOf "~!@$%^&*_-+=<>.?/" +nameChar = oneOf "~!@$%^&*_-+=<>.?/" -- | enclosing a simple symbol in vertical bars does not produce a -- new symbol, e.g. @abc@ and @|abc|@ are the /same/ symbol -- this is guaranteed by removing the bars symbol :: GenParser st Symbol -symbol = notFollowedBy (try reservedWord) >> (quotedSymbol <|> simpleSymbol "symbol") +symbol = notFollowedBy (try reservedWord) >> (quotedSymbol <|> simpleSymbol "symbol") where simpleSymbol = do c <- nameChar <|> letter cs <- many (alphaNum <|> nameChar) - return $ T.pack (c:cs) + return $ T.pack (c : cs) quotedSymbol = between (char '|') (char '|') $ T.pack <$> many (noneOf "\\|") keyword :: GenParser st Keyword -keyword = do char ':' - T.pack <$> many1 (alphaNum <|> nameChar) - +keyword = do + char ':' + T.pack <$> many1 (alphaNum <|> nameChar) -- * S-expressions (Sec. 3.2) @@ -286,52 +330,55 @@ -- | a constant must be followed by a space to delimit the end specConstant :: GenParser st SpecConstant -specConstant = SCDecimal <$> try decimal -- numeral can be a prefix - <|> SCNumeral <$> try numeral - <|> SCHexadecimal <$> try hexadecimal - <|> SCBinary <$> try binary - <|> SCString <$> try stringLiteral - "spec constants" +specConstant = + SCDecimal <$> try decimal -- numeral can be a prefix + <|> SCNumeral <$> try numeral + <|> SCHexadecimal <$> try hexadecimal + <|> SCBinary <$> try binary + <|> SCString <$> try stringLiteral + "spec constants" sexpr :: GenParser st SExpr -sexpr = SEList <$> try slist - <|> SEConstant <$> try specConstant - <|> SEReservedWord <$> try reservedWord - <|> SEKeyword <$> try keyword - <|> SESymbol <$> try symbol - "s-expressions" - +sexpr = + SEList <$> try slist + <|> SEConstant <$> try specConstant + <|> SEReservedWord <$> try reservedWord + <|> SEKeyword <$> try keyword + <|> SESymbol <$> try symbol + "s-expressions" -- * Identifiers (Sec 3.3) index :: GenParser st Index -index = IxNumeral <$> numeral - <|> IxSymbol <$> symbol +index = + IxNumeral <$> numeral + <|> IxSymbol <$> symbol identifier :: GenParser st Identifier -identifier = IdSymbol <$> symbol -- symbol cannot start with (, so no ambiguity - <|> idIndexed - "identifier" +identifier = + IdSymbol <$> symbol -- symbol cannot start with (, so no ambiguity + <|> idIndexed + "identifier" where idIndexed = betweenBrackets $ do char '_' <* spaces1 s <- symbol <* spaces1 IdIndexed s <$> sepSpace1 index - -- * Attributes (Sec. 3.4) attributeValue :: GenParser st AttributeValue -attributeValue = AttrValSpecConstant <$> specConstant - <|> AttrValSymbol <$> symbol - <|> AttrValSList <$> slist - "attribute value" +attributeValue = + AttrValSpecConstant <$> specConstant + <|> AttrValSymbol <$> symbol + <|> AttrValSList <$> slist + "attribute value" attribute :: GenParser st Attribute -attribute = AttrKeyValue <$> try (keyword <* spaces1) <*> attributeValue - <|> AttrKey <$> keyword - "attribute" - +attribute = + AttrKeyValue <$> try (keyword <* spaces1) <*> attributeValue + <|> AttrKey <$> keyword + "attribute" -- * Sorts (Sec 3.5) @@ -341,17 +388,18 @@ SortParameter i <$> sepSpace1 sort sort :: GenParser st Sort -sort = SortSymbol <$> try identifier +sort = + SortSymbol <$> try identifier <|> sortParameter "sort" - -- * Terms and Formulas (Sec 3.6) qualIdentifier :: GenParser st QualIdentifier -qualIdentifier = Unqualified <$> try identifier - <|> betweenBrackets annotation - "qual identifier" +qualIdentifier = + Unqualified <$> try identifier + <|> betweenBrackets annotation + "qual identifier" where annotation :: GenParser st QualIdentifier annotation = do @@ -366,9 +414,10 @@ sortedVar = betweenBrackets $ SortedVar <$> symbol <* spaces1 <*> sort matchPattern :: GenParser st MatchPattern -matchPattern = MPVariable <$> symbol - <|> mPConstructor - "pattern" +matchPattern = + MPVariable <$> symbol + <|> mPConstructor + "pattern" where mPConstructor = betweenBrackets $ do c <- symbol <* spaces1 @@ -380,7 +429,8 @@ MatchCase p <$> term term :: GenParser st Term -term = TermSpecConstant <$> try specConstant +term = + TermSpecConstant <$> try specConstant <|> TermQualIdentifier <$> try qualIdentifier <|> try application <|> try binding @@ -396,7 +446,7 @@ binding = betweenBrackets $ do tryStr "let" vbs <- betweenBrackets $ sepOptSpace1 varBinding - space + spaces TermLet vbs <$> term quantifyForall = betweenBrackets $ do tryStr "forall" @@ -417,7 +467,6 @@ t <- term <* spaces1 TermAnnotation t <$> sepSpace1 attribute - -- * Theory declarations (Sec 3.7) sortSymbolDecl :: GenParser st SortSymbolDecl @@ -427,16 +476,18 @@ SortSymbolDecl i n <$> sepSpace attribute metaSpecConstant :: GenParser st MetaSpecConstant -metaSpecConstant = string "NUMERAL" $> MSC_NUMERAL - <|> string "DECIMAL" $> MSC_DECIMAL - <|> string "STRING" $> MSC_STRING - "meta spec constant" +metaSpecConstant = + string "NUMERAL" $> MSC_NUMERAL + <|> string "DECIMAL" $> MSC_DECIMAL + <|> string "STRING" $> MSC_STRING + "meta spec constant" funSymbolDecl :: GenParser st FunSymbolDecl -funSymbolDecl = try (betweenBrackets funConstant) - <|> try (betweenBrackets funMeta) - <|> try (betweenBrackets funIdentifier) - "non-parametric function symbol declaration" +funSymbolDecl = + try (betweenBrackets funConstant) + <|> try (betweenBrackets funMeta) + <|> try (betweenBrackets funIdentifier) + "non-parametric function symbol declaration" where funConstant = do sc <- specConstant <* spaces1 @@ -453,9 +504,10 @@ return $ FunIdentifier i ss as parFunSymbolDecl :: GenParser st ParFunSymbolDecl -parFunSymbolDecl = NonPar <$> funSymbolDecl - <|> betweenBrackets par - "potentially parametric function symbol declaration" +parFunSymbolDecl = + NonPar <$> funSymbolDecl + <|> betweenBrackets par + "potentially parametric function symbol declaration" where par = do tryStr "par" @@ -466,17 +518,17 @@ ss <- sepSpace1 sort Par syms idt ss <$> sepSpace attribute - theoryAttribute :: GenParser st TheoryAttribute -theoryAttribute = tryAttr "sorts" *> betweenBrackets (TASorts <$> sepSpace1 sortSymbolDecl) - <|> tryAttr "funs" *> betweenBrackets (TAFuns <$> sepSpace1 parFunSymbolDecl) - <|> tryAttr "sorts-description" *> (TASortsDescription <$> stringLiteral) - <|> tryAttr "funs-description" *> (TAFunsDescription <$> stringLiteral) - <|> tryAttr "definition" *> (TADefinition <$> stringLiteral) - <|> tryAttr "values" *> (TAValues <$> stringLiteral) - <|> tryAttr "notes" *> (TANotes <$> stringLiteral) - <|> TAAttr <$> attribute - "theory attributes" +theoryAttribute = + tryAttr "sorts" *> betweenBrackets (TASorts <$> sepSpace1 sortSymbolDecl) + <|> tryAttr "funs" *> betweenBrackets (TAFuns <$> sepSpace1 parFunSymbolDecl) + <|> tryAttr "sorts-description" *> (TASortsDescription <$> stringLiteral) + <|> tryAttr "funs-description" *> (TAFunsDescription <$> stringLiteral) + <|> tryAttr "definition" *> (TADefinition <$> stringLiteral) + <|> tryAttr "values" *> (TAValues <$> stringLiteral) + <|> tryAttr "notes" *> (TANotes <$> stringLiteral) + <|> TAAttr <$> attribute + "theory attributes" theoryDecl :: GenParser st TheoryDecl theoryDecl = betweenBrackets $ do @@ -484,16 +536,16 @@ s <- symbol <* spaces1 TheoryDecl s <$> sepSpace1 theoryAttribute - -- * Logic Declarations (Sec 3.8) logicAttribute :: GenParser st LogicAttribute -logicAttribute = tryAttr "theories" *> betweenBrackets (LATheories <$> sepSpace1 symbol) - <|> tryAttr "language" *> (LALanguage <$> stringLiteral) - <|> tryAttr "extensions" *> (LAExtensions <$> stringLiteral) - <|> tryAttr "values" *> (LAValues <$> stringLiteral) - <|> tryAttr "notes" *> (LANotes <$> stringLiteral) - <|> LAAttr <$> attribute +logicAttribute = + tryAttr "theories" *> betweenBrackets (LATheories <$> sepSpace1 symbol) + <|> tryAttr "language" *> (LALanguage <$> stringLiteral) + <|> tryAttr "extensions" *> (LAExtensions <$> stringLiteral) + <|> tryAttr "values" *> (LAValues <$> stringLiteral) + <|> tryAttr "notes" *> (LANotes <$> stringLiteral) + <|> LAAttr <$> attribute logic :: GenParser st Logic logic = betweenBrackets $ do @@ -501,7 +553,6 @@ s <- symbol <* spaces1 Logic s <$> sepSpace1 logicAttribute - -- * Scripts (Sec 3.9) sortDec :: GenParser st SortDec @@ -520,9 +571,10 @@ ConstructorDec s <$> sepSpace selectorDec datatypeDec :: GenParser st DatatypeDec -datatypeDec = DDNonparametric <$> betweenBrackets (sepSpace1 constructorDec) - <|> parametric - "datatype declaration" +datatypeDec = + DDNonparametric <$> betweenBrackets (sepSpace1 constructorDec) + <|> parametric + "datatype declaration" where parametric = betweenBrackets $ do tryStr1 "par" @@ -545,41 +597,43 @@ FunctionDef s svs t <$> term propLiteral :: GenParser st PropLiteral -propLiteral = PLPositive <$> symbol - <|> PLNegative <$> betweenBrackets (tryStr1 "not" *> symbol) +propLiteral = + PLPositive <$> symbol + <|> PLNegative <$> betweenBrackets (tryStr1 "not" *> symbol) command :: GenParser st Command -command = cmd "assert" (Assert <$> term) - <|> cmd "check-sat" (pure CheckSat) - <|> cmd "check-sat-assuming" (betweenBrackets (CheckSatAssuming <$> sepSpace propLiteral)) - <|> cmd "declare-const" (DeclareConst <$> (symbol <* spaces1) <*> sort) - <|> cmd "declare-datatype" (DeclareDatatype <$> (symbol <* spaces1) <*> datatypeDec) - <|> cmd "declare-datatypes" declareDatatypes - <|> cmd "declare-fun" declareFun - <|> cmd "declare-sort" declareSort - <|> cmd "define-fun" (DefineFun <$> functionDef) - <|> cmd "define-fun-rec" (DefineFunRec <$> functionDef) - <|> cmd "define-funs-rec" defineFunsRec - <|> cmd "define-sort" defineSort - <|> cmd "echo" (Echo <$> stringLiteral) - <|> cmd "exit" (pure Exit) - <|> cmd "get-assertions" (pure GetAssertions) - <|> cmd "get-assignment" (pure GetAssignment) - <|> cmd "get-info" (GetInfo <$> infoFlag) - <|> cmd "get-model" (pure GetModel) - <|> cmd "get-option" (GetOption <$> keyword) - <|> cmd "get-proof" (pure GetProof) - <|> cmd "get-unsat-assumptions" (pure GetUnsatAssumptions) - <|> cmd "get-unsat-core" (pure GetUnsatCore) - <|> cmd "get-value" (GetValue <$> getValue) - <|> cmd "pop" (Pop <$> numeral) - <|> cmd "push" (Push <$> numeral) - <|> cmd "reset" (pure Reset) - <|> cmd "reset-assertions" (pure ResetAssertions) - <|> cmd "set-info" (SetInfo <$> attribute) - <|> cmd "set-logic" (SetLogic <$> symbol) - <|> cmd "set-option" (SetOption <$> scriptOption) - "command" +command = + cmd "assert" (Assert <$> term) + <|> cmd "check-sat" (pure CheckSat) + <|> cmd "check-sat-assuming" (betweenBrackets (CheckSatAssuming <$> sepSpace propLiteral)) + <|> cmd "declare-const" (DeclareConst <$> (symbol <* spaces1) <*> sort) + <|> cmd "declare-datatype" (DeclareDatatype <$> (symbol <* spaces1) <*> datatypeDec) + <|> cmd "declare-datatypes" declareDatatypes + <|> cmd "declare-fun" declareFun + <|> cmd "declare-sort" declareSort + <|> cmd "define-fun" (DefineFun <$> functionDef) + <|> cmd "define-fun-rec" (DefineFunRec <$> functionDef) + <|> cmd "define-funs-rec" defineFunsRec + <|> cmd "define-sort" defineSort + <|> cmd "echo" (Echo <$> stringLiteral) + <|> cmd "exit" (pure Exit) + <|> cmd "get-assertions" (pure GetAssertions) + <|> cmd "get-assignment" (pure GetAssignment) + <|> cmd "get-info" (GetInfo <$> infoFlag) + <|> cmd "get-model" (pure GetModel) + <|> cmd "get-option" (GetOption <$> keyword) + <|> cmd "get-proof" (pure GetProof) + <|> cmd "get-unsat-assumptions" (pure GetUnsatAssumptions) + <|> cmd "get-unsat-core" (pure GetUnsatCore) + <|> cmd "get-value" (GetValue <$> getValue) + <|> cmd "pop" (Pop <$> numeral) + <|> cmd "push" (Push <$> numeral) + <|> cmd "reset" (pure Reset) + <|> cmd "reset-assertions" (pure ResetAssertions) + <|> cmd "set-info" (SetInfo <$> attribute) + <|> cmd "set-logic" (SetLogic <$> symbol) + <|> cmd "set-option" (SetOption <$> scriptOption) + "command" where cmd s p = try $ betweenBrackets (tryStr s *> p) declareDatatypes = do @@ -587,8 +641,8 @@ spaces dds <- betweenBrackets $ sepSpace1 datatypeDec if length sds == length dds - then pure $ DeclareDatatypes sds dds - else unexpected "declare-datatypes: sorts and datatypes should have same length" + then pure $ DeclareDatatypes sds dds + else unexpected "declare-datatypes: sorts and datatypes should have same length" declareFun = do s <- symbol <* spaces1 ss <- betweenBrackets $ sepSpace sort @@ -602,8 +656,8 @@ spaces ts <- betweenBrackets $ sepSpace1 term if length fds == length ts - then pure $ DefineFunsRec fds ts - else unexpected "define-funs-rec: declarations and terms should have same length" + then pure $ DefineFunsRec fds ts + else unexpected "define-funs-rec: declarations and terms should have same length" defineSort = do s <- symbol <* spaces1 ss <- betweenBrackets $ sepSpace symbol @@ -615,64 +669,71 @@ script = spaces *> sepOptSpace command <* spaces bValue :: GenParser st BValue -bValue = string "true" $> BTrue - <|> string "false" $> BFalse - "bool value" +bValue = + string "true" $> BTrue + <|> string "false" $> BFalse + "bool value" scriptOption :: GenParser st ScriptOption -scriptOption = DiagnosticOutputChannel <$> opt "diagnostic-output-channel" stringLiteral - <|> GlobalDeclarations <$> optB "global-declarations" - <|> InteractiveMode <$> optB "interactive-mode" - <|> PrintSuccess <$> optB "print-success" - <|> ProduceAssertions <$> optB "produce-assertions" - <|> ProduceAssignments <$> optB "produce-assignments" - <|> ProduceModels <$> optB "produce-models" - <|> ProduceProofs <$> optB "produce-proofs" - <|> ProduceUnsatAssumptions <$> optB "produce-unsat-assumptions" - <|> ProduceUnsatCores <$> optB "produce-unsat-cores" - <|> RandomSeed <$> opt "random-seed" numeral - <|> RegularOutputChannel <$> opt "regular-output-channel" stringLiteral - <|> ReproducibleResourceLimit <$> opt "reproducible-resource-limit" numeral - <|> Verbosity <$> opt "verbosity" numeral - <|> OptionAttr <$> attribute - "script option" +scriptOption = + DiagnosticOutputChannel <$> opt "diagnostic-output-channel" stringLiteral + <|> GlobalDeclarations <$> optB "global-declarations" + <|> InteractiveMode <$> optB "interactive-mode" + <|> PrintSuccess <$> optB "print-success" + <|> ProduceAssertions <$> optB "produce-assertions" + <|> ProduceAssignments <$> optB "produce-assignments" + <|> ProduceModels <$> optB "produce-models" + <|> ProduceProofs <$> optB "produce-proofs" + <|> ProduceUnsatAssumptions <$> optB "produce-unsat-assumptions" + <|> ProduceUnsatCores <$> optB "produce-unsat-cores" + <|> RandomSeed <$> opt "random-seed" numeral + <|> RegularOutputChannel <$> opt "regular-output-channel" stringLiteral + <|> ReproducibleResourceLimit <$> opt "reproducible-resource-limit" numeral + <|> Verbosity <$> opt "verbosity" numeral + <|> OptionAttr <$> attribute + "script option" where opt s p = tryAttr s *> spaces1 *> p optB s = opt s bValue infoFlag :: GenParser st InfoFlag -infoFlag = tryAttr "all-statistics" $> AllStatistics - <|> tryAttr "assertion-stack-levels" $> AssertionStackLevels - <|> tryAttr "authors" $> Authors - <|> tryAttr "error-behavior" $> ErrorBehavior - <|> tryAttr "name" $> Name - <|> tryAttr "reason-unknown" $> ReasonUnknown - <|> tryAttr "version" $> Version - <|> IFKeyword <$> keyword - "info flag" +infoFlag = + tryAttr "all-statistics" $> AllStatistics + <|> tryAttr "assertion-stack-levels" $> AssertionStackLevels + <|> tryAttr "authors" $> Authors + <|> tryAttr "error-behavior" $> ErrorBehavior + <|> tryAttr "name" $> Name + <|> tryAttr "reason-unknown" $> ReasonUnknown + <|> tryAttr "version" $> Version + <|> IFKeyword <$> keyword + "info flag" -- ** Responses (Sec 3.9.1) genRes :: SpecificSuccessRes res => GenParser st (GeneralRes res) -genRes = tryStr "success" $> ResSuccess - <|> ResSpecific <$> specificSuccessRes - <|> tryStr "unsupported" $> ResUnsupported - <|> ResError <$> betweenBrackets (tryStr "error" *> spaces1 *> stringLiteral) +genRes = + tryStr "success" $> ResSuccess + <|> ResSpecific <$> specificSuccessRes + <|> tryStr "unsupported" $> ResUnsupported + <|> ResError <$> betweenBrackets (tryStr "error" *> spaces1 *> stringLiteral) resErrorBehaviour :: GenParser st ResErrorBehavior -resErrorBehaviour = tryStr "immediate-exit" $> ImmediateExit - <|> tryStr "continued-execution" $> ContinuedExecution - "response error behavior" +resErrorBehaviour = + tryStr "immediate-exit" $> ImmediateExit + <|> tryStr "continued-execution" $> ContinuedExecution + "response error behavior" resReasonUnknown :: GenParser st ResReasonUnknown -resReasonUnknown = tryStr "memout" $> Memout - <|> tryStr "incomplete" $> Incomplete - "response reason unknown" +resReasonUnknown = + tryStr "memout" $> Memout + <|> tryStr "incomplete" $> Incomplete + "response reason unknown" resModel :: GenParser st ResModel -resModel = def "define-fun" (RMDefineFun <$> functionDef) - <|> def "define-fun-rec" (RMDefineFunRec <$> functionDef) - <|> def "define-funs-rec" rMDefineFunsRec +resModel = + def "define-fun" (RMDefineFun <$> functionDef) + <|> def "define-fun-rec" (RMDefineFunRec <$> functionDef) + <|> def "define-funs-rec" rMDefineFunsRec where def s p = betweenBrackets $ tryStr s *> p rMDefineFunsRec = do @@ -680,8 +741,8 @@ spaces ts <- betweenBrackets $ sepSpace1 term if length fdcs == length ts - then pure $ RMDefineFunsRec fdcs ts - else unexpected "get-model response, declarations and terms should have same length" + then pure $ RMDefineFunsRec fdcs ts + else unexpected "get-model response, declarations and terms should have same length" instance SpecificSuccessRes ResModel where specificSuccessRes = resModel @@ -693,20 +754,22 @@ return (s, b) resCheckSat :: GenParser st ResCheckSat -resCheckSat = tryStr "sat" $> Sat - <|> tryStr "unsat" $> Unsat - <|> tryStr "unknown" $> Unknown +resCheckSat = + tryStr "sat" $> Sat + <|> tryStr "unsat" $> Unsat + <|> tryStr "unknown" $> Unknown instance SpecificSuccessRes ResCheckSat where specificSuccessRes = resCheckSat resInfo :: GenParser st ResInfo -resInfo = IRErrorBehaviour <$> (tryAttr "error-behavior" *> resErrorBehaviour) - <|> IRName <$> (tryAttr "name" *> stringLiteral) - <|> IRAuthours <$> (tryAttr "authors" *> stringLiteral) - <|> IRVersion <$> (tryAttr "version" *> stringLiteral) - <|> IRReasonUnknown <$> (tryAttr "reason-unknown" *> resReasonUnknown) - <|> IRAttr <$> attribute +resInfo = + IRErrorBehaviour <$> (tryAttr "error-behavior" *> resErrorBehaviour) + <|> IRName <$> (tryAttr "name" *> stringLiteral) + <|> IRAuthours <$> (tryAttr "authors" *> stringLiteral) + <|> IRVersion <$> (tryAttr "version" *> stringLiteral) + <|> IRReasonUnknown <$> (tryAttr "reason-unknown" *> resReasonUnknown) + <|> IRAttr <$> attribute instance SpecificSuccessRes (NonEmpty ResInfo) where specificSuccessRes = betweenBrackets $ sepSpace1 resInfo @@ -772,4 +835,3 @@ getValueRes :: GenParser st GetValueRes getValueRes = genRes - diff --git a/src/Language/SMT2/Syntax.hs b/src/Language/SMT2/Syntax.hs --- a/src/Language/SMT2/Syntax.hs +++ b/src/Language/SMT2/Syntax.hs @@ -1,83 +1,93 @@ -{-| - - Module : Language.SMT2.Syntax - - Description : SMT language parser - - Maintainer : yokis1997@pku.edu.cn - - Stability : experimental --} +-- | +-- - Module : Language.SMT2.Syntax +-- - Description : SMT language parser +-- - Maintainer : ubikium@gmail.com +-- - Stability : experimental module Language.SMT2.Syntax where -import Data.List.NonEmpty (NonEmpty) -import qualified Data.Text as T -import Text.Parsec.Text (GenParser) +import Data.List.NonEmpty (NonEmpty) +import qualified Data.Text as T +import Text.Parsec.Text (GenParser) -- * Lexicons (Sec. 3.1) + -- -- Note: semantics should be provided by specific theories. -- See Remark 1 of the refrence. -type Numeral = T.Text -type Decimal = T.Text -type Hexadecimal = T.Text -type Binary = T.Text +type Numeral = T.Text + +type Decimal = T.Text + +type Hexadecimal = T.Text + +type Binary = T.Text + type StringLiteral = T.Text -type ReservedWord = T.Text -type Symbol = T.Text -type Keyword = T.Text +type ReservedWord = T.Text +type Symbol = T.Text + +type Keyword = T.Text + -- * S-expressions (Sec. 3.2) -data SpecConstant = SCNumeral Numeral - | SCDecimal Decimal - | SCHexadecimal Hexadecimal - | SCBinary Binary - | SCString StringLiteral +data SpecConstant + = SCNumeral Numeral + | SCDecimal Decimal + | SCHexadecimal Hexadecimal + | SCBinary Binary + | SCString StringLiteral deriving (Eq, Show) -data SExpr = SEConstant SpecConstant - | SEReservedWord ReservedWord - | SESymbol Symbol - | SEKeyword Keyword - | SEList SList +data SExpr + = SEConstant SpecConstant + | SEReservedWord ReservedWord + | SESymbol Symbol + | SEKeyword Keyword + | SEList SList deriving (Eq, Show) type SList = [SExpr] - -- * Identifiers (Sec 3.3) -data Index = IxNumeral Numeral - | IxSymbol Symbol +data Index + = IxNumeral Numeral + | IxSymbol Symbol deriving (Eq, Show) -data Identifier = IdSymbol Symbol - | IdIndexed Symbol (NonEmpty Index) +data Identifier + = IdSymbol Symbol + | IdIndexed Symbol (NonEmpty Index) deriving (Eq, Show) - -- * Attributes (Sec. 3.4) -data AttributeValue = AttrValSpecConstant SpecConstant - | AttrValSymbol Symbol - | AttrValSList SList +data AttributeValue + = AttrValSpecConstant SpecConstant + | AttrValSymbol Symbol + | AttrValSList SList deriving (Eq, Show) -data Attribute = AttrKey Keyword - | AttrKeyValue Keyword AttributeValue +data Attribute + = AttrKey Keyword + | AttrKeyValue Keyword AttributeValue deriving (Eq, Show) - -- * Sorts (Sec 3.5) -data Sort = SortSymbol Identifier - | SortParameter Identifier (NonEmpty Sort) +data Sort + = SortSymbol Identifier + | SortParameter Identifier (NonEmpty Sort) deriving (Eq, Show) - -- * Terms and Formulas (Sec 3.6) -data QualIdentifier = Unqualified Identifier - | Qualified Identifier Sort +data QualIdentifier + = Unqualified Identifier + | Qualified Identifier Sort deriving (Eq, Show) data VarBinding = VarBinding Symbol Term @@ -86,24 +96,25 @@ data SortedVar = SortedVar Symbol Sort deriving (Eq, Show) -data MatchPattern = MPVariable Symbol - | MPConstructor Symbol (NonEmpty Symbol) +data MatchPattern + = MPVariable Symbol + | MPConstructor Symbol (NonEmpty Symbol) deriving (Eq, Show) data MatchCase = MatchCase MatchPattern Term deriving (Eq, Show) -data Term = TermSpecConstant SpecConstant - | TermQualIdentifier QualIdentifier - | TermApplication QualIdentifier (NonEmpty Term) - | TermLet (NonEmpty VarBinding) Term - | TermForall (NonEmpty SortedVar) Term - | TermExists (NonEmpty SortedVar) Term - | TermMatch Term (NonEmpty MatchCase) - | TermAnnotation Term (NonEmpty Attribute) +data Term + = TermSpecConstant SpecConstant + | TermQualIdentifier QualIdentifier + | TermApplication QualIdentifier (NonEmpty Term) + | TermLet (NonEmpty VarBinding) Term + | TermForall (NonEmpty SortedVar) Term + | TermExists (NonEmpty SortedVar) Term + | TermMatch Term (NonEmpty MatchCase) + | TermAnnotation Term (NonEmpty Attribute) deriving (Eq, Show) - -- * Theory declarations (Sec 3.7) data SortSymbolDecl = SortSymbolDecl Identifier Numeral [Attribute] @@ -112,43 +123,48 @@ data MetaSpecConstant = MSC_NUMERAL | MSC_DECIMAL | MSC_STRING deriving (Eq, Show) -data FunSymbolDecl = FunConstant SpecConstant Sort [Attribute] - | FunMeta MetaSpecConstant Sort [Attribute] - | FunIdentifier Identifier (NonEmpty Sort) [Attribute] -- ^ potentially overloaded +data FunSymbolDecl + = FunConstant SpecConstant Sort [Attribute] + | FunMeta MetaSpecConstant Sort [Attribute] + | -- | potentially overloaded + FunIdentifier Identifier (NonEmpty Sort) [Attribute] deriving (Eq, Show) -data ParFunSymbolDecl = NonPar FunSymbolDecl -- ^ non-parametric - | Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute] -- ^ parametric +data ParFunSymbolDecl + = -- | non-parametric + NonPar FunSymbolDecl + | -- | parametric + Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute] deriving (Eq, Show) -data TheoryAttribute = TASorts (NonEmpty SortSymbolDecl) - | TAFuns (NonEmpty ParFunSymbolDecl) - | TASortsDescription StringLiteral - | TAFunsDescription StringLiteral - | TADefinition StringLiteral - | TAValues StringLiteral - | TANotes StringLiteral - | TAAttr Attribute +data TheoryAttribute + = TASorts (NonEmpty SortSymbolDecl) + | TAFuns (NonEmpty ParFunSymbolDecl) + | TASortsDescription StringLiteral + | TAFunsDescription StringLiteral + | TADefinition StringLiteral + | TAValues StringLiteral + | TANotes StringLiteral + | TAAttr Attribute deriving (Eq, Show) data TheoryDecl = TheoryDecl Symbol (NonEmpty TheoryAttribute) deriving (Eq, Show) - -- * Logic Declarations (Sec 3.8) -data LogicAttribute = LATheories (NonEmpty Symbol) - | LALanguage StringLiteral - | LAExtensions StringLiteral - | LAValues StringLiteral - | LANotes StringLiteral - | LAAttr Attribute +data LogicAttribute + = LATheories (NonEmpty Symbol) + | LALanguage StringLiteral + | LAExtensions StringLiteral + | LAValues StringLiteral + | LANotes StringLiteral + | LAAttr Attribute deriving (Eq, Show) data Logic = Logic Symbol (NonEmpty LogicAttribute) deriving (Eq, Show) - -- * Scripts (Sec 3.9) data SortDec = SortDec Symbol Numeral @@ -160,8 +176,9 @@ data ConstructorDec = ConstructorDec Symbol [SelectorDec] deriving (Eq, Show) -data DatatypeDec = DDNonparametric (NonEmpty ConstructorDec) - | DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec) +data DatatypeDec + = DDNonparametric (NonEmpty ConstructorDec) + | DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec) deriving (Eq, Show) data FunctionDec = FunctionDec Symbol [SortedVar] Sort @@ -170,40 +187,44 @@ data FunctionDef = FunctionDef Symbol [SortedVar] Sort Term deriving (Eq, Show) -data PropLiteral = PLPositive Symbol - | PLNegative Symbol +data PropLiteral + = PLPositive Symbol + | PLNegative Symbol deriving (Eq, Show) -data Command = Assert Term - | CheckSat - | CheckSatAssuming [PropLiteral] - | DeclareConst Symbol Sort - | DeclareDatatype Symbol DatatypeDec - | DeclareDatatypes (NonEmpty SortDec) (NonEmpty DatatypeDec) -- ^ same number - | DeclareFun Symbol [Sort] Sort - | DeclareSort Symbol Numeral - | DefineFun FunctionDef - | DefineFunRec FunctionDef - | DefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) -- ^ same number - | DefineSort Symbol [Symbol] Sort - | Echo StringLiteral - | Exit - | GetAssertions - | GetAssignment - | GetInfo InfoFlag - | GetModel - | GetOption Keyword - | GetProof - | GetUnsatAssumptions - | GetUnsatCore - | GetValue (NonEmpty Term) - | Pop Numeral - | Push Numeral - | Reset - | ResetAssertions - | SetInfo Attribute - | SetLogic Symbol - | SetOption ScriptOption +data Command + = Assert Term + | CheckSat + | CheckSatAssuming [PropLiteral] + | DeclareConst Symbol Sort + | DeclareDatatype Symbol DatatypeDec + | -- | same number + DeclareDatatypes (NonEmpty SortDec) (NonEmpty DatatypeDec) + | DeclareFun Symbol [Sort] Sort + | DeclareSort Symbol Numeral + | DefineFun FunctionDef + | DefineFunRec FunctionDef + | -- | same number + DefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) + | DefineSort Symbol [Symbol] Sort + | Echo StringLiteral + | Exit + | GetAssertions + | GetAssignment + | GetInfo InfoFlag + | GetModel + | GetOption Keyword + | GetProof + | GetUnsatAssumptions + | GetUnsatCore + | GetValue (NonEmpty Term) + | Pop Numeral + | Push Numeral + | Reset + | ResetAssertions + | SetInfo Attribute + | SetLogic Symbol + | SetOption ScriptOption deriving (Eq, Show) type Script = [Command] @@ -211,26 +232,33 @@ data BValue = BTrue | BFalse deriving (Eq, Show) -data ScriptOption = DiagnosticOutputChannel StringLiteral - | GlobalDeclarations BValue - | InteractiveMode BValue - | PrintSuccess BValue - | ProduceAssertions BValue - | ProduceAssignments BValue - | ProduceModels BValue - | ProduceProofs BValue - | ProduceUnsatAssumptions BValue - | ProduceUnsatCores BValue - | RandomSeed Numeral - | RegularOutputChannel StringLiteral - | ReproducibleResourceLimit Numeral - | Verbosity Numeral - | OptionAttr Attribute +data ScriptOption + = DiagnosticOutputChannel StringLiteral + | GlobalDeclarations BValue + | InteractiveMode BValue + | PrintSuccess BValue + | ProduceAssertions BValue + | ProduceAssignments BValue + | ProduceModels BValue + | ProduceProofs BValue + | ProduceUnsatAssumptions BValue + | ProduceUnsatCores BValue + | RandomSeed Numeral + | RegularOutputChannel StringLiteral + | ReproducibleResourceLimit Numeral + | Verbosity Numeral + | OptionAttr Attribute deriving (Eq, Show) -data InfoFlag = AllStatistics | AssertionStackLevels | Authors - | ErrorBehavior | Name | ReasonUnknown - | Version | IFKeyword Keyword +data InfoFlag + = AllStatistics + | AssertionStackLevels + | Authors + | ErrorBehavior + | Name + | ReasonUnknown + | Version + | IFKeyword Keyword deriving (Eq, Show) -- ** Responses (Sec 3.9.1) @@ -241,16 +269,19 @@ data ResReasonUnknown = Memout | Incomplete | ResReasonSExpr SExpr deriving (Eq, Show) -data ResModel = RMDefineFun FunctionDef - | RMDefineFunRec FunctionDef - | RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) -- ^ same number +data ResModel + = RMDefineFun FunctionDef + | RMDefineFunRec FunctionDef + | -- | same number + RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) -data ResInfo = IRErrorBehaviour ResErrorBehavior - | IRName StringLiteral - | IRAuthours StringLiteral - | IRVersion StringLiteral - | IRReasonUnknown ResReasonUnknown - | IRAttr Attribute +data ResInfo + = IRErrorBehaviour ResErrorBehavior + | IRName StringLiteral + | IRAuthours StringLiteral + | IRVersion StringLiteral + | IRReasonUnknown ResReasonUnknown + | IRAttr Attribute deriving (Eq, Show) type ValuationPair = (Term, Term) @@ -284,10 +315,12 @@ type GetValueRes = GeneralRes (NonEmpty ValuationPair) -data GeneralRes res = ResSuccess | ResSpecific res - | ResUnsupported | ResError StringLiteral +data GeneralRes res + = ResSuccess + | ResSpecific res + | ResUnsupported + | ResError StringLiteral deriving (Eq, Show) class SpecificSuccessRes s where specificSuccessRes :: GenParser st s - diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -208,6 +208,8 @@ disjuctionTest = pfs script "test/files/disjuction-head.smt2" +preprocTest = pfs script "test/files/preproc_0004_cfg_red.smt2" + -- | remove the comments commentTest = TestList [ onlyComment, commentWithString, commentWithSymbol, commentStringInSymbol, commentSymbolInString ] where @@ -224,6 +226,7 @@ , TestLabel "horn" hornTest , TestLabel "disjuction" disjuctionTest , TestLabel "extra" extraTest + , TestLabel "preproc" preprocTest ] main :: IO ()