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
parseSource :: ParsecT String u Identity Source
parseSource = Pc.many $ parseCommand <* Pc.try emptySpace
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
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
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
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
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