SmtLib (empty) → 0.1.0.0
raw patch · 8 files changed
+1790/−0 lines, 8 filesdep +basedep +parsecdep +transformerssetup-changed
Dependencies added: base, parsec, transformers
Files
- LICENSE +16/−0
- Setup.hs +2/−0
- SmtLib.cabal +75/−0
- Smtlib/Parsers/CommandsParsers.hs +473/−0
- Smtlib/Parsers/CommonParsers.hs +453/−0
- Smtlib/Parsers/ResponseParsers.hs +333/−0
- Smtlib/Syntax/ShowSL.hs +198/−0
- Smtlib/Syntax/Syntax.hs +240/−0
+ LICENSE view
@@ -0,0 +1,16 @@+ WHAT THE FUCK YOU WANT TO PUBLIC LICENSE + Version 2, December 2004 + + Copyright (C) 2004 Sam Hocevar <sam@hocevar.net> + + Everyone is permitted to copy and distribute verbatim or modified + copies of this license document, and changing it is allowed as long + as the name is changed. + + DO WHAT THE FUCK YOU WANT TO PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. You just DO WHAT THE FUCK YOU WANT TO. + + +
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple +main = defaultMain
+ SmtLib.cabal view
@@ -0,0 +1,75 @@+-- Initial SmtLib.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +-- The name of the package. +name: SmtLib + +-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented. +-- http://www.haskell.org/haskellwiki/Package_versioning_policy +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 + +-- A short (one-line) description of the package. +synopsis: Library for parsing SMTLIB2 + +-- A longer description of the package. +-- description: + +-- URL for the project homepage or repository. +homepage: https://github.com/MfesGA/HsmtlibParser + +-- The license under which the package is released. +license: MIT + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s). +author: Roger + +description: SMTLib2 syntax and parsers. + + +-- An email address to which users can send suggestions, bug reports, and +-- patches. +maintainer: rogerp62@outlook.com + +-- A copyright notice. +-- copyright: + +category: Formal Methods + +build-type: Simple + +-- Constraint on the version of Cabal needed to build this package. +cabal-version: >=1.10 + + +library + -- Modules exported by the library. + exposed-modules: Smtlib.Parsers.CommonParsers, + Smtlib.Parsers.ResponseParsers, + Smtlib.Parsers.CommandsParsers, + Smtlib.Syntax.Syntax, + Smtlib.Syntax.ShowSL + + -- Modules included in this library but not exported. + -- other-modules: + + -- Other library packages from which modules are imported. + build-depends: base >= 4.6 && < 4.8 + , parsec ==3.1.* + , transformers ==0.4.* + + default-language: Haskell2010 + -- Directories containing source files. + -- hs-source-dirs: Smtlib + + +source-repository head + + type: git + location: https://github.com/MfesGA/HsmtlibParser
+ Smtlib/Parsers/CommandsParsers.hs view
@@ -0,0 +1,473 @@+{-| +Module : Smtlib.Parsers.CommandsParsers +Description : Parsers for Smtlib Commands +Copyright : Rogério Pontes 2015 +License : WTFPL +Maintainer : rogerp62@outlook.com +Stability : stable + +This module contains all the required individual parsers for each Smtlib command, +plus one parser to parse an entire SMTLib2 file, parseSource. + +-} +module Smtlib.Parsers.CommandsParsers where + +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Smtlib.Parsers.CommonParsers +import Smtlib.Syntax.Syntax +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc + + + +{- + ######################################################################### + # # + # Parser for an SMTLib2 File # + # # + ######################################################################### +-} + + +parseSource :: ParsecT String u Identity Source +parseSource = Pc.many $ parseCommand <* Pc.try emptySpace + + +{- + "###################### Parser For Commands ############################### +-} +parseCommand :: ParsecT String u Identity Command +parseCommand = Pc.try parseSetLogic + <|> Pc.try parseSetOption + <|> Pc.try parseSetInfo + <|> Pc.try parseDeclareSort + <|> Pc.try parseDefineSort + <|> Pc.try parseDeclareFun + <|> Pc.try parseDefineFun + <|> Pc.try parsePush + <|> Pc.try parsePop + <|> Pc.try parseAssert + <|> Pc.try parseCheckSat + <|> Pc.try parseGetAssertions + <|> Pc.try parseGetProof + <|> Pc.try parseGetUnsatCore + <|> Pc.try parseGetValue + <|> Pc.try parseGetAssignment + <|> Pc.try parseGetOption + <|> Pc.try parseGetInfo + <|> parseExit + + + +{- + ######################################################################### + # # + # Parser for each command # + # # + ######################################################################### +-} + + + + +parseSetLogic :: ParsecT String u Identity Command +parseSetLogic = do + _ <- aspO + _ <- emptySpace + _ <- string "set-logic" + _ <- emptySpace + symb <- symbol + _ <- emptySpace + _ <- aspC + return $ SetLogic symb + + +parseSetOption :: ParsecT String u Identity Command +parseSetOption = do + _ <- aspO + _ <- emptySpace + _ <- string "set-option" + _ <- emptySpace + attr <- parseOption + _ <- emptySpace + _ <- aspC + return $ SetOption attr + +parseSetInfo :: ParsecT String u Identity Command +parseSetInfo = do + _ <- aspO + _ <- emptySpace + _ <- string "set-info" + _ <- emptySpace <?> "foi aqui1?" + attr <- parseAttribute <?> "foi aqui2?" + _ <- emptySpace + _ <- aspC + return $ SetInfo attr + + +parseDeclareSort :: ParsecT String u Identity Command +parseDeclareSort = do + _ <- aspO + _ <- emptySpace + _ <- string "declare-sort" + _ <- emptySpace + symb <- symbol + _ <- emptySpace + nume <- numeral + _ <- emptySpace + _ <- aspC + return $ DeclareSort symb (read nume :: Int) + +parseDefineSort :: ParsecT String u Identity Command +parseDefineSort = do + _ <- aspO + _ <- emptySpace + _ <- string "define-sort" + _ <- emptySpace + symb <- symbol + _ <- emptySpace + _ <- aspO + symbs <- Pc.many $ symbol <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + sort <- parseSort + _ <- emptySpace + _ <- aspC + return $ DefineSort symb symbs sort + + +parseDeclareFun :: ParsecT String u Identity Command +parseDeclareFun = do + _ <-aspO + _ <- emptySpace + _ <- string "declare-fun" + _ <- emptySpace + symb <- symbol + _ <- emptySpace + _ <- aspO + _ <- emptySpace + sorts <- Pc.many $ parseSort <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + sort <- parseSort + _ <- emptySpace + _ <- aspC + return $ DeclareFun symb sorts sort + + +parseDefineFun :: ParsecT String u Identity Command +parseDefineFun = do + _ <- aspO + _ <- emptySpace + _ <- string "define-fun" + _ <- emptySpace + symb <- symbol + _ <- emptySpace + _ <- aspO + sVars <- Pc.many $ parseSortedVar <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + sort <- parseSort + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ DefineFun symb sVars sort term + + +parsePush :: ParsecT String u Identity Command +parsePush = do + _ <- aspO + _ <- emptySpace + _ <- string "push" + _ <- emptySpace + nume <- numeral + _ <- emptySpace + _ <- aspC + return $ Push (read nume :: Int) + + +parsePop :: ParsecT String u Identity Command +parsePop = do + _ <- aspO + _ <- emptySpace + _ <- string "pop" + _ <- emptySpace + nume <- numeral + _ <- emptySpace + _ <- aspC + return $ Pop (read nume :: Int) + + + +parseAssert :: ParsecT String u Identity Command +parseAssert = do + _ <- aspO + _ <- emptySpace + _ <- string "assert" + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ Assert term + + +parseCheckSat :: ParsecT String u Identity Command +parseCheckSat = do + _ <- aspO + _ <- emptySpace + _ <- string "check-sat" + _ <- emptySpace + _ <- aspC + return CheckSat + + +parseGetAssertions :: ParsecT String u Identity Command +parseGetAssertions = do + _ <- aspO + _ <-emptySpace + _ <- string "get-assertions" + _ <- emptySpace + _ <- aspC + return GetAssertions + +parseGetProof :: ParsecT String u Identity Command +parseGetProof = do + _ <- aspO + _ <- emptySpace + _ <- string "get-proof" + _ <- emptySpace + _ <-aspC + return GetProof + +parseGetUnsatCore :: ParsecT String u Identity Command +parseGetUnsatCore = do + _ <- aspO + _ <- emptySpace + _ <- string "get-unsat-core" + _ <- emptySpace + _ <- aspC + return GetUnsatCore + +parseGetValue :: ParsecT String u Identity Command +parseGetValue = do + _ <- aspO + _ <- emptySpace + _ <- string "get-value" + _ <- emptySpace + _ <- aspO + terms <- Pc.many1 $ parseTerm <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + _ <- aspC + return $ GetValue terms + +parseGetAssignment :: ParsecT String u Identity Command +parseGetAssignment = do + _ <- aspO + _ <- emptySpace + _ <- string "get-assignment" + _ <- emptySpace + _ <- aspC + return GetAssignment + + +parseGetOption :: ParsecT String u Identity Command +parseGetOption = do + _ <- aspO + _ <- emptySpace + _ <- string "get-option" + _ <- emptySpace + word <- keyword + _ <- emptySpace + _ <- aspC + return $ GetOption word + + +parseGetInfo :: ParsecT String u Identity Command +parseGetInfo = do + _ <- aspO + _ <- emptySpace + _ <- string "get-info" + _ <- emptySpace + flag <- parseInfoFlags + _ <- emptySpace + _ <- aspC + return $ GetInfo flag + + + +parseExit :: ParsecT String u Identity Command +parseExit = do + _ <- aspO + _ <- emptySpace + _ <- string "exit" + _ <- emptySpace + _ <- aspC + return Exit + + + + +{- + ######################################################################### + # # + # Parse Command Options # + # # + ######################################################################### +-} + +parseOption :: ParsecT String u Identity Option +parseOption = Pc.try parsePrintSuccess + <|> Pc.try parseExpandDefinitions + <|> Pc.try parseInteractiveMode + <|> Pc.try parseProduceProofs + <|> Pc.try parseProduceUnsatCores + <|> Pc.try parseProduceModels + <|> Pc.try parseProduceAssignments + <|> Pc.try parseRegularOutputChannel + <|> Pc.try parseDiagnosticOutputChannel + <|> Pc.try parseRandomSeed + <|> Pc.try parseVerbosity + <|> Pc.try parseOptionAttribute + + +-- parse PrintSucess +parsePrintSuccess :: ParsecT String u Identity Option +parsePrintSuccess = do + _ <- string ":print-success" + _ <- spaces + val <- parseBool + return $ PrintSucess val + + +parseExpandDefinitions :: ParsecT String u Identity Option +parseExpandDefinitions = do + _ <- string ":expand-definitions" + _ <- spaces + val <- parseBool + return $ ExpandDefinitions val + + +parseInteractiveMode :: ParsecT String u Identity Option +parseInteractiveMode = do + _ <- string ":interactive-mode" + _ <- spaces + val <- parseBool + return $ InteractiveMode val + +parseProduceProofs :: ParsecT String u Identity Option +parseProduceProofs = do + _ <- string ":produce-proofs" + _ <- spaces + val <- parseBool + return $ ProduceProofs val + + +parseProduceUnsatCores :: ParsecT String u Identity Option +parseProduceUnsatCores = do + _ <- string ":produce-unsat-cores" + _ <- spaces + val <- parseBool + return $ ProduceUnsatCores val + + +parseProduceModels :: ParsecT String u Identity Option +parseProduceModels = do + _ <- string ":produce-models" + _ <- spaces + val <- parseBool + return $ ProduceModels val + +parseProduceAssignments :: ParsecT String u Identity Option +parseProduceAssignments = do + _ <- string ":produce-assignnments" + _ <- spaces + val <- parseBool + return $ ProduceAssignments val + + +parseRegularOutputChannel :: ParsecT String u Identity Option +parseRegularOutputChannel = do + _ <- string ":regular-output-channel" + _ <- spaces + val <- str + return $ RegularOutputChannel val + + +parseDiagnosticOutputChannel :: ParsecT String u Identity Option +parseDiagnosticOutputChannel = do + _ <- string ":diagnostic-output-channel" + _ <- spaces + val <- str + return $ DiagnosticOutputChannel val + +parseRandomSeed :: ParsecT String u Identity Option +parseRandomSeed = do + _ <- string ":random-seed" + _ <- spaces + val <- numeral + return $ RandomSeed (read val :: Int) + + +parseVerbosity :: ParsecT String u Identity Option +parseVerbosity = do + _ <- string ":verbosity" + _ <- spaces + val <- numeral + return $ Verbosity (read val :: Int) + + +parseOptionAttribute :: ParsecT String u Identity Option +parseOptionAttribute = do + attr <- parseAttribute + return $ OptionAttr attr + + + + +{- + ######################################################################### + # # + # Parsers for Info FLags # + # # + ######################################################################### +-} + +parseInfoFlags :: ParsecT String u Identity InfoFlags +parseInfoFlags = parseErrorBehaviour + <|> parseName + <|> parseAuthors + <|> parseVersion + <|> parseStatus + <|> parseReasonUnknown + <|> parseInfoKeyword + <|> parseAllStatistics + + +parseErrorBehaviour :: ParsecT String u Identity InfoFlags +parseErrorBehaviour = string ":error-behaviour" *> return ErrorBehavior + + +parseName :: ParsecT String u Identity InfoFlags +parseName = string ":name" *> return Name + +parseAuthors :: ParsecT String u Identity InfoFlags +parseAuthors = string ":authors" *> return Authors + +parseVersion :: ParsecT String u Identity InfoFlags +parseVersion = string ":version" *> return Version + +parseStatus :: ParsecT String u Identity InfoFlags +parseStatus = string ":status" *> return Status + +parseReasonUnknown :: ParsecT String u Identity InfoFlags +parseReasonUnknown = string ":reason-unknown" *> return ReasonUnknown + +parseAllStatistics :: ParsecT String u Identity InfoFlags +parseAllStatistics = string ":all-statistics" *> return AllStatistics + +parseInfoKeyword :: ParsecT String u Identity InfoFlags +parseInfoKeyword = liftM InfoFlags keyword
+ Smtlib/Parsers/CommonParsers.hs view
@@ -0,0 +1,453 @@+{-| +Module : Smtlib.Parsers.CommandsParsers +Description : Common parsers for commands and responses. +Copyright : Rogério Pontes 2015 +License : WTFPL +Maintainer : rogerp62@outlook.com +Stability : stable + +This module contains some auxiliar parsers, used to parse commands or responses. +-} +module Smtlib.Parsers.CommonParsers where + + +{- + In the String terminal, it does not parse C-style characters. + Quoted Symbol does not parse all printable ASCII characters. +-} + +import Control.Applicative as Ctr hiding ((<|>)) +import Data.Functor.Identity +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc +import Smtlib.Syntax.Syntax +import Control.Monad + +(<:>) :: Applicative f => f a -> f [a] -> f [a] +(<:>) a b = (:) <$> a <*> b + +(<++>) :: Applicative f => f [a] -> f [a] -> f [a] +(<++>) a b = (++) <$> a <*> b + +parseBool :: ParsecT String u Identity Bool +parseBool = (true *> return True) <|> (false *> return False) + + +-- Parse a Numeral + +numeral :: ParsecT String u Identity String +numeral = many1 digit + +num :: ParsecT String u Identity String +num = Pc.many digit +-- Parse a decimal + +decimal :: ParsecT String u Identity String +decimal = numeral <++> dot <++> Pc.try zeros <++> num + +zeros :: ParsecT String u Identity String +zeros = Pc.many $ char '0' + + +dot :: ParsecT String u Identity String +dot = string "." + +-- parse a Hexadecimal + +hexadecimal :: ParsecT String u Identity String +hexadecimal = string "#x" *> many1 hexDigit + + +--parsea a Binary +binary :: ParsecT String u Identity String +binary = string "#b" *> many1 bin + +bin :: ParsecT String u Identity Char +bin = char '0' <|> char '1' + + +--parse a String +-- Dosent parse strings with escape characters +str :: ParsecT String u Identity String +str = string "\"" <++> Pc.many strChar <++> string "\"" + +strChar :: ParsecT String u Identity Char +strChar = alphaNum + <|> char ' ' + <|> char ':' + <|> char ',' + + +--parse a Symbol +symbol :: ParsecT String u Identity String +symbol = simpleSymbol <|> quotedSymbol + +quotedSymbol :: ParsecT String u Identity String +quotedSymbol = char '|' *> Pc.many (noneOf "|") <* char '|' + +simpleSymbol :: ParsecT String u Identity String +simpleSymbol = (letter <|> spcSymb) <:> sq + where sq = Pc.many (alphaNum <|> spcSymb) + +spcSymb :: ParsecT String u Identity Char +spcSymb = oneOf "+-/*=%?!.$_~^&<>@" + +-- parse a key word +keyword :: ParsecT String u Identity String +keyword = char ':' <:> Pc.many (alphaNum<|> spcSymb) + + +aspO :: ParsecT String u Identity Char +aspO = char '(' + +aspC :: ParsecT String u Identity Char +aspC = char ')' + +aspUS :: ParsecT String u Identity Char +aspUS = char '_' + + +true :: ParsecT String u Identity String +true = string "true" + +false :: ParsecT String u Identity String +false = string "false" + + +emptySpace :: ParsecT String u Identity String +emptySpace = Pc.try $ Pc.many $ + char ' ' <|> char '\n' <|> char '\t' <|> char '\r' + +reservedWords :: ParsecT String u Identity String +reservedWords = string "let" + <|> string "par" + <|> string "_" + <|> string "!" + <|> string "as" + <|> string "forall" + <|> string "exists" + <|> string "NUMERAL" + <|> string "DECIMAL" + <|> string "STRING" + + + + +{- + ######################################################################### + # # + # Parsers for Terms # + # # + ######################################################################### +-} + + +-- Term +parseTerm :: ParsecT String u Identity Term +parseTerm = parseTSPC + <|> Pc.try parseTQID + <|> Pc.try parseTQIT + <|> Pc.try parseTermLet + <|> Pc.try parseTermFA + <|> Pc.try parseTermEX + <|> parseTermAnnot + +parseTSPC :: ParsecT String u Identity Term +parseTSPC = liftM TermSpecConstant parseSpecConstant + +parseTQID :: ParsecT String u Identity Term +parseTQID = liftM TermQualIdentifier parseQualIdentifier + +parseTQIT :: ParsecT String u Identity Term +parseTQIT = do + _ <- aspO + _ <- emptySpace + iden <- parseQualIdentifier + _ <- emptySpace + terms <- Pc.many $ parseTerm <* Pc.try emptySpace + _ <- aspC + return $ TermQualIdentifierT iden terms + +parseTermLet :: ParsecT String u Identity Term +parseTermLet = do + _ <- aspO + _ <- emptySpace + _ <- string "let" + _ <- emptySpace + _ <- aspO + _ <- emptySpace + vb <- Pc.many $ parseVarBinding <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ TermLet vb term + +parseTermFA :: ParsecT String u Identity Term +parseTermFA = do + _ <- aspO + _ <- emptySpace + _ <- string "forall" + _ <- emptySpace + _ <- aspO + sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ TermForall sv term + + +parseTermEX :: ParsecT String u Identity Term +parseTermEX = do + _ <- aspO + _ <- emptySpace + _ <- string "exists" + _ <- emptySpace + _ <- aspO + sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace + _ <- aspC + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ TermExists sv term + +parseTermAnnot :: ParsecT String u Identity Term +parseTermAnnot = do + _ <- aspO + _ <- emptySpace + _ <- char '!' + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + attr <- Pc.many $ parseAttribute <* Pc.try emptySpace + _ <- aspC + return $ TermAnnot term attr + + +-- -- Parse Sorted Var +parseSortedVar :: ParsecT String u Identity SortedVar +parseSortedVar = do + _ <- aspO + _ <- emptySpace + symb <- symbol + _ <- emptySpace + sort <- parseSort + _ <- emptySpace + _ <- aspC + return $ SV symb sort + +-- -- Parse Qual identifier +parseQualIdentifier :: ParsecT String u Identity QualIdentifier +parseQualIdentifier = Pc.try parseQID <|> parseQIAs + +parseQID :: ParsecT String u Identity QualIdentifier +parseQID = liftM QIdentifier parseIdentifier + + + + +parseQIAs :: ParsecT String u Identity QualIdentifier +parseQIAs = do + _ <- aspO + _ <- emptySpace + _ <- string "as" + _ <- emptySpace + ident <- parseIdentifier + _ <- emptySpace + sort <- parseSort + _ <- emptySpace + _ <- aspC + return $ QIdentifierAs ident sort + + +-- -- Parse Var Binding +parseVarBinding :: ParsecT String u Identity VarBinding +parseVarBinding = do + _ <- aspO + _ <- emptySpace + symb <- symbol + _ <- emptySpace + term <- parseTerm + _ <- emptySpace + _ <- aspC + return $ VB symb term + + + + + +{- + ######################################################################### + # # + # Parsers for Attributes # + # # + ######################################################################### +-} + +--Parse Attribute Value +parseAttributeValue :: ParsecT String u Identity AttrValue +parseAttributeValue = parseAVSC <|> parseAVS <|> parseAVSexpr + +parseAVSC :: ParsecT String u Identity AttrValue +parseAVSC = liftM AttrValueConstant parseSpecConstant + +parseAVS :: ParsecT String u Identity AttrValue +parseAVS = liftM AttrValueSymbol symbol + +parseAVSexpr :: ParsecT String u Identity AttrValue +parseAVSexpr = do + _ <- aspO + _ <- emptySpace + expr <- Pc.many $ parseSexpr <* Pc.try emptySpace + _ <- aspC + return $ AttrValueSexpr expr + + + +-- Parse Attribute + +parseAttribute :: ParsecT String u Identity Attribute +parseAttribute = Pc.try parseKeyAttAttribute <|> parseKeyAttribute + + +parseKeyAttribute :: ParsecT String u Identity Attribute +parseKeyAttribute = liftM Attribute keyword + +parseKeyAttAttribute :: ParsecT String u Identity Attribute +parseKeyAttAttribute = do + kw <- keyword + _ <- emptySpace + atr <- parseAttributeValue + return $ AttributeVal kw atr + + +{- + ######################################################################### + # # + # Parsers Sort # + # # + ######################################################################### +-} + +-- Parse Sot + +parseSort :: ParsecT String u Identity Sort +parseSort = Pc.try parseIdentifierS <|> parseIdentifierSort + +parseIdentifierS :: ParsecT String u Identity Sort +parseIdentifierS = liftM SortId parseIdentifier + +parseIdentifierSort :: ParsecT String u Identity Sort +parseIdentifierSort = do + _ <- aspO + _ <- emptySpace + identifier <- parseIdentifier + _ <- emptySpace + sorts <- many1 (parseSort <* Pc.try emptySpace) + _ <- aspC + return $ SortIdentifiers identifier sorts + + + + +{- + ######################################################################### + # # + # Parsers Identifiers # + # # + ######################################################################### +-} + + +-- Parse Identifiers + +parseIdentifier :: ParsecT String u Identity Identifier +parseIdentifier = parseOnlySymbol <|> parseNSymbol + +parseOnlySymbol :: ParsecT String u Identity Identifier +parseOnlySymbol = liftM ISymbol symbol + +parseNSymbol :: ParsecT String u Identity Identifier +parseNSymbol = do + _ <- aspO + _ <- emptySpace + _ <- aspUS + _ <- emptySpace + symb <- symbol + _ <- emptySpace + nume <- many1 (numeral <* Pc.try spaces) + _ <- aspC + return $ I_Symbol symb (fmap (read) nume) + +{- + ######################################################################### + # # + # Parsers S-exprs # + # # + ######################################################################### +-} + + +-- parse S-expressions + +parseSexprConstant :: ParsecT String u Identity Sexpr +parseSexprConstant = liftM SexprSpecConstant parseSpecConstant + +parseSexprSymbol :: ParsecT String u Identity Sexpr +parseSexprSymbol = liftM SexprSymbol symbol + +parseSexprKeyword :: ParsecT String u Identity Sexpr +parseSexprKeyword = liftM SexprSymbol keyword + +parseAtomSexpr :: ParsecT String u Identity Sexpr +parseAtomSexpr = parseSexprConstant + <|> parseSexprSymbol + <|> parseSexprKeyword + + +parseListSexpr :: ParsecT String u Identity Sexpr +parseListSexpr = do + _ <- aspO + list <- Pc.many parseSexpr + _ <- aspC + return $ SexprSxp list + + + +parseSexpr :: ParsecT String u Identity Sexpr +parseSexpr = do + _ <- emptySpace + expr <- parseAtomSexpr <|> parseListSexpr + _ <- emptySpace + return expr + + + +-- parse Spec Constant +parseSpecConstant :: ParsecT String u Identity SpecConstant +parseSpecConstant = Pc.try parseDecimal + <|> parseNumeral + <|> Pc.try parseHexadecimal + <|> parseBinary + <|> parseString + + + +parseNumeral :: ParsecT String u Identity SpecConstant +parseNumeral = liftM SpecConstantNumeral (read <$> numeral) + +parseDecimal :: ParsecT String u Identity SpecConstant +parseDecimal = liftM SpecConstantDecimal decimal + +parseHexadecimal :: ParsecT String u Identity SpecConstant +parseHexadecimal = liftM SpecConstantHexadecimal hexadecimal + +parseBinary :: ParsecT String u Identity SpecConstant +parseBinary = liftM SpecConstantBinary binary + +parseString :: ParsecT String u Identity SpecConstant +parseString = liftM SpecConstantString str
+ Smtlib/Parsers/ResponseParsers.hs view
@@ -0,0 +1,333 @@+{-| +Module : Smtlib.Parsers.ResponseParsers +Description : Parsers for Smtlib commands response. +Copyright : Rogério Pontes 2015 +License : WTFPL +Maintainer : rogerp62@outlook.com +Stability : stable + +This module contains all the required individual parsers for each reasponse to +a Smtlib command, plus one parser to parse every result, parseCmdResult. + +-} + +module Smtlib.Parsers.ResponseParsers where + +import Control.Applicative as Ctr hiding ((<|>)) +import Control.Monad +import Data.Functor.Identity +import Smtlib.Parsers.CommonParsers +import Smtlib.Syntax.Syntax as CmdRsp +import Text.Parsec.Prim as Prim +import Text.ParserCombinators.Parsec as Pc + + + +parseCmdResult :: ParsecT String u Identity CmdResponse +parseCmdResult = Pc.try parseCmdGenResponse + <|> Pc.try parseCmdCheckSatResponse + <|> Pc.try parseCmdGetInfoResponse + <|> Pc.try parseCmdGetAssertions + <|> Pc.try parseCmdGetAssignment + <|> Pc.try parseCmdGetProof + <|> Pc.try parseCmdGetProof + <|> Pc.try parseCmdGetValueResponse + <|> parseCmdGetOptionResponse + +{- + ######################################################################### + # # + # Parser Cmd Gen Response # + # # + ######################################################################### +-} + +parseCmdGenResponse :: ParsecT String u Identity CmdResponse +parseCmdGenResponse = liftM CmdGenResponse parseGenResponse + +parseGenResponse :: ParsecT String u Identity GenResponse +parseGenResponse = parseUnsupported <|> parseSuccess <|> parseGenError + +parseSuccess :: ParsecT String u Identity GenResponse +parseSuccess = string "success" *> return Success + +parseUnsupported :: ParsecT String u Identity GenResponse +parseUnsupported = string "unsupported" *> return Unsupported + + +parseGenError :: ParsecT String u Identity GenResponse +parseGenError = do + _ <- aspO + _ <- emptySpace + _ <- string "error" + _ <- emptySpace + err <- str + _ <- emptySpace + _ <- aspC + return $ CmdRsp.Error err + + + + + + +{- + ######################################################################### + # # + # Parser get info response # + # # + ######################################################################### +-} + +parseCmdGetInfoResponse :: ParsecT String u Identity CmdResponse +parseCmdGetInfoResponse = liftM CmdGetInfoResponse parseGetInfoResponse + + +parseGetInfoResponse :: ParsecT String u Identity [InfoResponse] +parseGetInfoResponse = do + _ <-aspO + _ <- emptySpace + infoResp <- Pc.many $ parseInfoResponse <* Pc.try emptySpace + _ <- aspC + return infoResp + + + +parseInfoResponse :: ParsecT String u Identity InfoResponse +parseInfoResponse = + Pc.try parseResponseName <|> + Pc.try parseResponseErrorBehavior <|> + Pc.try parseResponseAuthors <|> + Pc.try parseResponseVersion <|> + Pc.try parseResponseReasonUnknown <|> + parseResponseAttribute + + + + +parseResponseName :: ParsecT String u Identity InfoResponse +parseResponseName = string ":name" *> emptySpace *> liftM ResponseName str + + +parseResponseErrorBehavior :: ParsecT String u Identity InfoResponse +parseResponseErrorBehavior = string ":error-behavior" *> emptySpace *> + liftM ResponseErrorBehavior parseErrorBehavior + +parseErrorBehavior :: ParsecT String u Identity ErrorBehavior +parseErrorBehavior = + (string "immediate-exit" >> return ImmediateExit) <|> + (string "continued-execution" >> return ContinuedExecution) + + +parseResponseAuthors :: ParsecT String u Identity InfoResponse +parseResponseAuthors = string ":authors" *> emptySpace *> + liftM ResponseAuthors str + +parseResponseVersion :: ParsecT String u Identity InfoResponse +parseResponseVersion = string ":version" *> emptySpace *> + liftM ResponseVersion str + + + +parseResponseReasonUnknown :: ParsecT String u Identity InfoResponse +parseResponseReasonUnknown = string "reason" *> emptySpace *> + liftM ResponseReasonUnknown parseRReasonUnknown + +parseRReasonUnknown :: ParsecT String u Identity ReasonUnknown +parseRReasonUnknown = + (string "memout" >> return Memout) <|> + (string "incomplete" >> return Incomplete) + + + +parseResponseAttribute :: ParsecT String u Identity InfoResponse +parseResponseAttribute = liftM ResponseAttribute parseAttribute + + + + + + + +{- + ######################################################################### + # # + # Parser check sat response # + # # + ######################################################################### +-} + + + +parseCmdCheckSatResponse :: ParsecT String u Identity CmdResponse +parseCmdCheckSatResponse = liftM CmdCheckSatResponse parseCheckSatResponse + + + +-- Parser for check sat response +parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse +parseCheckSatResponse = + (string "sat" >> return Sat) <|> + (string "unsat" >> return Unsat) <|> + (string "unknown" >> return Unknown) + + + + +{- + ######################################################################### + # # + # Parser get assertions cmd # + # # + ######################################################################### +-} + + +parseCmdGetAssertions :: ParsecT String u Identity CmdResponse +parseCmdGetAssertions = + liftM CmdGetAssertionsResponse parseGetAssertionsResponse + + + +-- parse Get Assertion Response +parseGetAssertionsResponse :: ParsecT String u Identity [Term] +parseGetAssertionsResponse = do + _ <- aspO + _ <- emptySpace + terms <- Pc.many $ parseTerm <* Pc.try emptySpace + _ <- aspC + return terms + +{- + ######################################################################### + # # + # Parser get proof response # + # # + ######################################################################### +-} + + +parseCmdGetProof :: ParsecT String u Identity CmdResponse +parseCmdGetProof = liftM CmdGetProofResponse parseGetProofResponse + +-- parse Get Proof response +parseGetProofResponse :: ParsecT String u Identity Sexpr +parseGetProofResponse = parseSexpr + + + +{- + ######################################################################### + # # + # Parser get unsat core response # + # # + ######################################################################### +-} + + +parseCmdGetUnsatCore :: ParsecT String u Identity CmdResponse +parseCmdGetUnsatCore = liftM CmdGetUnsatCoreResponse parseGetUnsatCoreResp + + +-- parse Get unsat core response +parseGetUnsatCoreResp :: ParsecT String u Identity [String] +parseGetUnsatCoreResp = do + _ <- aspO + _ <- emptySpace + symb <- Pc.many $ symbol <* Pc.try emptySpace + _ <- aspC + return symb + + +{- + ######################################################################### + # # + # Parser Cmd Get value response # + # # + ######################################################################### +-} + + +parseCmdGetValueResponse :: ParsecT String u Identity CmdResponse +parseCmdGetValueResponse = liftM CmdGetValueResponse parseGetValueResponse + + + +-- parse Get Value response +parseGetValueResponse :: ParsecT String u Identity [ValuationPair] +parseGetValueResponse = + aspO *> (Pc.many $ parseValuationPair <* Pc.try emptySpace) <* aspC + +parseValuationPair :: ParsecT String u Identity ValuationPair +parseValuationPair = do + _ <- aspO + _ <- emptySpace + term1 <- parseTerm + _ <- emptySpace + term2 <- parseTerm + _ <- emptySpace + _ <- aspC + return $ ValuationPair term1 term2 + + +{- + ######################################################################### + # # + # Parser Cmd get assignment Resp # + # # + ######################################################################### +-} + + +parseCmdGetAssignment :: ParsecT String u Identity CmdResponse +parseCmdGetAssignment = liftM CmdGetAssignmentResponse parseGetAssignmentResp + +-- parse get Assignent Response +parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair] +parseGetAssignmentResp = do + _ <- aspO + _ <- emptySpace + pairs <- Pc.many $ parseTValuationPair <* Pc.try emptySpace + _ <- aspC + return pairs + +-- parse t valuation pair +parseTValuationPair :: ParsecT String u Identity TValuationPair +parseTValuationPair = do + _ <- aspO + _ <- emptySpace + symb <- symbol + _ <- emptySpace + bval <- parseBool + _ <- emptySpace + _ <-aspC + return $ TValuationPair symb bval + + + + + +{- + ######################################################################### + # # + # Parser Cmd get option response # + # # + ######################################################################### +-} + + +parseCmdGetOptionResponse :: ParsecT String u Identity CmdResponse +parseCmdGetOptionResponse = liftM CmdGetOptionResponse parseGetOptionResponse + + +-- parse Get Option Response +parseGetOptionResponse :: ParsecT String u Identity AttrValue +parseGetOptionResponse = parseAttributeValue + +{- + ######################################################################### + # # + # Parser check-sat Alterg'os response # + # # + ######################################################################### +-}
+ Smtlib/Syntax/ShowSL.hs view
@@ -0,0 +1,198 @@+{-| +Module : Smtlib.Syntax.ShowSL +Description : Instance to print the syntax. +Copyright : Rogério Pontes 2015 +License : WTFPL +Maintainer : rogerp62@outlook.com +Stability : stable + +Functions to print the syntax as a SMTLib. + +-} +module Smtlib.Syntax.ShowSL where + +import Data.List +import Smtlib.Syntax.Syntax + + +joinA ::(ShowSL a) => [a] -> String +joinA = unwords.fmap showSL + +joinNs :: [Int] -> String +joinNs = unwords.fmap show + + +class ShowSL a where + showSL :: a -> String + + + +{- + ######################################################################### + # # + # ShowSL for an SMTLib2 File # + # # + ######################################################################### +-} + + +instance ShowSL Command where + showSL (SetLogic s) = "(set-logic " ++ s ++ ")" + showSL (SetOption opt) = "(set-option " ++ showSL opt ++ ")" + showSL (SetInfo info) = "(set-info " ++ showSL info ++ ")" + showSL (DeclareSort str val) = "(declare-sort " ++ str ++ + " " ++ show val ++ ")" + showSL (DefineSort str strs sort) = "(define-sort " ++ str ++ + " (" ++ unwords strs ++ ") " ++ showSL sort ++ ") " + showSL (DeclareFun str sorts sort) = "(declare-fun " ++ str ++ + " (" ++ joinA sorts ++ ") " ++ showSL sort ++ ") " + showSL (DefineFun str srvs sort term) = "( define-fun " ++ str ++ + " (" ++ joinA srvs ++ ") " ++ showSL sort ++ " " ++ showSL term ++ ")" + showSL (Push n) = "(push " ++ show n ++ ")" + showSL (Pop n) = "(pop " ++show n ++ ")" + showSL (Assert term) = "(assert " ++ showSL term ++ ")" + showSL CheckSat = "(check-sat)" + showSL GetAssertions = "(get-assertions)" + showSL GetProof = "(get-proof)" + showSL GetUnsatCore = "(get-unsat-core)" + showSL (GetValue terms) = "( (" ++ joinA terms ++ ") )" + showSL GetAssignment = "(get-assignment)" + showSL (GetOption opt) = "(get-option " ++ opt ++ ")" + showSL (GetInfo info) = "(get-info " ++ showSL info ++ ")" + showSL Exit = "(exit)" + + +instance ShowSL Option where + showSL (PrintSucess b) = ":print-sucess " ++ show b + showSL (ExpandDefinitions b) = ":expand-definitions " ++ show b + showSL (InteractiveMode b) = ":interactive-mode " ++ show b + showSL (ProduceProofs b) = ":produce-proofs " ++ show b + showSL (ProduceUnsatCores b) = ":produce-unsat-cores " ++ show b + showSL (ProduceModels b) = ":produce-models " ++ show b + showSL (ProduceAssignments b) = ":produce-assignments " ++ show b + showSL (RegularOutputChannel s) = ":regular-output-channel " ++ s + showSL (DiagnosticOutputChannel s) = ":diagnostic-output-channel " ++ s + showSL (RandomSeed n) = ":random-seed " ++ show n + showSL (Verbosity n) = ":verbosity'" ++ show n + showSL (OptionAttr attr) = showSL attr + +instance ShowSL InfoFlags where + showSL ErrorBehavior = ":error-behavior" + showSL Name = ":name" + showSL Authors = ":authors" + showSL Version = ":version" + showSL Status = ":status" + showSL ReasonUnknown = ":reason-unknown" + showSL AllStatistics = ":all-statistics" + showSL (InfoFlags s) = s + + +instance ShowSL Term where + showSL (TermSpecConstant sc) = showSL sc + showSL (TermQualIdentifier qi) = showSL qi + showSL (TermQualIdentifierT qi terms) = + "(" ++ showSL qi ++ " " ++ joinA terms ++ ")" + showSL (TermLet vb term) = + "(let (" ++ joinA vb ++ ") " ++ showSL term ++ ")" + showSL (TermForall svs term) = + "(forall (" ++ joinA svs ++ " ) " ++ showSL term ++ ")" + showSL (TermExists svs term) = + "(exists (" ++ joinA svs ++ " ) " ++ showSL term ++ ")" + showSL (TermAnnot term atts) = + "(! " ++ showSL term ++ " " ++ joinA atts ++ ")" + +instance ShowSL VarBinding where + showSL (VB str term) = "("++ show str ++ " " ++ showSL term ++ ")" + +instance ShowSL SortedVar where + showSL (SV str sort) = "(" ++ show str ++ " " ++ showSL sort ++ ")" + +instance ShowSL QualIdentifier where + showSL (QIdentifier iden) = showSL iden + showSL (QIdentifierAs iden sort) = + "(as " ++ showSL iden ++ " " ++ showSL sort ++ ")" + +instance ShowSL AttrValue where + showSL (AttrValueConstant spc) = showSL spc + showSL (AttrValueSymbol str) = str + showSL (AttrValueSexpr sexprs) = "(" ++ joinA sexprs ++ ")" + +instance ShowSL Attribute where + showSL (Attribute str) = str + showSL (AttributeVal str attrVal) = str ++ " " ++ showSL attrVal + +instance ShowSL Identifier where + showSL (ISymbol str) = str + showSL (I_Symbol str ns) = "( _ " ++ str ++ " " ++ joinNs ns ++ ")" + +instance ShowSL Sort where + showSL (SortId iden) = showSL iden + showSL (SortIdentifiers iden sorts) = + "(" ++ show iden ++ " " ++ joinA sorts ++ ")" + +instance ShowSL SpecConstant where + showSL (SpecConstantNumeral n) = show n + showSL (SpecConstantDecimal str) = str + showSL (SpecConstantHexadecimal str) = str + showSL (SpecConstantBinary str) = str + showSL (SpecConstantString str) = str + +instance ShowSL Sexpr where + showSL (SexprSpecConstant sc) = showSL sc + showSL (SexprSymbol str) = str + showSL (SexprKeyword str) = str + showSL (SexprSxp srps) = "(" ++ joinA srps ++ ")" + + +{- + ######################################################################### + # # + # Command Response # + # # + ######################################################################### +-} + +instance ShowSL CmdResponse where + showSL (CmdGenResponse x) = showSL x + showSL (CmdGetInfoResponse x) = "(" ++ joinA x ++ ")" + showSL (CmdCheckSatResponse x) = showSL x + showSL (CmdGetAssertionsResponse x) = "(" ++ joinA x ++ ")" + showSL (CmdGetAssignmentResponse x) = "(" ++ joinA x ++ ")" + showSL (CmdGetProofResponse x) = showSL x + showSL (CmdGetUnsatCoreResponse x) = "(" ++ unwords x ++ ")" + showSL (CmdGetValueResponse x) = "(" ++ joinA x ++ ")" + showSL (CmdGetOptionResponse x) = showSL x + + +instance ShowSL GenResponse where + showSL Unsupported = "unsupported" + showSL Success = "Success" + showSL (Error s) = "(error " ++ s ++ ")" + +instance ShowSL ErrorBehavior where + showSL ImmediateExit = "immediate-exit" + showSL ContinuedExecution = "continued-execution" + +instance ShowSL ReasonUnknown where + showSL Memout = "memout" + showSL Incomplete = "imcomplete" + +instance ShowSL CheckSatResponse where + showSL Sat = "sat" + showSL Unsat = "unsat" + showSL Unknown = "unknown" + +instance ShowSL InfoResponse where + showSL (ResponseErrorBehavior x) = ":error-behaviour " ++ showSL x + showSL (ResponseName s) = ":name " ++ s + showSL (ResponseAuthors s) = ":authors " ++ s + showSL (ResponseVersion s) = ":version" ++ s + showSL (ResponseReasonUnknown x) = ":reason-unknown " ++ showSL x + showSL (ResponseAttribute x) = showSL x + +instance ShowSL ValuationPair where + showSL (ValuationPair term1 term2) = + "(" ++ showSL term1 ++ " " ++ showSL term2 ++ ")" + +instance ShowSL TValuationPair where + showSL (TValuationPair str b) = "(" ++ str ++ " " ++ show b ++ ")"
+ Smtlib/Syntax/Syntax.hs view
@@ -0,0 +1,240 @@+{-| +Module : Smtlib.Parsers.CommandsParsers +Description : Smtlib Syntax +Copyright : Rogério Pontes 2015 +License : WTFPL +Maintainer : rogerp62@outlook.com +Stability : stable + +This module contains The syntax to create commands and responses. + +-} +module Smtlib.Syntax.Syntax where + +{- + ######################################################################### + # # + # Parser for an SMTLib2 File # + # # + ######################################################################### +-} + + +type Source = [Command] + + +data Command = SetLogic String + | SetOption Option + | SetInfo Attribute + | DeclareSort String Int + | DefineSort String [String] Sort + | DeclareFun String [Sort] Sort + | DefineFun String [SortedVar] Sort Term + | Push Int + | Pop Int + | Assert Term + | CheckSat + | GetAssertions + | GetProof + | GetUnsatCore + | GetValue [Term] + | GetAssignment + | GetOption String + | GetInfo InfoFlags + | Exit + deriving (Show,Eq) + +data Option = PrintSucess Bool + | ExpandDefinitions Bool + | InteractiveMode Bool + | ProduceProofs Bool + | ProduceUnsatCores Bool + | ProduceModels Bool + | ProduceAssignments Bool + | RegularOutputChannel String + | DiagnosticOutputChannel String + | RandomSeed Int + | Verbosity Int + | OptionAttr Attribute + deriving (Show,Eq) + + +data InfoFlags = ErrorBehavior + | Name + | Authors + | Version + | Status + | ReasonUnknown + | AllStatistics + | InfoFlags String + deriving (Show,Eq) + +-- Terms + +data Term = TermSpecConstant SpecConstant + | TermQualIdentifier QualIdentifier + | TermQualIdentifierT QualIdentifier [Term] + | TermLet [VarBinding] Term + | TermForall [SortedVar] Term + | TermExists [SortedVar] Term + | TermAnnot Term [Attribute] + deriving (Show,Eq) + + + +data VarBinding = VB String Term deriving (Show,Eq) + + + +data SortedVar = SV String Sort deriving (Show,Eq) + + + +data QualIdentifier = QIdentifier Identifier + | QIdentifierAs Identifier Sort + deriving (Show,Eq) + + + + + + + +-- Attributes + +data AttrValue = AttrValueConstant SpecConstant + | AttrValueSymbol String + | AttrValueSexpr [Sexpr] + deriving (Show,Eq) + + + +data Attribute = Attribute String + | AttributeVal String AttrValue + deriving (Show,Eq) + +-- Identifiers + +data Identifier = ISymbol String + | I_Symbol String [Int] deriving (Show,Eq) + +-- Sorts + +data Sort = SortId Identifier | SortIdentifiers Identifier [Sort] + deriving (Show,Eq) + + +-- S-expressions +data SpecConstant = SpecConstantNumeral Integer + | SpecConstantDecimal String + | SpecConstantHexadecimal String + | SpecConstantBinary String + | SpecConstantString String + deriving (Show, Eq) + + + +data Sexpr = SexprSpecConstant SpecConstant + | SexprSymbol String + | SexprKeyword String + | SexprSxp [Sexpr] + deriving (Show, Eq) + + + + + + + + + +{- + ######################################################################### + # # + # Command Response # + # # + ######################################################################### +-} + + + +-- CmdResponse + +data CmdResponse = CmdGenResponse GenResponse + | CmdGetInfoResponse GetInfoResponse + | CmdCheckSatResponse CheckSatResponse + | CmdGetAssertionsResponse GetAssertionsResponse + | CmdGetAssignmentResponse GetAssignmentResponse + | CmdGetProofResponse GetProofResponse + | CmdGetUnsatCoreResponse GetUnsatCoreResponse + | CmdGetValueResponse GetValueResponse + | CmdGetOptionResponse GetOptionResponse + deriving (Show, Eq) + + +-- Command Responses + + +-- Gen Response + +data GenResponse = Unsupported | Success | Error String deriving (Show, Eq) + + +-- Error behavior + +data ErrorBehavior = ImmediateExit | ContinuedExecution deriving (Show, Eq) + + +-- Reason unknown + +data ReasonUnknown = Memout | Incomplete deriving (Show, Eq) + +-- Status + +data CheckSatResponse = Sat | Unsat | Unknown deriving (Show, Eq) + +-- Info Response + +type GetInfoResponse = [InfoResponse] + +data InfoResponse = ResponseErrorBehavior ErrorBehavior + | ResponseName String + | ResponseAuthors String + | ResponseVersion String + | ResponseReasonUnknown ReasonUnknown + | ResponseAttribute Attribute + deriving (Show, Eq) + +-- Get Assertion Response + +type GetAssertionsResponse = [Term] + + +-- Get Proof Response + +type GetProofResponse = Sexpr + + +--Get Unsat Core Response + +type GetUnsatCoreResponse = [String] + + +-- Get Valuation Pair + +data ValuationPair = ValuationPair Term Term deriving (Show, Eq) + + +type GetValueResponse = [ValuationPair] + + +-- get Assignment Response + +data TValuationPair = TValuationPair String Bool deriving (Show, Eq) + +type GetAssignmentResponse = [TValuationPair] + + +-- Get Option Response + +type GetOptionResponse = AttrValue