smt2-parser (empty) → 0.1.0.0
raw patch · 8 files changed
+1431/−0 lines, 8 filesdep +HUnitdep +basedep +parsecsetup-changed
Dependencies added: HUnit, base, parsec, smt2-parser, text
Files
- ChangeLog.md +6/−0
- LICENSE +30/−0
- README.md +34/−0
- Setup.hs +2/−0
- smt2-parser.cabal +58/−0
- src/Language/SMT2/Parser.hs +775/−0
- src/Language/SMT2/Syntax.hs +293/−0
- test/Spec.hs +233/−0
+ ChangeLog.md view
@@ -0,0 +1,6 @@+# Changelog for smt2-parser++## 0.1.0.0++Initial release.+
+ LICENSE view
@@ -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.
+ README.md view
@@ -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+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ smt2-parser.cabal view
@@ -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 <https://github.com/crvdgc/smt2-parser#readme>+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
+ src/Language/SMT2/Parser.hs view
@@ -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+
+ src/Language/SMT2/Syntax.hs view
@@ -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+
+ test/Spec.hs view
@@ -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 "<sas" ("<sas" :: Symbol)+ , pS "<adf>" ("<adf>" :: 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+