smt2-parser 0.1.0.0 → 0.1.0.1
raw patch · 5 files changed
+544/−444 lines, 5 filesdep ~HUnitdep ~basedep ~parsecPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: HUnit, base, parsec, text
API changes (from Hackage documentation)
Files
- ChangeLog.md +4/−0
- smt2-parser.cabal +10/−12
- src/Language/SMT2/Parser.hs +355/−293
- src/Language/SMT2/Syntax.hs +172/−139
- test/Spec.hs +3/−0
ChangeLog.md view
@@ -4,3 +4,7 @@ Initial release. +## 0.1.0.1++Relax dependency constraints.+
smt2-parser.cabal view
@@ -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 <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+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
src/Language/SMT2/Parser.hs view
@@ -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-
src/Language/SMT2/Syntax.hs view
@@ -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-
test/Spec.hs view
@@ -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 ()