diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,6 @@ +# Changelog for smt2-parser + +## 0.1.0.0 + +Initial release. + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright crvdgc (c) 2020 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of crvdgc nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,34 @@ +# smt2-parser + +A Haskell parser for [SMT-LIB](http://smtlib.cs.uiowa.edu/) version 2.6 [^1]. [The language reference](http://smtlib.cs.uiowa.edu/language.shtml) is available in [pdf](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf). + +## Usage + +Run a parser with an input string: + +```hs +-- parseStringEof :: Parser a -> T.Text -> Either ParseError a + +parseStringEof numeral "0" === Right ("0" :: Numeral) +parseStringEof identifier "(_ BitVec 32)" === Right (IdIndexed ("BitVec" :: Symbol) (fromList [IxNumeral "32"])) +``` + +Run a parser from a file string, possibly leading and trailing by spaces and having comments + +```hs +-- parseFileMsg :: Parser a -> T.Text -> Either T.Text a +>>> parseFileMsg script (T.pack "(set-logic HORN)\n\n(declare-fun |sum$unknown:2|\n ( Int Int ) Bool\n)\n(assert\n (forall ( (|$V-reftype:10| Int) (|$alpha-1:n| Int) (|$knormal:1| Int) (|$knormal:2| Int) (|$knormal:3| Int) )\n (=>\n ( and (= |$knormal:2| (- |$alpha-1:n| 1)) (= (not (= 0 |$knormal:1|)) (<= |$alpha-1:n| 0)) (= |$V-reftype:10| (+ |$alpha-1:n| |$knormal:3|)) (not (not (= 0 |$knormal:1|))) (|sum$unknown:2| |$knormal:3| |$knormal:2|) true )\n (|sum$unknown:2| |$V-reftype:10| |$alpha-1:n|)\n )\n )\n)(check-sat)") + +Right [ SetLogic "HORN" + , DeclareFun "sum$unknown:2" [SortSymbol (IdSymbol "Int"),...] (SortSymbol (IdSymbol "Bool")) + , Assert (TermForall ...) + , CheckSat + ] +``` + +## Known Issue + +`removeComment` may cause performance issue. Use `parseCommentFreeFileMsg` on a preprocessed comment-free file instead. + +[^1]: Barrett, Clarke, Pascal Fontaine and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical Report BarFT-RR-17, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/smt2-parser.cabal b/smt2-parser.cabal new file mode 100644 --- /dev/null +++ b/smt2-parser.cabal @@ -0,0 +1,58 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 4f628659c75828fd69bbaa9653ea5cc2f1b03a1f2a64632313f69a9874e522fc + +name: smt2-parser +version: 0.1.0.0 +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 +copyright: 2020 crvdgc +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + ChangeLog.md + +source-repository head + type: git + location: https://github.com/crvdgc/smt2-parser + +library + exposed-modules: + Language.SMT2.Parser + Language.SMT2.Syntax + other-modules: + Paths_smt2_parser + hs-source-dirs: + src + build-depends: + base >=4.13.0 && <4.14 + , parsec >=3.1.14 && <3.2 + , text >=1.2.4 && <1.3 + default-language: Haskell2010 + +test-suite smt2-parser-test + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Paths_smt2_parser + hs-source-dirs: + 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 + , smt2-parser + , text >=1.2.4 && <1.3 + default-language: Haskell2010 diff --git a/src/Language/SMT2/Parser.hs b/src/Language/SMT2/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMT2/Parser.hs @@ -0,0 +1,775 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-| + - Module : Language.SMT2.Parser + - Description : SMT language parser + - Maintainer : yokis1997@pku.edu.cn + - Stability : experimental +-} +module Language.SMT2.Parser + ( -- * Utils + -- $utils + parseString + , parseStringEof + , parseFileMsg + , parseCommentFreeFileMsg + , stripSpaces + , removeComment + -- * Lexicons (Sec. 3.1) + -- $lexicon + , numeral + , decimal + , hexadecimal + , binary + , stringLiteral + , reservedWord + , symbol + , keyword + -- * S-expressions (Sec. 3.2) + , slist + , specConstant + , sexpr + -- * Identifiers (Sec 3.3) + , index + , identifier + -- * Attributes (Sec. 3.4) + , attributeValue + , attribute + -- * Sorts (Sec 3.5) + , sort + -- * Terms and Formulas (Sec 3.6) + , qualIdentifier + , varBinding + , sortedVar + , matchPattern + , matchCase + , term + -- * Theory declarations (Sec 3.7) + , sortSymbolDecl + , metaSpecConstant + , funSymbolDecl + , parFunSymbolDecl + , theoryAttribute + , theoryDecl + -- * Logic Declarations (Sec 3.8) + , logicAttribute + , logic + -- * Scripts (Sec 3.9) + , 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 + -- *** instances + , 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) + +parseString :: Parser a -> T.Text -> Either ParseError a +parseString p = parse p "" + +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) + +-- * Utils +-- $utils +-- commonly used combinators + +-- | overlay @String@ to @Data.Text@ +text :: String -> GenParser st T.Text +text = (T.pack <$>) . string + + +-- | skip one or more @spaces@ +spaces1 :: GenParser st () +spaces1 = skipMany1 space + +-- | between round brackets +betweenBrackets :: GenParser st a -> GenParser st a +betweenBrackets = try . between (char '(' <* spaces) (spaces *> char ')') + +-- | @many p@, separated by @spaces1@, possibly has a trailing @spaces1@ +sepSpace :: GenParser st a -> GenParser st [a] +sepSpace p = sepEndBy p spaces1 + +-- | @many1 p@, separated by @spaces1@, possibly has a trailing @spaces1@ +sepSpace1 :: GenParser st a -> GenParser st (NonEmpty a) +sepSpace1 p = fromList <$> sepEndBy1 p spaces1 + +-- | @many p@, separated by @spaces@, possibly has a trailing @spaces@ +sepOptSpace :: GenParser st a -> GenParser st [a] +sepOptSpace p = sepEndBy p spaces + +-- | @many1 p@, separated by @spaces@, possibly has a trailing @spaces@ +sepOptSpace1 :: GenParser st a -> GenParser st (NonEmpty a) +sepOptSpace1 p = fromList <$> sepEndBy1 p spaces + +-- | match an string, ignore @spaces@ after, +-- input is not consumed if failed +tryStr :: String -> GenParser st () +tryStr s = try $ string s *> spaces $> () + +-- | match an string, must have @spaces1@ after, ignore them, +-- input is not consumed if failed +tryStr1 :: String -> GenParser st () +tryStr1 s = try $ string s *> spaces1 $> () + +tryStrBraket :: String -> GenParser st () +tryStrBraket s = try $ string s *> (spaces1 <|> lookLeftBraket) $> () + where + lookLeftBraket = try $ lookAhead (char '(') $> () + +-- | like @tryStr@, but prefix with a @':'@ +tryAttr :: String -> GenParser st () +tryAttr s = tryStr (':':s) + +-- | like @tryStr1@, but prefix with a @':'@ +tryAttr1 :: String -> GenParser st () +tryAttr1 s = tryStr1 (':':s) + +-- | strip away the leading and trailing @spaces@ +stripSpaces :: GenParser st a -> GenParser st a +stripSpaces p = spaces *> p <* spaces + +-- | remove comments +removeComment :: T.Text -> T.Text +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 + 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 + -- 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 + -- 3. for comments ended with \n\r or \r\n, the second is left + nextPos x acc = rc (acc `T.snoc` x) + +-- * Lexicons (Sec. 3.1) +-- $lexicon +-- Parsers for lexicons. +-- +-- For a numeral, a decimal, or a string literal, the parsed result is the same. +-- 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) + +decimal :: GenParser st Decimal +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 + +binary :: GenParser st Binary +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 + 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" + ] + +-- | accept all reserved words, +-- the exact content should be checked later in the parsing procedure +reservedWord :: GenParser st ReservedWord +reservedWord = choice (parseWord <$> reservedWords) + where + parseWord :: String -> GenParser st ReservedWord + parseWord w = try (text w) <* notFollowedBy anyChar + + +-- | characters allowed in a name +nameChar :: GenParser st Char +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") + where + simpleSymbol = do + c <- nameChar <|> letter + cs <- many (alphaNum <|> nameChar) + 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) + + +-- * S-expressions (Sec. 3.2) + +slist :: GenParser st SList +slist = betweenBrackets . sepSpace $ sexpr + +-- | 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" + +sexpr :: GenParser st SExpr +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 + +identifier :: GenParser st 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" + +attribute :: GenParser st Attribute +attribute = AttrKeyValue <$> try (keyword <* spaces1) <*> attributeValue + <|> AttrKey <$> keyword + "attribute" + + +-- * Sorts (Sec 3.5) + +sortParameter :: GenParser st Sort +sortParameter = betweenBrackets $ do + i <- identifier <* spaces1 + SortParameter i <$> sepSpace1 sort + +sort :: GenParser st Sort +sort = SortSymbol <$> try identifier + <|> sortParameter + "sort" + + +-- * Terms and Formulas (Sec 3.6) + +qualIdentifier :: GenParser st QualIdentifier +qualIdentifier = Unqualified <$> try identifier + <|> betweenBrackets annotation + "qual identifier" + where + annotation :: GenParser st QualIdentifier + annotation = do + tryStrBraket "as" + id <- identifier <* spaces1 + Qualified id <$> sort + +varBinding :: GenParser st VarBinding +varBinding = betweenBrackets $ VarBinding <$> symbol <* spaces1 <*> term + +sortedVar :: GenParser st SortedVar +sortedVar = betweenBrackets $ SortedVar <$> symbol <* spaces1 <*> sort + +matchPattern :: GenParser st MatchPattern +matchPattern = MPVariable <$> symbol + <|> mPConstructor + "pattern" + where + mPConstructor = betweenBrackets $ do + c <- symbol <* spaces1 + MPConstructor c <$> sepSpace1 symbol + +matchCase :: GenParser st MatchCase +matchCase = betweenBrackets $ do + p <- matchPattern <* spaces1 + MatchCase p <$> term + +term :: GenParser st Term +term = TermSpecConstant <$> try specConstant + <|> TermQualIdentifier <$> try qualIdentifier + <|> try application + <|> try binding + <|> try quantifyForall + <|> try quantifyExists + <|> try match + <|> try annotation + "term" + where + application = betweenBrackets $ do + id <- qualIdentifier <* spaces + TermApplication id <$> sepOptSpace1 term + binding = betweenBrackets $ do + tryStr "let" + vbs <- betweenBrackets $ sepOptSpace1 varBinding + space + TermLet vbs <$> term + quantifyForall = betweenBrackets $ do + tryStr "forall" + svs <- betweenBrackets $ sepOptSpace1 sortedVar + spaces + TermForall svs <$> term + quantifyExists = betweenBrackets $ do + tryStr "exists" + svs <- betweenBrackets $ sepOptSpace1 sortedVar + spaces + TermExists svs <$> term + match = betweenBrackets $ do + tryStr "match" + t <- term <* spaces + TermMatch t <$> betweenBrackets (sepOptSpace1 matchCase) + annotation = betweenBrackets $ do + char '!' <* spaces1 + t <- term <* spaces1 + TermAnnotation t <$> sepSpace1 attribute + + +-- * Theory declarations (Sec 3.7) + +sortSymbolDecl :: GenParser st SortSymbolDecl +sortSymbolDecl = betweenBrackets $ do + i <- identifier <* spaces1 + n <- numeral <* spaces -- if no attribute, don't need space + 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" + +funSymbolDecl :: GenParser st FunSymbolDecl +funSymbolDecl = try (betweenBrackets funConstant) + <|> try (betweenBrackets funMeta) + <|> try (betweenBrackets funIdentifier) + "non-parametric function symbol declaration" + where + funConstant = do + sc <- specConstant <* spaces1 + s <- sort <* spaces1 + FunConstant sc s <$> sepSpace attribute + funMeta = do + m <- metaSpecConstant <* spaces1 + s <- sort <* spaces1 + FunMeta m s <$> sepSpace attribute + funIdentifier = do + i <- identifier <* spaces1 + ss <- sepSpace1 sort + as <- sepSpace attribute + return $ FunIdentifier i ss as + +parFunSymbolDecl :: GenParser st ParFunSymbolDecl +parFunSymbolDecl = NonPar <$> funSymbolDecl + <|> betweenBrackets par + "potentially parametric function symbol declaration" + where + par = do + tryStr "par" + syms <- betweenBrackets . sepSpace1 $ symbol + spaces1 + betweenBrackets $ do + idt <- identifier <* spaces1 + 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" + +theoryDecl :: GenParser st TheoryDecl +theoryDecl = betweenBrackets $ do + tryStr "theory" + 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 + +logic :: GenParser st Logic +logic = betweenBrackets $ do + tryStr "logic" + s <- symbol <* spaces1 + Logic s <$> sepSpace1 logicAttribute + + +-- * Scripts (Sec 3.9) + +sortDec :: GenParser st SortDec +sortDec = betweenBrackets $ do + s <- symbol <* spaces1 + SortDec s <$> numeral + +selectorDec :: GenParser st SelectorDec +selectorDec = betweenBrackets $ do + s <- symbol <* spaces1 + SelectorDec s <$> sort + +constructorDec :: GenParser st ConstructorDec +constructorDec = betweenBrackets $ do + s <- symbol <* spaces1 + ConstructorDec s <$> sepSpace selectorDec + +datatypeDec :: GenParser st DatatypeDec +datatypeDec = DDNonparametric <$> betweenBrackets (sepSpace1 constructorDec) + <|> parametric + "datatype declaration" + where + parametric = betweenBrackets $ do + tryStr1 "par" + ss <- betweenBrackets $ sepSpace1 symbol + spaces + DDParametric ss <$> betweenBrackets (sepSpace1 constructorDec) + +functionDec :: GenParser st FunctionDec +functionDec = betweenBrackets $ do + s <- symbol <* spaces + svs <- betweenBrackets $ sepSpace sortedVar + spaces + FunctionDec s svs <$> sort + +functionDef :: GenParser st FunctionDef +functionDef = betweenBrackets $ do + s <- symbol <* spaces + svs <- betweenBrackets $ sepSpace sortedVar + t <- spaces *> sort <* spaces1 + FunctionDef s svs t <$> term + +propLiteral :: GenParser st PropLiteral +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" + where + cmd s p = try $ betweenBrackets (tryStr s *> p) + declareDatatypes = do + sds <- betweenBrackets $ sepSpace1 sortDec + 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" + declareFun = do + s <- symbol <* spaces1 + ss <- betweenBrackets $ sepSpace sort + spaces1 + DeclareFun s ss <$> sort + declareSort = do + s <- symbol <* spaces1 + DeclareSort s <$> numeral + defineFunsRec = do + fds <- betweenBrackets $ sepSpace1 functionDec + 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" + defineSort = do + s <- symbol <* spaces1 + ss <- betweenBrackets $ sepSpace symbol + spaces1 + DefineSort s ss <$> sort + getValue = betweenBrackets $ sepSpace1 term + +script :: GenParser st Script +script = spaces *> sepOptSpace command <* spaces + +bValue :: GenParser st BValue +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" + 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" + +-- ** 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) + +resErrorBehaviour :: GenParser st ResErrorBehavior +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" + +resModel :: GenParser st ResModel +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 + fdcs <- betweenBrackets $ sepSpace1 functionDec + 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" + +instance SpecificSuccessRes ResModel where + specificSuccessRes = resModel + +tValuationPair :: GenParser st TValuationPair +tValuationPair = betweenBrackets $ do + s <- symbol <* spaces1 + b <- bValue + return (s, b) + +resCheckSat :: GenParser st ResCheckSat +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 + +instance SpecificSuccessRes (NonEmpty ResInfo) where + specificSuccessRes = betweenBrackets $ sepSpace1 resInfo + +-- *** instances + +checkSatRes :: GenParser st CheckSatRes +checkSatRes = genRes + +instance SpecificSuccessRes StringLiteral where + specificSuccessRes = stringLiteral + +echoRes :: GenParser st EchoRes +echoRes = genRes + +instance SpecificSuccessRes [Term] where + specificSuccessRes = betweenBrackets $ sepSpace term + +getAssertionsRes :: GenParser st GetAssertionsRes +getAssertionsRes = genRes + +instance SpecificSuccessRes [TValuationPair] where + specificSuccessRes = betweenBrackets $ sepSpace tValuationPair + +getAssignmentRes :: GenParser st GetAssignmentRes +getAssignmentRes = genRes + +getInfoRes :: GenParser st GetInfoRes +getInfoRes = genRes + +getModelRes :: GenParser st GetModelRes +getModelRes = genRes + +instance SpecificSuccessRes AttributeValue where + specificSuccessRes = attributeValue + +getOptionRes :: GenParser st GetOptionRes +getOptionRes = genRes + +instance SpecificSuccessRes SExpr where + specificSuccessRes = sexpr + +getProofRes :: GenParser st GetProofRes +getProofRes = genRes + +instance SpecificSuccessRes [Symbol] where + specificSuccessRes = betweenBrackets $ sepSpace symbol + +getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes +getUnsatAssumpRes = genRes + +getUnsatCoreRes :: GenParser st GetUnsatCoreRes +getUnsatCoreRes = genRes + +valuationPair :: GenParser st ValuationPair +valuationPair = betweenBrackets $ do + t1 <- term <* spaces1 + t2 <- term + return (t1, t2) + +instance SpecificSuccessRes (NonEmpty ValuationPair) where + specificSuccessRes = betweenBrackets $ sepSpace1 valuationPair + +getValueRes :: GenParser st GetValueRes +getValueRes = genRes + diff --git a/src/Language/SMT2/Syntax.hs b/src/Language/SMT2/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/SMT2/Syntax.hs @@ -0,0 +1,293 @@ +{-| + - Module : Language.SMT2.Syntax + - Description : SMT language parser + - Maintainer : yokis1997@pku.edu.cn + - Stability : experimental +-} +module Language.SMT2.Syntax where + +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 StringLiteral = 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 + deriving (Eq, Show) + +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 + deriving (Eq, Show) + +data Identifier = IdSymbol Symbol + | IdIndexed Symbol (NonEmpty Index) + deriving (Eq, Show) + + +-- * Attributes (Sec. 3.4) + +data AttributeValue = AttrValSpecConstant SpecConstant + | AttrValSymbol Symbol + | AttrValSList SList + deriving (Eq, Show) + +data Attribute = AttrKey Keyword + | AttrKeyValue Keyword AttributeValue + deriving (Eq, Show) + + +-- * Sorts (Sec 3.5) + +data Sort = SortSymbol Identifier + | SortParameter Identifier (NonEmpty Sort) + deriving (Eq, Show) + + +-- * Terms and Formulas (Sec 3.6) + +data QualIdentifier = Unqualified Identifier + | Qualified Identifier Sort + deriving (Eq, Show) + +data VarBinding = VarBinding Symbol Term + deriving (Eq, Show) + +data SortedVar = SortedVar Symbol Sort + deriving (Eq, Show) + +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) + deriving (Eq, Show) + + +-- * Theory declarations (Sec 3.7) + +data SortSymbolDecl = SortSymbolDecl Identifier Numeral [Attribute] + deriving (Eq, Show) + +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 + deriving (Eq, Show) + +data ParFunSymbolDecl = NonPar FunSymbolDecl -- ^ non-parametric + | Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute] -- ^ parametric + deriving (Eq, Show) + +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 + deriving (Eq, Show) + +data Logic = Logic Symbol (NonEmpty LogicAttribute) + deriving (Eq, Show) + + +-- * Scripts (Sec 3.9) + +data SortDec = SortDec Symbol Numeral + deriving (Eq, Show) + +data SelectorDec = SelectorDec Symbol Sort + deriving (Eq, Show) + +data ConstructorDec = ConstructorDec Symbol [SelectorDec] + deriving (Eq, Show) + +data DatatypeDec = DDNonparametric (NonEmpty ConstructorDec) + | DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec) + deriving (Eq, Show) + +data FunctionDec = FunctionDec Symbol [SortedVar] Sort + deriving (Eq, Show) + +data FunctionDef = FunctionDef Symbol [SortedVar] Sort Term + deriving (Eq, Show) + +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 + deriving (Eq, Show) + +type Script = [Command] + +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 + deriving (Eq, Show) + +data InfoFlag = AllStatistics | AssertionStackLevels | Authors + | ErrorBehavior | Name | ReasonUnknown + | Version | IFKeyword Keyword + deriving (Eq, Show) + +-- ** Responses (Sec 3.9.1) + +data ResErrorBehavior = ImmediateExit | ContinuedExecution + deriving (Eq, Show) + +data ResReasonUnknown = Memout | Incomplete | ResReasonSExpr SExpr + deriving (Eq, Show) + +data ResModel = RMDefineFun FunctionDef + | RMDefineFunRec FunctionDef + | RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term) -- ^ same number + +data ResInfo = IRErrorBehaviour ResErrorBehavior + | IRName StringLiteral + | IRAuthours StringLiteral + | IRVersion StringLiteral + | IRReasonUnknown ResReasonUnknown + | IRAttr Attribute + deriving (Eq, Show) + +type ValuationPair = (Term, Term) + +type TValuationPair = (Symbol, BValue) + +data ResCheckSat = Sat | Unsat | Unknown + deriving (Eq, Show) + +-- *** instances + +type CheckSatRes = GeneralRes ResCheckSat + +type EchoRes = GeneralRes StringLiteral + +type GetAssertionsRes = GeneralRes [Term] + +type GetAssignmentRes = GeneralRes [TValuationPair] + +type GetInfoRes = GeneralRes (NonEmpty ResInfo) + +type GetModelRes = GeneralRes ResModel + +type GetOptionRes = GeneralRes AttributeValue + +type GetProofRes = GeneralRes SExpr + +type GetUnsatAssumpRes = GeneralRes [Symbol] + +type GetUnsatCoreRes = GeneralRes [Symbol] + +type GetValueRes = GeneralRes (NonEmpty ValuationPair) + +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 new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,233 @@ +{-# LANGUAGE OverloadedStrings #-} +import Data.List.NonEmpty (fromList) +import qualified Data.Text as T +import qualified Data.Text.IO as TIO +import Language.SMT2.Parser +import Language.SMT2.Syntax +import Test.HUnit +import Text.Parsec.Text (GenParser) + +-- * Parsing tests +-- Test cases are from +-- 1. the original [spec](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf). +-- 2. HORN clause samples from [SV-COMP](https://github.com/sosy-lab/sv-benchmarks) & [benchmarks](https://github.com/hopv/benchmarks/). +-- 3. Examples of horn-like clauses with disjuction on heads. + +-- | parse and test a string, expecting @a@ +pe :: (Eq a, Show a) => GenParser () a -> T.Text -> a -> Test +pe p s expected = TestCase $ case parseStringEof p s of + Right actual -> expected @=? actual + Left _ -> assertFailure $ "should succeed for " <> T.unpack s + +parseTest :: (T.Text -> Assertion) -> (T.Text -> Assertion) -> GenParser () a -> T.Text -> Assertion +parseTest success failure p s = case parseStringEof p s of + Left _ -> failure s + Right _ -> success s + +-- | parse and success, an assertion +pas :: GenParser () a -> T.Text -> Assertion +pas = parseTest (\_ -> pure ()) (\s -> assertFailure $ "should succeed for " <> T.unpack s) + +-- | parse and failure, an assertion +paf :: GenParser () a -> T.Text -> Assertion +paf = parseTest (\s -> assertFailure $ "should fail for " <> T.unpack s) (\_ -> pure ()) + +-- | parse and success +ps :: GenParser () a -> T.Text -> Test +ps p s = TestCase $ pas p s + +-- | parse and failure +pf :: GenParser () a -> T.Text -> Test +pf p s = TestCase $ paf p s + +-- | parse file success +pfs :: GenParser () a -> FilePath -> Test +pfs p f = TestCase $ do + s <- TIO.readFile f + pas (stripSpaces p) (removeComment s) + + +-- | Sec 3.1 +lexiconTest = TestList [ pN "0" ("0" :: Numeral) + , pN "42" ("42" :: Numeral) + , pf numeral "02" -- should not start with 0 + , pf numeral "221b" -- should not contain letters + , pD "0.0" ("0.0" :: Decimal) + , pD "0.00" ("0.00" :: Decimal) + , pD "0.1" ("0.1" :: Decimal) + , pD "13.37" ("13.37" :: Decimal) + , pD "1.010" ("1.010" :: Decimal) + , pf decimal ".5" + , pH "#x0" ("0" :: Hexadecimal) + , pH "#xa04" ("a04" :: Hexadecimal) -- alphabet + , pH "#xA04" ("a04" :: Hexadecimal) -- alphabet, to lower case + , pH "#x01Ab" ("01ab" :: Hexadecimal) -- mixture + , pH "#x61ff" ("61ff" :: Hexadecimal) + , pH "#xdeadbeef" ("deadbeef" :: Hexadecimal) + , pf hexadecimal "#x#x" -- signs + , pf hexadecimal "#xA1G01" -- letter is not hex degit + , pB "#b0" ("0" :: Binary) + , pB "#b1" ("1" :: Binary) + , pB "#b001" ("001" :: Binary) + , pB "#b101011" ("101011" :: Binary) + , pf binary "#b02" + , pL "\"this is a string literal\"" ("this is a string literal" :: StringLiteral) + , pL "\"\"" ("" :: StringLiteral) + , pL "\"She said: \"\"Bye bye\"\" and left.\"" ("She said: \"Bye bye\" and left." :: StringLiteral) + , pL "\"this is a string literal\nwith a line break in it\"" ("this is a string literal\nwith a line break in it" :: StringLiteral) + , pR "par" ("par" :: ReservedWord) + , pR "NUMERAL" ("NUMERAL" :: ReservedWord) + , pR "_" ("_" :: ReservedWord) + , pR "!" ("!" :: ReservedWord) + , pR "as" ("as" :: ReservedWord) + , pR "set-logic" ("set-logic" :: ReservedWord) + , pf reservedWord "asleep" -- prefix + , pf symbol "par" -- symbol should not be a reserved word + , pf symbol "NUMERAL" + , pf symbol "_" + , pf symbol "!" + , pf symbol "as" + , pS "asleep" ("asleep" :: Symbol) -- prefixed by a reserved word + , pS "+" ("+" :: Symbol) + , pS "<=" ("<=" :: Symbol) + , pS "x" ("x" :: Symbol) + , pS "**" ("**" :: Symbol) + , pS "$" ("$" :: Symbol) + , pS "" ("" :: Symbol) + , pS "abc77" ("abc77" :: Symbol) + , pS "*$s&6" ("*$s&6" :: Symbol) + , pS ".kkk" (".kkk" :: Symbol) + , pS ".8" (".8" :: Symbol) + , pS "+34" ("+34" :: Symbol) + , pS "-32" ("-32" :: Symbol) + , pS "|this is a single quoted symbol|" ("this is a single quoted symbol" :: Symbol) + , pS "|so is\nthis one|" ("so is\nthis one" :: Symbol) + , pS "||" ("" :: Symbol) + , pS "|\" can occur too|" ("\" can occur too" :: Symbol) + , pS "|af kljˆ∗(0asfsfe2(&∗)&(#ˆ$>>>?”’]]984|" ("af kljˆ∗(0asfsfe2(&∗)&(#ˆ$>>>?”’]]984" :: Symbol) + , pS "|abc|" ("abc" :: Symbol) -- quoted simple symbol is the same + , pS "abc" ("abc" :: Symbol) + , pK ":date" ("date" :: Keyword) + , pK ":a2" ("a2" :: Keyword) + , pK ":foo-bar" ("foo-bar" :: Keyword) + , pK ":<=" ("<=" :: Keyword) + , pK ":56" ("56" :: Keyword) + , pK ":->" ("->" :: Keyword) + , pK ":~!@$%^&*_-+=<>.?/" ("~!@$%^&*_-+=<>.?/" :: Keyword) + ] + where + pN = pe numeral + pD = pe decimal + pH = pe hexadecimal + pB = pe binary + pL = pe stringLiteral + pR = pe reservedWord + pS = pe symbol + pK = pe keyword + +syntaxTest = TestList [ pI "plus" (IdSymbol "plus") + , pI "+" (IdSymbol "+") + , pI "<=" (IdSymbol "<=") + , pI "Real" (IdSymbol "Real") + , pI "|John Brown|" (IdSymbol "John Brown") + , pI "(_ vector-add 4 5)" (IdIndexed ("vector-add" :: Symbol) (fromList [IxNumeral "4", IxNumeral "5"])) + , pI "(_ BitVec 32)" (IdIndexed ("BitVec" :: Symbol) (fromList [IxNumeral "32"])) + , pI "(_ move up)" (IdIndexed ("move" :: Symbol) (fromList [IxSymbol "up"])) + , pI "(_ move down)" (IdIndexed ("move" :: Symbol) (fromList [IxSymbol "down"])) + , pI "(_ move left)" (IdIndexed ("move" :: Symbol) (fromList [IxSymbol "left"])) + , pI "(_ move right)" (IdIndexed ("move" :: Symbol) (fromList [IxSymbol "right"])) + , pA ":left-assoc" (AttrKey ("left-assoc" :: Keyword)) + , pA ":status unsat" (AttrKeyValue ("status" :: Keyword) (AttrValSymbol ("unsat" :: Symbol))) + , pA ":my_attribute (humpty dumpty)" (AttrKeyValue + ("my_attribute" :: Keyword) + (AttrValSList [ SESymbol "humpty" + , SESymbol "dumpty"])) + , pA ":authors \"Jack and Jill\"" (AttrKeyValue + ("authors" :: Keyword) + (AttrValSpecConstant . SCString $ "Jack and Jill")) + , pT "Int" (SortSymbol . IdSymbol $ "Int") + , pT "Bool" (SortSymbol . IdSymbol $ "Bool") + , pT "(_ BitVec 3)" (SortSymbol . IdIndexed "BitVec" $ fromList [IxNumeral "3"]) + , pT "(List (Array Int Real))" (SortParameter + (IdSymbol "List") + (fromList [SortParameter + (IdSymbol "Array") + (fromList [ SortSymbol . IdSymbol $ "Int" + , SortSymbol . IdSymbol $ "Real"])])) + , pT "((_ FixedSizeList 4) Real)" (SortParameter + (IdIndexed "FixedSizeList" (fromList [IxNumeral "4"])) + (fromList [SortSymbol . IdSymbol $ "Real"])) + , pT "(Set (_ Bitvec 3))" (SortParameter + (IdSymbol "Set") + (fromList [SortSymbol . IdIndexed "Bitvec" $ fromList [IxNumeral "3"]])) + , ps term $ mkTerm [ "(forall ((x (List Int)) (y (List Int)))" + , "(= (append x y)" + , "(ite (= x (as nil (List Int)))" + , "y" + , "(let ((h (head x)) (t (tail x)))" + , "(insert h (append t y))))))" + ] + , ps term $ mkTerm [ "(forall ((l1 (List Int)) (l2 (List Int)))" + , "(= (append l1 l2)" + , "(match l1 (" + , "(nil l2)" + , "((cons h t) (cons h (append t l2)))))))" + ] -- Axiom for list append: version 1 + , ps term $ mkTerm [ "(forall ((l1 (List Int)) (l2 (List Int)))" + , "(= (append l1 l2)" + , "(match l1 (" + , "((cons h t) (cons h (append t l2)))" + , "(_ l2)))))" + ] -- Axiom for list append: version 2 + , psP "(+ Real Real Real :left-assoc)" + , psP "(and Bool Bool Bool :left-assoc)" + , psP "(par (X) (insert X (List X) (List X) :right -assoc))" + , psP "(< Real Real Bool :chainable)" + , psP "(equiv Elem Elem Bool :chainable)" + , psP "(par (X) (Disjoint (Set X) (Set X) Bool :pairwise))" + , psP "(par (X) (distinct X X Bool :pairwise))" + ] + where + pI = pe identifier + pA = pe attribute + pT = pe sort + psP = ps parFunSymbolDecl + mkTerm = T.intercalate "\n" + +-- | test the theory declaration from Fig. 3.1 (http://smtlib.cs.uiowa.edu/theories-Core.shtml) +theoryCoreTest = pfs theoryDecl "test/files/Theories-Core.smt2" + +logicLIATest = pfs logic "test/files/Logic-LIA.smt2" + +specTest = TestList [ lexiconTest, syntaxTest, theoryCoreTest, logicLIATest ] + +hornTest = TestList [ pfs script "test/files/sum.smt2" + , pfs script "test/files/buildheap.nts.smt2" + ] + +disjuctionTest = pfs script "test/files/disjuction-head.smt2" + +-- | remove the comments +commentTest = TestList [ onlyComment, commentWithString, commentWithSymbol, commentStringInSymbol, commentSymbolInString ] + where + onlyComment = rc "; this is a comment\n;so is this\r" " \n \r" + commentWithString = rc "; this is a comment,\n\"but this isn't, even after ; it won't be\";however\n" " \n\"but this isn't, even after ; it won't be\" \n" + commentWithSymbol = rc "|;here we go;\n|;not so fast\n\r" "|;here we go;\n| \n\r" + commentStringInSymbol = rc "|;wait\n I speak \"symbolism;&others\n\";next|;finally\n" "|;wait\n I speak \"symbolism;&others\n\";next| \n" + commentSymbolInString = rc "\"A |quoted symbol ;example\n| ;actually no\r\n\";unless\r" "\"A |quoted symbol ;example\n| ;actually no\r\n\" \r" + rc before after = removeComment before ~?= after + +extraTest = TestList [ commentTest ] + +tests = TestList [ TestLabel "spec" specTest + , TestLabel "horn" hornTest + , TestLabel "disjuction" disjuctionTest + , TestLabel "extra" extraTest + ] + +main :: IO () +main = do + counts <- runTestTT tests + print counts +